Concurrent programs are prevalent these days due to the pervasive availability of multi-core and many-core systems. Concurrency bugs are undesirable outcomes that arise when two programs execute concurrently but do not show up if execute sequentially. They are notoriously hard to detect and fix.

Nowadays, several works have been done on detecting and fixing concurrency bugs, but they do not address the fundamental problem, which is to develop techniques that are capable of preventing concurrency bugs systematically in the first place. A good way to do this is to design a fine-tuned locking policy and implement systematically. There have been multiple attempts on getting programmers to write specifications as locking policy, and yet specifications are scarce in practice.

In this work, we aim to prevent concurrency bugs by fully automating the process of generating thread-safe classes from sequential programs. That is, given a class which is assumed to be correct in a sequential environment, we automatically generate a thread-safe class, and do it in a way without requiring a specification of the class. Our approach takes three main steps: (1) infer access annotations through static analysis, (2) synthesize a locking policy based on the access annotations, and (3) consistently and automatically implement the locking policy. Furthermore, we optimize the generated class safely (without breaking linearizability) by reducing the scope of locking. For correctness, we prove that the generated class is linearizable (modulo some assumptions) to the sequential class and is always deadlock-free. Our approach is implemented as a self-contained toolkit called AutoLock for Java programs, and empirically evaluated on a set of 45 benchmark programs (with a total of 64,447 lines).

This work has been accepted by ASE’20 .