# 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

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.