Many online transaction scheduler architectures and algorithms for various software transactional memories have been designed in order to maintain good system performance even for high concurrency workloads. Most of these algorithms were directly implemented in a target programming language, and experimentally evaluated, without theoretical proofs of correctness and analysis of their performance. Only a small number of these algorithms were modeled using formal methods, such as process algebra CSP, in order to verify that they satisfy properties such as deadlock-freeness and starvation-freeness. However, as this paper shows, using solely formal methods has its disadvantages, too. In this paper, we first analyze the previous CSP model of PSTM transaction scheduler by comparing the model checker PAT results with the manually derived expected results, for the given test workloads. Next, according to the results of this analysis, we correct and extend the CSP model. Finally, based on PAT results for the new CSP model, we analyze the performance of PSTM online transaction scheduling algorithms from the perspective of makespan, number of aborts, and throughput. Based on our findings, we may conclude that for the complete formal verification of trustworthy software, both formal verification and it's testing must be jointly used.

翻译：许多针对各种软件事务内存的在线事务调度器架构和算法已被设计出来，以在即使高并发工作负载下也能保持良好系统性能。这些算法大多直接在目标编程语言中实现并经过实验评估，而缺乏正确性的理论证明及其性能分析。仅有少数算法通过形式化方法（如进程代数CSP）建模，以验证其满足无死锁和无饥饿等性质。然而，如本文所示，仅使用形式化方法也存在其局限性。本文首先通过比较模型检查器PAT的结果与给定测试工作负载下手动推导的预期结果，分析了先前的PSTM事务调度器CSP模型。其次，根据分析结果，我们修正并扩展了该CSP模型。最后，基于新CSP模型的PAT结果，我们从完工时间、中止次数和吞吐量角度分析了PSTM在线事务调度算法的性能。基于研究发现，我们得出结论：对于可信软件的完整形式化验证，必须联合使用形式化验证及其测试。