Type inference for atomicity
- 10 January 2005
- conference paper
- Published by Association for Computing Machinery (ACM)
Abstract
Atomicity is a fundamental correctness property in multithreaded programs. This paper presents an algorithm for verifying atomicity via type inference. The underlying type system supports guarded, write-guarded, and unguarded fields, as well as thread-local data, parameterized classes and methods, and protected locks. We describe an implementation of this algorithm for Java and discuss its performance and usability on benchmarks totaling sixty thousand lines of code.Keywords
This publication has 30 references indexed in Scilit:
- Checking Concise Specifications for Multithreaded Software.The Journal of Object Technology, 2004
- Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-CheckingPublished by Springer Nature ,2004
- Type Inference for Parameterized Race-Free JavaPublished by Springer Nature ,2004
- Type Inference Against RacesPublished by Springer Nature ,2004
- Transactional Monitors for Concurrent ObjectsPublished by Springer Nature ,2004
- Transactions for Software Model CheckingElectronic Notes in Theoretical Computer Science, 2003
- Introduction to set constraint-based program analysisScience of Computer Programming, 1999
- Polymorphic type, region and effect inferenceJournal of Functional Programming, 1992
- Linearizability: a correctness condition for concurrent objectsACM Transactions on Programming Languages and Systems, 1990
- ReductionCommunications of the ACM, 1975