Monitoring atomicity in concurrent programs

Azadeh Farzan, P. Madhusudan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We study the problem of monitoring concurrent program runs for atomicity violations. Unearthing fundamental results behind scheduling algorithms in database control, we build space-efficient monitoring algorithms for checking atomicity that use space polynomial in the number of active threads and entities, and independent of the length of the run monitored. Second, by interpreting the monitoring algorithm as a finite automaton, we solve the model checking problem for atomicity of finite-state concurrent models. This establishes (for the first time) that model checking finite-state concurrent models for atomicity is decidable, and remedies incorrect proofs published in the literature. Finally, we exhibit experimental evidence that our atomicity monitoring algorithm gives substantial time and space benefits on benchmark applications.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 20th International Conference, CAV 2008, Proceedings
Pages52-65
Number of pages14
DOIs
StatePublished - 2008
Event20th International Conference on Computer Aided Verification, CAV 2008 - Princeton, NJ, United States
Duration: Jul 7 2008Jul 14 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5123 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other20th International Conference on Computer Aided Verification, CAV 2008
CountryUnited States
CityPrinceton, NJ
Period7/7/087/14/08

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Monitoring atomicity in concurrent programs'. Together they form a unique fingerprint.

Cite this