Expressive modular fine-grained concurrency specification

Compared to coarse-grained external synchronization ofoperations on data structures shared between concurrentthreads, fine-grained, internal synchronization can offerstronger progress guarantees and better performance. However,fully specifying operations that perform internalsynchronization modularly is a hard, open problem. The state ofthe art approaches, based on linearizability or on concurrentabstract predicates, have important limitations on theexpressiveness of specifications. Linearizability does notsupport ownership transfer, and the concurrent abstractpredicates-based specification approach requires hardcoding aparticular usage protocol. In this paper, we propose a novelapproach that lifts these limitations and enables fully generalspecification of fine-grained concurrent data structures. Thebasic idea is that clients pass the ghost code required toinstantiate an operation's specification for a specific clientscenario into the operation in a simple form of higher-orderprogramming.We machine-checked the theory of the paper using the Coq proofassistant. Furthermore, we implemented the approach in ourprogram verifier VeriFast and used it to verify two challengingfine-grained concurrent data structures from the literature: amultiple-compare-and-swap algorithm and a lock-coupling list.status: publishe