The overall problem addressed in this paper is the long-standing problem of program correctness, and in particular programs that describe systems of parallel executing processes. We propose a new method for proving correctness of parallel implementations of high-level transition system specifications. The implementation language underlying the method is based on the model of active (or concurrent) objects. The method defines correctness in terms of a simulation relation between the transition system which specifies the program semantics 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 particular model of active objects considered in this paper. As a proof-of-concept we apply our method to the correctness of a parallel simulator of multicore memory systems.

翻译：本文探讨的核心问题是程序正确性这一长期存在的难题，特别关注描述并行执行进程系统的程序。我们提出了一种新方法，用于证明高层过渡系统规范的并行实现的正确性。该方法所基于的实现语言以主动（或并发）对象模型为基础。该方法通过模拟关系来定义正确性，该关系连接了指定程序语义的过渡系统与由正确性规范描述的过渡系统。该模拟关系本身通过利用本文所考虑的特定主动对象模型的全局合流性质，从并行进程的细粒度交错中抽象出来。作为概念验证，我们将该方法应用于多核内存系统并行模拟器的正确性验证。