Reducing State Explosion for Software Model Checking with Relaxed Memory Consistency Models

TL;DR

This paper investigates the challenges of state explosion in software model checking under relaxed memory models, proposes optimizations, and demonstrates their effectiveness through experimental verification of concurrent copying protocols.

Contribution

It identifies causes of state explosion with multiple memory models, introduces specific optimizations, and applies them to McSPIN for the first time to verify complex protocols.

Findings

Optimizations reduce state explosion in model checking.

McSPIN effectively verifies protocols under relaxed memory models.

First successful model checking of concurrent copying protocols with relaxed memory models.

Abstract

Software model checking suffers from the so-called state explosion problem, and relaxed memory consistency models even worsen this situation. What is worse, parameterizing model checking by memory consistency models, that is, to make the model checker as flexible as we can supply definitions of memory consistency models as an input, intensifies state explosion. This paper explores specific reasons for state explosion in model checking with multiple memory consistency models, provides some optimizations intended to mitigate the problem, and applies them to McSPIN, a model checker for memory consistency models that we are developing. The effects of the optimizations and the usefulness of McSPIN are demonstrated experimentally by verifying copying protocols of concurrent copying garbage collection algorithms. To the best of our knowledge, this is the first model checking of the concurrent copying protocols under relaxed memory consistency models.