Brookes共享状态语义的两排序代数分解
编程语言
2025-06-10 v3 分布式、并行与集群计算
计算机科学中的逻辑
摘要
我们采用两种排序的代数效应等式理论来建模具有抢占交错的并发共享状态，精确恢复Brookes于1996年的基于轨迹的模型。该分解允许我们以独立但相互作用的组件形式对Brookes模型进行代数分析。多种排序将术语划分为层次。我们使用两种排序：一种用于禁止环境内存访问交错的"持有"（hold）排序，类似于持有内存的全局锁；另一种用于相反情况的数据排序。该代数签名由独立的相互交织组件构成：两种用于在这些排序之间切换的新运算符，划定原子层，类似于获取和释放全局锁；非确定性选择；以及访问状态的运算符。公理同样清晰地划分：分隔符表现为闭合对；所有运算符都是严格的，并且分布在非空非确定性选择之上；非确定性全局状态遵循Plotkin和Power的全局状态呈现。我们的表示定理将自由代数表示为带有适当闭合条件的轨迹集合。当持有排序中没有变量时，我们恢复Brookes的轨迹语义。
引用
@article{arxiv.2501.15104,
title = {Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics},
author = {Yotam Dvir and Ohad Kammar and Ori Lahav and Gordon Plotkin},
journal= {arXiv preprint arXiv:2501.15104},
year = {2025}
}