并发ML稳定器：安全检查点机制和异常处理在多线程程序中的应用

理论计算机科学电子札记174（2007）85-115www.elsevier.com/locate/entcs用于原子性的Lukasz Ziarek1普渡大学美国西拉法叶菲利普·沙茨2普渡大学美国西拉法叶Suresh Jagannathan3普渡大学美国西拉法叶摘要大规模软件系统中出现的瞬时故障通常可以通过重新执行代码来修复在其中发生。然而，为多线程代码中的安全重新执行指定有意义的语义并不明显。为了使线程正确地重新执行代码区域，它必须确保在该区域内目睹其不需要的事件的所有其他线程也恢复到有意义的早期状态。如果操作不当，可能会导致数据不一致和其他不良行为。然而，自动确定什么构成一致的全局检查点并不简单，因为线程交互是程序的动态属性。在本文中，我们提出了一个安全，高效的检查点机制并发ML（CML），可用于从瞬态故障恢复。我们引入了一种新的语言抽象，称为稳定器，允许指定每个线程的监视器和恢复全局一致的检查点。全局状态是通过线程之间的通信事件的轻量级监视来计算的（例如，消息传递对共享变量的操作或更新）。我们的检查点抽象在状态恢复期间提供原子性和隔离性保证，确保恢复的全局状态是安全的。我们在几个现实的，多线程的，服务器风格的CML应用程序，包括Web服务器和窗口工具包的实验结果表明，使用稳定器的开销很小，并导致我们得出结论，他们是一个可行的机制定义安全检查点在并发函数程序。我们的实验最后的案例研究，说明如何建立开放的嵌套事务，从我们的检查点机制。关键词：并发编程，错误恢复，检查点，事务，并发ML，异常处理，原子性1电子邮件：lziarek@cs.purdue.edu2电子邮件：schatzp@cs.purdue.edu3电子邮件：suresh@cs.purdue.edu1571-0661 © 2007 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.04.00886L. Ziarek等人/理论计算机科学电子笔记174（2007）851介绍瞬时错误是一种异常情况，通常可以通过重新执行引发该错误的代码来修复。通常，这些故障是由资源的暂时不可用引起的。例如，试图通过网络进行通信的程序可能会遇到超时异常，因为在发出请求时网络负载很高。由于资源本身不可靠，也可能出现瞬时故障;考虑不保证数据包传递的网络协议。在由许多独立执行的组件组成的大型系统中，即使在检测到故障之后，一个组件的故障也可能导致其他组件的瞬时故障[7]。例如，进入不可恢复错误状态的客户端-服务器应用程序可能需要重新启动;在这里，服务器对其客户端表现为暂时不可用的资源，客户端必须重新发出在服务器重新启动期间发送的请求。由于违反了程序不变量，也可能发生瞬时故障。在软件事务系统中发生的可串行性违规[18，20，40]通常通过中止正在结束的事务并重新执行来纠正。瞬时故障恢复的一个简单解决方案是在可能触发这种故障的操作执行之前捕获程序的全局如果错误发生并引发异常，处理程序只需要恢复以前保存的程序状态。不幸的是，瞬态故障经常发生在长期运行的服务器应用程序，本质上是多线程的，但仍然必须表现出良好的容错特性，捕捉全局程序状态是昂贵的，在这些环境中。另一方面，简单地重新执行计算而不考虑先前的线程交互可能导致不一致的程序状态并导致进一步的错误，例如违反可串行化性。当一个线程被还原时，它的所有对象都必须与程序的其余部分隔离假设在两个线程之间发生了通过消息传递的通信事件，发送方随后重新执行此代码以从瞬时故障中恢复由于接收方不知道发送方的重新执行已经发生，因此可能导致对（重新）发送的消息的虚假的未经处理的执行。因此，它不需要期望重新传输先前执行的消息。 一般来说，计算瞬态故障的敏感检查点的问题需要计算线程和必须重新执行的代码部分之间的依赖关系清单的传递闭包。为了减轻并发函数程序中定义和恢复安全有效检查点的负担，我们提出了一种新的语言抽象，称为稳定器。 稳定器包含两个操作。 第一个启动对通信和线程创建事件的代码监控，并在评估监控的代码时建立这个线程本地检查点可以被看作是在执行被监视区域期间遇到的任何瞬时故障的恢复点。当检测到瞬时故障时，第二个操作将控制和状态恢复到安全的全局检查点当控制被恢复时，被监视区域的原子性和隔离被强制执行。被监视的区域被原子地展开，并且其所有全局效果也被恢复。L. Ziarek等人/理论计算机科学电子笔记174（2007）8587由稳定器定义的检查点是第一类的，并且是可组合的：被监控的过程可以自由地创建和返回其他被监控的过程。稳定器可以任意嵌套，并且在存在动态变化的线程数量和非确定性选择性通信的情况下工作。我们演示了稳定器在并发ML中编写的几个大型服务器应用程序中的使用，并提供了一个案例研究，描述了如何通过在执行监控代码期间提供原子性和隔离保证来将稳定器扩展到事务中。稳定器在操作系统或编译器注入的检查点所定义的透明度与用户注入的检查点所定义的精度之间提供了一个中间地带 在我们的方法中，线程本地状态紧接在非本地操作（例如线程通信，线程创建等）之前。 被认为是该线程的可能检查点。此外，应用程序可以显式地识别应该采取本地检查点的程序点，并且可以将程序区域与这些指定点相关联。当回滚操作发生时，控制将恢复到每个线程的这些保存的检查点之一。启动回滚以从瞬时故障中恢复。所选择的检查点的确切集合由安全条件确定，即被监视的代码被原子地恢复当一个线程被回滚到线程本地检查点状态C时，我们的方法保证与该线程通信的其他线程将被置于与C一致的状态。本文有四个贡献：(i) 稳定器的设计和语义，一种新的并发函数式程序的模块化语言抽象据我们所知，稳定器是第一个以语言为中心的检查点设施设计，为具有动态线程创建和选择性通信的程序中的瞬时故障恢复提供全局一致性和安全保证[31]。(ii) 一个轻量级的动态监控算法忠实于语义，构造有效的全局检查点的基础上，在其中执行恢复动作的上下文。效率是根据确保所有线程在检查点恢复到一致的全局状态后恢复执行所需的回滚量来定义的(iii) 对Concurrent ML的详细评估研究，量化了在各种开源服务器式应用程序上使用稳定器的成本我们的研究结果表明，定义和监控线程状态的成本很小，通常只会增加不超过4%到6%的总执行时间开销。内存开销同样适中。(iv) 一个案例研究，说明如何扩展稳定器及其原子性和隔离保证，以实现软件事务。我们的案例研究定义了支持开放嵌套的稳定器的扩展本文其余部分的结构如下。第2节描述了88L. Ziarek等人/理论计算机科学电子笔记174（2007）85稳定剂提取第3节提供了一个激励性的示例，突出了与高度多线程Web服务器中的瞬时故障恢复相关的问题，以及如何使用稳定器来减轻复杂性并提高鲁棒性。第4节给出了操作语义。第5节中给出了检查点信息的增量构造策略。实施细节见第6节。第7节详细评估了使用稳定器进行瞬态故障恢复的成本和开销，第8节给出了一个案例研究，展示了如何实现软件事务，第9节介绍了相关工作，第10节给出了结论。2编程模型稳定器通过使用具有以下签名的两个原语来创建、恢复和回收：稳定：稳定段是一个受监控的代码段，它的结果被保证作为一个单独的单元恢复。原始稳定用于定义稳定截面。给定函数f，对稳定f的求值产生一个新函数f除了有趣的通信、共享内存访问、锁和派生之外，事件被监视和分组。因此，稳定段中的所有操作都与同一个检查点相关联。这种语义与经典的检查点方案相反，在经典的检查点方案中，检查点和动作集合之间没有明显的分组。第二个原语stabilize将执行还原为动态计算的全局状态;此状态将始终对应于在执行稳定段、通信事件或线程每个线程的spawn point。我们通过观察到在需要恢复的稳定段内发生的外部不可恢复操作（例如I/O、外部函数调用等）来限定这种说法。必须在调用稳定操作之前由应用程序显式处理。注意，类似于也不返回的raise或exit，稳定化的结果类型被合成从它发生的背景中。非正式地，稳定操作恢复在稳定部分内执行的所有事件，就像中止操作恢复事务内的所有然而，事务在提交发生之前强制原子性和隔离性，而稳定器仅在稳定操作发生时强制这些属性。因此，在稳定部分内执行的动作立即对外部可见;当稳定动作发生时，这些动作连同它们的目击者被恢复。与经典的检查点方案[34]或异常处理机制不同，调用稳定的结果并不能保证控制恢复到与动态最接近的稳定部分对应的状态。控制权在哪里恢复取决于线程在触发稳定调用的稳定部分中采取的操作L. Ziarek等人/理论计算机科学电子笔记174（2007）8589T1T2S1S3S2T1T2S1S3S2(a)（b）第（1）款Fig. 1.稳定截面之间的相互作用。可组合性是稳定器的一个重要设计特征：对需要监控的程序没有先验分类，对嵌套稳定部分也没有任何限制。稳定器将监视代码区域的构造与状态的捕获分离。只有当一个被监视的亲-应用了CLOCK，从而建立了潜在的线程局部恢复点。这种程序的应用可能反过来导致建立其他独立构建的监控程序。此外，这些过程本身可以被应用并且适当地保存程序状态;因此，在不损害其他被监视过程的行为的情况下确定状态保存和恢复决策。2.1稳定截面当稳定操作发生时，匹配的线程间事件将成对展开。如果发送被展开，匹配的接收也必须被还原。如果一个线程在一个正在展开的稳定区中产生了另一个线程，这个新线程（及其所有操作）也必须被丢弃。如果写入值的线程被展开到写入之前的状态，则所有从共享变量读取的线程都对于一个语句来说，如果没有线程在这个状态下执行（例如，所有线程都在执行语句及其传递结果之前的一个点上），则程序状态是稳定的。例如，考虑线程t1进入稳定段S1并发起与线程t2的通信事件（参见图1（a））。假设t1随后进入另一个稳定段S2，并再次与线程t2建立通信。进一步假设t2在它自己的稳定区间S3内接收到这些事件.紧接在S1和S2之前的程序状态表示由程序员确定的可行检查点，在示例中用白色圆圈表示。如果在S2内发起回滚，则一致的全局状态将要求t2恢复到与S3的开始相关联的状态，因为它已经从t1接收到在S2内发起的通信。然而，丢弃内部的操作，90L. Ziarek等人/理论计算机科学电子笔记174（2007）85图二.用于处理请求的转向模块交互（实线）和用于超时的错误处理控制和数据流（虚线）。线上方的数字表示通信操作发生的顺序。S3现在强制t1在S1开始时恢复执行，因为它在S1到t2（在S3内执行）内发起了通信事件。这种情况也可能在没有嵌套稳定段的情况下出现。考虑图1（b）中的例子。再一次，程序必须返回t1，因为稳定段S3跨越了来自S1和S2的通信事件。3激励的例子Swerve[22]（见图2）是一个开源的第三方Web服务器， 并发ML服务器由五个独立的交互模块组成。模块和线程之间的通信广泛使用CML消息传递语义。线程通过显式定义的通道进行通信，它们可以发送或接收值。 为了激励稳定器的使用，我们考虑了Swerve的三个模块的交互：文件管理器、文件处理器和文件管理器管理器。HTTP模块接收传入的HTTP请求，并将文件服务需求委托给并发执行的处理线程。对于每个新连接，都会产生一个新的侦听器;因此，每个连接都有一个主要的管理实体。文件处理器模块处理对底层文件系统的访问。每个将要托管的文件都由一个文件处理器线程读取，该线程将文件分块，并通过消息传递将其发送到侦听器委托的线程超时是通过使用通道上的定时事件4由网络管理器线程可以轮询这些通道以检查是否超时。在超时的情况下，通道将保持一个标志，表示时间已过期，否则为空。超时是服务器中最常见的瞬时故障，很难简单地处理。实际上，系统考虑图2中给出的典型执行流程。当接收到新请求时，侦听器4实际实现使用C-vars，为了简单起见，我们提供了通道方面的抽象描述。我们的实现支持所有CML同步变量。L. Ziarek等人/理论计算机科学电子笔记174（2007）8591fun fileReader name abort consumer =let fun sendFile（）=let fun loop strm =如果超时，则中止then CML.send（consumer，consumer）else let val chunk =BinIO.inputN（strm，fileChunk）in. 阅读文件的一部分... 并发送到接收器循环串）端in（case BinIOReader.openIt abortname of NONE =>（）| SOME h =>（loop（BinIOReader.get h）;BinIOReader.closeIt h）端fun fileReader name abort consumer =let fun sendFile（）=let fun loop strm =let val chunk =BinIO.inputN（strm，fileChunk）in. 阅读文件的一部分... 并发送到接收器循环串）端在stable fn（）中=>(case BinIOReader.openIt abort name ofNONE =>（）| SOME h =>（loop（BinIOReader.geth）;BinIOReader.closeIt h））（）端图三. 《档案》节选转向中的处理模块。 顶部显示了修改后的代码，使用稳定剂。斜体标记原始代码中更改的区域为这个连接生成一个新的线程，负责托管请求的这个托管线程首先与超时管理器建立一个超时量子（1），然后通知文件处理器（2）。如果文件处理线程可用于处理请求，则通知托管线程可以对文件进行分块（2）。托管线程将其将接收其超时通知的通道传递给文件处理线程（2）。文件处理线程现在负责检查显式超时通知（3）。由于超时可能发生在特定请求开始处理文件（4）之前（例如，在托管模块定义的托管线程内）或处理文件（5）期间（例如，在文件处理器内），因此产生的错误处理代码很麻烦。此外，超时本身的检测由第三个模块，即服务器管理器处理。其结果是一个复杂的消息传递过程，它跨越多个模块，每个模块都必须弄清楚如何处理适当的暂停。这种代码组织的不幸的副作用是模块化受到了损害。代码现在包含无法抽象的隐式交互（6）（例如，文件处理器必须显式通知超时的时间转弯设计说明了处理复杂并发系统中的瞬时故障：我们如何正确处理跨多个模块的故障，而不引入显式的跨模块依赖关系来处理每个这样的故障？图3显示了fileReader的定义，它是文件处理模块中的一个Swerve函数，通过将文件内容分块到一系列较小的数据包中，将请求的文件发送到托管线程文件由BinIOReader打开，92L. Ziarek等人/理论计算机科学电子笔记174（2007）85int front（）=>letfun receiver（）=caseCML.recv consumerofinfo=>（sendInfo info;.）| chunk=>（sendString;.）| timeout=>错误处理代码| done=>....在... ;环路接收端stable fn（）=>letfun receiver（）=caseCML.recv consumerofinfo=>（sendInfo info;.）| chunk=>（sendString;.）| done=>....在... ;环路接收端图五. Swerve中的JavaScript模块的摘录。宿主线程的主要处理被包装在稳定部分中，并且可以删除超时处理代码。顶部显示了修改后使用稳定器的代码。斜体标记原始代码中更改的区域letfund expired（chan）= isSome（CML.poll chan）fun trigger（chan）=CML.send（chan，timeout）...在... 触发结束Let fun trigger（chan）= stabilize（）...在stable（fn（）=>. ; trigger（chan））（）end见图4。Swerve中的数据库管理器模块的摘录。顶部显示了修改后使用稳定器的代码。过期的函数可以被删除，触发器现在调用stabilize。斜体标记区域在原来的代码被改变。文件处理模块中的实用程序功能。fileReader函数必须在文件处理循环的每次迭代中检查是否发生了超时，方法是调用. expired函数，因为CML线程不能被显式中断。 如果发生超时，则过程有义务通过显式的发送通道使用者通知接收方（宿主线程）。稳定器允许我们通过将sendFile的文件处理逻辑包装在一个稳定节中来抽象这个显式的通知过程。假设一个稳定化调用取代了对CML.send（consumer，consumer）的调用。这个动作会导致sendFile和接收器的动作同时展开，因为接收器正在接收文件块。一个更干净的解决方案出现了。假设我们修改了stable模块的定义来调用stable，并将其操作包装在一个stable部分中，如图4所示。现在，任何线程都不需要轮询超时事件。由于宿主线程通过com建立超时量程与文件管理器通信并将此信息传递给文件处理器线程，由文件管理器执行的任何稳定操作将展开与处理此文件相关的所有操作。 因此，这种转换允许我们指定无需嵌入非本地超时处理逻辑的超时机制L. Ziarek等人/理论计算机科学电子笔记174（2007）8593在每个线程中，潜在地可能是被中断的。宿主线程本身也被简化了（如图5所示）;通过将其逻辑包装在稳定部分中，我们也可以删除其所有超时错误处理代码。现在，超时完全通过使用位于模块内部的稳定器来处理。这种改进的关注点模块化不会导致功能减少，鲁棒性实际上，稳定操作会导致超时的请求被透明地重新处理，或者允许Web服务器处理新的请求，这取决于所需的行为。因此，每个模块只需管理自己的组件，而不必在超时错误的情况下显式地与其他模块通信。4语义我们的语义是根据具有线程原语的核心按值调用函数语言来定义的（见图6）。为了清晰起见，我们首先提出了一个稳定器的解释，其中稳定部分的评估立即导致捕获一致的全局检查点。此外，我们将语言限制为仅在进入稳定部分时捕获检查点，而不是在任何通信或线程创建操作时。这种语义反映了比第2节中的非正式描述更简单的检查点特征。在第5节中，我们改进了这种方法，以增量方式构建检查点。在下文中，我们使用元变量v来对值进行范围，δ来对稳定部分或检查点标识符进行范围。 我们还使用P表示线程项，使用e表示表达式。我们用过杠来表示一个有限的有序序列，例如，f表示f1f2. fn.项α.α表示序列的前缀扩展α有一个元素α，α.α是SU_x扩张，ααJ表示序列关联，φ表示空序列和空集合，当α是αJ的前缀时，α≤αJ成立.我们写|α|表示序列α的长度。我们的通信模型是一个具有同步发送和接收操作的消息传递系统。我们不对通道上的通信动作施加严格的排序;同一通道上的通信动作是非确定性配对的。为了对异步发送进行建模，我们只需生成一个线程来执行发送5.在这个核心语言中，我们添加了两个新的原语：stable和稳住当应用稳定函数时，建立全局检查点，并且在该检查点的上下文中评估其主体（表示为stable（e）），并且使用第二原语stabilize来发起回滚。该语言的语法和语义在图6和图7中给出。例如变量、表示通道的位置、λ-抽象、函数应用、线程创建、在通道上发送和接收消息的通信动作，或定义稳定部分的操作，以及将全局状态稳定到一致检查点。我们不考虑这个核心语言中的引用，因为它们可以根据通道上的操作进行建模。我们在6.2节中描述了如何在实现中有效地处理引用。5 如果没有邮箱抽象，异步接收是不可行的。94L. Ziarek等人/理论计算机科学电子笔记174（2007）85语法：P：：=PP|t[e]δe：：= x| L| λx。e|e（e）|mkCh () | send（e，e） | 回收 | spawn (e)|stable(e)|稳定的| stabilize()EVALUATION CCONTEXTS：E：：=· | E（e）| v（E）|发送d（E，e）|sen d（l，E）|回收（E）| 稳定（E）| 稳定（E）Et，P[e]：：=Pt[E[e]]δδ程序状态：P∈过程t∈Tidx ∈VarEt，Pδe →eJLR[e]， Δ=ΔEt，Pδ [eJ]， Δl∈通道δ∈StableIdv∈ Val=单位| λx。e| 稳定（λx. e）、 | lα，β∈Op={LR，SP，cOMM，SS，ST，ES}Λ∈StableState =Process×StableMapΔ∈StableMap=StableId→finStableStateLO cAL E估值规则：λx。e（v）→e[v/x]mkCh（）→l，lfresh图六、稳定器的核心按值调用语言程序被定义为线程的集合。每个线程被唯一地标识，并且还与稳定部分标识符（由δ表示）相关联，该稳定部分标识符指示线程当前正在其中执行的稳定部分。稳定段标识符是在一个允许我们比较它们的关系下排序的（例如，它们可以被认为是由全局计数器递增的整数）。因此，我们写道：L. Ziarek等人/理论计算机科学电子笔记174（2007）8595δδJEt，PG股估值规则：tJfreshSPJδ[spawn（e）]，Δ=Pt[E[unit]]δt[e]φ，ΔtJfreshP=Pjt[E[send（l，v）]]tJ[EJ[recv（l）]]JcOMMJ J JP，Δ =Pt[E[unit]]δt[E[v]]δJ，ΔδJfreshδ∈Dom（Δ），δJ≥δΔJ=Δ[δJ›→（Et，P[stable e（λx. e）（v）]，Δ）]δΛ = ΔJ（δmin），δmin≤δ∈Dom（ΔJ）ΛJ=Et，P[stable（e[v/x]）]，Δ[δJ<$→Λ]δ.δEt，P党卫队[stable（λx. e）（v）]，Δ = Δ ΛδES[稳定（v）]，Δ=Δδ.δEt，P[v]，Δ−{δ}δEt，PΔ（δ）=（PJ，ΔJ）圣杰杰δ.δ [stabilize（）]，Δ=ΔP，Δ见图7。 稳定器的核心按值调用语言t[e]δifahradwit hidentietit稳定的部分标识符与序列顺序反映嵌套关系。在适当的时候，我们省略了用稳定的节标识符来装饰一个术语 我们的语义被定义为对这些数据进行合并（PPJPjP）。我们写了Pg{t[e]}表示不包括具有标识符t的线程的线程集合，以及请{t[e]}注意，执行扩展时，必须执行以下操作：e与标识符t。我们使用求值上下文来指定线程内的求值顺序，并防止过早地对封装在spawnexpress ion中的表达式求值。我们定义了一个hre和dcontextEt，P[e]tode不适用于xpressioneavail ableδ对于在上下文E中由线程t∈P执行;序列δ指示嵌套的稳定部分的有序序列，其中表达式求值。一个程序状态由一个求值线程的集合（P）和一个稳定映射（Δ）组成，它定义了一个将稳定段标识符与状态关联起来的有限函数一个程序开始求值时有一个空的稳定映射。项目评估是Et，P96L. Ziarek等人/理论计算机科学电子笔记174（2007）85⇒αJ J由全局归约关系P，Δ =ΔP， Δ指定，该关系映射程序一个新的程序状态。我们用一个动作α来标记每个评估步骤，定义通过计算表达式而产生的结果。我们写=α=α来表示这个关系的自相关的传递闭包。感兴趣的操作是那些涉及通信事件或操纵稳定部分的操作。我们使用标签LR来表示局部归约操作，SP表示线程创建，COMM表示线程通信，ss表示稳定段的开始，ST表示稳定运行，ES表示从稳定段退出线程内的局部约简由辅助关系e→eJ指定，该关系将某个线程内的表达式e求值为新的表达式eJ。局部评估规则是标准的：函数应用程序替换在函数体中为formal添加实际参数，通道创建导致创建一个新位置，该位置充当消息传输和接收的容器。有五个全局评估规则。第一个描述了当创建一个对表达式e求值的线程时全局状态的变化;新线程在没有任何稳定标识符的上下文中对e第二个描述了一个通信事件如何同步地将一个试图在一个线程中沿特定通道传输值的发送方与另一个线程中在同一通道上等待的接收方剩下的三个，也是最有趣的，全局求值规则是涉及稳定部分的规则。当新进入一个稳定段时，会生成一个新的稳定段标识符;这些标识符在一个总序下相关，该总序允许语义表达关于这些段的生存期和作用域的属性新创建的标识符被映射到当前全局状态，都记录在马厩地图上 此状态表示可能的检查点。 的该标识符的实际检查点被计算为由最不稳定标识符映射的稳定映射中的状态。此标识符表示最早的活动检查点状态。在稳定映射为空的情况下，该状态是刚刚检查点的状态，或者表示由另一个稳定部分采用的某个较早的检查点状态。在这种情况下，我们的检查点方案是保守的，如果一个稳定段开始执行，我们假设它可能依赖于所有其他当前活动的稳定段。因此，我们将新进入的稳定部分的检查点设置为最旧的活动稳定部分开始时的检查点。当一个稳定段退出时，线程上下文被适当地更新，以反映进入该段时捕获的状态不再代表一个感兴趣的检查点;稳定段标识符从产生的稳定映射中删除稳定操作只是恢复到稳定部分开始时捕获的状态。虽然很容易定义，但语义是高度保守的，因为可能存在语义未识别的涉及较少展开的考虑图8中给出的示例，其中两个线程执行对被监视函数的f，h，g按这个顺序因为f是被监控的，所以在调用它现在，假设线程2对h的调用发生在调用L. Ziarek等人/理论计算机科学电子笔记174（2007）8597φThread 1 Thread 2fun f（）=.fun g（）=.回收（c）...在稳定g（stable f（））letfun h（）=在稳定h（）端...send（c，v）...端见图8。 线程通信和稳定部分的交互。f完成。观察h通过通道c上的同步通信动作与函数g通信。假设程序中没有其他线程，h在g接受通信之前无法完成。因此，当调用g时，由与调用相关联的稳定部分计算的最早全局检查点是由与f相关联的稳定部分建立的检查点，其恰好是由监视h的稳定部分引用的检查点。换句话说，在H或G内执行的稳定动作将导致全局状态恢复到F的执行开始，即使F成功完成。这种策略虽然正确，但正如我们在下文中所描述的那样，科.语义的可靠性由稳定动作的擦除属性定义。 考虑包含可能执行的动作序列α 一个程序。 假设有一个稳定操作发生在α之后。 此操作的结果是将当前全局程序状态恢复到较早的检查点。 然而，考虑到程序执行成功地继续在稳定调用之后，接着存在来自检查点状态的动作序列，其产生与原始状态相同的状态，但是其不涉及稳定操作的执行。换句话说，稳定动作永远不会产生新的状态，因此对最终状态没有影响。方案评价我们在下面的安全定理中形式化这个属性。定理4.1（安全性）：设t，PααJST.β JJJJEφ[e]， Δ =ΔP，Δ =ΔPt[v]，Δf如果α非空，则存在等价求值αJ.βEt，P[e]，Δ=Pjt[v]，Δf使得αJ≤ α。5渐进式构造虽然正确，我们的语义是过于保守的，因为一个全局检查点状态计算后，进入每个稳定的部分。此外，在检查点计算中不考虑建立线程间依赖性的因此，所有线程，即使是那些由发生在98L. Ziarek等人/理论计算机科学电子笔记174（2007）85检查点建立和恢复之间的时间间隔。更好的替代方法是根据线程在检查点间隔内见证的操作来恢复线程状态。 如果线程T观察到动作α，当由线程TJ执行并且T被恢复到执行α之前的状态时，TJ可以被恢复到其遵守α之前的最新本地检查点状态。 如果T没有看到其他线程的动作，则它不受任何稳定器的这些线程可能会发出的呼叫。该策略通过降低恢复检查点的严重性，将影响限制在仅那些见证全局事件的线程上，并将其回滚点建立为在时间上尽可能接近其当前状态，从而改进了检查点算法。图10、图11和图12呈现了对作为程序执行的一部分增量地构造依赖图的语义的细化。这个新的定义不需要稳定的部分标识符或稳定的地图来定义检查点。相反，它捕获数据结构中线程执行的通信操作。该结构由一组表示中间程序点的节点和连接具有共享依赖关系的节点的边组成节点由有序的节点标识符索引，并保存线程状态。我们还定义了映射，将线程与节点及其活动稳定部分集相非正式地，图中每个线程的动作由一个节点链表示，该backdges被建立到代表稳定部分的节点;这些节点定义了可能的每个线程的检查点。后退边缘的来源是发生在稳定段内的通信动作，或者是嵌套的稳定段的出口。边还连接属于不同线程的节点以捕获线程间通信事件。当执行稳定动作时，图可达性用于确定全局检查点：当线程T执行稳定调用时，检查图中从T如果一个线程不是由该线程在执行回滚时，它不会恢复到任何较早的状态。这些检查点的集合构成了一个全局状态。P，G~αPJ，GJ值的关系式P，G ~ α P j，Gj值的作用是Pxx以产生新的进程PJ和新的图GJ。因此，该方法并不意味着该方法的可靠性、可靠性和可靠性。程序最初开始相对于空图进行评估。辅助关系t[e]， G∈GJ模是与图p中的t[e]，G∈ G j模的反作用。它创建了一个新的节点来捕获线程本地状态，并将线程的当前节点标记设置为这个节点。 此外，如果动作发生在稳定段内，则后沿 是从那个节点到这个部分建立的。 这个后缘用于识别一个潜在的回滚点如果一个节点有一个backedge，恢复点将通过遍历这些backedge来确定，因此不存储这些节点的线程上下文是安全的（在这种情况下，线程存储在节点中）。添加到图中的新节点是使用保证大于任何现有节点的节点标识符创建的。L. Ziarek等人/理论计算机科学电子笔记174（2007）8599芬φ行动：SS、SS、ES、SS、COMMT1N1SST2T1N1SST2N2（一）（b）第（1）款T1N1SST2N2T1N1CommT2N2N3N3N5（c）第（1）款N4（d）其他事项见图9。 增量检查点构造的示例。S语法和 E赋值 C上下文P：：=PP|t[e]δEt，P[e]：：=Pt[E[e]]δδe →eJEt，P[e]， GL~REt，P[eJ]， Gδ δ程序状态n∈Node=NodeId×（进程+进程）n<$→nJ∈Edge=Node×Nodeδ∈StableIDη∈CurNode=Thread→finNodeσ∈StableSections=StableID→节点G∈Graph=P（Node）× P（Edge）×CurNode×StableSections见图10。增量检查点构造。当稳定化动作发生时，计算从代表封闭稳定区段的节点可到达的节点的集合。新的图反映了恢复，G/N是去掉以n∈N为根的子图后的图G.我们定义了以下定理，该定理形式化了增量检查点构造比全局时间点检查导致更少回滚点策略：定理5.1（E-效率）：如果和Et，P[e]，Δ0α。圣路易=PJ，ΔJEt，P[e]， Gα~. STPJJ，GJ100L. Ziarek等人/理论计算机科学电子笔记174（2007）85φ0L. Ziarek等人/理论计算机科学电子笔记174（2007）85101δδδδδδG_ E赋值规则n=ADDNODE（t[E[e]]φ，N）GJ=<$N<${n}，E<${η（t）<$$> →n}，η[t<$→n]， σ<$t[E[e]]φ，<$N，E，η， σ<$<$GJt[E[spawn（e）]]δ， GN，E，η， σtJfreshn=ADDNODE（tJ[e]φ，N）GJ=<$N<${n}，E<${η（t）<$$> →n}，η[tJ<$→n]， σ<$Et，P[spawn（e）]， G~SPPt[E[unit]]tJ[e]，GJδδφP=Pjt[E[send（l，v）]]tJ[EJ[recv（l）]]t[E[send（l，v）]]， G<$GJtJ[E[recv（l）]]，GJ<$GJJGJJ=<$ N， E，η，σ<$GJJJ=<$N，E<${η（t）<$→η（tJ），η（tJ）<$→η（t）}，η， σ<$P，GcO~MMPjt[E[unit]]tJ[EJ[v]]，GJJJ见图11。增量检查点构造。则PJ，ΔJβ= ΔPJJ，Δ JJ。5.1实施例为了说明语义，考虑基于图8中给出的示例的图9中所示的动作序列。节点n_1表示稳定区间监视函数f（a）的开始。接下来，创建h的被监视的实例化，并且在图（b）中分配与该上下文相关联的新节点。 没有当f退出其稳定部分时，需要对图进行改变。对函数g的监控会导致第一个线程的新节点与前一个节点的边最后，考虑两个线程在通道c上交换一个值。 与通信对应的节点被创建，其各自的稳定部分（d）具有后边缘。回想一下，全局检查点方案将恢复到在f的监控版本产生时创建的全局检查点，而不管稳定操作发生在哪里。相反，使用该增量方案在g或h的执行内发生的稳定调用将把第一线程恢复到存储在节点n3中的本地检查点（对应于紧接在对g的调用之前的上下文），并且将把第二线程恢复到存储在节点n2中的检查点（对应于紧接在对g的调用之前102L. Ziarek等人/理论计算机科学电子笔记174（2007）85δ.δG.评价规则续n=σ（δ）nJ=ADDNODE（δ，N）GJ=<$N<${nJ}，E<${η（t）<$$> →nJ，nJ<$$> →n}，η[t<$→nJ]， σ<$t[E[e]]，<$N，E，η， σ<$<$GJG= N， E，η，σ δ新鲜n=ADDNODE（t[E[stable e（λx. e）（v）]]δ，N）GJ=<$N，E<${η（t）<$$> →n}，η[t<$→n]，σ[δ<$→n]<$Et，P[stable（λx. e）（v）]， G~SSEt，P[stable（e[v/x]）]，GJδ δ.δG=<$ N， E，η，σ<$ GJ =<$ N， E，η，σ−{δ}<$Et，P[stable（v）]， GE~SEt，P[v]，GJδ.δ δG=<$ N， E，η，σ<$σ（δ）=n τ=REACH（n，E）PJ={t[e]|i，t[e] t. i≤j<$$>j，t[eJ]<$∈τ}PJJ=PJ（PgPJ）GJ=G/τEt，P[stabilizee（）]， G~STPJJ，GJδ.δREACH（n，E）={n}<$REACH（nJ，E− {n<$→nJ}） J.T. n<$→nJ∈E见图12。增量检查点构造。对H的调用）。6执行我们的实现被合并到MLton [22]中，这是一个标准ML的全程序优化编译器底层基础设施的主要变化是插入写屏障来跟踪共享内存更新，并挂钩到并发ML [31]库以更新通信图。因此，状态恢复是恢复延续和恢复引用的组合。实现大约是2K行代码来支持我们的数据结构，检查点和恢复代码，以及大约200行对CML的更改。L. Ziarek等人/理论计算机科学电子笔记174（2007）851036.1支持一流的活动由于我们的实现是核心CML库的扩展，因此它支持第一类事件[31]以及基于通道的通信。对事件的处理与我们对消息的处理没有什么不同。 如果一个线程在一个有关联通道的事件上被阻塞，我们将从该线程的当前节点向通道插入一条边。我们支持CML的选择性通信，而不改变基本算法。由于CML对通信事件施加了严格的排序，因此在稳定操作之后，必须清除每个通道中的虚假或无效数据。CML为每个通信动作使用事务标识符，或者在选择性通信的情况下，使用一系列通信动作。CML已经实现了在发生同步操作时清除通道中的虚假数据，选择性沟通这是通过标记事务标识符来懒洋洋地完成如消费。通信操作检查并删除任何如此标记的数据。我们在稳定行动中利用这个相同的过程来清理通道6.2处理引用到目前为止，我们已经省略了关于如何跟踪共享内存访问的细节，以便在存在引用的情况下正确地支持状态恢复操作。单纯地分别跟踪每个读和写操作是不明智的。有两个问题必须解决：（1）不必要的写入不应该被记录;（2）应该避免由读取引起的虚假依赖。请注意，对于给定的稳定段，监视第一次写入 给定的存储器位置，因为每个稳定部分作为单个单元展开。为了监控写操作，我们创建了一个版本列表，在其中存储引用/值对。对于列表中