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

07/01/2021
by   Heike Wehrheim, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset