Sergey, I;
Nanevski, A;
Banerjee, A;
(2015)
Mechanized Verification of Fine-Grained Concurrent Programs.
In:
(Proceedings) 36th ACM SIGPLAN Conference on Programming Language Design and Implementation.
(pp. pp. 77-87).
ACM
Preview |
Text
fcsl-pldi15.pdf - Accepted Version Download (511kB) | Preview |
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.
| Type: | Proceedings paper |
|---|---|
| Title: | Mechanized Verification of Fine-Grained Concurrent Programs |
| Event: | 36th ACM SIGPLAN Conference on Programming Language Design and Implementation |
| Location: | Portland, OR |
| Dates: | 13 June 2015 - 17 June 2015 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/2737924.2737964 |
| Publisher version: | http://doi.org/10.1145/2737924.2737964 |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Compositional program verification, concurrency, separation logic, mechanized proofs, dependent types |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10030730 |
Archive Staff Only
 |
View Item |
