Atomizer: a dynamic atomicity checker for multithreaded programs. Ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected interactions between concurrent threads. Much previous work has focused on detecting race conditions, but the absence of race conditions does not by itself prevent undesired thread interactions. We focus on the more fundamental non-interference property of atomicity; a method is atomic if its execution is not affected by and does not interfere with concurrently-executing threads. Atomic methods can be understood according to their sequential semantics, which significantly simplifies (formal and informal) correctness arguments.This paper presents a dynamic analysis for detecting atomicity violations. This analysis combines ideas from both Lipton’s theory of reduction and earlier dynamic race detectors. Experience with a prototype checker for multithreaded Java code demonstrates that this approach is effective for detecting errors due to unintended interactions between threads. In particular, our atomicity checker detects errors that would be missed by standard race detectors, and it produces fewer false alarms on benign races that do not cause atomicity violations. Our experimental results also indicate that the majority of methods in our benchmarks are atomic, supporting our hypothesis that atomicity is a standard methodology in multithreaded programming.

This software is also peer reviewed by journal TOMS.

References in zbMATH (referenced in 17 articles )

Showing results 1 to 17 of 17.
Sorted by year (citations)

  1. Bouajjani, Ahmed; Emmi, Michael; Enea, Constantin; Ozkan, Burcu Kulahcioglu; Tasiran, Serdar: Verifying robustness of event-driven asynchronous programs against concurrency (2017)
  2. Mukherjee, Suvam; Kumar, Arun; D’Souza, Deepak: Detecting all high-level dataraces in an RTOS kernel (2017)
  3. Beckert, Bernhard; Klebanov, Vladimir: A dynamic logic for deductive verification of multi-threaded programs (2013)
  4. Gligoric, Milos; Majumdar, Rupak: Model checking database applications (2013)
  5. Navabi, Armand; Zhang, Xiangyu; Jagannathan, Suresh: Dependence analysis for safe futures (2012)
  6. Guerraoui, Rachid; Henzinger, Thomas A.; Singh, Vasu: Verification of STM on relaxed memory models (2011)
  7. Wang, Chao; Kundu, Sudipta; Limaye, Rhishikesh; Ganai, Malay; Gupta, Aarti: Symbolic predictive analysis for concurrent programs (2011)
  8. Martin, Jean-Phillipe; Hicks, Michael; Costa, Manuel; Akritidis, Periklis; Castro, Miguel: Dynamically checking ownership policies in concurrent C/C++ programs (2010)
  9. Usui, Takayuki; Behrends, Reimer; Evans, Jacob; Smaragdakis, Yannis: Adaptive locks: combining transactions and locks for efficient concurrency (2010)
  10. Wang, Chao; Limaye, Rhishikesh; Ganai, Malay; Gupta, Aarti: Trace-based symbolic analysis for atomicity violations (2010)
  11. Farzan, Azadeh; Madhusudan, P.: The complexity of predicting atomicity violations (2009)
  12. Groves, Lindsay; Colvin, Robert: Trace-based derivation of a scalable lock-free stack algorithm (2009)
  13. Sadowski, Caitlin; Freund, Stephen N.; Flanagan, Cormac: SingleTrack: a dynamic determinism checker for multithreaded programs (2009)
  14. Flanagan, Cormac; Freund, Stephen N.: Atomizer: A dynamic atomicity checker for multithreaded programs (2008)
  15. Wojcicki, Margaret A.; Strooper, Paul: Maximising the information gained from a study of static analysis technologies for concurrent software (2007) ioport
  16. Ringenburg, Michael F.; Grossman, Dan: AtomCaml: first-class atomicity via rollback (2005)
  17. Flanagan, Cormac; Freund, Stephen N.: Atomizer: a dynamic atomicity checker for multithreaded programs (2004)