跳转到内容
← 返回计算理论
计算理论当代约 21 分钟阅读

Shavit–Touitou 1995:软件事务内存怎样把无锁写成运行时而不是每只对象的手工艺

Software Transactional Memory

软件事务内存STMPODC 1995乐观并发帮助

1995 年 8 月,尼尔·沙维特(Nir Shavit)与丹·图伊图(Dan Touitou)在第 14 届分布式计算原理研讨会(PODC)发表《Software Transactional Memory》,页码 204 至 213。DOI 为 10.1145/224964.224987。沙维特当时署名麻省理工学院与特拉维夫大学;图伊图在特拉维夫大学。期刊长文于 1997 年刊于 Distributed Computing 第 10 卷第 2 期,页码 99 至 116。DOI 为 10.1007/s004460050028。收稿 1996 年 1 月,修订 6 月,接受 8 月。本页的对象是 1995 年这份已发表的软件运行时提案:把事务写成一段对共享单元的代码,用现成的加载链接与条件存储去装提交与中止,使非阻塞数据结构不必为每一种对象手写一套算法,也不必等待赫利希与莫斯那种事务缓存指令进入芯片。

它不是 Herlihy–Moss 1993。那一页的装置在一级缓存与一致性协议上;本页明确借用事务写法,同时拒绝那套硬件实现。它不是 等待自由层级。1991 年问的是何种原语能为多少进程给出等待自由实现。本页给出的活性更弱:系统里只要还有人在反复尝试,就会有某笔事务(不必是同一人、也不必是同一笔)在有限步内成功。它也不是 线性化。1990 年给出的是安全性一侧的正确性条件。本页假定成功的事务必须能被收成合法顺序,问的是软件里怎样用所有权记录与帮助把这种效果装出来。它更不是无锁队列菜谱,不是比较并交换循环,也不是后来某代处理器上的锁省略功能。数据库事务 的可串行化、日志与两阶段提交,是亲戚而不是对象。内存一致性模型 谈的是普通访存在何时可见,不是这笔软件事务的提交合同。分布式共识算法 要锁定的是一个以后不能偷换的值;本页要锁定的是一组预先写明的地址。

破除误解:软件事务内存不是芯片上的事务缓存,也不是数据库事务搬进运行时

第一层误解把标题听成 硬件事务内存 的软件译本,或听成「把那六条指令用普通加载存储模拟一遍」。1993 年的提案给多处理器加上事务加载、独占事务加载、事务存储、提交、中止与校验,用所有权式缓存协议侦测冲突。沙维特与图伊图写明:他们采纳的是事务这条编程合同,不是那套缓存。当时的机器至多提供单字的加载链接与条件存储。双字比较并交换、三字比较并交换、拼接一类文献里已经用过的原语,近在眼前却进不了芯片。硬件事务内存被他们写成阻塞的:一个进程若在事务中途被反复换出,可以永远提交不成;若两笔事务按不同顺序写两处,理论上也可以互相打断到无限。本页要卖的,是同一套事务语言可以在现有机器上做成非阻塞,并且可在机器之间移植。把 1995 年听成 1993 年的微码,会把一份运行时收成指令表。

第二层误解把软件事务内存收进 共识数,或收成「从此任意对象都等待自由」。论文自己把活性分成三档。等待自由:任何人反复尝试同一笔事务,都能靠自己的有限步成功。非阻塞:反复尝试蕴含系统中有人成功,成功者不必是发起者,事务也不必相同。对换出容忍:若假定没有人被无限次换出,则非阻塞成立。他们证明的实现落在非阻塞。赫利希那种把整个对象拷进新块再摆指针的译法,是另一条通用构造,共识数无穷的比较并交换已经够用;它不支持对不相交部分的并发更新,大对象的失败代价按对象体积收费。本页不重写那张分层表。把 STM 听成 1991 年的普遍性定理,类型就错了。

第三层误解把「事务」收进 数据库事务,或收进两阶段提交。名字共享,装置不同。数据库事务要覆盖磁盘、日志与崩溃恢复,数据集合可以远大于一级缓存,持续时间可以跨越多次调度。本页的事务被写成同步原语的写法:一段有限的事务性读与事务性写,要么失败,要么成功并使改动对别人原子可见。没有持久性合同,没有「已准备」字据,也没有协调者去广播全局决定。隔离在这里靠的是所有权向量上的占有,不是锁表与日志。把运行时听成把锁管理器搬进用户进程,会把短命的内存事务写成库引擎。

