Automatic Inference of Symbolic Permissions for Sequential Java Programs

TL;DR

This paper introduces Sip4J, a framework that automatically infers permission-based dependencies in sequential Java programs to facilitate concurrency verification, reducing manual annotation overhead and improving program correctness analysis.

Contribution

The paper presents an automated static analysis approach to extract permission-based dependencies and extends verification tools to analyze concurrent behaviors in sequential Java code.

Findings

High accuracy in inferred permission annotations

Effective verification of concurrent correctness

Enables implicit concurrency in sequential programs

Abstract

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.