发表机构
Nanjing University; The Chinese University of Hong Kong, Shenzhen; Hunan University（南京大学; 香港中文大学（深圳）; 湖南大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究在Rocq中首次形式化验证了事务性异常模式（TAPs）及其弱隔离级别表征，修复了原始定义中的两个缺陷，并集成到检查器Plume中。
AI 中文摘要
最近提出的事务性异常模式（TAPs）为弱隔离级别提供了语义表征，并作为基于TAP的隔离检查的基础。然而，这些表征目前仅以纸笔证明的形式存在。我们在Rocq中首次提出了TAPs及其相关弱隔离级别的机器检查形式化。我们进一步建立了相应基于TAP的表征定理的机器检查证明。机械化过程揭示了原始表述中的两个微妙问题：一个欠指定的事务历史模型，以及一个不完整的读原子性隔离级别的TAP表征，该表征未能捕获会话保证的违反。我们通过细化事务历史的定义和相应的TAP定义来解决这些问题，并在Rocq中重新建立了所有表征定理。这些细化已进一步集成到弱隔离检查器Plume中。
英文摘要
Recently proposed transactional anomalous patterns (TAPs) provide a semantic characterization of weak isolation levels and serve as the foundation for TAP-based isolation checking. Yet, these characterizations currently exist only as pen-and-paper proofs. We present the first machine-checked formalization of TAPs and their associated weak isolation levels in Rocq. We further establish machine-checked proofs of the corresponding TAP-based characterization theorems. The mechanization process revealed two subtle issues in the original presentation: an underspecified transaction history model and an incomplete TAP characterization of the Read Atomicity isolation level that failed to capture violations of session guarantees. We address these issues by refining the definition of transaction histories and the corresponding TAP definitions, and re-establish all characterization theorems in Rocq. These refinements have further been integrated into the weak isolation checker Plume.
Comments19 pages, 13 figures, 1 table
