Monitoring Atomicity in Concurrent Programs

  • Madhusudan Parthasarathy | University of Illinois at Urbana-Champaign

A relatively new technique for finding errors in concurrent programs proceeds by identifying *generic* properties that capture correct concurrent interaction patterns, and by identifying errors by observing deviations from these specifications. One such generic specification is that of identifying blocks of code that one expects to be atomicity.

We study the problem of monitoring concurrent program runs for atomicity (serializability) 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.

Speaker Details

Madhusudan Parthasarathy has a long name. He is an assistant professor at University of Illinois at Urbana-Champaign working in formal verification, model-checking and automata theory. He graduated from the Institute of Mathematical Sciences in Chennai with a PhD, and spent three years as a post-doctoral fellow under Rajeev Alur at the University of Pennsylvania prior to his move to the midwest.

Watch Next