From Traces To Proofs: Proving Concurrent Program Safe
This addresses the problem of verifying concurrent program safety for developers and researchers, with incremental improvements in efficiency over existing methods.
The paper tackles the difficulty of proving correctness in concurrent programs by introducing a novel algorithm to directly construct alternative finite automatons (AFAs) from data-flow dependencies, implemented in a tool called ProofTraPar that shows encouraging results compared to state-of-the-art tools.
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.