From Traces To Proofs: Proving Concurrent Program Safe

TL;DR

This paper introduces a novel algorithm for constructing automata that capture data-flow dependencies in concurrent programs, enabling efficient proofs of correctness under sequential consistency.

Contribution

It presents a new algorithm for directly constructing automata from data-flow graphs, improving efficiency in proving concurrent program correctness.

Findings

The algorithm is implemented in the ProofTraPar tool.

ProofTraPar effectively proves correctness of cyclic programs.

Results compare favorably to existing tools.

Abstract

Nondeterminism in scheduling is the cardinal reason for difficulty in proving correctness of concurrent programs. A powerful proof strategy was recently proposed [6] to show the correctness of such programs. The approach captured data-flow dependencies among the instructions of an interleaved and error-free execution of threads. These data-flow dependencies were represented by an inductive data-flow graph (iDFG), which, in a nutshell, denotes a set of executions of the concurrent program that gave rise to the discovered data-flow dependencies. The iDFGs were further transformed in to alternative finite automatons (AFAs) in order to utilize efficient automata-theoretic tools to solve the problem. In this paper, we give a novel and efficient algorithm to directly construct AFAs that capture the data-flow dependencies in a concurrent program execution. We implemented the algorithm in a tool called ProofTraPar to prove the correctness of finite state cyclic programs under the sequentially consistent memory model. Our results are encouranging and compare favorably to existing state-of-the-art tools.