Wessel Sinnema: Verifying memory consistency in mCRL2

Event Details

We present a general method to verify an mCRL2 model of a multiprocessor with respect to memory consistency and prove the correctness of this method.

Consequently, we present a way to reformulate most memory models that are defined in terms of serial views using observations. We prove that any execution of a program by a multiprocessor satisfying this formulation is memory consistent under the original memory consistency model. We then express this as a set of predicates on the traces allowed by an mCRL2 model and prove that if all traces allowed by the mCRL2 model satisfy these predicates, then  all executions allowed by the mCRL2 model are consistent with respect to the original memory consistency model.

We also formulate a subset of the C++ memory model in terms of serial views. We prove that if such that serial view exists for every execution allowed by a multiprocessor, then every execution allowed by that processor is consistent under the C++ memory model. The predicates on mCRL2 traces are then expressed as mu-calculus formulas and are used to verify an mCRL2 model of a multiprocessor with respect to local consistency and cache consistency, which are subsets of the serial view representing the C++ memory model. We use these mu-calculus formulas to benchmark the verification an example CPU model using the mCRL2 toolset.