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

• Aleksandar Nanevski (IMDEA Software Institute)
• Ruy Ley-Wild (Google)
• Ilya Sergey (Yale-NUS College/Zilliqa Research)
• Anindya Banerjee (National Science Foundation/IMDEA Software Institute)
• Germán Andrés Delbianco (Nomadic Labs)
• Jesús Domínguez (IMDEA Software Institute)
• Ignacio Fábregas (Universidad Complutense de Madrid)
• Joakim Öhman (IMDEA Software Institute)
• Anton Trunov (Zilliqa Research)
• František Farka (BedRock Systems)
• Alexander Gryzlov (IMDEA Software Institute)

Artifacts

• FCSL source files of September 2022, requires Ssreflect/Mathcomp and FCSL-PCM libraries (see installation instructions);
  [ZIP archive | Instructions]


• VM image with FCSL version of November 2020 for Oracle VirtualBox, running Xubuntu 20.04.1 LTS with installed Coq 8.12, Ssreflect 1.11, CoqIDE, Emacs 26.3 + ProofGeneral and FCSL sources, ready for experiments (~1.5 Gb, user/password: fcsl/fcsl).
  [OVA]

Documentation

• Mechanized Verification of Fine-grained Concurrent Programs in Fine-grained Concurrent Separation Logic.
  User Manual and Code Commentary. Most parts of this document are outdated.
  Aleksandar Nanevski, Ilya Sergey, Ruy Ley-Wild, Anindya Banerjee and Germán Andrés Delbianco. April 2017.
  [PDF]
  

Publications

• On Algebraic Abstractions for Concurrent Separation Logics
  František Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco and Ignacio Fábregas
  Symposium on Principles of Programming Languages (POPL 2021).
  [PDF | arXiv]
  


• Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations
  Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco and Ignacio Fábregas
  34th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2019).
  [PDF | arXiv]
  


• Concurrent Data Structures Linked in Time
  Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee
  In Proceedings of the 31st European Conference on Object-Oriented Programming (ECOOP 2017), LIPIcs, Vol. 74, pp. 8:1-8:30, 2017. Leibniz International Proceedings in Informatics Schloss Dagstuhl - Leibniz - Zentrum fuer Informatik, Dagstuhl Publishing, Germany.
  [PDF | DOI | arXiv | Artifact@DARTS]
  


• Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects
  Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee and Germán Andrés Delbianco
  31st ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2016). Amsterdam, The Netherlands, November 2016. ACM.
  [PDF | arXiv]
  


• Separation Logic and Concurrency
  Aleksandar Nanevski
  Lecture notes for Oregon Programming Languages Summer School (OPLSS 2016)
  Eugene, OR, USA, June 2016.
  [PDF | OPLSS16 page | YouTube]
  


• 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.
  [PDF | Video Abstract | Slides]
  


• 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 | Slides]
  


• 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]
  


• Subjective Auxiliary State for Coarse-Grained Concurrency
  Ruy Ley-Wild and Aleksandar Nanevski
  40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013). Rome, Italy, January 2013. ACM.
  [PDF]