The happens-before orders have been widely adopted to model thread interleaving behaviors of concurrent programs. A dedicated ordering theory solver, usually composed of theory propagation, consistency checking, and conflict clause generation, plays a central role in concurrent program verification. We propose a novel preventive reasoning approach that automatically preserves the ordering consistency and makes consistency checking and conflict clause generation omissible. We implement our approach in a prototype tool and conduct experiments on credible benchmarks; results reveal a significant improvement over existing state-of-the-art concurrent program verifiers.

@article{paperbot1424,
  title = {Consistency-preserving propagation for SMT solving of concurrent program verification},
  author = {Zhihang Sun and Hongyu Fan and Fei He},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {6},
  number = {OOPSLA2},
  year = {2022},
  doi = {10.1145/3563321}
}