Sciweavers

Share
CAV
2004
Springer

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

11 years 3 months ago
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...
Ganesh Gopalakrishnan, Yue Yang, Hemanthkumar Siva
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where CAV
Authors Ganesh Gopalakrishnan, Yue Yang, Hemanthkumar Sivaraj
Comments (0)
books