并发修订确定性的形式化
计算机科学中的逻辑
2019-12-23 v1
摘要
并发修订是一种旨在保证确定性的并发控制模型，即程序的输出被唯一确定。本文描述了该模型操作语义的 Isabelle/HOL 形式化以及确定性的证明。我们讨论并解决了操作语义中细微的歧义，并简化了确定性的证明。尽管我们的发现似乎并不对应于实现中的缺陷，但该形式化凸显了在并发控制模型的设计与验证中所涉及的一些挑战。
引用
@article{arxiv.1912.09741,
title = {Formalizing Determinacy of Concurrent Revisions},
author = {Roy Overbeek},
journal= {arXiv preprint arXiv:1912.09741},
year = {2019}
}
备注
To appear in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '20), January 20--21, 2020, New Orleans, LA, USA. ACM, New York, NY, USA