一句话：提出基于模拟关系的方法，证明 actor/active object 并行实现相对于转移系统规范的正确性。
本文研究描述并行执行进程系统的程序正确性问题，即如何证明并行实现符合以转移系统表达的高层模型。作者提出一种新的正确性证明方法，其实现语言基于 actor 和 active object 并发模型。方法将程序正确性定义为两个转移系统之间的模拟关系：一个给出并行程序的程序语义，另一个由正确性规范描述。该模拟关系利用实现语言并发模型的全局合流性（confluence），从而抽象掉并行进程的细粒度交错。作为概念验证，作者将该方法应用于多核内存系统的并行模拟器，证明其正确性，展示了方法在复杂并行实现验证中的可行性。
This article addresses the long-standing problem of program correctness for programs that describe systems of parallel executing processes. We propose a new method for proving correctness of parallel implementations of high-level models expressed as transition systems. The implementation language underlying the method is based on the concurrency model of actors and active objects. The method defines program correctness in terms of a simulation relation between the transition system that specifies the program semantics of the parallel program and the transition system that is described by the correctness specification. The simulation relation itself abstracts from the fine-grained interleaving of parallel processes by exploiting a global confluence property of the concurrency model of the implementation language considered in this article. As a proof of concept, we apply our method to the correctness of a parallel simulator of multicore memory systems.
@article{paperbot2672,
title = {Proving Correctness of Parallel Implementations of Transition System Models},
author = {Frank de Boer and Einar Broch Johnsen and Violet Ka I Pun and Silvia Lizeth Tapia Tarifa},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {46},
number = {3},
year = {2024},
doi = {10.1145/3660630}
}