A Verifier of Directed Acyclic Graphs for Model Checking with Memory Consistency Models A Verifier of Directed Acyclic Graphs for Model Checking with Memory Consistency Models

Tatsuya Abe. A verifier of directed acyclic graphs for model checking with memory consistency models. In Proceedings of the 13th Haifa Verification Conference (HVC), volume 10629 of Lecture Notes in Computer Science, pages 51–66. Haifa, November 2017. DOI:10.1007/978-3-319-70389-3_4

This paper introduces VeriDAG, a verification tool for directed acyclic graphs that represent concurrent programs under memory consistency models. VeriDAG has two novel aspects. First, VeriDAG does not handle concurrent programs directly, but operates on directed acyclic graphs whose edges denote dependencies between instructions in the concurrent programs. This provides software model checking under various memory consistency models by replacing the definitions of edge connections, whereas many model checkers are specific to certain memory consistency models. Second, an engine for exploring execution traces is fully implemented in Haskell with manageable exploration strategies. In contrast, similar model checkers use external engines such as SMT solvers and model checkers that ignore relaxed memory consistency models. Thus, VeriDAG provides a research framework on which we can design new memory consistency models and apply exploration strategies for execution traces under memory consistency models. As evidence, this paper compares VeriDAG with an existing model checker, and implements reordering controls, which are heuristic searches for counterexample detection in directed model checking.