首页> 外文会议>International Conference on Rigorous State-Based Methods >Adding Concurrency to a Sequential Refinement Tower
【24h】

Adding Concurrency to a Sequential Refinement Tower

机译:向顺序精炼塔添加并发

获取原文

摘要

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.
机译:本文定义了一种概念和验证方法,该方法和验证方法用于基于数据精炼和组件结构向抽象状态机的顺序精炼塔中添加并发。我们之前已经为Flashix文件系统开发了这样的优化塔,从中我们可以生成可执行代码(C和Scala)。我们在本文中回答的问题是如何在不破坏初始模块化结构的情况下,基于锁向此类精炼塔添加并发。我们仅通过增强相关组件并添加中间原子性改进来补充已经存在的数据改进,就可以实现这一目标。我们还为这种原子性改进提供了一种验证方法。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号