Abstract

In the past decade, significant progress has been made towards design and development of efficient fine-grained (i.e., lock-free) concurrent data structures and algorithms, which take full advantage of parallel computations. Due to sophisticated interference scenarios and a large number of possible interactions between concurrent threads, working over the same shared data structures and employing fine-grained synchronization primitives (e.g., compare-and-swap command), ensuring correctness of fine-grained concurrent programs is challenging and error-prone.

In my talk, through a series of examples, I will introduce Fine-grained Concurrent Separation Logic (FCSL) – a mechanized logical framework for implementing and verifying fine-grained concurrent programs.

FCSL models effects of concurrent threads, manipulating shared resources, via two basic mathematical structures: state-transition systems (STSs) and partial commutative monoids (PCMs). Being simple enough, this model of concurrent resources, in combination with a small number of program and proof-level commands, is sufficient to give useful specifications and verify a large class of state-of-the-art concurrent libraries. By employing expressive type theory as a way to ascribe specifications to effectful programs, FCSL achieves scalability: even though the proofs for libraries might be large, they are done just once.

FCSL was proved sound with respect to the denotational semantic of action trees and implemented as a monadic embedding in Coq, a general-purpose mechanized framework for formal proofs. That is, concurrent programs written in FCSL ’s language are also Coq programs, so they can make use of all Coq’s features as a programming language. As a part of my talk, I will demonstrate how proofs about concurrent programs in FCSL can be done directly in Coq, taking advantage of Coq’s interactive proof construction machinery.