May-happen-in-parallel analysis with condition synchronization

Abstract

Concurrent programs can synchronize by means of conditions and/or message passing. In the former, processes communicate and synchronize by means of shared variables that several processes can read and write. In the latter, communication is by sending, receiving and waiting for messages. Condition synchronization is often more efficient but also more difficult to analyze and reason about. In this paper, we leverage an existing may-happen-in-parallel (MHP) analysis, which was designed for a particular form of message passing based on future variables, to handle condition synchronization effectively, thus enabling the analysis of programs that use both mechanisms. This is done by developing a must-have-finished analysis which is used to refine the MHP relations inferred by the original MHP analysis. The information inferred by an MHP has been proven to be essential to infer both safety properties (e.g., deadlock freedom) and liveness properties (termination and resource boundedness) of concurrent programs.