2021/07/01 by Heike Wehrheim, Wehrheim, Heike
Computer Science · Social Sciences · #Access Control and Trust #Distributed #Distributed systems and fault tolerance #FOS: Computer and information sciences #Parallel #Parallel Computing and Optimization Techniques #Petri Nets in System Modeling #and Cluster Computing (cs.DC)
paper · pdf · doi:10.48550/arxiv.2107.00271
openalex publication_date 2021/07/01 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
Software Transactional Memory (STM) algorithms provide programmers with a\nsynchronisation mechanism for concurrent access to shared variables. Basically,\nprogrammers can specify transactions (reading from and writing to shared state)\nwhich execute "seemingly" atomic. This property is captured in a correctness\ncriterion called opacity. For model checking opacity of an STM algorithm, we --\nin principle -- need to check opacity for all possible combinations of\ntransactions writing to and reading from potentially unboundedly many\nvariables.\n To still apply automatic model checking techniques to opacity checking, a so\ncalled small model theorem has been proven which states that model checking on\ntwo variables and two transactions is sufficient for correctness verification\nof STMs. In this paper, we take a fresh look at this small model theorem and\ninvestigate its applicability to opacity checking of STM algorithms.\n