Preventing Atomicity Violations with Contracts

TL;DR

This paper introduces a contract-based approach to prevent atomicity violations in concurrent programs, especially when using third-party modules, by specifying correlated method executions and verifying correctness through static analysis.

Contribution

It proposes a novel contract system for concurrency that specifies correlated methods to ensure atomicity and a static analysis methodology to verify these contracts in real-world software.

Findings

Identified atomicity violation in Tomcat 6.0

Developed a static analysis tool for contract verification

Successfully applied to real-world software packages

Abstract

Software developers are expected to protect concurrent accesses to shared regions of memory with some mutual exclusion primitive that ensures atomicity properties to a sequence of program statements. This approach prevents data races but may fail to provide all necessary correctness properties.The composition of correlated atomic operations without further synchronization may cause atomicity violations. Atomic violations may be avoided by grouping the correlated atomic regions in a single larger atomic scope. Concurrent programs are particularly prone to atomicity violations when they use services provided by third party packages or modules, since the programmer may fail to identify which services are correlated. In this paper we propose to use contracts for concurrency, where the developer of a module writes a set of contract terms that specify which methods are correlated and must be executed in the same atomic scope. These contracts are then used to verify the correctness of the main program with respect to the usage of the module(s). If a contract is well defined and complete, and the main program respects it, then the program is safe from atomicity violations with respect to that module. We also propose a static analysis based methodology to verify contracts for concurrency that we applied to some real-world software packages. The bug we found in Tomcat 6.0 was immediately acknowledged and corrected by its development team.