FCSL: Fine-grained Concurrent Separation Logic


FCSL is the first completely formalized framework for mechanized verification of full functional correctness of fine-grained concurrent programs. It is implemented as an embedded domain-specific language (DSL) in the dependently-typed language of the Coq proof assistant, and is powerful enough to reason about programming features such as higher-order functions and local thread spawning. By incorporating a uniform concurrency model, based on state-transition systems and partial commutative monoids (PCM), FCSL makes it possible to build proofs about concurrent libraries in a thread-local, compositional way, thus facilitating scalability and reuse: libraries are verified just once, and their specifications are used ubiquitously in client-side reasoning.

This project site provides access to the Coq-based development of FCSL as a logic and as a verification framework. The development includes the description of the logic's semantic domain, denotations of effectful statements and types, as well as structural lemmas, playing the role of the logic's inference rules.

The PCM subpart of the framework has been released on OPAM package manager. The source code is available on GitHub at imdea-software/fcsl-pcm.


Contributors


Artifacts

Documentation


Publications


Last modified: Thu Sep 22 14:35:21 CET 2022