Abstract | ||
---|---|---|
Efficient concurrent programs and data structures rarely employ coarse-grained synchronization mechanisms (i.e., locks); instead, they implement custom synchronization patterns via fine-grained primitives, such as compare-and-swap. Due to sophisticated interference scenarios between threads, reasoning about such programs is challenging and error-prone, and can benefit from mechanization. In this paper, we present the first completely formalized framework for mechanized verification of full functional correctness of fine-grained concurrent programs. Our tool is based on the recently proposed program logic FCSL. It is implemented as an embedded 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. We illustrate the proof layout in FCSL by example, outline its infrastructure, and report on our experience of using FCSL to verify a number of concurrent algorithms and data structures. |
Year | DOI | Venue |
---|---|---|
2015 | 10.1145/2737924.2737964 | PLDI |
Keywords | Field | DocType |
Compositional program verification,concurrency,dependent types,mechanized proofs,separation logic | Data structure,Separation logic,Programming language,Concurrency,Computer science,Correctness,Theoretical computer science,Thread (computing),Mathematical proof,Scalability,Proof assistant | Conference |
Volume | Issue | ISSN |
50 | 6 | 0362-1340 |
Citations | PageRank | References |
28 | 0.80 | 38 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Ilya Sergey | 1 | 39 | 1.95 |
Aleksandar Nanevski | 2 | 583 | 27.01 |
Anindya Banerjee | 3 | 1324 | 70.68 |