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.
Contributors:
Aleksandar Nanevski
Ilya Sergey
Ruy Ley-Wild
German Delbianco
Anindya Banerjee
Source code for FCSL and associated tools:
In case if you decide to build and run Coq/FCSL natively in your
system, you will require the following files and documents:
- 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
- Coq 8.4 source files
[Tarball];
- Ssreflect 1.4 source files
[Tarball];
- Proof General source files
[Tarball].
Supplementary material:
- Accompanying tutorial
and code commentary (in PDF), complementing the library, and the PLDI 2015
research paper with a
description of the structure of the sources and instructions for
compiling/browsing through FCSL.
-
Subjective Auxiliary State for Coarse-Grained Concurrency
Aleksandar Nanevski and Ruy Ley-Wild. POPL 2013.
This paper introduces subjective auxiliary state (in a coarse-grained setting), which is based on the following two ideas.
First, auxiliary state in concurrent programs
should be endowed with the algebraic structure of partial commutative monoids (PCM). Second,
concurrent programs should contain two thread-local auxiliary variables: one capturing the
contribution of the thread itself, and another capturing the combined contributions of all other threads.
The ideas are illustrated on several verified examples, including the first verification of a
higher-order iterator.
-
Communicating State Transition
Systems for Fine-Grained Concurrent Resources (Extended version)
Aleksandar Nanevski, Ruy Ley-Wild,
Ilya Sergey and Germán Andrés Delbianco. ESOP 2014.
This paper adapts subjective auxiliary state to the fine-grained setting, thus introducing FCSL. It
explains the logical foundations of FCSL and presents
the formalization of the CAS-lock and a coarse-grained
incrementor. The appendix contains a detailed description of FCSL's
semantics, as well as the intuition behind formalization of the
Ticketed lock.
-
Specifying and Verifying
Concurrent Algorithms with Histories and Subjectivity
(Extended version)
Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee. ESOP 2015.
This paper introduces auxiliary resources in the form of
time-stamped histories as a method for specifying and verifying
coarse- and fine-grained data structures. It illustrates the approach
by a number of examples, including the Treiber stack,
Producer/Consumer and the Flat Combiner.
- Mechanized verification of fine-grained concurrent programs
Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee. PLDI 2015.
This paper presents the implementation of FCSL in Coq, and illustrates
it on an example of a fine-grained algorithm for
in-place construction of a spanning tree of a graph. The example shows
that auxiliary state in the subjective setting suffices for easy verification
of concurrent algorithms over data structures with "deep sharing", such as graphs.