Determining whether one concurrent operation completed before another began is a fundamental prerequisite for reasoning about the correctness of concurrent systems. We formalize this challenge as the Causal Observability Problem (COP): assign timestamps to the observable boundary events of a concurrent execution, invocations and responses, that faithfully reflect real-time operation order. A solution is complete if it never misses a genuine precedence, and sound if it never reports a spurious one. We prove that a strongly consistent solution, one that is simultaneously complete and sound, is unachievable at the observable boundary. We then show that the placement of instrumentation events relative to operation boundaries deterministically governs what a monitor can guarantee: internal placement yields completeness, external placement yields soundness, and neither achieves both. This dichotomy holds independently of the underlying timestamp mechanism. We instantiate this framework with three non-blocking implementations of a Causal Monitor object: FAInc (centralized atomic counter), Striped (decentralized counter), and Collect (iterative register snapshot). FAInc and Striped are linearizable; Collect is only quiescently consistent. Despite this internal consistency gap, we prove that all three provide identical COP guarantees: placement alone determines observable behavior. We validate these claims empirically on a 64-core NUMA architecture, showing that Striped matches Collect in throughput while preserving linearizability, resolving the cache-contention bottleneck of FAInc at high thread counts.


翻译:确定一个并发操作是否在另一个操作开始之前完成,是推理并发系统正确性的基本前提。我们将这一挑战形式化为因果可观测性问题(COP):为并发执行的可观测边界事件(即调用与响应)分配时间戳,使其忠实反映操作的实时顺序。若一个解法能捕获所有真实的前序关系,则称为完备的;若从不报告虚假的前序关系,则称为可靠的。我们证明,在可观测边界上无法实现同时具备完备性与可靠性的强一致性解法。进一步表明,检测事件相对于操作边界的位置决定了监测器所能保证的性质:内部布局保证完备性,外部布局保证可靠性,而二者无法兼得。这一二分法独立于底层时间戳机制。我们通过三种因果监测器对象的非阻塞实现来实例化该框架:FAInc(集中式原子计数器)、Striped(去中心化计数器)与Collect(迭代寄存器快照)。其中FAInc与Striped是可线性化的,而Collect仅满足静默一致性。尽管存在这种内部一致性差距,我们证明三者提供的COP保证完全相同:仅布局决定可观测行为。我们在64核NUMA架构上通过实验验证了这些结论,表明Striped在保持可线性化的同时,吞吐量可与Collect媲美,并解决了高线程数下FAInc的缓存竞争瓶颈。

0
下载
关闭预览

相关内容

【博士论文】在时空系统中学习因果表示
专知会员服务
34+阅读 · 2025年2月25日
因果推断,Causal Inference:The Mixtape
专知会员服务
110+阅读 · 2021年8月27日
专知会员服务
66+阅读 · 2021年1月6日
因果关联学习,Causal Relational Learning
专知会员服务
185+阅读 · 2020年4月21日
「因果推理」概述论文,13页pdf
专知
16+阅读 · 2021年3月20日
基于深度元学习的因果推断新方法
图与推荐
12+阅读 · 2020年7月21日
论文浅尝 | 时序与因果关系联合推理
开放知识图谱
36+阅读 · 2019年6月23日
用深度学习揭示数据的因果关系
专知
28+阅读 · 2019年5月18日
因果推理学习算法资源大列表
专知
27+阅读 · 2019年3月3日
从信息瓶颈理论一瞥机器学习的“大一统理论”
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
21+阅读 · 2013年12月31日
国家自然科学基金
26+阅读 · 2011年12月31日
国家自然科学基金
23+阅读 · 2008年12月31日
Arxiv
0+阅读 · 6月2日
Arxiv
29+阅读 · 2023年2月10日
VIP会员
最新内容
网状网络及其在军事领域的运用
专知会员服务
4+阅读 · 今天6:18
无美国参与的欧洲战争方式(万字长文)
专知会员服务
4+阅读 · 今天5:54
《国防领域敏感性分析白皮书》
专知会员服务
5+阅读 · 今天3:42
综述 | 从问答到任务完成:Agent系统与Harness设计
Agentic RL:框架、实践与长程智能体训练
专知会员服务
3+阅读 · 6月24日
重新思考无人机时代的生存能力
专知会员服务
8+阅读 · 6月24日
装甲突击旅:现代战争思考、战斗与组织
专知会员服务
6+阅读 · 6月24日
在人工智能加速决策环境中拓展OODA循环
专知会员服务
8+阅读 · 6月24日
军事欺骗:供作战战术指挥官使用的工具
专知会员服务
6+阅读 · 6月24日
相关VIP内容
【博士论文】在时空系统中学习因果表示
专知会员服务
34+阅读 · 2025年2月25日
因果推断,Causal Inference:The Mixtape
专知会员服务
110+阅读 · 2021年8月27日
专知会员服务
66+阅读 · 2021年1月6日
因果关联学习,Causal Relational Learning
专知会员服务
185+阅读 · 2020年4月21日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
21+阅读 · 2013年12月31日
国家自然科学基金
26+阅读 · 2011年12月31日
国家自然科学基金
23+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员