第四层误解把这篇听成无锁栈手册,或听成「数据集合可以边跑边长」的完整引擎。论文给出两种写法。静态事务事先知道要碰哪些地址,因而可以被想成一份原子过程:参数是数据集合加上一个确定性的转移函数,过程更新内存并交回旧值。\(k\) 字比较并交换是静态的例子。非静态事务的数据集合随读到的值变化——从双向链表头出队时,要不要改尾,取决于头的后继是不是空。图 1 被标成非静态。实现与证明停在静态。后来文献里的动态 STM,是邻居,不是本页装出来的引擎。本页拒绝把存在性的运行时写成某一种数据结构的步骤。

静态与动态、所有权记录,以及帮助何以不是递归合作

事务被写成单个进程执行的一串有限指令。事务性读把共享单元读进私有寄存器;事务性写把寄存器里的值存进共享单元。数据集合是这些共享地址的集合。任何一笔事务要么失败,要么成功完成,成功则改动对别人原子可见。静态事务的数据集合事先已知。非静态事务的数据集合可以在执行中途才被发现。论文把实现焦点放在前者,并声称这一类已经覆盖文献里大多数已知或被提议的同步原语。\(k\) 字比较并交换按静态来写:先按旧向量校验,再按新向量写入。出队按非静态来写:下一步地址要等这一步读完。两种都是事务作为代码。只有第一种被装成他们证明过的引擎。

实现用两份长度为 \(M\) 的共享向量。Memory 存放事务内存里的数据。Ownerships 标明每个单元此刻被哪一笔事务占有。每个进程在共享内存里另有一份记录,指向当前由它发起的事务:数据集合大小、按地址升序排好的地址向量、旧值向量、状态、是否已稳定、是否已全部写完,以及版本号。发起者先把记录初始化,再把稳定位置为真,从而任何后来的帮助者读到的都是同一份描述。版本号在事务结束后递增。帮助者在条件存储之前核对版本;读到过期描述的进程,从此不再改共享结构。稳定位与版本号一起,把「许多人执行同一笔事务」收成「看起来像一个人在跑」。

所有权按地址升序获取。静态事务因此先消掉循环等待:两笔事务不会因为相反的获取顺序而互相卡住。获取失败,则状态被写成失败并带上肇事地址,已经拿到的所有权被释放。获取全部成功,且状态仍未定,则有人把状态写成成功。成功之后,执行进程把旧值写入记录,按转移函数算出新值,写入 Memory,再释放所有权。AllWritten 在写完内存、释放所有权之前被置位,用来挡住一个已经掉队的帮助者在所有权已经放开之后还去改内存。失败的事务不改 Memory。线性化点被收在成功事务把 AllWritten 置为真的那一次条件存储:在那之前,写集合对别人尚未成为事实;在那之后,同一笔事务的执行进程不得再更新内存。

延迟、换出或崩溃会把持有所有权的进程冻住。若没有帮助,别人只能等,非阻塞立刻失败。帮助被写成:发起者若在某地址上获取失败,并且自己不是帮助者,则去执行占有该地址的那一笔事务——条件是对方记录已经稳定。要点被说成:要释放一个单元,只需帮助它唯一的所有者。不必沿依赖链递归帮下去。巴恩斯 1993 年的缓存方法,以及图雷克、沙沙与普拉卡什 1992 年、以色列与拉波波特 1994 年那类合作式 \(k\) 字比较并交换,把帮助写成沿锁依赖递归合作。论文给出的反例是:\(P\) 要占 \(a\) 与 \(b\),\(Q\) 已占 \(b\)。合作式让 \(P\) 先帮完 \(Q\) 再继续;若 \(Q\) 已改过 \(b\),\(P\) 仍失败,等 \(a\) 的人还要再帮一轮。STM 里 \(P\) 获取失败就释放、帮助、自己作为事务失败;等 \(b\) 的人不必帮 \(P\)。非冗余帮助再下一层:若帮助时发现对方版本已变,这次帮助就是多余的,以后对同一人少帮。活性证明走地址序:无限失败则取最高的反复失败地址;帮助前已释放更低地址,于是必有人在更高处失败,矛盾。这是几何,不是重试菜谱。

