A Refined Ordering Consistency Theory: Full Sequential Consistency and Generalized Preventive Reasoning

Abstract SMT solving with ordering consistency theory achieves state-of-the-art efficiency in bounded model checking of concurrent programs. At its core is a dedicated theory solver that derives the write-serialization (WS) and from-read (FR) orders on the fly, thereby allowing their explicit encodings to be omitted. Additionally, the solver is equipped with preventive propagation , which proactively eliminates theory-level conflicts. This work presents a refined ordering consistency theory that overcomes two existing limitations. First, we address the weak SC problem , where the solver may fail to reconstruct a total WS order and thus admit executions weaker than Sequential Consistency. We identify the core reason as insufficient constraints on WS totality. As a solution, we restore the WS encodings to ensure its totality, while preserving WS derivation to curb the resulting growth in the search space. Second, the existing framework for preventive propagation does not support WS variables or atomicity constraints. We extend it to incorporate these elements, yielding a more general and principled propagation mechanism. Experiments show that our approach soundly prevents weak-SC behaviors, enables effective propagation, and maintains competitive overall performance.