分区一致性：弱内存一致性系统建模及其实现正确性证明的实例研究
Partition Consistency: A Case Study in Modeling Systems with Weak Memory Consistency and Proving Correctness of their Implementations
摘要：
多进程系统，包括网格系统、多处理器和多核计算机，包含各种专用硬件和软件机制，这些机制加快了计算速度，但导致复杂的内存行为。因此，并发程序的可能结果可能是不可预料的。存储器一致性模型是对这种系统的行为的描述。抽象内存一致性模型的目标是捕获具体的实现和架构。因此，实现或体系结构的形式化规范是必要的，并且需要证明抽象模型和具体模型之间的对应关系。本文提供了一个案例研究这一进程。我们指定了一个新的模型，分区一致性，概括了许多现有的一致性模型。一个具体的消息传递网络模型也被指定。在此网络模型上实现了分区一致性，并证明了其正确性。一个中间层次的抽象是用来促进证明。所有三个抽象层次都是使用同一个框架来指定的。本文旨在说明一个一般的方法和技术，指定内存一致性模型，并证明其实现的正确性。
英文摘要：
Multiprocess systems, including grid systems, multiprocessors and multicore computers, incorporate a variety of specialized hardware and software mechanisms, which speed computation, but result in complex memory behavior. As a consequence, the possible outcomes of a concurrent program can be unexpected. A memory consistency model is a description of the behaviour of such a system. Abstract memory consistency models aim to capture the concrete implementations and architectures. Therefore, formal specification of the implementation or architecture is necessary, and proofs of correspondence between the abstract and the concrete models are required. This paper provides a case study of this process. We specify a new model, partition consistency, that generalizes many existing consistency models. A concrete message-passing network model is also specified. Implementations of partition consistency on this network model are then presented and proved correct. A middle level of abstraction is utilized to facilitate the proofs. All three levels of abstraction are specified using the same framework. The paper aims to illustrate a general methodology and techniques for specifying memory consistency models and proving the correctness of their implementations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
