Purifying Causal Atomicity
in submission, 2008
Abstract
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, 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. Purity avoids imprecision for several key idioms, but it has previously been used only in the type-system 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.
Links
- Full text:
- Project page:
- available here
Contact
- Email (essential):
- (first initial + last name) {at} ccs.neu.edu
- Location (likely):
- West Village H, Office 326
- Post (possible):
-
Northeastern University
Khoury College of Computer Sciences
360 Huntington Ave, 2nd floor
Boston, MA 02115
