Concurrent separation logic is distinguished by transfer of state ownership upon parallel composition and framing. The algebraic structure that underpins ownership transfer is that of partial commutative monoids (PCMs). Extant research considers ownership transfer primarily from the logical perspective while comparatively less attention is drawn to the algebraic considerations. This paper provides an algebraic formalization of ownership transfer in concurrent separation logic by means of structure-preserving partial functions (i.e., morphisms) between PCMs, and an associated notion of separating relations. Morphisms of structures are a standard concept in algebra and category theory, but haven't seen ubiquitous use in separation logic before. Separating relations are binary relations that generalize disjointness and characterize the inputs on which morphisms preserve structure. The two abstractions facilitate verification by enabling concise ways of writing specs, by providing abstract views of threads' states that are preserved under ownership transfer, and by enabling user-level construction of new PCMs out of existing ones.


翻译:以平行组成和框架方式转让国家所有权,是同时分离逻辑的区别。支撑所有权转让的代数结构是部分混合单体(PCMs)的代数结构。 扩展研究主要从逻辑角度考虑所有权转让,而相对较少注意代数因素。本文件通过结构结构保护PCM之间的部分功能(即形态)和相关分离概念,提供了同时分离逻辑中所有权转让的代数正规化,提供了结构结构保留部分功能(即形态)和相关分离概念。结构的摩尔主义是代数理论和类别理论中的一个标准概念,但以前从未看到在分离逻辑中普遍使用过。 分离关系是二元关系,一般地说明脱节性,说明形态结构所保护的投入。 两种抽象概念有助于核查,通过简洁的写图谱,提供在所有权转让中保存的线系状态的抽象观点,以及使用户能够从现有模式中构建新的PCMs。

0
下载
关闭预览

相关内容

Fariz Darari简明《博弈论Game Theory》介绍,35页ppt
专知会员服务
109+阅读 · 2020年5月15日
深度强化学习策略梯度教程,53页ppt
专知会员服务
178+阅读 · 2020年2月1日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
CCF推荐 | 国际会议信息8条
Call4Papers
9+阅读 · 2019年5月23日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
人工智能 | SCI期刊专刊信息3条
Call4Papers
5+阅读 · 2019年1月10日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
大数据 | 顶级SCI期刊专刊/国际会议信息7条
Call4Papers
10+阅读 · 2018年12月29日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
计算机类 | 期刊专刊截稿信息9条
Call4Papers
4+阅读 · 2018年1月26日
【今日新增】IEEE Trans.专刊截稿信息8条
Call4Papers
7+阅读 · 2017年6月29日
Arxiv
0+阅读 · 2021年4月30日
Arxiv
0+阅读 · 2021年4月29日
Arxiv
0+阅读 · 2021年4月28日
Arxiv
0+阅读 · 2021年4月27日
VIP会员
相关资讯
CCF推荐 | 国际会议信息8条
Call4Papers
9+阅读 · 2019年5月23日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
人工智能 | SCI期刊专刊信息3条
Call4Papers
5+阅读 · 2019年1月10日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
大数据 | 顶级SCI期刊专刊/国际会议信息7条
Call4Papers
10+阅读 · 2018年12月29日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
计算机类 | 期刊专刊截稿信息9条
Call4Papers
4+阅读 · 2018年1月26日
【今日新增】IEEE Trans.专刊截稿信息8条
Call4Papers
7+阅读 · 2017年6月29日
Top
微信扫码咨询专知VIP会员