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.
@article{arxiv.2107.00271,
title = {On the (Non-)Applicability of a Small Model Theorem to Model Checking STMs},
author = {Heike Wehrheim},
journal= {arXiv preprint arXiv:2107.00271},
year = {2021}
}