Adding Concurrency to a Sequential Refinement Tower
Adding Concurrency to a Sequential Refinement Tower
复制标题
DOI：
10.1007/978-3-030-48077-6_2
复制
发表时间：
2020-04-22
期刊：
影响因子：
--
通讯作者：
Reif W
中科院分区：
文献类型：
--
作者：
Schellhorn G;Bodenmüller S;Pfähler J;Reif W
本文定义了一种概念和验证方法，用于在抽象状态机的顺序改进塔中添加并发，该塔是基于数据改进和组件结构。我们较早地为Flashix文件系统开发了这样的改进塔，我们从中生成可执行文件（C和Scala）代码。
我们在本文中回答的问题是，如何将基于锁的并发性添加到这种改进塔中，而不会破坏初始模块化结构。我们仅通过增强相关组件并添加中间原子性改进来实现这一目标，从而补充已经存在的数据改进。我们还提供了这种原子性改进的验证方法。
This paper defines a concept and a verification methodology for adding concurrency to a sequential refinement tower of abstract state machines, that is based on data refinement and a component structure. We have developed such a refinement tower for the Flashix file system earlier, from which we generate executable (C and Scala) Code. The question we answer in this paper, is how to add concurrency based on locks to such a refinement tower, without breaking the initial modular structure. We achieve this by just enhancing the relevant components, and adding intermediate atomicity refinements that complement the data refinements that are already there. We also give a verification methodology for such atomicity refinements.
登录
查看更多内容
影响因子：
1.3
作者：
HERLIHY, MP;WING, JM
通讯作者：
WING, JM
影响因子：
22.7
作者：
LIPTON, RJ
通讯作者：
LIPTON, RJ
DOI：
10.1007/s10009-014-0308-3
发表时间：
2015-11-01
影响因子：
1.5
作者：
Ernst, Gidon;Pfaehler, Joerg;Reif, Wolfgang
通讯作者：
Reif, Wolfgang
影响因子：
1
作者：
LYNCH, N;VAANDRAGER, F
通讯作者：
VAANDRAGER, F
影响因子：
1.1
作者：
ABADI, M;LAMPORT, L
通讯作者：
LAMPORT, L