仿真用的是布鲁尔等人的 Proteus,对着 64 处理器的总线监听机器与类 Alewife 的目录机器。模拟器当时没有加载链接与条件存储,实验改用带时间戳的 64 位比较并交换。对照包括赫利希的整对象拷贝译法、以色列与拉波波特的合作式 \(k\) 字比较并交换,以及梅勒-克拉米与斯科特的排队锁。四组合成基准分别是共享计数器、随机取若干地址的资源分配、堆优先队列,以及数组里的双向链表队列。论文报告:在稳定、无故障的前提下,STM 始终优于巴恩斯风格的合作方法;进程数足够大时优于赫利希的拷贝译法。计数器没有内置并行,拷贝译法与排队锁仍然更快。资源分配在若干参数下,STM 甚至超过排队锁。他们同时写明:一般而言,STM 与其他非阻塞译法仍低于标准的、不提供容错的锁方法。这是提案里的证据,不是操作单。

它证明了什么,也就划出了它没有覆盖什么。它证明:事务可以作为代码写在软件里;静态数据集合上的提交与中止可以用所有权向量与帮助做成非阻塞;不相交的事务不必沿依赖链互相帮忙;在现有的单字原语上,不必为每一种对象另设计一套无锁算法,也不必等待事务缓存指令。它没有证明等待自由。它没有给出非静态、边跑边发现地址的实现。它没有把失败事务看见的中间状态写成一种正确性条件——那是后来不透明性要管的事。它没有声称软件事务已经快过精心设计的锁。赫利希等人 2003 年的动态大小 STM,戴斯、沙列夫与沙维特 2006 年的第二代事务锁(TL2),格拉维与卡帕乌卡 2008 年的不透明性,都是后继邻居。TL2 用全局版本时钟在提交时校验,并接受用户级用锁;不透明性要求连中止的事务也不得看见任何一次串行执行都产生不了的状态。1995 年的引擎在占齐所有权之前不算转移函数,孤儿跑用户代码而除以零,主要是动态 STM 把任意代码放进事务之后才尖锐起来的问题。把后来的库或某代硬件事务扩展读回 1995 年,会把一份 PODC 提案收成使用说明。

概念证据到此为止。本页不提供如何布置事务重试、如何把临界区改成锁省略、如何用帮助去干扰别人的进展,也不提供如何实现一只非阻塞栈的步骤。所有权回答的是「静态数据集合在软件里怎样被唯一占有」;帮助回答的是「占有者被延迟时,提案选择让谁把那一笔跑完」。两句都不是操作单。

跨域连接

  • 硬件事务内存:1993 年把提交与中止做成缓存本地操作,冲突靠所有权协议侦测。1995 年把同一份编程合同从芯片挪到运行时:没有事务缓存,只有 Memory 与 Ownerships 两份向量,外加现成的加载链接与条件存储。硬件提案被本页写成阻塞的;软件提案要证明的是非阻塞。容量上限在那边是事务缓存的行数,在这边是事先写明的地址表。把软件听成微码,或把硬件听成库,会把两条装置收成同一个产品页。
  • 线性化:成功事务必须能被收成一份合法的顺序历史,并且交回它开始之前数据集合上的值。失败事务被证明不改 Memory,因而可以从这份额外顺序里拿掉。线性化点不是发起者调用 StartTransaction 的瞬间,而是成功一侧那次把「已全部写完」置位的条件存储。帮助者不另开一笔事务:许多人执行同一份记录,看起来仍是一个线性化点。条件在 1990 年已经写下;1995 年回答的是静态 STM 这份实现够不够用。把「我们做了 STM」说成「我们重新定义了线性化」,类型就错了。
  • 数据库事务:可串行化与原子性被借用;持久性、锁表、崩溃恢复与两阶段提交被排除。数据库允许数据集合在执行中途随读到的元组变化,也必须处理中止事务读过不一致快照之后还继续跑的应用代码。1995 年的引擎先占齐地址再算新值,应用代码并不在所有权尚未闭合时看见中间内存。后来的动态 STM 更像数据库:读写集合边跑边长,于是才需要不透明性去管「中止者看见了什么」。亲属不是对象。把 STM 听成把 ACID 搬进用户进程,会把同步原语误认成库引擎。
  • 科学哲学:论文把「同步操作是什么」从一种对象类型、或一条芯片指令,改写成可以对地址施用的编程抽象。结尾甚至把计算能力的问题写成:对单元施用多种操作,对比把同步想成对象,哪一种抽象更强。证伪条件很具体。若静态数据集合上的帮助仍会沿不相交的地址递归传开,非冗余帮助的效率主张就垮。若单进程被反复换出时硬件事务仍能独自完成,把 1993 年写成阻塞也就垮。它们按论文自己的模型没有垮。后来共同体从「STM 必须非阻塞」转向「用户级用锁也可以」,是辅助假设被换掉,不是这份静态引擎被否证。本页只提供一份判决记录:事务被从缓存协议的默认位置拿掉之后,运行时才作为并发对象进场。
  • 内存一致性模型:普通加载与存储何时对别人可见,是弱内存要写的合同。本页的可见性闭合在事务成功:新值在 AllWritten 之前对别人尚未发生,之后不得被观察成仍未发生。模型底层被写成带标记的加载链接与条件存储,失败的条件存储不写。把 STM 的提交听成「再加一道栅栏就等于顺序一致」,会把事务合同还原成访存序。一边管普通地址,一边管事先声明的数据集合。

