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...

• Type: Conference
• Year: 2008
• Where: CONCUR
• Authors: Rachid Guerraoui, Marko Vukolic
• Keywords: CONCUR 2008, Distributed And Parallel Computing, Oblivious Atomicity Assertion, Register Operations, Single-writer Multi-reader Register