Sciweavers

CHARME
2003
Springer

Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT

14 years 16 days ago
Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT
We present a non-operational approach to specifying and analyzing shared memory consistency models. The method uses higher order logic to capture a complete set of ordering constraints on execution traces, in an axiomatic style. A direct encoding of the semantics with a constraint logic programming language provides an interactive and incremental framework for exercising and verifying finite test programs. The framework has also been adapted to generate equivalent boolean satisfiability (SAT) problems. These techniques make a memory model specification executable, a powerful feature lacked in most non-operational methods. As an example, we provide a concise formalization of the Intel Itanium memory model and show how constraint solving and SAT solving can be effectively applied for computer aided analysis. Encouraging initial results demonstrate the scalability for complex industrial designs.
Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, K
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where CHARME
Authors Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind
Comments (0)