Benjamin Lerner

Purifying Causal Atomicity

copyright notice

Benjamin Lerner and Dan Grossman

in submission, 2008


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.



download vcard icon
Email (essential):
Location (likely):
West Village H, Office 326
Post (possible):
Northeastern University
Khoury College of Computer Sciences
360 Huntington Ave, 2nd floor
Boston, MA 02115
work Lecturer Office 326