Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
复制标题
具有依赖/保证条件的原子分裂以及数据具体化
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
K. G. Pierce
中科院分区：
文献类型：
--
作者：
Cliff B. Jones;K. G. Pierce
本文提出了一种非平凡并行程序的新颖形式开发：异步通信机制 (ACM) 的 Simpson 实现。尽管“4 槽算法”的正确性已在其他地方得到证明，但早期的发展绝不是直观的。本文的目的既包括呈现可理解的（但正式的）设计历史，也包括建立另一种“分裂（软件）原子”的方式。使用“原子性虚构”作为理解开发初始步骤的帮助，将顶层规范开发为代码。这里，依赖保证方法与读/写帧和“分阶段”规范的概念相结合；依赖/保证条件隐含的原子性假设是通过巧妙选择数据表示来实现的。本着合作的精神，本文将开发方法与其他方法进行了比较，因为作者相信建设性比较阐明了“4 槽”规范/开发以及一般并行程序中的许多细节。
This paper presents a novel formal development of a non-trivial parallel program: Simpson's implementation of asynchronous communication mechanisms (ACMs). Although the correctness of the "4-slot algorithm" has been shown elsewhere, earlier developments are by no means intuitive. The aims of this paper include both the presentation of an understandable (yet formal) design history and the establishment of another way of "splitting (software) atoms". Using the "fiction of atomicity" as an aid to understanding the initial steps of development, the top-level specification is developed to code. The rely-guarantee approach is, here, combined with notions of read/write frames and "phased" specifications; the atomicity assumptions implied by rely/guarantee conditions are realised by clever choice of data representation. The development method herein is compared with other approaches ---in a spirit of cooperation--- as the authors believe that constructive comparison elucidates many of the finer points in the "4-slot" specification/development and of parallel programs in general.