基于CSP和测试的PSTM事务调度器验证
摘要：在线事务调度器体系结构和算法已经设计了很多，以便保持良好的系统性能，即使对于高并发工作负载也是如此。这些算法中的大部分是直接在目标编程语言中实现的，并进行了实验评估，但没有关于其正确性的理论证明和性能分析。只有少数算法使用形式化方法建模，例如进程代数CSP，以验证它们是否满足无死锁和无饥饿等属性。然而，正如本文所示，仅使用形式化方法也有其不足之处。在本文中，我们首先通过将模型检验器PAT的结果与手工推导得到的预期结果进行比较，分析了之前的CSP模型对PSTM事务调度器的适用性。根据这个分析的结果，我们纠正和扩展了CSP模型。最后，基于新的CSP模型的PAT结果，我们从作业完成时间、中止数和吞吐量的角度分析了PSTM在线事务调度算法的性能。根据我们的发现，我们可以得出结论，为了对值得信赖的软件进行完整的形式化验证，必须同时使用形式化验证和测试。
作者：Miroslav Popovic, Marko Popovic, Branislav Kordic, Huibiao Zhu
论文ID：2305.08380
分类：Distributed, Parallel, and Cluster Computing
分类简称：cs.DC
提交时间：2023-05-16