Sciweavers

ISSTA
2004
ACM

Exploiting purity for atomicity

13 years 9 months ago
Exploiting purity for atomicity
The notion that certain procedures are atomic is a fundamental correctness property of many multithreaded software systems. A procedure is atomic if for every execution there is an equivalent serial execution in which the actions performed by any thread while executing the atomic procedure are not interleaved with actions of other threads. Several existing tools verify atomicity by using commutativity of actions to show that every execution reduces to a corresponding serial execution. However, experiments with these tools have highlighted a number of interesting procedures that, while intuitively atomic, are not reducible. In this paper, we exploit the notion of pure code blocks to verify the atomicity of such irreducible procedures. If a pure block terminates normally, then its evaluation does not change the program state, and hence these evaluation steps can be removed from the program trace before reduction. We develop a static analysis for atomicity based on this insight, and we i...
Cormac Flanagan, Stephen N. Freund, Shaz Qadeer
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Where ISSTA
Authors Cormac Flanagan, Stephen N. Freund, Shaz Qadeer
Comments (0)