Satisfiability modulo ordering consistency theory for multi-threaded program verification
Fei He, Zhihang Sun, Hongyu Fan
Abstract
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.
Topics & Concepts
Computer scienceSequential consistencyConsistency (knowledge bases)Consistency modelThread (computing)ModuloSatisfiabilityCache coherenceLocal consistencyWeak consistencySatisfiability modulo theoriesTheoretical computer scienceSolverAlgorithmProgramming languageParallel computingData consistencyDistributed computingStrong consistencyConstraint satisfaction problemMathematicsArtificial intelligenceCPU cacheDiscrete mathematicsCache algorithmsCacheEstimatorProbabilistic logicStatisticsFormal Methods in VerificationLogic, programming, and type systemsSoftware Testing and Debugging Techniques