MPEC: A Multiprocessor Execution Checker

by
Yu Yang

Advised by
Ganesh Gopalakrishnan

The consistency between shared memory multiprocessor execution and shared memory models is very important. We formalize Itanium memory model and design a MultiProcessor Execution Checker (MPEC) to automatically check whether an execution follows the Itanium memory model specification or not. The basic idea is to convert constaints into SAT problems and use SAT solvers to find the answer. Besides, MPEC can give out a feasible path if the multiprocessor execution is allowed, otherwise it will give out an counterexample to explain the failure.