KRust: A Formal Executable Semantics of Rust
- 1 August 2018
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Rust is a new and promising high-level system programming language. It provides both memory safety and thread safety through its novel mechanisms such as ownership, moves and borrows. Ownership system ensures that at any point there is only one owner of any given resource. The ownership of a resource can be moved or borrowed according to the lifetimes. The ownership system establishes a clear lifetime for each value and hence Rust does not necessarily need garbage collection. These novel features bring Rust high performance, fine-grained low-level control over memory without garbage collection, which differentiate Rust from other existing prevalent languages. For formal analysis of Rust programs and helping programmers learn its new mechanisms and features, a formal semantics of Rust is desired and useful as a fundament for developing related tools. In this paper, we present a formal executable operational semantics of a subset of Rust, called KRust. The semantics is defined in K, a rewriting-based executable semantic framework for programming languages. The executable semantics yields automatically a formal interpreter and verification tools for Rust programs. KRust has been validated by testing with 182 tests, including 157 tests from the official Rust test suite. We individually found an error in the Rust compiler.Keywords
This publication has 11 references indexed in Scilit:
- POSTERPublished by Association for Computing Machinery (ACM) ,2017
- Engineering the servo web browser engine using RustPublished by Association for Computing Machinery (ACM) ,2016
- Fuzzing the Rust Typechecker Using CLP (T)Published by Institute of Electrical and Electronics Engineers (IEEE) ,2015
- Crust: A Bounded Verifier for Rust (N)Published by Institute of Electrical and Electronics Engineers (IEEE) ,2015
- KJS: a complete formal semantics of JavaScriptPublished by Association for Computing Machinery (ACM) ,2015
- Defining the undefinedness of CPublished by Association for Computing Machinery (ACM) ,2015
- K-JavaPublished by Association for Computing Machinery (ACM) ,2015
- The rust languagePublished by Association for Computing Machinery (ACM) ,2014
- An executable formal semantics of C with applicationsPublished by Association for Computing Machinery (ACM) ,2012
- An overview of the K semantic frameworkThe Journal of Logic and Algebraic Programming, 2010