Satisfiability modulo ordering consistency theory for multi-threaded program verification
| Autor: | Fei He, Hongyu Fan, Zhihang Sun |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Theoretical computer science
Computer science Sequential consistency Concurrency Modulo 020207 software engineering 02 engineering and technology Thread (computing) Solver Satisfiability Consistency theory Consistency (database systems) 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing |
| Zdroj: | PLDI |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|