参考文献

  • Nir Shavit & Dan Touitou, "Software Transactional Memory", Proceedings of the 14th Annual ACM Symposium on Principles of Distributed Computing, 1995, pp. 204–213. DOI: 10.1145/224964.224987. —— 本文对象:静态 STM、所有权记录、帮助与非阻塞。
  • Nir Shavit & Dan Touitou, "Software Transactional Memory", Distributed Computing 10(2), 1997, pp. 99–116. DOI: 10.1007/s004460050028. —— 会议后的期刊长文,含线性化与非阻塞证明及 Proteus 实验。
  • Maurice Herlihy & J. Eliot B. Moss, "Transactional Memory: Architectural Support for Lock-Free Data Structures", Proceedings of the 20th Annual International Symposium on Computer Architecture, 1993, pp. 289–300. DOI: 10.1145/165123.165164. —— 论文明确借用又划界的硬件事务内存。
  • Maurice Herlihy, "Wait-Free Synchronization", ACM Transactions on Programming Languages and Systems 13(1), 1991, pp. 124–149. DOI: 10.1145/114005.102808. —— 等待自由与共识数,用以标明本页停在非阻塞。
  • Maurice P. Herlihy & Jeannette M. Wing, "Linearizability: A Correctness Condition for Concurrent Objects", ACM Transactions on Programming Languages and Systems 12(3), 1990, pp. 463–492. DOI: 10.1145/78969.78972. —— 并发对象的正确性条件,本页实现按此线性化。
  • Greg Barnes, "A Method for Implementing Lock-Free Shared Data Structures", Proceedings of the 5th ACM Symposium on Parallel Algorithms and Architectures, 1993, pp. 261–270. DOI: 10.1145/165231.165265. —— 论文对照的缓存译法与递归帮助。
  • Amos Israeli & Lihu Rappoport, "Disjoint-Access-Parallel Implementations of Strong Shared Memory Primitives", Proceedings of the 13th Annual ACM Symposium on Principles of Distributed Computing, 1994, pp. 151–160. DOI: 10.1145/197917.198079. —— 合作式 \(k\) 字比较并交换,用以对照非冗余帮助。

延伸阅读

  • 与 硬件事务内存 对读:事务语言被共用;缓存所有权与软件所有权向量是两套装置。
  • 与 等待自由层级 对读:非阻塞躲开的是一个人停住就把别人冻住;等待自由还要求每个人都能靠自己的步数完成。本页不提供后一句。
  • 与 线性化 对读:先看并发历史怎样被收成合法顺序,再看本页用 AllWritten 去逼近多字原子性。
  • 与 数据库事务 对读:原子性被借用;持久性、锁表与中止者的中间视图被明确排除或留给后继。
  • 与 内存一致性模型 对读:普通访存的可见顺序不是静态事务在所有权向量上的提交合同。
  • Maurice Herlihy, Victor Luchangco, Mark Moir & William N. Scherer III, "Software Transactional Memory for Dynamic-Sized Data Structures", Proceedings of the 22nd Annual ACM Symposium on Principles of Distributed Computing, 2003, pp. 92–101. DOI: 10.1145/872035.872048. —— 动态大小 STM,本页静态引擎的后继邻居。
  • Dave Dice, Ori Shalev & Nir Shavit, "Transactional Locking II", Proceedings of the 20th International Symposium on Distributed Computing, LNCS 4167, 2006, pp. 194–208. DOI: 10.1007/11864219_14. —— 全局版本时钟与提交时加锁;沙维特本人参与的后继路线,接受用户级用锁。
  • Rachid Guerraoui & Michał Kapałka, "On the Correctness of Transactional Memory", Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2008, pp. 175–184. DOI: 10.1145/1345206.1345233. —— 不透明性:中止的事务也不得看见不一致状态。