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, 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.

Contributors

• Aleksandar Nanevski
• Ilya Sergey
• Anindya Banerjee
• Germán Andrés Delbianco

Past contributors

• Ruy Ley-Wild

Artifacts

Main files

• VM image with FCSL version of April 2015 for Oracle VirtualBox, running Ubuntu 14.04 (32 bit) with installed Coq, Ssreflect, GNU Emacs with Proof General, and FCSL sources, ready for experiments (~1.9Gb, user/password: coquser/coquser).
  [OVA]


• Mechanized Verification of Fine-grained Concurrent Programs. Accompanying user manual and code commentary.
  Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee. April 2015.
  [PDF]
  

Additional files

• FCSL source files [ZIP archive] (run make from the folder fcsl-pldi15 to build the project);
• Installation and set-up guide for Coq, Ssreflect and Emacs with Proof General [Instructions];
• Coq 8.4 source files [Tarball];
• Ssreflect 1.4 source files [Tarball];
• Proof General source files [Tarball].

Papers and manuscripts

• Mechanized Verification of Fine-grained Concurrent Programs
  Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee
  36th ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2015). Portland, OR, USA, June 2015. ACM.
  [Draft PDF]
  


• Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
  Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee
  24th European Symposium on Programming (ESOP 2015). London, UK, April 2015. Springer.
  [PDF | Extended version | arXiv]
  


• Communicating State Transition Systems for Fine-Grained Concurrent Resources
  Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey and Germán Andrés Delbianco
  23rd European Symposium on Programming (ESOP 2014). Grenoble, France, April 2014. Springer.
  [PDF | Extended version | Slides]