Concurrent C Minor project

People Rationale Publications

Concurrent C Minor is an international research project to connect machine-verified source programs in sequential and concurrent programming languages to machine-verified optimizing compilers. It takes inspiration from Xavier Leroy's design of the (sequential) C Minor language and verified compiler and has goals complementary to Leroy's CompCert project.

We develop program logics (such as Concurrent Separation Logic) that have machine-checked proofs of soundness w.r.t. the C Minor operational semantics; this connects to the correctness proof of the CompCert compiler.

There are applications to embedded systems (for C programs) and to high-assurance high-level programming (via machined-verified translators from high-level languages to C).

Examples of research results

Small-step operational semantics for sequential C minor, with machine-checked soundness proof of sequential Separation Logic (Appel & Blazy, TPHOL 2007)
Coq tactics for separation logic (Appel, tech report 2006)
Concurrent C Minor operational semantics with machine-checked soundness proof (Appel, Hobor, Zappa Nardelli, ESOP 2008)
Theory and models of multimodal separation logic (Dockins, Appel, Hobor, MFPS 2008)
Formal verification of coalescing graph-coloring register allocation (Blazy, Robillard, Appel)
A fresh look at separation algebras and share accounting (Dockins, Hobor, Appel, submitted for publication)
Redesign of CompCert memory model to accomodate separation, concurrency, and fractional ownership (Appel)
Modular formulation of a model for a Goedel-Loeb separation logic (Hobor, Dockins, Appel, work in progress)

Participants

Andrew W. Appel
Princeton University

Robert Dockins
Princeton University

Aquinas Hobor
National U. of Singapore

Collaborators and affiliated researchers

Xavier Leroy
INRIA

John Hatcliff
Kansas State U.

Sandrine Blazy
Univ. Rennes I

Francesco Zappa Nardelli
INRIA

Rationale

In some application domains it is not enough to build reliable software systems, one wants proved-correct software. This is the case for safety-critical systems (where software bugs can cause injury or death) and for security-critical applications (where an attacker is deliberately searching for, and exploiting, software bugs). Since proofs are large and complex, the proof-checking must be mechanized. Machine-checked proofs of real software systems are difficult, but now should be possible, given the recent advances in the theory and engineering of mechanized proof systems applied to software verification. But there are several challenges:

Real software systems are usually built from components in different programming languages.
Some parts of the program need full correctness proofs, which must be constructed with great effort; other parts need only safety proofs, which can be constructed automatically.
One reasons about correctness at the source-code level, but one runs a machine-code program translated by a compiler; the compiler must be proved correct.
These proofs about different properties, with respect to different programming languages, must be integrated together end-to-end in a way that is also proved correct and machine-checked.

We address these challenges by defining a high-level intermediate language, Concurrent C Minor (CCm), with a small-step operational semantics representable in machine-checked proof assistants (we use Coq). We define a Concurrent Separation Logic for reasoning directly about source programs written in CCm. In addition, CCm is suitable as a target language for compilers from Java, C, C#, ML, and other languages. This will allow safe and well-specified interaction of program modules written in different programming languages. Finally, CCm is a concurrent language with a threads-and-locks model similar to Cthreads.

Publications

Foundational High-level Static Analysis, by Andrew W. Appel. In CAV 2008 Workshop on Exploiting Concurrency Efficiently and Correctly, July 2008.

Multimodal Separation Logic for Reasoning About Operational Semantics, by Robert Dockins, Andrew W. Appel, and Aquinas Hobor, (to appear) in Twenty-fourth Conference on the Mathematical Foundations of Programming Semantics, May 2008.

Automating Separation Logic for Concurrent C Minor, by William Mansky. Undergraduate thesis, May 2008.

Oracle Semantics for Concurrent Separation Logic by Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. European Symposium on Programming (ESOP), April 2008. Extended version with appendix.

Separation Logic for Small-step C Minor, by Andrew W. Appel and Sandrine Blazy. in TPHOLs 2007: 20th International Conference on Theorem Proving in Higher-Order Logics, September 2007. Tactics for Separation Logic, by Andrew W. Appel, January 2006.

Funding

Parts of this research are funded by:

Air Force Office of Scientific Research (via subcontract to Kansas State University), Evidence-based trust in large-scale MLS systems.
National Science Foundation, Combining Foundational and Lightweight Formal Methods to Build Certifiably Dependable Software.

This research has also been supported by Princeton University, INRIA, and National Science Foundation Grant CCF-0540914.

Last overhaul of this page: June 2009.