Parameterized Model Checking Modulo Explicit Weak Memory Models

TL;DR

This paper introduces a modular framework for model checking parameterized systems with explicit weak memory models, extending existing tools to handle various memory models like TSO and PSO, demonstrated through initial promising experiments.

Contribution

It extends the MCMT framework with explicit weak memory models and implements it in Cubicle-W, enabling seamless switching between different memory models.

Findings

Initial experiments with TSO-like memory model are promising.

Framework allows flexible adaptation to different weak memory models.

Implementation in Cubicle-W demonstrates practical applicability.

Abstract

We present a modular framework for model checking parameterized array-based transition systems with explicit access operations on weak memory. Our approach extends the MCMT (Model Checking Modulo Theories) framework of Ghilardi and Ranise with explicit weak memory models. We have implemented this new framework in Cubicle-W, an extension of the Cubicle model checker. The modular architecture of our tool allows us to change the underlying memory model seamlessly (TSO, PSO...). Our first experiments with a TSO-like memory model look promising.