Atomic Set Inferencer
The Atomic Set Inferencer helps programmers to convert multi-threaded Java programs from lock-based synchronization to atomic sets.
Atomic sets are a synchronization mechanism in which
the programmer specifies the groups of data that must be accessed
atomically, for example the fields entries and length of an
array-based list implementation. The compiler can check this
specification for consistency, detect deadlocks, and automatically add
the primitives to prevent interleaved access. Atomic sets relieve the
programmer from the burden of recognizing and pruning execution paths
which lead to interleaved access, thereby reducing the potential for
data races. However, manually converting programs from lock-based
synchronization to atomic sets requires reasoning about the program's
concurrency structure, which can be a challenge even for small
programs. Our analysis and tool chain eliminates the challenge by
automating the reasoning.
Publications
- Peter Dinges, Minas Charalambides, and Gul Agha. Automated inference of atomic sets for safe concurrent execution. In Stephen Freund and Corina S. Păsăreanu, editors, PASTE 2013 - 11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, colocated with PLDI 2013, Seattle, WA, USA, June 20, 2013.
- Peter Dinges, Minas Charalambides, and Gul Agha. Automated inference of atomic sets for safe concurrent execution. Technical Report, University of Illinois at Urbana--Champaign, March 2013.
Downloads
See the project's Github page for the source code of the inference tool chain, the data used in above publications, as well as the documentation.
License
The Atomic Set Inferencer tool chain may be used, copied, and modified for education, research, and non-profit purposes as described in the LICENSE file. Copyright (c) 2013 The University of Illinois Board of Trustees. All Rights Reserved.
Acknowledgments
This work was supported in part by sponsorships from the Army Research Office under award number W911NF-09-1-0273, as well as the Air Force Research Laboratory and the Air Force Office of Scientific Research under agreement number FA8750-11-2-0084.
Contact
Please contact Peter Dinges if you have questions, remarks, or suggestions regarding the project.