A Scalable and Oblivious Atomicity Assertion

9 years 7 months ago
A Scalable and Oblivious Atomicity Assertion
Abstract. This paper presents SOAR: the first oblivious atomicity assertion with polynomial complexity. SOAR enables to check atomicity of a single-writer multi-reader register implementation. The basic idea underlying the low overhead induced by SOAR lies in greedily checking, in a backward manner, specific points of an execution where register operations could be linearized, rather than exploring all possible precedence relations among these. We illustrate the use of SOAR by implementing it in +CAL. The performance of the resulting automatic verification outperforms comparable approaches by more than an order of magnitude already in executions with only 6 read/write operations. This difference increases to 3-4 orders of magnitude in the "negative" scenario, i.e., when checking some nonatomic execution, with only 5 operations. For example, checking atomicity of every possible execution of a single-writer single-reader (SWSR) register with at most 2 write and 3 read operation...
Rachid Guerraoui, Marko Vukolic
Added 18 Oct 2010
Updated 18 Oct 2010
Type Conference
Year 2008
Authors Rachid Guerraoui, Marko Vukolic
Comments (0)