同步协作线程的参数在多项式时间内终止的静态分析方法

理论计算机科学电子笔记154（2006）33-43www.elsevier.com/locate/entcs同步协作线程罗伯托·M Amadio1Universit'edeParis7Fr'ed'ericDabrowski2INRIA索菲亚-安提波利斯摘要我们关注的是由合作线程组成的程序，这些线程的执行在称为瞬时的同步轮中进行。我们开发的静态分析方法，以保证每个时刻终止于时间多项式的大小的程序的参数在开始的计算。关键词：同步与合作规划，资源界限，拟解释，终止，多项式时间。1引言在[8]中，Boussinot和De Simone介绍了同步语言（SL）。SL中的程序是一组通过共享信号进行交互的协作线程，其执行在称为瞬时的同步轮中进行。该模型的一个基本假设是，对一个瞬间内没有信号的反应只能发生在下一个瞬间。反应性是SL程序必须保证的基本这意味着，在每一个时刻，输入的程序将SL语言已逐渐发展成为并发应用程序的通用编程语言，并已在各种编程环境中实现，如C、JAVA、SCHEME和CAML。用这些语言成功开发的典型应用包括事件驱动控制器、数据流1电子邮件地址：amadio@cmi.univ-mrs.fr2电子邮件：frederic. inria.fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.05.00534R.M. Amadio，F.Dabrowski/Electronic Notes in Theoretical Computer Science 154（2006）33架构、图形用户界面、模拟、web服务和多玩家游戏（参见，例如，，[13，5]）。上面提到的SL语言的所有扩展都引入了数据类型，如整数，列表，树。在这种情况下，确保反应性意味着什么？我们可以考虑三个日益雄心勃勃的目标。第一，确保每一个瞬间都结束。 第二，是保证一个时刻的计算终止于可行的界限，这取决于在时刻开始时的参数的大小。 第三个是保证程序的参数保持在一定的范围内，因此程序执行所需的资源在任意多个时刻都受到控制在本说明中，我们介绍了一个基本版本的SL模型丰富的数据类型和开发静态分析方法，以保证每个瞬间终止于时间多项式的大小的程序在开始计算的参数。根据作者之一[1]的工作，该方法基于项重写系统的标准终止技术和基于准解释概念的计算值大小的分析的组合。相对于[1]，主要的创新之处是：（1）模型的更一般和抽象的形式化。(2)一种产生不等式的方法，其在适当结构中的满足需要在任意多个时刻对程序参数的大小有多项式界（定理4.2）。(3)提出了一种保证多项式时间终止的新方法，尺寸变化终止的专门化（定理5.1）。2模型程序是由相互递归的类型、函数和行为定义列表描述的多线程集。线程通过共享信号进行交互，共享信号可能携带通用值（包括信号）。该语言应被视为一种中间代码，其中复杂的控制结构已被编译成一个简单的尾递归形式。类型和构造函数。我们假设一个类型列表t，t，J，. 以及构造器c，c，J，.. . .对于特定的“信号”类型的构造函数，我们可以使用符号R，R J，. 并将其作为参考值。值v是由构造函数构建的一阶项。大小|v|值v的定义为：|C| = 0w及|c (v1,...，v n）|= 1 + |v1|+···+|v n|.我们将使用符号a来表示向量a1，. ，n个元素，并且用σ，σJ，. 将变量映射为值的代换[v/x]。类型和构造函数由具有以下形状之一的方程组声明(1) t =···|t1的c，. ，tn|···（2）t = Sig（tJ），其中···|r：= v|···在等式（1）中，我们声明了一个类型t和一个函数类型为（t1，.，t n）→t.在等式（2）中，我们声明了一种类型的评估信号，包括信号r，其在每个时刻的开始处的值是v。我们的意图是，值v具有类型tJ（见下文），为了简单起见，我们假设|v| =0。信号可以被读取和写入，并且它们的值总是被定义的。R.M. Amadio，F.Dabrowski/Electronic Notes in Theoretical Computer Science 154（2006）3335方程组遵循通常的约定，即其中出现的类型和构造函数只声明一次。这意味着我们可以为每个构造函数分配一个唯一的类型（t1，.，t n）→t，其中n≥ 0。对于这种赋值，值是根据规则类型化的：值c（v1，..，v n）具有类型t如果c被分配类型（t1，.，t n）→t，并且值v i具有类型t i，i = 1，.，n.最后，我们有一个特殊的行为类型beh：这种类型的元素不返回值，而是产生副作用。在下文中，我们将操作各种句法概念：变量、值、模式、表达式、表达式体、替换、行为、程序等。我们总是假定它们是正确的类型。打字规则是标准的，被省略了。表情 设x，y，. 表示值范围内的变量。 模式p是由构造函数和变量构建的良好类型的术语。特别地，线性模式p是其变量都是不同的模式。在下文中，所有模式都假定为线性。表达式e具有形状h（e1，. 其中n≥ 0且h可以是变量x、构造函数c或函数符号f。类型为（t1，.，t n）→t由方程f（x）= eb指定。这里eb是由语法定义的表达式体：eb：：= e|将x与···peb···匹配。简化在表示中，我们假设一个（良好类型的）值恰好匹配一个模式。封闭表达式体eb根据以下标准规则计算为值v，写作ebv，其中σ表示匹配替换，ev代表e1v1，.。，e n n.（e1）埃吉夫c（e）（e2）叶尔佐夫，f（x）=eb，[v/x]ebvf（e）vσp=vJσebv（e3）将vJ与···peb···v线程行为。在下面，我们让Q，QJ，. 范围涵盖变量和参考值。我们用b，BJ，. 行为定义如下：b：：=停止||f（e）||产量.b ||next.f（e）||：= e.b||将x与···p b···匹配||用···p b···[x] f（e）读其中f是类型（t1，.，t n）→beh，由方程f（x）= b定义。在示例中，我们可以省略读指令的分支pb或分支[x]b行为产生副效应，它们的执行与存储相关，存储的元素用s，sJ，. 存储是一个有限部分函数将引用值映射到类型兼容的值。我们将用so表示默认存储，在每个时刻开始时使用该默认存储初始化计算。行为减少由下面的八条规则描述。 减少（b，s）（bJ，sJ）意味着行为b与存储s运行原子操作36R.M. Amadio，F.Dabrowski/Electronic Notes in Theoretical Computer Science 154（2006）33直到BJ，产生存储SJ并将控制返回给调度器。（b1） （stop，s）停止（stop，s）（b2） （yield.b，s）σp=v，（σb，s）<$（bJ，sJ）（b3）（next.f（e），s）<$（next.f（e），s）（b4）（matchvwit h· ··p<$b· ··，s）<$（bJ，sJ）ev（b，s[v/r]）（bJ，sJ）没有模式匹配s（r）（b5）（r：=e. （b，s）（bJ，sJ）（b6）（readr. . . ，s）（readr. . . （s）（b7） s（r）=σp，（σb，s）<$（bJ，sJ）（rearwith.）.... . . 你 好 。 pb.. . ，s）n（bJ，sJ）（b8）e<$v，f（x）=b，（[v/x]b，s）<$（bJ，sJ）（f（e），s）（bJ，sJ）各种指令的效果非正式地描述如下：stop，永远终止执行线程;yield.b，停止执行并将控制权移交给调度程序-控制权应在同一时刻稍后返回线程，并使用b继续执行;f（e）和next.f（e）切换到另一个立即或在下一瞬间开始时的行为;r：=e.b，eval-评估表达式e，将其值赋给r，并继续评估b;用.读取r。我... [x]f（e），等待直到r的值与模式p之一匹配（可能没有延迟），否则产生控制;如果在最后线程总是在等待一个匹配值的时刻被卡住，然后它在下一个时刻开始行为f（e），其中x是结束时r的值。 瞬间;与...匹配pb根据模式过滤值vp;执行永远不会阻塞，因为我们假设总是有匹配的模式。 我们说，一个行为b与存储s被挂起，写为（b，s），如（b，s）借高度证明表1证明（b1）、（b3）或（b6））。因此，暂停行为b必然具有形状停止或下一个。. ）或读···。程序. 我们抽象地表示一个程序P作为一个非空的多行为集。具有存储s的程序P的求值定义如下：（p1）<$b∈P（b，s）<$（P，s）（[Ps，s]）（p2）<$b∈P（<$（b，s）<$（b，s）（bJJ，sJJ）（P\{b} <${bJJ}，sJJ）<$（PJ，sJ））（P，s）（PJ，sJ）其中表示在该时刻结束时线程的执行结果的程序[P]s定义如下：[Ps={|[b]|b∈P|} [stops=stop[下一个.f（e）s = f（e）][read r.. . [x] f（e）s =[s（r）/x]f（e）注释2.1[公平性]程序在一个瞬间的执行包括一系列行为的执行，直到所有行为都被暂停。规则（p2）允许对行为进行完全不确定的调度。我们说，如果有一个行为运行（至少）两次，并且在两次运行之间有一个连续启用但从未运行的不同行为，则执行（在瞬间内）是不公平的。方案包括yield指令可以依赖于所有执行都是公平的假设（参见，实施例3.2）。R.M. Amadio，F.Dabrowski/Electronic Notes in Theoretical Computer Science 154（2006）33373约束生成我们引入一个合适的控制流分析与一个程序的一组不等式一阶项。Read once条件我们要求线程执行任何给定的读指令在一个瞬间最多一次这可以通过简单的控制流程分析来检查拒绝可能在同一个读指令的瞬间内遍历几次的程序在这个检查之后，我们为程序中的每个读指令分配一个不同的新标签y，并且我们以有序序列y1，...，y m.在下文中，我们有时会使用记法来读yQ，并... 在行为的代码中，使读取指令的标签可见。然后，对于每个定义行为的函数符号f，我们关联一个列表yf，该列表由我们可能在从f开始的瞬间内执行的读指令的标签组成。重要的一点是，在瞬间内f的计算可以被认为是作为参数和瞬时内读取的值的函数控制点。控制点是三元组（f（p），be，i），其中，直观地，f是当前调用的函数，p表示到目前为止在函数定义中交叉的模式，加上可能仍然必须执行的读取指令的标签，因为是控制点，并且d是将被用来与各种条件的控制点相关联的整数。如果函数f返回一个值，并且由方程f（x）= eb定义，那么我们将f与集合C（f，x，eb）定义如下：C（f，p，eb）=情况ebe：{（f（p），e，0）}匹配x。......你好。p eb J.. .：···C（f，[p/x]p，eb J）···另一方面，假设函数f通过方程f（x）=b定义一个行为。然后，我们生成一个新的函数符号f+，其arity是f加上yf中的变量数（对应于f在一个瞬间内可以执行的读指令的有序标签序列当展开C的定义时，函数f+的参数x和标签yf可以用模式代替。当从一个瞬间到下一个瞬间时，我们需要控制参数的大小。其基本思想是，如果f可以在当前时刻或之后调用g，则f的参数应该控制参数的大小 ofG.这个想法必须小心地实现，因为某些值可能取决于读取指令，并且某些参数可能在下一时刻开始之前被丢弃。因此，我们首先确定可能启动行为的函数符号。它们包括我们可以用来开始线程计算的所有函数符号，以及跟随下一条指令或a[y] pour. 分公司我们称这些函数符号为初始的。接下来我们需要一些符号设0是一个新的常数。如果h是元数n的函数，且I∈ {1，.，n}则h（e1，.，e n）I被定义为h（eJ，.，eJ）其中eJ= e i，如果i∈I且eJ= 01ni i否则，请执行以下操作。直 观 地，在h（e1，. ，e n）I我们将所有不在I中的参数设置为0。38R.M. Amadio，F.Dabrowski/Electronic Notes in Theoretical Computer Science 154（2006）33FG！FG对于每个函数符号f，定义一个arity n的行为与arityn+m的相关函数符号f+，我们定义一个集合I f{1，.，n}，条件是I f={1，... ，n}，则f是初始的。特别地，这意味着我们忽略与读指令相对应的所有按照这种约定，与f+相关联的控制点的集合是C（f+，（x，yf），b）定义如下：C（f+，p，b）=情况b（C1）停止：（C2）g（e）：{（f+（p），g+（e，yg），0），（f+（p）I，g+（e，yg）I，2）}（C3）产率d. bJ：C（f+，p，bJ）（C4）next. g（e）：{（f+（p）I，g+（e，yg）I，2）}（C5）：=e. bJ：{（f+（p），e，1）} <$C（f+，p，bJ）（C6）m.Atch xwit h. . . p.j.. . ** . . C（f+，（[p/x]p），bJ） . .读（y）与.. .{（f+（p）I，g+（e，yg）I，2）}（C7）：fgp.j.. . [y][e] . . C（f+，[p/y]p，bJ）。 . .注意，在子句（C2）中，只读一次条件保证标签yg出现在模式p中。控制点（f（p），be，i）的实例是表达式体或行为beJ=σ（be），其中σ是自由变量的替换映射在价值观上。为了进行证明，可以方便地对控制点实例进行表达式体评价和行为评价在定理4.2的证明中给出了如何做到这一点的提示，并且在[1]中可以得到完整的处理。我们把一个控制点（f（p），be，i）与一个约束f+（p）≥ibe（i=0，1，2）联系起来，并说这个约束的索引是i。直观地说，我们依赖于索引0的约束来强制终止瞬间，依赖于索引0， 1的约束来强制限制瞬间内计算值的大小，索引为0、 1、 2的那些，以保证任意多个时刻的计算值的大小的界限。请注意，约束是纯一阶项，这一属性允许我们重用标准项重写框架中开发的技术例3.1作为一个运行的例子，我们考虑服务器f（s，x）的情况，它在每个时刻都产生控制，读取信号s上的请求列表，并为请求提供服务：f（s，x）=产量。用l读s <$f J（s，x，l）fJ（s，x，l）= match l with nil next.f（s，x）|cons（ req（r，y），lJ）=h1（y，x）.fJ（s，h2（y，x），lJ）服务器维护状态X。请求包含数据y和返回信号r。我们不指定函数h1和h2;第一个用于回复请求，第二个用于计算服务器的以下状态。希望使用服务器的客户端g（s，r，y）可以定义如下：g（s，r，y）=用l读取s = cons（req（r，y），l）。产率用z读r。. .请注意，在列表中插入消息的操作需要一个读操作，因此readonce条件禁止在瞬间执行此类操作然而，任意多个行为可以在R.M. Amadio，F.Dabrowski/Electronic Notes in Theoretical Computer Science 154（2006）3339瞬间 我们计算索引0， 1， 2的约束，假设f是初始的，fJ不是初始的，并且If={ 1， 2} =IfJ。fJ+（s，x，cons（req（r，y），lJ））≥0fJ+（s，h2（y，x），l）f+（s，x，l）≥0fJ+（s，x，l）fJ+（s，x，cons（req（r，y），lJ））≥1h1（y，x）f+（s，x，0）≥2fJ+（s，x，0）FJ+（s，x，0）≥2f+（s，x，0）FJ+（s，x，0）≥2FJ+（s，h2（y，x），0）例3.2[寄存器]在我们的框架中，寄存器可以被视为从一个时刻到下一个时刻保持其值我们可以用一个信号（具有相同的名称）和一个线程来模拟寄存器r，该线程的行为f（r）由下式描述：f（x）=readx with[y]g（x，y），g（x，y）=x：=y.f（x）行为f（r）等待读取r的值y的时刻结束，并在接下来的时刻将y再次写入r。由于在模拟中r是一个信号，在开始的瞬间，它的值被重置。然后我们必须确保行为f（r）在任何其他行为试图读取r之前运行。为了这个目的，我们依赖于公平假设（cf。注2.1），并转换所有其他行为定义，使它们以收益率开始。我们可以从这个模拟中提取条件来控制寄存器中值的大小。特别地，我们注意到，约束f+（x，0）≥2g+（x，y）只有在寄存器中包含的值y具有有界大小时才能满足这是我们必须施加的一个重要限制关于编程语言4大小界限为了限制由程序计算的值的大小，我们依赖于 qu asi-interpretationn的n o tion（see[6，2，3，7]）。在这里，函数符号f的qu是一个数值函数，它确保存在一个常数k，使得当用参数v1， . . ，vnisbondoundedbyqf（k|v1|. . . . ，k|vn|）.准解释的合成在某种程度上可以机械化。准解释的存在并不需要终止，但它确实允许控制计算函数的复杂性，下面是众所周知的结果：S. Cook [9]证明了一个多项式有界的辅助下推自动机可以通过图灵机在指数时间内使用一个“表”来存储中间结果来模拟我们参考[3]对这些问题进行扩展讨论。解释和准解释。假设给定一个程序。一个赋值q与每个构造函数和函数符号h相关联，一个自然数N上的函数qh使得：(1)如果c是一个具有元数n的构造函数，则qc= 0，如果n = 0，则qc（x1，.，xn）= d + π i∈1. nx i如果n > 0，其中d∈N且d≥ 1（这保证了值的准解释与其大小成比例）。特别地，在约束中引入的特殊常数0的准解释是自然数0。(2)Iff是一个函数，它具有如下性质：qf：（N）n→N是自然数上的一个单调函数.40R.M. Amadio，F.Dabrowski/Electronic Notes in Theoretical Computer Science 154（2006）33我们说一个函数U：N → N有界于赋值q，如果<$x ∈ N q h（x，. ，x）≤U（x）。特别地，我们说q是多项式有界的，如果函数U可以是多项式。我们将一个没有变量的表达式e与一个自然数qe联系起来，如下所示：qh （ e1 ， . ， en ） = qh （ qe1 ， . ， qen ） 。（1）我们写q| = e1≥e2，如果赋值q满足约束e1≥e2，其中e1，e2是表达式（可能有变量）。这被定义为：Q|=e1≥e2如果<$σqσe1≥qσe2（2）其中σ是将值与变量相关联的替换。我们也写：q| = e1>e2，如果<$σ qσe1> qσe2。一个赋值q是一个准解释，如果它满足程序生成的索引0，1，2的约束，而且如果它满足f（x1，. ，xn）≥ xi，对于所有i = 1，. ，n和所有函数符号f。最后一个条件允许控制函数计算的值的大小，而不仅仅是其结果的大小 因此，如果f（v1，.，v n），则我们知道qf（v1，.，vn）≥q v，而且对于任何通过函数Qf（v1，.. . ，vn）≥qu.例4.1我们定义了运行例3.1的准解释。 我们假设函数h1和h2在有界大小的值上运算。 然后我们可以取qh1 = qh2 = λ（x，y）·k，其中k ∈ N是适当的常数.我们还可以设置qcons（x，l）=x+l+ 1和qreq（r，y）=r+y+ 1。然后我们可以通过假设qf+（s，x，l）=QFJ+（s，x，l）=max（l，k）来满足所有约束。定理4.2如果程序P具有多项式有界的拟解释q，则由P计算的最大值的大小是计算开始时程序参数大小的多项式。为了证明定理4.2，我们定义了控制点实例上行为的一小步约简。该减少使得存储器和调度器抽象化，同时取决于将值与读取指令的标签相关联的赋值δ赋值δ是一种oracle，它为线程提供它在当前时刻可能读取的值。每当我们从一个时刻移动到下一个时刻时，都会生成一个新的赋值（规则bJ3和bJ6）。（BJ2）（f+（p），yield.b，σ，δ）→（f+（p），b，σ，δ）（BJ3）（f+（p），ne× t. g（e），σ，δ） →（f+（p），g（e），σ，δJ）（bJ4）（f+（p），matchxwit h· ··p<$b··，σ，δ）→（f+（[p/x]p），b，σ1<$σ，δ）if（1）（BJ5）（f+（p），σ：=e.b，σ，δ）→（f+（p），b，σ，δ）如果σe≠v（bJ6）（f+（p），read（y）） ， . . [y]g（e），σ，δ）→（f+（p），g（e），[δ（y）/y]σ，δJ）if（2）（bJ7）（f+（p），改为（y）。. . p b.. 、.、σ，δ）→（f+（p），b，σ1<$σ，δ）如果（3）（b，J，8）（f+（p），g（e），σ，δ）→（g+（x，y，g），b，σ，δ）if（4）其 中 ： （ 1） <$σ1p=σx ， （ 2） <$（ 没 有 模 式 匹 配 δ （ y ） ） ， （ 3） <$σ1 （ p ） =δ （ y） ， 以 及 （ 4）<$（σe<$v，g（x）=b，σJ=[v/x]）。 依靠小步骤语义，我们然后证明下面的引理，定理4.2直接遵循。引理4.3假设q是具有m个不同读指令和n个线程的程序P的多项式有界准解释。让i表示程序的线程，P（i）表示相关的 行为。R.M. Amadio，F.Dabrowski/Electronic Notes in Theoretical Computer Science 154（2006）3341(1) 假设在计算开始时，P（i）=f（v），并且P（i）=（e）在下一时刻开始时。 则qf（v）≥ qg（e）.(2) 假设在一个瞬间P（i）= f（v）的开始。 然后，由该线程计算的值的大小由 q f+（v，u）来确定，其中u是在线程读取信号时包含在信号中的值（或否则为默认值）。(3) 假设c是一个边界上的拟解释的参数，在一个时刻的开始，U是一个多项式上的拟解释。 那么程序P在一个瞬间计算的值的大小（多项式）由U n·m +1（c）限定。5多项式时间反应性Marion等人。[11，6，7]已经展示了如何通过将多项式有界的准解释的存在与递归路径排序的适当限制的终止相结合来确保多项式空间或时间中的终止（参见，例如，，[4]）。在本节中，我们提出了一种更灵活的方法，我们使用准解释而不是限制递归路径顺序来比较函数索引为0的约束具有以下形状之一：（A）f（p）≥0e或（B）f+（p）≥0g+（e）.我们从建立最小的前序（自相关和传递）开始。≥F在函数符号上使得f≥Fg如果f出现在左手边并且g在索引为0的约束的右手侧。如果f≥Fg且g≥Ff，我们记为f=Fg。 我们注意到，返回值的函数符号永远不能调用一个函数符号，产生一个行为，所以我们有，后者总是大于前者。与递归路径排序一样，我们将状态与每个函数符号相关联，它决定了如何比较函数的参数。在我们的案例中，我们考虑字典式或多集合状态。我们假设关于前序≥ F等价的函数符号具有相同的元数和相同的状态。根据[7]，我们说一个约束是线性的，如果在右手边最多有一个函数符号与左手边的函数符号等价。但是，我们假设索引为0的所有约束都是线性的（请注意，形状（B）的约束总是线性的）。假设给定程序的多项式有界拟解释q。我们依靠准解释来比较等价函数符号的参数因此，我们偏离标准RPO方法，并依赖于[10]中的大小变化分析。为了进行词典比较，我们写：q |=（p1，. ，p n）>lex（el，. ，en）如果<在所有σ，qσp1≥qσe1， . . ，qσpi−1 ≥qσei−1，且ndqσpi>qσei。 对于多集合比较，我们写：|=（p1，.，p n）>mset（e1，.，e n）如果对于所有σ，{|q σp，...，q σp|联系 我们|qσe，.，qσe|......这是什么？|... |}是我们对多-1nmset1n42R.M. Amadio，F.Dabrowski/Electronic Notes in Theoretical Computer Science 154（2006）33MSET集合和>N是自然数上的多集序。 我们说准解释是兼容的顺序，如果在所有约束的索引0的形状：f（p1，. ，p n）≥0C [g（e1，. ，e n）]其中C是一个单洞上下文，f=Fg，状态st∈ {lex，mset}，我们有Q| =（p1，.，p n）>st（el，.，e n）。定理5.1假设程序有相容的多项式有界的拟解释。然后，瞬间的计算终止于瞬间开始时参数大小的P屋顶提示。在我们的语言中，所有的函数定义都是一阶的。 然后，每个线程的状态可以由帧堆栈表示。 框架是一个三元组（f，pc，v1···vn），其中f是函数的名称，pc指向要执行的函数的指令，v1···vn是值的堆栈。 可以静态地确定可以在堆栈上的值的最大数量。 所以，帧由堆栈上可以找到的值的大小决定准解释提供了一个多项式界。我们的任务是限制线程在一个瞬间内可以分配的帧的数量函数符号f的秩是最长函数链的长度，使得f > Ff1> F···> Ff n相对于函数符号上的前序。我们使用索引0的约束的线性和准解释是在自然数上的假设来估计秩为o的函数f在用大小至多为B的参数调用时可以生成的帧数ncall（o）。Q例5.2参考运行的例3.1和4.1，我们假设f+> F fJ+，函数f j +的字典序状态（从右到左）。注5.3[7]中的方法是基于递归路径排序的，它与构造子上的同胚嵌入Demb相 我们观察到，如果pDembpJ和q是一个分配，则q |= p> pJ. 因此，这里提出的方法当[7]中的函数成功时（因此所有PTIME函数都可以表示）。反之则失败，因为当e包含函数符号时，我们永远不会有pDembe6结论我们已经提出了一个静态分析，保证由同步合作线程组成的程序在计算开始时的参数大小的时间多项式中的每一个时刻作出反应。我们所施加的条件完善并扩展了[1]中提出的条件，以便在瞬间控制资源。正如可以预料的那样，在任意多个瞬间控制资源的可能性是有代价的。 首先，每个线程的参数 在每个瞬间的开始，必须基本上不增加尺寸。为了满足这一要求，通常需要依赖于公平收益假设并重新编程应用程序，使得瞬间足够大;通常，R.M. Amadio，F.Dabrowski/Electronic Notes in Theoretical Computer Science 154（2006）3343时刻对应于协议事务或逻辑仿真步骤。其次，寄存器（或持久信号）必须携带有界大小的值，而无界数据结构仍然可以分配给信号（在每个时刻开始时重置）。致谢作者得到ACI CRISS的部分支持。这本书是在UniversesitédedeProvence的基础上编写的。引用[1] R. Amadio和S.达-齐里奥同步合作线程的资源控制。在Proc.CONCUR，SLNCS 3170，2004中。扩展版本出现在理论计算机科学。[2] R.阿玛迪奥最大加准解释。在TLCA的Proc.中，Springer LNCS 2701，2003。[3] R.阿玛迪奥max-plus拟解释的合成。InFundamenta Informaticae，65（1-2）：29-60，2005.[4] F. Baader和T.尼普科学期重写之类的。剑桥大学出版社，1998年。[5] L. Mandel和M.普泽 Reactive ML是ML的一种扩展。 InProc. ACM PPDL，2005.[6] G. Bonfante，J.-Y. 马里恩和J. -Y. 莫扬关于具有空间约束证明的终止方法在Proc. PSI，SLNCS 2244，2001中。[7] G. Bonfante，J.- Y.马里恩和J. - Y.莫扬准诠释。2004年11月草案。 可从作者处获得。[8] F. Boussinot和R.De Simone，SL同步语言。 IEEE Trans. 软件工程，22（4）：256 -266，1996.[9] S.厨师.下推机的时间有界计算机刻画。Journal of the ACM，18（1）：4[10] C.李，N. Jones和A.本·阿姆拉姆程序终止的大小变化原理。InProc. ACM POPL，2001.[11] J. -是的 Marion。 C om lexiteimplicitedescalculs，de lapratiqe.我不知道你是谁。H a bili tation`adirigerdesrecchercches，2000年。[12] J·奥斯特豪特为什么线程是一个坏主意（对于大多数目的）。1996年USENIX技术会议邀请演讲[13] 响应式编程，INRIA Sophia-Antipolis，Mimosa项目。http://www-sop.inria.fr/mimosa/rp网站。