Expressive modular fine-grained concurrency specification

Expressive modular fine-grained concurrency specification,10.1145/1925844.1926417,Sigplan Notices,Bart Jacobs,Frank Piessens

Expressive modular fine-grained concurrency specification   (Citations: 2)
BibTex | RIS | RefWorks Download
Compared to coarse-grained external synchronization of operations on data structures shared between concurrent threads, fine-grained, internal synchronization can offer stronger progress guarantees and better performance. However, fully specifying operations that perform internal synchronization modularly is a hard, open problem. The state of the art approaches, based on linearizability or on concurrent abstract predicates, have important limitations on the expressiveness of specifications. Linearizability does not support ownership transfer, and the concurrent abstract predicates-based specification approach requires hardcoding a particular usage protocol. In this paper, we propose a novel approach that lifts these limitations and enables fully general specification of fine-grained concurrent data structures. The basic idea is that clients pass the ghost code required to instantiate an operation's specification for a specific client scenario into the operation in a simple form of higher-order programming. We machine-checked the theory of the paper using the Coq proof assistant. Furthermore, we implemented the approach in our program verifier VeriFast and used it to verify two challenging fine-grained concurrent data structures from the literature: a multiple-compare-and-swap algorithm and a lock-coupling list.
Journal: Sigplan Notices - SIGPLAN , pp. 271-282, 2011
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Sort by: