Types for Atomicity: Static Checking and Inference for Java by Cormac Flanagan, Stephen N. Freund, Marina Lifshin, and Shaz Qadeer:
Atomicity is a fundamental correctness property in multithreaded programs. A method is atomic if, for every execution, there is an equivalent serial execution in which the actions of the method are not interleaved with actions of other threads. Atomic methods are amenable to sequential reasoning, which signiï¬cantly facilitates subsequent analysis and veriï¬cation. This article presents a type system for specifying and verifying the atomicity of methods in multithreaded Java programs using a synthesis of Lipton’s theory of reduction and type systems for race detection. The type system supports guarded, write-guarded, and unguarded ï¬elds, as well as thread-local data, parameterized classes and methods, and protected locks. We also present an algorithm for verifying atomicity via type inference. We have applied our type checker and type inference tools to a number of commonly used Java library classes and programs. These tools were able to verify the vast majority of methods in these benchmarks as atomic, indicating that atomicity is a widespread methodology for multithreaded programming. In addition, reported atomicity violations revealed some subtle errors in the synchronization disciplines of these programs.
Recent comments
17 weeks 10 hours ago
17 weeks 13 hours ago
17 weeks 13 hours ago
39 weeks 1 day ago
43 weeks 3 days ago
45 weeks 21 hours ago
45 weeks 21 hours ago
47 weeks 5 days ago
1 year 2 days ago
1 year 2 days ago