关于小模型定理对模型检验STM的（不）适用性
On the (Non-)Applicability of a Small Model Theorem to Model Checking STMs
摘要：
软件事务存储器（STM）算法为程序员提供了一种同步机制，用于并发访问共享变量。基本上，程序员可以指定“看似”原子执行的事务（从共享状态读取和向共享状态写入）。这个属性在一个称为不透明度的正确性标准中被捕获。对于STM算法的模型检验不透明性，原则上，我们需要检查对潜在无限多变量进行读写的事务的所有可能组合的不透明性。为了仍然将自动模型检验技术应用于不透明性检验，已经证明了所谓的小模型定理，该小模型定理指出，对两个变量和两个事务的模型检验足以用于STM的正确性验证。在本文中，我们重新审视这个小模型定理，并探讨其适用性STM算法的不透明性检查。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
