In this paper we present a theory for the refinement of shared-memory concurrent algorithms from specifications. Our approach avoids restrictive atomicity contraints. It provides a range of constructs for specifying concurrent programs and laws for refining these to code. We augment pre and post condition specifications with Jones' rely and guarantee conditions, which we encode as commands within a wide-spectrum language. Program components are specified using either partial and total correctness versions of end-to-end specifications. Operations on shared data structures and atomic machine operations (e.g. compare-and-swap) are specified using an atomic specification command. All the above constructs are defined in terms of a simple core language, based on four primitive commands and a handful of operators, and for which we have developed an extensive algebraic theory in Isabelle/HOL. For shared memory programs, expression evaluation is subject to fine-grained interference and we have avoided atomicity restrictions other than for read and write of primitive types (words). Expression evaluation and assignment commands are also defined in terms of our core language primitives, allowing laws for reasoning about them to be proven in the theory. Control structures such as conditionals, recursion and loops are all defined in terms of the core language. In developing the laws for refining to such structures from specifications we have taken care to develop laws that are as general as possible; our laws are typically more general than those found in the literature. In developing our concurrent refinement theory we have taken care to focus on the algebraic properties of our commands and operators, which has allowed us to reuse algebraic theories, including well-known theories, such as lattices and boolean algebra, as well as programming-specific algebras, such as our synchronous algebra.


翻译:在本文中,我们提出了一个理论,用于完善来自规格的共享模拟并行算法。我们的方法避免了限制性原子反向。它提供了一系列结构,用于为完善这些算法而具体指定并行的程序和法律。我们通过琼斯的依靠和保证条件来增加条件前和后规格,我们将这些条件编码为宽频语言中的指令。我们用端到端规格的局部和完全正确性版本来指定方案构成部分。关于共享数据结构和原子机器操作(例如比较和擦拭)的操作,使用原子规格指令来指定。所有上述构造都是用简单的核心语言来定义的,以四种原始指令和少数操作者为基础,我们为此在伊莎贝尔/HOL中制定了广泛的代数理论。对于共同记忆程序,表达评价会受到精细的干扰,我们避免了原子限制,而不是读和写原始类型(言词)的原子限制。表达评估和分配指令也可以用我们的核心语言原始语言术语来定义,允许用法律来解释它们,在理论中进行推理。 控制这些理论结构,例如修炼法,例如修炼法,我们一般的精细的精炼,我们一般的精炼法,我们从修的精炼法,我们从修的精炼到修的精炼法,我们有。 等的精炼法,我们从修的精细的精细的精细的精细的精细的精细的精细的精细的精细的精细的精细。

0
下载
关闭预览

相关内容

GitHub 发布的文本编辑器。
专知会员服务
25+阅读 · 2021年4月2日
【干货书】机器学习速查手册,135页pdf
专知会员服务
125+阅读 · 2020年11月20日
专知会员服务
52+阅读 · 2020年9月7日
【DeepMind】强化学习教程,83页ppt
专知会员服务
151+阅读 · 2020年8月7日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
150+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
LibRec 精选:AutoML for Contextual Bandits
LibRec智能推荐
7+阅读 · 2019年9月19日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Deep Compression/Acceleration:模型压缩加速论文汇总
极市平台
14+阅读 · 2019年5月15日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
Disentangled的假设的探讨
CreateAMind
9+阅读 · 2018年12月10日
LibRec 精选:推荐系统的论文与源码
LibRec智能推荐
14+阅读 · 2018年11月29日
【推荐】自然语言处理(NLP)指南
机器学习研究会
35+阅读 · 2017年11月17日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Arxiv
0+阅读 · 2021年5月19日
Arxiv
4+阅读 · 2019年2月8日
Arxiv
3+阅读 · 2018年2月24日
VIP会员
相关VIP内容
专知会员服务
25+阅读 · 2021年4月2日
【干货书】机器学习速查手册,135页pdf
专知会员服务
125+阅读 · 2020年11月20日
专知会员服务
52+阅读 · 2020年9月7日
【DeepMind】强化学习教程,83页ppt
专知会员服务
151+阅读 · 2020年8月7日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
150+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
相关资讯
LibRec 精选:AutoML for Contextual Bandits
LibRec智能推荐
7+阅读 · 2019年9月19日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Deep Compression/Acceleration:模型压缩加速论文汇总
极市平台
14+阅读 · 2019年5月15日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
Disentangled的假设的探讨
CreateAMind
9+阅读 · 2018年12月10日
LibRec 精选:推荐系统的论文与源码
LibRec智能推荐
14+阅读 · 2018年11月29日
【推荐】自然语言处理(NLP)指南
机器学习研究会
35+阅读 · 2017年11月17日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Top
微信扫码咨询专知VIP会员