We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.DC

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Distributed, Parallel, and Cluster Computing

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

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.
Subjects: Distributed, Parallel, and Cluster Computing (cs.DC)
Cite as: arXiv:2107.00271 [cs.DC]
  (or arXiv:2107.00271v1 [cs.DC] for this version)

Submission history

From: Heike Wehrheim [view email]
[v1] Thu, 1 Jul 2021 07:44:14 GMT (24kb)

Link back to: arXiv, form interface, contact.