Skip to content

定义Definition

并发对象历史

Concurrent object history · Invocation-response history

按线程记录对象操作调用与匹配返回的有限或无限事件序列。

形式陈述 ​

并发对象历史 H 是调用与返回事件的有限或无限序列。调用事件至少记录线程、对象、操作名、参数与请求标识;返回事件记录相同请求标识及结果。线程 P 的投影 H|P 保留属于 P 的事件。标准同步对象历史称为 well-formed,若每个 H|P 从调用开始,并在每次新调用前出现与上一调用匹配的返回;因此每线程至多有一个 outstanding operation。future、coroutine 或异步 API 允许多个并发请求时,应以请求标识定义匹配,而不能套用这一交替约定。

调用与返回都出现时构成完整操作,只有调用而没有返回时称为 pending。若操作 o1 的返回事件在 H 中早于 o2 的调用事件,定义实时顺序

o1<Ho2.

该关系比较完整操作区间的端点,而不是比较调用先后:先调用但迟返回的操作仍可能与后调用操作重叠。区间重叠的操作在此关系下不可比。历史的 completion 可为部分 pending 调用补上匹配返回,再删除仍未完成的调用;采用哪种 completion 由具体正确性条件规定。

直觉

对象历史刻意只保留客户端可见接口,把锁、CAS 重试和缓存操作隐藏起来。两个实现内部走过完全不同的路径,只要产生同一调用—返回历史,对顺序规格而言便不可区分。操作区间重叠留下的“尚无实时先后”正是并发模型允许选择线性化顺序的空间。

最终对象状态不足以代替历史:相同终态可能伴随不同返回值或违反实时顺序。正确性因此是历史集合上的条件,而不只是终态不变量。

例子与边界

线程 P 调用 enqueue(1),随后 Q 调用 dequeue(),Q 返回 1,P 尚未返回便崩溃。历史只有三个事件:P 的调用、Q 的调用、Q 的返回。若直接删除 P 的 pending 调用,就会得到“空队列弹出 1”的非法历史;适当 completion 为 P 补上成功返回,再把入队排在出队之前,才能解释已观察结果。补返回是规格中的存在性见证,不是声称崩溃进程真的收到过回复。

相反,若没有任何 enqueue(2) 调用而 Q 返回 2,completion 不能凭空创造一次新调用,因此无法修复该历史。这个区别把“请求可能已经生效”与“任何返回都可以事后圆回来”分开。

若 write(1) 已返回,另一线程才调用 read(),便有 write<Hread;在没有其他写时,线性一致读只能返回 1。读写区间重叠时,实时关系不排序二者,读返回旧值或新值可能都可解释。最终寄存器值相同,不能抹去这些返回值和边界差别。

推论与应用

线性一致性在合法顺序历史之外还保持 <H,顺序一致性只保持每线程投影。内存一致性模型在更细的读写事件上规定允许历史;并发对象、原子操作和历史检查器都以本条作为共同接口。

参考资料
  • Maurice P. Herlihy and Jeannette M. Wing, “Linearizability: A Correctness Condition for Concurrent Objects,” ACM TOPLAS 12(3), 1990.
  • Maurice Herlihy and Nir Shavit, The Art of Multiprocessor Programming, rev. 1st ed., Morgan Kaufmann, 2012, Chapter 3.
关系图谱32 个相邻概念 · 1 类关系

拖动节点调整位置。

显示关系

显示:依赖

  1. 前置三跳
  2. 前置二跳
  3. 前置一跳
  4. 当前条目
  5. 后续一跳
  6. 后续二跳
  7. 后续三跳
文字版关系按与当前条目的最短距离分组