并发程序调试工具集：路径条件计算、交互式执行、代码转换、可视化流程图

128理论计算机科学电子笔记70第4期（2002）网址：http://www.elsevier.nl/locate/entcs/volume70.html14页跟踪并发程序Elsa Gunter，a Doron Peledba 新泽西理工学院计算机科学系美国新泽西州纽瓦克，邮编：07102-1982b 英国华威大学计算机科学系摘要检查软件的可靠性是一个不断增长的挑战。试图覆盖整个状态空间的全自动工具经常会因为状态爆炸而失败相反，我们提出了一个工具集，采用一些不那么雄心勃勃，但有用的方法来协助软件调试。该工具集提供了将代码自动转换为可视化的流程图的功能，允许用户交互式地选择执行路径。它通过计算路径条件和探索邻域来帮助用户的路径。它还允许用户交互式地逐步执行程序，由有限序列上解释的时间公式指导。我们将展示几种使用这些功能调试顺序和并发程序的不同方法。1介绍现在的计算机程序与二十年前甚至十年前相比，其规模和复杂性都有很大的不同。软件项目由大型程序员团队承担，编写数千行代码。许多新开发的软件系统包括并行性。系统的不同部分可能驻留在不同的机器上，有时在不同的位置，并通过某种协调机制（如消息传递）进行交互软件开发团队，就像软件本身一样，并行工作，相互连接，以完成一个连贯的产品。现代软件的结构和规模，以及不断增长的压力，以肉紧的开发期限导致软件与次优的可靠性。在过去的几十年里，已经有许多尝试来开发用于增强软件可靠性的技术和工具。最早的，也是最广泛使用的方法是软件测试[16]。2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。129这种方法规定有经验的测试人员（通常是高素质的程序员）构建一个测试用例的集合，通常是程序的执行。测试用例是程序执行的一个样本，并且应该提供一个良好的覆盖率，试图捕获大多数（如果不是所有）错误。测试用例的构建通常基于测试人员的经验和直觉测试用例通常是通过让测试人员首先检查代码来生成的，其中有一些常见的重复错误，例如，使数组索引越界，并试图产生将显示此类失败的执行测试方法在很大程度上取决于测试人员的质量，并且已知可以消除许多编程错误，但不是全部。最近的一种方法是程序验证[2，7]，试图正式证明程序是正确的，关于一些正确性标准和规范，并在一些证明系统内。 演绎定理证明是基于公理的，往往是相当昂贵的。它主要是在小例子上演示的，并且不能很好地扩展尽管如此，它对程序员在开发软件时的思维方式有着重要的贡献特别是，程序验证提出了一个有用的不变量概念，以及相关的前置条件和后置条件。有限状态系统的自动验证，称为模型检查[4，5]，试图在系统具有有限多个状态的有限情况下，以最少的人为干预执行验证任务一个天真的尝试，检查所有的系统状态的系统枚举往往会失败，由于状态爆炸问题。许多启发式方法被用来缓解这个问题。 使用今天模型检查的一个主要限制是，它只能在被检查的属性被正式指定后才能发现错误我们在这里采取的方法是开发一个易于使用的软件分析工具，利用来自上述各种软件可靠性方法的技术该工具某些功能的初步版本我们遵循几项原则。第一个是将目标限制在探索执行路径上，由一系列程序状态或程序指令组成我们不试图解决整个程序的正确性程序，也不提供全面的状态空间搜索或分析。我们处理程序代码中的执行序列和路径，并提供各种算法来探索和分析这些路径。虽然该工具能够帮助获得程序的形式证明（在顺序程序的部分正确性的情况下，正如将要演示的那样），但这不是它的主要用途。第二个原则是使用可视化和交互式方法。我们相信，使用可视化的形式主义来说明软件问题更容易，正如UML工具所展示的那样[6]。在这个过程中允许用户交互并不一定意味着我们不能自动提供信息，130信息，而是我们正在利用用户2路径操作软件测试是以检查路径为基础的。因此，允许方便地选择执行路径非常重要。不同的复盖技术为一个项目的适当复盖提供了标准。我们的工具将路径的选择留给用户。一旦源代码被编译成一个流程图或一组流程图，用户就可以通过点击流程图上的节点来选定的路径也会出现在一个单独的窗口中，其中每一行列出选定的节点、进程和形状（这些行也会根据它们所属的进程编号缩进）。为了使代码、流程图和所选路径之间的联系清晰，使用了敏感的突出显示例如，当光标指向路径窗口中的某个节点时，流程图中的相应节点将突出显示，流程的相应文本也将一旦路径被固定，执行它的条件就被计算出来了。该工具允许通过以相反的顺序从末端删除节点来更改路径例如，这允许在移除被选择为超过该条件的节点之后，为该条件选择替代选择改变路径的另一种方法在处理并发程序时，来自不同节点的转换的执行是交错的，这可能是问题的最重要来源。该工具允许用户对路径上的相邻转换的顺序进行排序，如果它们属于不同的进程。设m = s1s2. sn是节点的序列。对于路径上的每个节点si，我们定义：type （ si ） 是 si 中 转 换 的 类 型 。 它 可 以 是 下 列 之 一 ： begin 、 end 、condition、wait、assign。条件节点是从if或while语句中获得的。等待节点类似于条件，但只有真正的出口。它用于同步并发进程，因为除非条件成立，否则proc（si）是si所属的进程。cond（si）是si上的条件，如果si是条件或等待node.branch（si）是节点si上的标签，如果它在路径中有属于同一进程的后继者，则是一个条件，否则是expr（si）是赋值给某个变量的表达式，如果si是一个赋值语句。var（si）是赋值的变量，如果si是赋值语句。131⇒∧¬p[v/e]是谓词p，其中变量v的所有（自由）出现都被表达式e替换。以下是用于计算路径条件的算法。它向后工作，从序列的尾部到头部current pred：=开始大小写类型（si）do条件casebranch（si）docurrent pred：= current pred_cond（si）current pred：= current predcond（si）当前pred：=当前pred结束情况等待current pred：= current predpredcond（si）分配当前pred：=当前pred [var（si）/expr（si）]结束情况简化（当前pred）端所提供的重要信息是执行所选路径的条件。一组流程图中的执行路径实际上是一个边序列，当限制到所涉及的每个过程时，形成一个连续序列。选择节点并不总是告诉我们它是如何执行的：一个条件节点的执行，对应于一个if-the-else条件，一个while条件，或类似的，是由它的因此，如果条件节点是所选路径中某个进程的最后一个节点，则它不会对路径条件有贡献，因为没有给出关于它如何执行的信息计算出的路径条件的意义对于顺序程序和并发程序是不同的。在由一个过程组成的顺序程序中，前提条件表示所有可能的赋值，这些赋值将确保从第一个选定的节点开始执行选定的路径。在这种情况下，当控制位于其起点时，路径条件对于路径执行是必要的和足够的。当允许并发性或非确定性时，前提条件表示使所选路径的执行成为可能的赋值。 在这种情况下，该条件是必要的，但可能不足以执行路径。因此，当并发或132∧∧∧- 你好−∀ ∀∀如果存在不确定性，则路径先决条件不保证执行所选路径，因为可能存在具有相同变量分配的替代路径简化表达式是一项艰巨的任务。首先，不清楚是否存在一个好的度量，在这个度量中，一个表达式比另一个表达式更简单。另一个原因是，一般来说，判定一阶公式的可满足性或有效性是不可判定的。然而，这样的限制不应该放弃简化公式的启发式尝试，并且对于某些较小类别的公式，这样的决策过程确实存在。简化一阶公式的方法是首先尝试应用几个简单的项重写规则，以执行一些常识和通用的简化。此外，检查公式是否是Presburger算术的特殊形式，即， 允许加法、乘以常数和比较。如果是这种情况，可以使用一些决策程序来简化公式。执行的简化包括以下重写：• 布尔简化，例如，true转换为• 消除了不断的比较，例如，将1> 2替换为false。• 常数替换。例如，在公式（x= 5）中，x在中的每一次（自由）出现都被5取代。• 算术抵消。例如，表达式（x+2）3被简化为x1，x0被替换为0。然而，请注意，（x/2）2并没有被简化，因为整数除法不是整数乘法的逆。如果公式是Presburger算术，我们可以决定公式是否不满足，即，如果它总是假的，或者它是有效的，即，不断真实。第一种情况是通过决定<$x1<$x2. 第二种情况是决定x1x2. 其中x1. xn是出现在图中的变量。如果公式不是Presburger算术的，人们仍然可以尝试判断它的每个最大Presburger子公式是否等价于真或假。公式简化是符号模型检验和定理证明的重要组成部分有几个用于公式简化的软件包ω-库[3]。在[14]中描述了使用程序路径的符号评估的现有工具这个早期的工具（1976）可以计算顺序PL/I程序中选定路径的路径条件。路径是从程序文本中选择的。该计算使用向前符号执行。3示例考虑图1中的简单协议，旨在获得互斥。在该协议中，如果共享的1330：开真5、2：turn=1？真假6：假4：转：3：严重1：无操作0：开真5、2：turn=0？真假6：假4：转3：严重1：无操作Fig. 1. 互斥的例子变量turn不具有其他过程的值。第一个进程mutex0（在Figuremutex的左边）的代码如下：开始While true dobeginwhile turn=1 do begin（* no-op *）end;（*critical section *）turn：=1 end端第二个进程mutex1（右侧）与此类似，常量值1变为0。我们自动获得以下路径，该路径允许第二个进程mutex1，而第一个进程mutex0正忙着等待，如下所示：（mutex0： 0）（mutex1： 0）<互斥1： 5><互斥0： 5><互斥1： 2><互斥0： 2>[互斥量1： 3][互斥0： 1]我们得到路径条件turn = 1，即如果变量turn的初始值为1，则第二个过程将首先进入其临界区。接下来，我们检查一条立即进入两个临界区的路径。134联系我们关于我们（mutex0： 0）（mutex1： 0）<互斥1： 5><互斥0： 5><互斥0： 2><互斥1： 2>[互斥0： 3][互斥量1： 3]我们得到一个路径条件turn= 1turn = 0。这个条件表明，如果初始值为2，我们就不会实现互斥这表明协议设计中存在错误问题是，如果turn没有设置为另一个进程的值，则该这可以通过允许进程进入临界区来修复，如果turn被设置为它自己的值。应用图形交互工具与计算路径条件并简化它们的能力相结合，对于获得程序的直觉和调试程序有几种用途。证明部分正确性本文证明了顺序程序关于某些初始条件和最终断言的部分正确性。 符号P表示如果在执行开始时成立，并且程序终止（部分正确性不包括程序终止的断言），则在终止时成立。为了验证一个程序的部分正确性，做下面的事情就足够了。我们首先用不变量来注释子图的边缘，当控制通过这些边缘时，这些不变量保持不变。从开始节点开始的边用初始条件注释，而到结束节点的边用最终断言注释。我们需要找到将程序的所有执行切割成有限多个有限路径σ1，σ2的边，每个这样的路径包括入口边缘和出口边缘。路径σi的输入边用不变量μi注释，出口边用不变量νi注释。我们必须证明以下几点：如果σi是从满足μi的状态开始执行的，那么它将以满足νi的状态结束。为了证明这一点，我们可以交互式地添加一个新进程，包括以下代码：开始等待结束。我们让系统将代码编译成一个简单的三节点流程图。我们选择路径σi，然后选择νi的节点和相应135/结束节点。该工具生成路径条件σi，σi。 这是执行路径σi并达到满足νi的状态的条件。现在我们计算路径条件<$σi。这是执行路径的条件。我们必须证明逻辑蕴涵（μi<$$> σi）→<$νi，σi。这种情况断言如果路径σi开始处的条件μi成立，并且σi被执行（因此μσi成立），则νi在执行σi结束时成立，即，νi，σi在其执行之前保持。我们可以尝试使用我们的工具的简化功能来处理这个条件：这是通过构建另一个进程来完成的，该进程将此含义作为等待条件，类似于上面创建的进程。这可以通过交互式地添加新进程来实现先等待（不是（μi和σi））或νi，σi结束。系统会自动对此公式应用简化但是，即使公式有效，也不能保证系统将成功地将其简化为真生成测试用例在白盒单元测试中，我们通常对寻找覆盖程序各种执行的测试用例感兴趣。为了覆盖执行中的路径，我们可以在我们的系统中选择路径，并让系统计算路径条件。为了生成一个将通过该路径的测试用例，我们需要用一个令人满意的赋值实例化路径条件根据所需的程序覆盖率，我们可能希望将路径专门化到其节点的执行之外。例如，传递一个标记为条件x= 3或y =4的节点s，我们可能希望在x= 3y = 4时测试路径，并在x= 3y = 4时再次测试路径（当x=3 y= 4时，路径将不会被选择）。我们可以创建，例如，第一种情况，通过交互用代码创建一个新进程开始等待x=3，而不是y=4结束。我们选择所需的路径，但在选择节点s之后为wait语句添加新节点（以及相应的end）。然后我们继续原来的道路。玩交互式符号操作方法是非常灵活的，并允许我们在代码执行过程中研究程序变量之间的连接 它不限制我们在开始时启动程序或初始化所有变量。通过动态地添加与我们的代码交互和干扰的过程，我们可以以正式的方式模拟许多与代码检查相关的心理活动例如，我们可以检查如果程序从x= 0，y = 3和z= 4的某个点我们通过产生一个新的136过程：begin x：=0; y：=3; z：=4 end.我们选择这些节点，然后是原始程序路径的节点。路径条件仍然可以是一个公式，其中x，y或z以外的程序变量显示为自由变量。如果没有其他的程序变量，选择路径与量来模拟它;涉及常数的公式的自动简化将导致在这种情况下路径条件将被限制为真和假。在执行死刑的地方给定其中发生错误的执行路径，重要的是能够检查类似的路径，即，邻居[18] 查看相关路径可以帮助我们精确定位错误的确切位置（它不一定是我们开始获得错误值的第一个点它还可以帮助我们为bug建议修复程序，并检查修复程序是否只能局部解决我们的工具允许我们查看两种相关路径：(i) 有相互前缀的路径。假设在路径的某些前缀中发生了错误，我们可以很容易地检查具有相同前缀的其他路径，看看它们是否有同样的问题。(ii) 具有相同指令但交错顺序不同的路径在并发系统中，以不同顺序排列事件的可能性是导致编程错误的主要原因。4第一千一百零六章时间的终结者我们扩展了时间规范逻辑的使用，用于交互式控制系统的调试 我们允许指定有限序列的时间属性。 我们的调试器具有通过满足时间属性的有限状态序列从一个步骤进展到另一个步骤的能力。通常的调试模式涉及通过执行一个或多个转换（具有不同的粒度，例如，转换可以涉及过程的执行并发系统更难，因为有几个需要监视的协作进程。可以以多种不同的方式逐步执行不同的过渡。相反，我们允许应用一个时间属性来描述一个有限的并发事件序列，这些事件需要从当前状态执行，跳到下一个状态。并发和反应系统的最流行的规范形式主义之一其语法如下：：：=（|¬ϕ |ϕ ∨ ϕ |ϕ ∧ ϕ |Ⓧ ϕ |Ⓧϕ| ✷ϕ |✸ϕ |ϕ U ϕ |V |p137Ⓧ| |∈ PPⓍ ⓍⓍ∨¬ ∧ ¬ VU<$$><$V <$$> U <$ⓍⓍUV其中p，带有一组命题字母。我们用σ表示一个2 P上的命题序列，用σ（i）表示它的第i个状态（其中第一个状态编号为0），用σ（i）表示它从第i个状态开始的子集。我们在有限序列上解释线性时态逻辑（LTL）。[9]中从LTL到有限状态自动机的自动转换设σ是序列的长度，它是一个自然数。LTL的语义解释如下：• σ |=|σ|>1和σ（1）|= 0。• σ |=<$U <$i<$σ（j）|对于某些0 ≤ j<，|σ|使得对于每个0 ≤ i0和σ（0）|=p。其余的操作符可以使用上述操作符定义。特别是，==（（）（ ）），=（（）（），真=p p，假= p p，假=p p，假= p p，假= p p，假= p p，假= p，假 = p p，假= p，假=p 操作者是一个“弱”版本的操作符. 而如果当前状态不是序列中的最后一个状态，那么从下一个状态开始的序列的suprx满足条件。注意到（1）（）（）=（），这是因为RE已经要求RE将是下一状态。另一个有趣的观察是，公式false在处于死锁或终止的状态下成立。运算符和可以使用递归方程来表征，这对于理解下一个序列中介绍的变换算法很有用 因此，U=（U）和V=（（V））。我们利用时间规范来控制步进通过并发系统的不同状态。调试器的基本操作是以有效的方式在系统的不同状态在这样做的同时，可以获得关于系统行为的进一步信息。给定系统s的当前全局状态，我们正在搜索一个序列：s = s0s1. sn这样，• s0= s。• n小于给定的某个限制（可能是默认值）。• ξ |= 0。我们的工具的时间堆栈由不同的序列组成，用于到目前为止获得的模拟或调试它包含几个时间步骤，每个步骤对应于某个满足的时间公式的138时间步骤的结束状态也是下一步骤的开始状态我们搜索满足当前时间公式的时间步长。当找到这样的步骤时，将其添加到时间堆栈。然后，我们可以有几个选择如何继续搜索，如下所述搜索路径可以使用对搜索来完成：来自系统的联合状态空间的状态和属性自动机的状态此外，每个新的时态公式需要搜索空间的新副本递归是在这个空间内处理的。因此，当开始搜索公式1时，我们使用状态空间的一个副本当寻找用于T2的新时间步长时，我们就重新开始复制如果我们回溯第二步，我们回溯第二次搜索，寻找一个新的有限序列，满足条件2。如果我们去掉最后一步，回到公式1，我们去掉第二个状态空间信息，并回溯第一个状态空间搜索。 为此我们我们需要保留足够的信息，使我们能够在执行和回溯其他临时步骤后恢复搜索调试会话包括通过临时堆栈搜索系统在每一点上，我们可以执行以下操作之一引入一个新的时间公式，并尝试从当前状态搜索满足该公式新的时间步长被添加到搜索堆栈中。为时态公式创建一个新的自动机，并形成该自动机与具有当前状态的新初始状态的系统自动机的乘积时间步长是通过在这个乘积自动机中找到一条通往接受状态的路径来找到的。删除一个步骤。在这种情况下，我们在堆栈中后退了一步。我们忘记了最近给出的时间公式，可以用一个新的公式来代替它，以便继续搜索。我们还丢弃了为该时间步骤生成的时间回溯最近的步骤。最新步骤的搜索过程使用最初为该时间步骤创建的自动机从其停止的位置这是试图找到另一种满足最后一个给定公式的我们要么找到一个新的时间步骤来替换前一个，要么报告不存在这样的步骤（在这种情况下，我们回到堆栈中的一个步骤，并丢弃为该步骤创建的自动机）。我们还允许简单的调试步骤，例如，在一个进程中执行一个语句这样的步骤可以被描述为平凡的时间步骤（使用nexttime时间操作符）。除了步长的最小值和最大值之外，还有用于选择时间步长的其他参数。当回溯一个时间步骤以找到满足相同时间公式的替代步骤允许或禁止以与以前相同的系统状态结束的不同步骤。在前一种情况下，我们可以要求采取替代步骤，·····139¬ ∧ ¬∨✛✘ ✛✘✛✟✘✟✟✯✚❍✙❍❍❥✛✟✘✟✟✯✚❍✙❍❍❥✛✘✯✚❍✙❍❍❥✛✟✘✟✟✯✚❍✙❍❍❥✛✟✘✟✟✯✚✙❥✚✙ ✚✙图二. 序列的指数数到达完全相同的系统状态，但在途中经过不同的路径。后一种情况很容易通过向在时间步结束时达到的每个系统状态添加特殊的标记来允许或不允许相同的系统状态序列重复。例如，在以下情况下可能发生这种重复规范的形式为（p）（q）。考虑一系列系统状态，其中（p）（q）成立，直到p和q都开始的某个状态保持，同时。这样的序列可以与不同的属性自动机状态配对以生成两个不同的路径。覆盖系统的状态、边缘或执行的算法的选择典型的搜索，如深度优先或广度优先搜索，不会遍历满足给定公式的所有可能路径。如果一个状态（在我们的例子中，是一对）在搜索之前就参与了，我们就不会继续朝那个方向搜索由于这个原因，以这种方式可以获得的路径的数量存在拓扑情况，其中要求所有路径导致比用上述搜索策略获得的路径呈指数级更多的路径，参见例如，图2中的案例由于反复回溯而产生类似序列的情况，起初似乎对调试不太有用直觉上，我们可能会放弃详尽无遗的可能性，逐步通过相当不同的序列。然而，在一个非常实际的情况下，我们在选择搜索类型和回溯效果方面的选择可能具体来说，在许多情况下，同时在内存中保存多个状态并比较不同的状态可能是不切实际的。在这种情况下，我们可能希望执行无记忆搜索，就像为Verisoft系统开发的那样[10]。在这种情况下，我们可能会执行广度优先搜索，深度越来越高（直到某些用户定义的限制）。我们在搜索堆栈中只保留允许我们根据某种顺序生成不同序列并重新生成状态的信息。这样的信息可以包括从初始状态执行的转换的标识* 示例例如，考虑图1中的两个过程。我们可以试着检查一下mutex1at 0Umutex 0at 3··140此属性断言进程互斥体0是否可以进入其临界区，而进程互斥体1尚未移动。我们的实现假设系统将所有变量都设为0，我们得到一条路径：（mutex0：0）（mutex1：0）<互斥0：5>[mutex0：3]我们现在可以添加另一个时间步骤，通过检查：我们可以获得以下时间步长：<互斥0：4><互斥1：5><互斥量1：2>[互斥量1：3]或者（取决于搜索顺序和搜索选项），我们可以获得以下步骤：<互斥1：5>[mutex1：1]<互斥0：4><互斥1：2><互斥1：3>引用[1] R. Alzheimer，G. Holzmann，D.张文龙，一种新的消息序列图分析器，计算机软件，第1卷，1996年，第70[2] K. R. Apt，E. R. Olderog，顺序和并发程序的验证，Springer-Verlag，1991（第二版，1997）。[3] T. 布 尔 坦 河 Gerber ， W. Pugh ， Model-checking Concurrent Systems withUnboundedNonlinearVariables：SymbolicRepresentations，Approximations ， and Experimental Results ， TOPLAS 21 （ 4 ） ， 747-789（1999）.[4] E. M. Clarke，E. A. Emerson，使用分支时间时序逻辑的同步框架的设计和合成。程序逻辑研讨会，约克敦高地，纽约，计算机科学讲义131，Springer-Verlag，1981，52[5] E. A. Emerson，E. M. Clarke，Characterizing correctness properties of parallelprograms using fixpoints，International Colloquium on Automata，Languagesand Programming，Lecture Notes in Computer Science 85，Springer-Verlag，July 1980，169141[6] M. Fowler ， K. Scott ， UML Distilled ： Applying the Standard ObjectModeling Language，Addison-Wesley，1997.[7] N. Francez，Program Verification，Addison Wesley，1992年。[8] 急诊室Gansner，S.C.陈文，一个开放的图形可视化系统及其在软件工程中的应用，软件[9] R. Gerth，D. Peled，M.Y. Vardi，P. Wolper，线性时序逻辑的简单在线自动验证，PSTV 95，协议规范测试和验证，3[10] P. Godefroid，Model checking for programming languages using Verisoft，POPL 1997，174[11] G.计算机协议的设计和验证，Prentice Hall。[12] E. Gunter ， D. Peled ， 路 径 探 索 工 具 ， TACAS 1999 ， LNCS 1579 ，Springer，405[13] E. Gunter，D.张文，并行系统的时间调试，2002，LNCS 2280，Springer，431-444。[14] J. C. King，Symbolic execution and program testing，Communication of theACM，1976，385[15] ITU-T建议Z.120，消息序列图（MSC），1993年3月。[16] G.J. Myers，The Art of Software Testing，John Wiley and Sons，1979.[17] B. Selic ， G. Gullekson ， P. T. Ward ， Real-Time Object-OrientedModeling，Wiley，1993。[18] N. Sharygina，D. Peled，软件可靠性的组合测试和验证方法，FME 2001，LNCS 2021，611[19] A. Pnueli，程序的时序逻辑，第18届IEEE计算机科学基础研讨会，1977年，46