Proving Linearizability Using Reduction
Lipton的约简理论为推导并发程序的无干扰性提供了一种直观而简单的方法，但很难直接应用该技术来验证复杂的细粒度并发数据结构的线性化。在本文中，我们提出了三种基于约简的证明方法，可以处理这样的数据结构。我们的约简方法背后的关键思想是，不可约操作可以被视为更高抽象级别的原子操作。这使我们能够专注于与其抽象语义相关的操作的归约属性。我们已经成功地应用这些方法来验证11个并发数据结构，包括最具挑战性的：Herlihy和Wing队列，基于HSY消除的堆栈，时间戳队列和懒惰列表。我们的方法继承了Lipton约简的直观性和简单性，并发数据结构设计者可以轻松快速地学习使用这些方法。
2018-08-30 cs.DC cs.LO cs.PL
Synthesis of Large Dynamic Concurrent Programs from Dynamic Specifications
我们提出了一个易于处理的方法合成任意大的并发程序，共享内存模型与常见的硬件可用的原语，如原子寄存器，比较和交换，加载链接/存储条件等，我们合成的程序是动态的：新的进程可以创建和添加在运行时，所以我们的程序是不有限的状态，一般。尽管如此，我们成功地利用自动合成和模型检查方法的命题时序逻辑的基础上。我们的方法在算法上是有效的，在任何时候都是“活”的组件进程（程序）的数量的复杂性多项式。我们的方法不显式地构造所有进程的自动机理论产品，从而避免了\intr{state explosion}。相反，对于每一对相互作用的过程，我们的方法构建了一个自动机理论产品（\intr{pair-machine}），它体现了这两个过程的所有可能的相互作用。从每个配对机器，我们可以合成一个正确的\intr{pair-program}，它根据需要协调两个相关的过程。我们允许这样的配对程序在运行时动态添加。然后，它们与当前活动的配对程序“合取组合”，以重新合成程序，因为它在添加新的配对程序后产生。因此，我们能够在运行时添加新的行为，从而满足新的属性。我们建立了一个“大模型”定理，该定理表明合成的大程序继承了配对程序的正确性属性。
2008-01-10 cs.LO
On Algebraic Abstractions for Concurrent Separation Logics
并发分离逻辑的特点是在并行组合和成帧时状态所有权的转移。支撑所有权转移的代数结构是部分交换幺半群（PCM）。现有的研究主要从逻辑的角度考虑所有权转移，而相对较少注意代数的考虑。本文利用保结构的部分函数（即，态射）之间的PCM，以及分离关系的相关概念。结构的态射是代数和范畴论中的标准概念，但在分离逻辑中还没有普遍使用过。分离关系是二元关系，它推广了不相交性，并描述了态射保持结构的输入。这两个抽象通过实现编写规范的简洁方式，通过提供在所有权转移下保留的线程状态的抽象视图，以及通过实现从现有PCM中构造新PCM的用户级构造，来促进验证。
2021-03-04 cs.LO cs.PL
Go with the Flow: Compositional Abstractions for Concurrent Data Structures (Extended Version)
并发分离逻辑有助于显着简化并发数据结构的正确性证明。然而，这种证明中反复出现的问题是，由于复杂的共享和覆盖，在顺序设置中工作良好的数据结构抽象在并发设置中更难推理。为了解决这个问题，我们提出了一种新的方法来抽象区域的堆编码的数据结构不变到一个局部条件的每个节点。该条件可以取决于与在整个堆图上被计算为固定点的节点相关联的量。我们把这个量称为流量。流可以编码堆的结构属性（例如从根形成树的可达节点）以及数据不变量（例如排序）。然后，我们引入了流接口的概念，它表示依赖和保证堆区域施加在其上下文上，以保持局部流相对于全局堆不变。我们的主要技术成果是，这个概念导致了一个新的语义模型的分离逻辑。在这个模型中，流接口提供了一个通用的抽象机制来描述复杂的数据结构。这种抽象机制允许在各种各样的数据结构上推广的证明规则。为了证明我们的方法的多功能性，我们展示了如何扩展逻辑RGSep流接口。我们已经使用这种新的逻辑来证明非平凡并发数据结构的线性化和内存安全性。特别是，我们获得参数线性化证明并发字典算法，抽象的底层数据结构表示的细节。使用现有的分离逻辑提供的抽象机制，这些证明不能容易地表达。
2017-11-09 cs.DS cs.LO cs.PL
Concurrent Realizability on Conjunctive Structures
本文的重点是利用证明论和可实现性技术来探索并发计算的公理化。为了解决这个问题，我们重新定义的并发可实现性Beffara作为实现者的$π$ -演算与全球融合。我们定义一个变种的合取结构的RumeMiquey作为一个一般的结构，属于实现者和真值的可实现性。在安全可实现性方面，我们遵循Honda & Yoshida的工作，通过组合表示将实现子编码到代数结构中。在这第一项工作中，我们限制工作与$π$ -演算没有复制和其相应的类型系统是乘法线性逻辑（MLL）。
2021-12-29 cs.LO math.LO
Concurrent Game Structures with Roles
在下面的论文中，我们提出了一个新的语义著名的战略逻辑ATL。它基于向并发博弈结构添加角色，即在每个状态下，每个代理都属于一个角色，并且角色指定在该状态下他可以采取什么行动。我们展示了新语义的优势，提供了激励的例子，基于传感器网络，并分析了模型检验的复杂性。
2013-03-04 cs.LO cs.MA
The Semantics of Package Management via Event Structures
我们提出了一种方法，包管理的语义，它涉及到一般的事件结构，著名的数学对象中使用的并发，不确定性系统的语义。在这种方法中，包存储库的数据被视为一个不确定的并发程序的声明性规范。我们介绍了一个过程演算对应于此数据，并调查其操作和分类语义。我们希望这为进一步正式研究包管理奠定了基础，在这种研究中，可以利用现有的工具。
2021-07-04 cs.DC cs.LO cs.PL
Concurrent Process Histories and Resource Transducers
本文扩展了资源可转换性的范畴理论以处理并发交互，通过弦图给出直观表示，并研究了具有独特结构的资源转换器范畴。
2023-01-16 cs.LO math.CT
Partially Observable Concurrent Kleene Algebra
我们引入部分可观察并发Kleene代数（POCKA），一个代数框架的原因与控制结构，如条件和循环的并发程序。POCKA允许对可以访问变量和值的程序进行推理，我们通过具体的例子来说明。我们证明POCKA是一个健全的和完整的部分观测模型的公理化，并显示语义通过了重要的检查顺序一致性。
2020-07-22 cs.FL cs.LO cs.PL
Characterising Probabilistic Alternating Simulation for Concurrent Games
概率博弈结构结合了非确定性和随机性，参与者重复地同时采取行动，以进入并发博弈的下一个状态。概率交替模拟是比较不同概率博弈结构行为的重要工具。在本文中，我们提出了一个健全的和完整的模态特性的模拟关系，提出了一个新的逻辑概率分布的基础上。该逻辑使玩家能够在下一个状态或分布中强制执行属性。它的不动点扩张也是模拟关系的特征，在实际应用中可以表达许多有趣的性质。
2019-07-09 cs.LO
A Concurrent Program Logic with a Future and History
细粒度的乐观并发程序仍然是一个悬而未决的问题。现代程序逻辑提供了抽象机制和组合推理原则来处理固有的复杂性。然而，它们的使用主要局限于纸张和纸张或机械化的证明。我们设计了一个新的分离逻辑，面向缺乏自动化。虽然本地推理是众所周知的自动化是至关重要的，我们是第一个展示如何保持这种局部性（i）推理归纳属性，而不需要幽灵代码，和（ii）推理计算历史的事后诸葛亮。我们在一个工具中实现了我们的新逻辑，并使用它来自动验证具有挑战性的并发搜索结构，这些结构需要归纳属性和事后推理，例如Harris集。
2022-11-11 cs.LO cs.PL
From Thin Concurrent Games to Generalized Species of Structures (Extended Version)
本文在线性逻辑的薄并发博弈动态模型与结构广义物种静态模型间构建形式化桥梁，通过双范畴刻画二维关系，构造对称幺半函子并调整博弈语义方法得到笛卡尔闭伪函子，为λ演算研究提供新视角。
2025-10-27 cs.LO
Formal Verification of Chase-Lev Deque in Concurrent Separation Logic
本论文利用并发分离逻辑并在 Coq proof assistant 中对 Chase-Lev deque 进行了形式化验证，采用无界现实实现与 linearizability 强规范，满足最小可信计算基等三大标准，并扩展支持安全内存回收与松弛内存模型基础。
2023-05-20 cs.LO cs.PL
Restructuring a concurrent refinement algebra
本文重构支持 rely/guarantee 推理的并发精化代数，统一其 quantale/biquantale 结构并强化交换与分配性质，且在 Isabelle/HOL 中实现。
2024-05-09 cs.LO
Simulating reachability using first-order logic with applications to verification of linked data structures
本文介绍了如何利用现有的一阶逻辑定理证明器自动验证执行动态存储分配和破坏性更新的指针值结构字段的命令式程序的安全属性。其中一个主要的障碍是指定和证明（缺乏）的可达性动态分配的细胞之间的属性。主要的技术贡献是使用一阶公式以保守的方式模拟可达性的方法-该公式描述了一组程序状态的超集，如果有一个精确的方式来表达可达性，则会指定该超集。这些方法用于半自动程序验证（即，使用程序员提供的循环不变量），例如标记并清除垃圾回收和单链表的破坏性反转。(The标记和扫描的例子以前已经被报道为超出了ESC/Java的能力。
2009-05-27 cs.LO cs.PL
A Tree Clock Data Structure for Causal Orderings in Concurrent Executions
本文提出了树时钟这一新数据结构，替代向量时钟以高效计算并发程序执行中的因果序，有效克服了线程数较大时的计算瓶颈，并在 HB、SHB 和 MAZ 偏序计算中实现了显著的性能提升。
2022-01-17 cs.DC cs.DS cs.LO
Concurrent Games over Relational Structures: The Origin of Game Comonads
该研究提出将Spoiler-Duplicator博弈视为事件结构的新框架，给出单边博弈共代数的通用构造方法，刻画双边博弈策略，为有限模型理论提供范畴论新工具。
2025-06-14 cs.LO cs.PL math.CT
Concurrent computing machines and physical space-time
具体的计算机器，无论是顺序的还是并发的，都依赖于计算和时间之间的密切关系。我们回顾物理时间和目前实现的计算系统的一般特性。我们强调计算干扰的作用，即避免它们的必要性，以便为逻辑运算提供因果实现。我们比较了同步和异步系统，并简要介绍了一些用于处理计算干扰的方法。使用图形表示，我们表明，同步和异步电路反映了相同的反对牛顿和相对论的因果结构的物理时空。
2001-12-17 cs.DC cs.LO gr-qc
Reasoning about Temporary Coalitions and LTL-definable Ordered Objectives in Infinite Concurrent Multiplayer Games
我们建议加强使用命题表示的决定和战略，如CTL* 建立时间的语言，如果解释并发游戏模型。该增强功能允许指定不同的联盟结构。在量化的CTL* 这种技术也可以量化联盟结构，我们用它来量化一个扩展形式的战略配置文件，捕捉临时联盟。我们还扩展CTL* 的一个时间形式的二元偏好算子，可以追溯到冯赖特的工作。由此产生的量化CTL* 的扩展可以用来阐明并发多人游戏中行为的合理性条件，例如出现在解决方案概念中的行为，玩家有多个个人目标和偏好，并考虑到形成临时联盟的可能性。我们提出了完整的公理化扩展CTL* 的时间偏好算子。逻辑的可判定性不受这种扩展的影响。
2020-11-07 cs.LO cs.MA
Data reification in a concurrent rely-guarantee algebra
本文将顺序程序中成熟的数据具体化/精化技术扩展到并发环境，提出支持 rely-guarantee 推理的代数理论，并以并发版 Galler-Fischer 等价关系结构为例展示具体表示的逐步开发。
2024-05-09 cs.LO cs.SE
On-the-fly Unfolding with Optimal Exploration for Linear Temporal Logic Model Checking of Concurrent Software and Systems
针对并发系统LTL模型检测中的状态爆炸与即时展开难题，本文基于PDNet提出带延迟变迁探索树的最优即时展开算法，实现工具并在基准上优于SPIN与DiVine。
2024-06-12 cs.FL cs.LO
Rational Capability in Concurrent Games
本文在并发博弈结构中引入偏好与基于占优的理性概念，扩展 CL 和 ATL 以表达联盟理性强制属性的能力，并给出可满足性、模型检查复杂性及公理化结果。
2025-02-17 cs.LO cs.MA
A History of BlockingQueues
本文描述了一种形式化描述并发数据结构行为的方法。当指定并发数据结构时，主要的挑战是使规范稳定，即，以确保它们不会被其他线程无效。为此，我们建议使用基于历史的规范：而不是描述方法行为的对象的状态，我们指定它在对象的状态历史。历史被定义为状态更新的列表，它在所有点上都可以与实际对象的状态相关。我们在java.util.concurrent库中的BlockingQueue层次结构上演示了该方法。我们将展示如何指定接口BlockingQueue的行为，并将一些决定留给后代类。实现接口的类正确地继承了规范。作为一种规约语言，我们使用JML和基于权限的分离逻辑的组合，包括抽象谓词。这导致了一种抽象、模块化和自然的方式来指定并发队列的行为。这些规范可用于派生有关队列的高级属性，例如，显示元素的顺序被保留。此外，该方法可以很容易地适用于其他并发数据结构。
2012-09-11 cs.LO cs.SE
