Analyzing multi-threaded programs is hard due to the number of thread interleavings. Partial orders can be used for modeling and analyzing multi-threaded programs. However, there is no dedicated decision procedure for solving partial-order constraints. In this paper, we propose a novel ordering consistency theory for multi-threaded program verification under sequential consistency, and we elaborate its theory solver, which realizes incremental consistency checking, minimal conflict clause generation, and specialized theory propagation to improve the efficiency of SMT solving. We conducted extensive experiments on credible benchmarks; the results show significant promotion of our approach.
Zord is the tool that implements our approach. The source code contains all source code of Zord. Please refer to readme.txt for instructions to compile Zord.
The supplementary archive contains all data, tables and used benchmark programs in our evaluation. The following files are in the archive:
benchmarks/SVCOMP-Benchmarks/*: Benchmarks from SV-COMP 2019, used in our main experiments (Sections 6.2 and 6.3).
benchmarks/Nidhugg-Benchmarks/* : Benchmarks from Nidhugg suite, used in our experiment with stateless model checkers (Section 6.4).
logs/* : The raw outputs of each tool in all experiments.
tables/* : Processed results of all experiments.