Declarative fence insertion

4 years 7 months ago
Declarative fence insertion
Previous work has shown how to insert fences that enforce sequential consistency. However, for many concurrent algorithms, sequential consistency is unnecessarily strong and can lead to high execution overhead. The reason is that, often, correctness relies on the execution order of a few specific pairs of instructions. Algorithm designers can declare those execution orders and thereby enable memory-modelindependent reasoning about correctness and also ease implementation of algorithms on multiple platforms. The literature has examples of such reasoning, while tool support for enforcing the orders has been lacking until now. In this paper we present a declarative approach to specify and enforce execution orders. Our fence insertion algorithm first identifies the execution orders that a given memory model enforces automatically, and then inserts fences that enforce the rest. Our benchmarks include three off-the-shelf transactional memory algorithms written in C/C++ for which we speci...
John Bender, Mohsen Lesani, Jens Palsberg
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Authors John Bender, Mohsen Lesani, Jens Palsberg
Comments (0)