Causal Atomicity

Atomicity-checking is a powerful approach for finding subtle concurrency errors in shared-memory multithreaded code. The goal is to verify that certain code sections appear to execute atomically to all other threads. This paper extends Farzan and Madhusudan's recent work on causal atomicity [1], which uses a translation to Petri nets to avoid much of the imprecision of type-system based approaches, to support purity annotations in the style of Flanagan et al. [2]. Purity avoids imprecision for several key idioms, but it has previously been used only in the typesystem setting. Our work is (1) compositional: a different purity analysis could be implemented with minimal extra effort, and similarly another atomicity criterion could be checked without changing the purity analysis, and (2) a conservative extension: the analysis of any program that does not use purity annotations is equivalent to the original analysis.

• Type: Conference
• Year: 2006
• Where: CAV
• Authors: Azadeh Farzan, P. Madhusudan
• Keywords: CAV 2006, Hardware, Purity Analysis, Purity Annotations, Purity Avoids Imprecision