On the (Non-)Applicability of a Small Model Theorem to Model Checking STMs

TL;DR

This paper examines whether the small model theorem, which simplifies model checking for STM algorithms, is applicable to verifying the opacity correctness criterion in concurrent shared memory systems.

Contribution

The paper critically analyzes the applicability of the small model theorem to opacity verification in STM algorithms, challenging previous assumptions.

Findings

The small model theorem may not always hold for opacity checking in STM.

Certain conditions under which the theorem is applicable are identified.

Implications for model checking practices in concurrent systems are discussed.

Abstract

Software Transactional Memory (STM) algorithms provide programmers with a synchronisation mechanism for concurrent access to shared variables. Basically, programmers can specify transactions (reading from and writing to shared state) which execute "seemingly" atomic. This property is captured in a correctness criterion called opacity. For model checking opacity of an STM algorithm, we -- in principle -- need to check opacity for all possible combinations of transactions writing to and reading from potentially unboundedly many variables. To still apply automatic model checking techniques to opacity checking, a so called small model theorem has been proven which states that model checking on two variables and two transactions is sufficient for correctness verification of STMs. In this paper, we take a fresh look at this small model theorem and investigate its applicability to opacity checking of STM algorithms.