Sciweavers

Share
ASPLOS
2011
ACM

Specifying and checking semantic atomicity for multithreaded programs

8 years 25 days ago
Specifying and checking semantic atomicity for multithreaded programs
In practice, it is quite difficult to write correct multithreaded programs due to the potential for unintended and nondeterministic interference between parallel threads. A fundamental correctness property for such programs is atomicity—a block of code in a program is atomic if, for any parallel execution of the program, there is an execution with the same overall program behavior in which the block is executed serially. We propose semantic atomicity, a generalization of atomicity with respect to a programmer-defined notion of equivalent behavior. We propose an assertion framework in which a programmer can use bridge predicates to specify noninterference properties at l of abstraction of their application. Further, we propose a novel algorithm for systematically testing atomicity specifications on parallel executions with a bounded number of interruptions— i.e. atomic blocks whose execution is interleaved with that of other threads. We further propose a set of sound heuristics ...
Jacob Burnim, George C. Necula, Koushik Sen
Added 24 Aug 2011
Updated 24 Aug 2011
Type Journal
Year 2011
Where ASPLOS
Authors Jacob Burnim, George C. Necula, Koushik Sen
Comments (0)
books