Automatic Inference of Symbolic Permissions for Sequential Java Programs
In mainstream programming languages such as Java, a common way to enable concurrency is to manually introduce explicit concurrency constructs such as multi-threading. In multi-threaded programs, managing synchronization between threads is a complicated and challenging task for the programmers due to thread interleaving and heap interference that leads to problems such as deadlocks, data races. With these considerations in mind, access permission-based dependencies have been investigated as an alternative approach to verify the correctness of multi-threaded programs and to exploit the implicit concurrency present in sequential programs without using explicit concurrency constraints. However, significant annotation overhead can arise from manually adding permission-based specifications in a source program, diminishing the effectiveness of existing permission-based approaches. In this paper,we present a framework, Sip4J, to automatically extract access permission-based implicit dependencies from sequential Java programs, by performing inter-procedural static analysis of the source code. Moreover, we integrate and extend an existing permission-based verification tool, Pulse, to automatically verify correctness of the inferred specifications and to reason about their concurrent behaviors. Our evaluation on some widely-used benchmarks gives strong evidence of the correctness of the inferred annotations and their effectiveness in enabling concurrency in sequential programs.