Automatic Generation of Contracts for Concurrent Java Programs

System Design

This work addresses automatic contract generation for concurrent Java programs, tackling the difficulty of managing atomic sequences in large, multi-threaded applications. Programs with hundreds of atomic blocks or locks are prone to concurrency errors, as developers cannot feasibly reason about all interleavings. The solution involves Contracts for Concurrency, which specify sequences of method calls that must execute atomically. These contracts can serve as documentation, development aids, or as input to a static analysis tool, which verifies atomicity violations. The core contribution of this paper is a set of heuristics that improve automatic contract generation in a SAT, reducing spurious clauses, analysis time, and false positives, while preserving accuracy.

Method Overview

The proposed system operates as follows:

1. Static Analysis of Atomic Blocks: Extract methods invoked within synchronized or atomic regions of Java code.
2. Contract Generation Heuristics:
   • Minimum Number of Atomic Executions: Only create clauses for sequences executed atomically at least n times.
   • Threshold Heuristics: Generate clauses based on sequences consistently executed atomically across the program or within individual modules.
   • Parameterized Contracts: Restrict clauses to sequences operating on the same object to reduce false positives.
   • Partial Verification: Allow smaller clauses for large atomic blocks to ensure all dependencies are captured.
   • Default Contract: Include common clauses from widely-used libraries for quick initial checks.
3. Validation with SAT: Verify that generated contracts correctly represent atomic dependencies and detect potential violations.

This methodology ensures that contracts are fewer, more precise, and reflective of real program dependencies.

Research Questions

• Efficiency: Can automatic heuristics reduce the number of contract clauses and analysis time for large programs?
• Accuracy: Do parameterized and threshold-based contracts correctly capture atomic dependencies without introducing false positives?
• Scalability: Can Gluon handle real-world large-scale software with these heuristics?

Bibtex

@inproceedings{Pereira2022automatic,
    author = {Hugo Gamaliel Pereira and Diogo G Sousa and Jeremy Bradbury and Joao M Lourenço},
    title = {Automatic Generation of Contracts for Concurrent Java Programs},
    booktitle = {INForum 2022 - 14th Simpósio de Informática},
    year = {2022},
}

Acknowledgments

This work was supported by Research Grants ‘PTDC/CCI-COM/32456/2017’ & ‘LISBOA-01-0145-FEDER-032456’. The author acknowledges support from advisors and fellow colleagues who provided guidance during this project.