Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Reports, Documentation, and Standards
  4. A Scalable and Oblivious Atomicity Assertion
 
report

A Scalable and Oblivious Atomicity Assertion

Guerraoui, Rachid  
•
Vukolic, Marko
2008

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 non-atomic 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 operations with the state of the art oblivious assertion takes more than 58 hours to complete, whereas SOAR takes just 9 seconds.

  • Files
  • Details
  • Metrics
Type
report
Author(s)
Guerraoui, Rachid  
Vukolic, Marko
Date Issued

2008

Subjects

Atomicity

•

Assertion

•

Model checking

•

Obliviosness

•

Scalability

Note

Concur 2008 19th International Conference on Concurrency Theory

Written at

EPFL

EPFL units
DCL  
Available on Infoscience
June 8, 2008
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/26145
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés