Publications
Sharing a Sequential Program: Correctness and Concurrency Analysis
Abstract
It seems to be generally accepted that designing correct and efficient concurrent software is a sophisticated task that can only be held by experts. A crucial challenge then is to convert sequential code produced by a “mainstream” programmer into concurrent one. Various synchronization techniques may be used for this, eg, locks or transactional memory, but what does it mean for the resulting concurrent implementation to be correct? And which synchronization primitives provide more efficiency at the end? In this paper, we introduce a correctness criterion for a concurrent “wrapper” of a sequential program, ie, a transformation that enables the use of a sequential data structure in a concurrent system. Informally, we require the resulting concurrent implementation to be locally sequential: concurrent threads simply run the given sequential code and let the implementation worry about the potential conflicts. To make sense globally, the implementation should also be linearizable with respect to the object type of the data structure. We then evaluate the performance of different concurrent implementations in terms of the sets of schedules (interleavings of steps of the sequential code) they accept. Intuitively, this captures the amount of concurrency that a given implementation can stand. This allowed us to analyze relative power of seemingly incomparable synchronization techniques, such as various forms of locking and transactional memory.
- Date
- 2012
- Authors
- Vincent Gramoli, Petr Kuznetsov, Srivatsan Ravi
- Journal
- arXiv preprint arXiv:1203.4751