QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings

We study the problem of formally verifying shared memory multiprocessor executions against memory consistency models--an important step during post-silicon verification of multiprocessor machines. We employ our previously reported style of writing formal specifications for shared memory models in higher order logic (HOL), obtaining intuitive as well as modular specifications. Our specification consists of a conjunction of rules that constrain the global visibility order. Given an execution to be checked, our algorithm generates Boolean constraints that capture the conditions under which the execution is legal under the visibility order. We initially took the approach of specializing the memory model HOL axioms into equivalent (for the execution to be checked) quantified boolean formulae (QBF). As this technique proved inefficient, we took the alternative approach of converting the HOL axioms into a program that generates a SAT instance when run on an execution. In effect, the quantific...

• Type: Conference
• Year: 2004
• Where: CAV
• Authors: Ganesh Gopalakrishnan, Yue Yang, Hemanthkumar Sivaraj
• Keywords: Boolean Constraints, CAV 2004, Hardware, Memory Model, Shared Memory