理论计算机科学电子笔记144（2006）27-44www.elsevier.com/locate/entcs开源模型检查Radu Grosu1计算机科学系美国纽约州立大学石溪分校X. Huang，S. Jain和S.A. 斯莫尔卡2计算机科学系美国纽约州立大学石溪分校摘要我们提出了GMC2，GCC的软件模型检查器，从自由软件基金会（FSF）的开源编译器GMC2是SUNYStony Brook正在开发的GCC的GMC静态分析和模型检查工具套件的一部分，可以被视为蒙特卡洛模型检查对并发过程编程语言设置的扩展。蒙特卡罗模型检验是一种新发展起来的技术，它利用几何随机变量理论，本文提出了一种LTL模型检验的随机化算法，该算法是基于LTL模型检验的一种新算法，它是基于LTL模型检验的一种新算法。为了处理C/C++等过程语言中固有的函数调用/返回机制，GMC2中实现的检查针对下推自动机模型进行了优化。我们的实验结果表明，这种方法产生了一个有效的和可扩展的软件模型检查GCC。保留字：GCC，Gimple-Tree，蒙特卡罗模型检验1介绍在过去的15年里，GCC已经从一个普通的C编译器发展成为一个成熟的多语言编译器，可以为30多个目标体系结构生成代码GCC现在处理的编程语言集1电子邮件：grosu@cs.sunysb.edu2 电子邮件：{xhuang，sumit，sas}@ cs.sunysb.edu1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.01.00328R. Grosu等人/理论计算机科学电子笔记144（2006）27包括C、C++、Fortran、Java和Ada。这种语言和架构的多样性使GCC成为当前使用的最流行的编译器之一传统上，GCC在应用任何优化之前将源代码直接翻译为RTL（寄存器这不可避免地使优化作为低级别执行为了弥补这种情况，GCC的Tree-SSA分支[19]导致GCC增加了两种新的中间语言：GENERIC，它为抽象语法树分析和优化提供了一个公共基础设施;GIMPLE三地址代码，它为CFG（控制流图）分析和优化提供了一个公共基础设施。GENERIC和GIMPLE及其相关的API使Tree-SSA不仅适合作为高级代码优化技术的开发平台，而且适合作为新的静态分析工具，适用于GCC开源社区对Tree-SSA分支的接受，在过去的一年中，导致它与Release Version3.5中的主线合并。在本文中，我们描述了一个软件模型检查器的GCC，我们已经设计和实现在树SSA级别。我们的模型检查器，我们称之为GMC2，用于基于GCC的模型检查，是Monte Carlo模型检查技术[8]的扩展，用于并发过程编程语言的设置。Monte Carlo模型检验是近年来发展起来的一种新技术，它利用几何随机变量理论、统计概率检验和随机抽样方法，实现了LTL模型检验的单边误差、随机化算法为了处理C/C++等过程语言中固有的函数调用/返回机制，GMC2中实现的Monte Carlo模型检查版本针对下推自动机模型进行了优化。GMC2的核心是一个GIMPLE CFG解释器，它使用Tree-SSA语句迭代器succ、tsucc和fsucc遍历CFG，根据其语义解释遇到的每个状态。特别感兴趣的是处理过程创建和同步语句的方式，其在需要上下文切换时强制返回，以及函数调用和返回语句，其在散列表GMC2上引入用于套索检测的分层结构。GMC2和interpret是我们为GCC的Tree-SSA级别开发的GMC分析和验证工具套件的一部分，其中还包括一个过程内切片器和一个符号执行R. Grosu等人/理论计算机科学电子笔记144（2006）2729发动机为GIMPLE CFGs。该工具套件旨在为基于GCC的静态分析和模型检查提供一个开源框架。本文的主要贡献可概括如下。• 由于GMC2是在Tree-SSA级别上实现的，因此它同时是GCC的6种输入语言和30多种目标体系结构的软件模型检查器• GMC2是一个开源的模型检查器：它集成到GCC中，使得它可以被开源社区方便地广泛使用、评论和扩展• GMC2在并发过程编程语言的设置中实现了Monte Carlo模型检查技术[8]。因此，在GMC2中实现的Monte Carlo模型检查版本针对下推自动机模型进行了优化。• 我们的实验结果表明，蒙特卡罗方法产生了一个有效的和可扩展的软件模型检查GCC。本文的其余部分沿着以下思路展开第2节考虑蒙特卡罗模型检验技术第3节提供了GCC编译过程的概述第4节介绍了GMC2，我们的软件模型检查GCC，而第5节总结了我们的实验结果。第6节讨论相关工作。第7节是我们的结论和未来工作的方向GMC2模型检查器可从[21]获得。2蒙特卡罗模型检验MONTECARLOMODELCHECKING[8]在一个Bu¨Chi自动机（BA）中实现了一个随机化的套索随机化算法，用于LTL模型检测.在本节中，我们将概述此技术。在第4节中，我们将如何在软件模型检测的背景下将该技术扩展到层次的Buüchi自动机（HBA）Buéch i automataa.ABuéchiautommatonA=（A，Q，Q0，δ， F）是一个五元组，其中：A是一个有限的输入字母表;Q是一个有限的状态集;Q0<$Q是初始状态集;δ<$Q×<$×Q是跃迁关系;F<$Q是接受态的集合。我们假设，不失一般性，BA的每个状态至少具有一个输出转换，即使该转换是自循环。序列σ=s0→a0s1→a1，. ，其中s0∈Q0且对所有i≥0，s→aisi+1∈δ称为A的无限游程，如果序列是无限且有限的我30R. Grosu等人/理论计算机科学电子笔记144（2006）27i1ai否则跑。一个无穷游程被称为接受，如果存在一个无穷指数集J<$N，使得对于所有i∈J，si∈F。我们说σ是最终周期的，如果存在i ≥ 0，l ≥ 1使得对所有j≥0，si+j=si+jmodl. 这意味着σ由有限个前缀s0→a0组成···a− ，然后是ai+l−1 S.i−1→i→···→i如果对所有0≤j，则称该循环为简单k l，si+jSi+ k;即，循环不会访问同一个节点两次。在下文中，我们将提到这样一个可达的简单循环作为套索，并说套索是接受的，如果它的简单循环包含一个接受状态。设S是一个并发系统，AS是BA编码的S利用表方法，可以构造一个接受这种相似性的布契自动机A<$aA[5]。TheLTL模型检验问题|因此，自然地根据空问题B=AS×A，这归结为在B中找到接受套索[22]。随机套索和假设检验。我们不是在B的整个状态空间中搜索接受套索，而是通过在B中执行随机游走，连续生成B的M个套索。遍历是均匀的，因为它们是通过对当前状态沿遍历的传出转换施加均匀分布而生成的。如果当前生成的套索是接受的，我们已经找到了空的反例，停止。为了确定我们需要生成的套索数量M，我们的目标是在置信度为1-δ且误差范围为δ的情况下回答以下问题：我们需要生成多少个独立的套索，直到其中一个被接收？ 答案是基于几何随机变量理论，统计假设检验设X是几何随机变量，由伯努利随机变量Z（定义如下）参数化，其值为1的概率为pZ，值为0的概率为qZ= 1−pZ。直觉上，pZ是B的任意套索接受的概率对于Z的N次独立试验，X的累积分布函数为：F（N）=Pr[X≤N]= 1−（1−pZ）N。要求F（N）= 1−δ得到：N= ln（δ）/ln（1−pZ）。假定pZ是我们想要确定的，我们假设此时pZ≥π。将pZ替换为n，得到M= ln（δ）/ln（1−n），它大于N，因此Pr[X≤M]≥Pr[X≤N] = 1−δ。总结：pZ≥ππPr[X≤M]≥ 1−δ其中M = ln（δ）/ln（1−π）（1）不等式1给出了我们需要达到R. Grosu等人/理论计算机科学电子笔记144（2006）27311234在假设pZ≥0的情况下，成功地获得了置信度δ。排除这种假设的标准方法是使用统计假设检验（参见[18]）。将零假设H0定义为pZ≥0的假设。重写不等式1关于H0，我们得到：Pr[X≤M|H0]≥1−δ（ 2）我们现在进行M次试验。如果没有找到反例，即，如果X> M，我们拒绝H0。这可能会引入第一类错误：即使我们没有找到反例，H0也可能为真然而，犯此错误的概率受δ限制;这在不等式3中示出，其通过取在不等式2中X≤M的补数：Pr[X>M]|H0]<δ（ 3）因为我们寻求获得单侧错误决策程序，所以我们在假设检验的应用中不考虑II型错误：一旦我们发现反例，我们就停止采样并决定（概率为1）一|= 0。蒙特卡洛模型检验算法。对于BAB，定义概率空间（P（L），Pr），其中L=La<$Ln是B的所有套索的集合，La和Ln分别是B套索的概率Pr[σ]σ=s0→a0an−1... →sn归纳定义如下：Pr[s0] =k如果|Q0|= k且Pr[s→a0an−1S ]=Pr[a0an−2an−1一J−10个...... → ns0→. →sn−1]·π[sn−1→sn]其中π[s→s] =m如果s→asJ∈δ且|δ（s）|=m。[8]中建立了t（P（L），Pr）是一个可靠的空间例2.1[套索的概率]考虑图1的BAB。它包含四个核，11，1244，1231和12344，其概率分别为1/2，1/4，1/8和1/8第1231章接受了Fig. 1. 示例套索概率空间。定义2.2[Lasso Bernoulli变量]定义了与布吕克希自动机B的概率空间（P（L），P_r）相关的随机变量Z公式如下：pZ=Pr[Z=1]=λn∈LnPr[λn].λa∈LaPr[λa]和qZ = Pr [Z] = 0]= 0−132R. Grosu等人/理论计算机科学电子笔记144（2006）27E xample2.3[La sosBernoullivariable e]F 或 图 1 中 的 Buéchi 自 动 机 B ，lassosBernoullivariable具有socialdprobabilitiespZ=1/8和qZ=7/8。在定义了Z、X和H0之后，我们现在准备好提出我们的MonteC算法，该算法用于布尔希自动机（称为MC2在[8]中。MC2由三个语句组成。第一个使用不等式1来确定M的值，给定参数δ和δ。第二个语句是一个for循环，它通过调用random lasso（rLasso）例程连续采样M个套索，如第4节所述。如果找到接受套索l，MC2判定为假并返回l作为反例。如果在M次试验中没有发现接受套索，MC2决定为真，并报告概率小于δ，pZ> δ。bool×classoMC2（BAB=（A，Q，Q0，δ，F），float0G，δ1）{M=lnδ/ln（1−G）;for（i =1;i≤ M; i++）if（rLasso（B）==（true，l））return（false，l）;returnn（true，nil）;/*Pr[X>M|H0]<δ*/;}定理2.4（[8]）设B 为 B 的 Bu′chi算 子 ， 且 算子为 δ和ε，若 MC2为假，则L（B ） /=δ. 在其 他情 况下 ， Pr[X>M|<当M = ln （δ）/ln （1 −n）且H0∈pZ≥ n时，H 0 ] δ。MC2在时间和空间上都非常高效。一个布希自动机B的递归直径是B中从一个初始状态开始的最长的无故障路径定理2.5（[8]）LetB是一个Bu¨chiau tom a t o m a，D是它的递归函数，M=ln（δ）/ln（1 −δ）.时间复杂度为O（n），空间复杂度为O（n）.在最坏的情况下，D是指数，|S| + |ϕ|因此MC2并没有改进典型模型检验器的空间复杂度。然而，在实践中，人们可以期望MC2的表现比这好得多3GCC概述图2的框图提供了从源输入文件到目标代码的GCC编译过程GCC的语言特定前端将源输入文件转换为（语言特定的）解析树。后端在很大程度上与语言无关，并处理代码优化和最终代码生成。传统上，GCC翻译R. Grosu等人/理论计算机科学电子笔记144（2006）2733C文件C++文件C解析器SSA/C++解析器...Java解析器解析泛化GenASTGimplify树GPLASTBldCFGGPLRstCMPRTL代码生成对象CFG代码代码Tree SSA框架前端后端图二、GCC编译过程的框图源代码直接到RTL（寄存器传输级），一个非常低级的中间语言，在应用任何优化。这不可避免地使优化作为低级别执行，因为更高级别的语义信息，如数据类型，结构和字段在翻译过程中丢失。树-SSA。为了弥补这种情况，GCC的 Tree-SSA分支[19]增加了两种新的中间语言（IL）：GENERIC和GIMPLE[16]。加上它们的API，这些IL使Tree-SSA不仅适合作为高级代码优化技术的开发平台，而且适合作为新的静态分析工具，适用于GCC开源社区对Tree-SSA的接受，在过去的一年中，导致它在Release Version3.5中与主线合并int main（）函数{1.intmain {int a，b，c;2.int a，b，c;a= 5;3.intT1，T2，T3，T4;b = a +10;4.a= 5;（a，b）;=>5.b = a +10;如果（a>b+c）6.int foo（a，b）;c=b++/a+（b*a）;7.T2=b+ T1;bits（a，b，c）;8.如果（a>T2）转到fi9.T3 = b/a;10.T4 = b *a;11.c = T2 + T312.b = b +1;13.f1：bar（a，b，c）;}图三. 示例C程序和相应的GIMPLE表示。GENERIC通过为特定语言前端生成的所有解析树结构GIMPLE是一个类C的三地址（3A）代码，它为CFG级（控制流图）分析和优化提供了一个公共的基础设施像往常一样，复杂的表达式（可能带有副作用）通过引入新的临时变量被分解为简单的3A语句类似地，复杂的控制语句通过引入新的标签被分解为简单的3A在语法上，GIMPLE是GENERIC的一个子集。每个GIMPLE树用于构造GIMPLE-CFG，其本身随后可以被转换为静态单-34R. Grosu等人/理论计算机科学电子笔记144（2006）27a b c T1 T2 T3 T4intintintintintintintFUNCTION_DECL条目一a = 5;b = a +10;T1 = foo（a，b）; T2 = b +T1;如果（a>T2），则转到B;CECE：化合物有效期=CE一5=CEBT3 = b / a;T4 = b * a; c= T3 + T4;b = b +1;真塔尔塞B+CE=Cbar（a，b，c）;一=如果10T1呼叫ExpT2+B>出口GIMPLE树fooa bb T1 a T2分配（SSA）形式。图3显示了一个C程序及其相应的GIMPLE表示，它保留了源代码级别的信息，如数据类型和过程调用。虽然在示例中没有显示，但GIMPLE类型还包括指针和结构。一旦一个函数被转换成GIMPLE形式，Tree-SSA框架就会构建其相关的控制流程图。CFG中的每个节点都链接到一个基本块（非分支指令序列），表示为GIMPLE AST。CFG转换对应于（条件）goto指令。例如，图3的GIMPLE程序的CFG如图4所示。见图4。 控制流程图为例的C程序。Tree-SSA API提供了操作和遍历CFG、其关联的AST及其变量列表的函数。例如，succ返回非分支语句的直接后继语句的地址，tsucc和fsucc返回分支语句的直接true和false后继语句的地址类似地，如果a是CFG中的变量，则其类型属性a。type也是一个GIMPLE AST，包含各种信息，如类型名称、大小和对齐方式。Tree-SSA API还提供了基本的数据流、控制流、别名和可达性分析例程。4蒙特卡罗软件模型检验我们已经实现了一个软件模型检查GCC的基础上的通用蒙特卡罗模型检查算法的第2节。我们的模型检查器GMC2适用于任何用GCC支持的过程语言（如C）编写的程序。将此程序称为要验证的目标程序。GMC2还需要一个过程或函数作为输入，称之为属性函数，表示感兴趣的LTL属性目标程序可以包含类似于Verisoft模型支持的并发原语R. Grosu等人/理论计算机科学电子笔记144（2006）2735=checker [6].在安全属性的情况下，调用属性函数来检查目标程序中的属性冲突 在活性属性的情况下，属性函数被调用来检查目标程序的接受状态是否被无限频繁地访问，将目标程序视为一个布希自动机的成功表示。GMC2在Tree-SSA级别上运行，并假设目标程序和属性函数已经编译成CFG。设P是对应于目标程序的CFG的数组，每个函数对应一个，设P是属性函数的CFGGMC2的核心是一个CFG解释器，它使用Tree-SSA的语句迭代器遍历P中的CFG，这使得GMC2可以在内存上生成目标程序的随机套索。4.1主程序由于空间的考虑，我们限制我们的讨论，以处理的安全性。给定目标C程序的CFGs的数组P，编码安全属性的C函数的CFGs，以及参数δ和δ，GMC2连续生成至多ln（δ）/ln（1−δ）个P的随机套索;参见第2节。在生成套索时，将调用classo来检查在新进入程序状态。 如果是，则GMC2停止并返回通向违反状态的反例路径。如果所有抽样执行的所有状态满足条件，GMC2停止并以大于1−δ的置信度报告，拒绝H0。 pZ≥0.GMC2的核心是用于生成随机套索的rLasso例程通过解释它们的C语句（可能是并发的）并检查是否违反属性，对P中的CFG4.2rLassoRandom-Lasso例程为了检测（全局）套索，每次发生上下文切换时，将（并发）程序状态存储在哈希表ht这是为了提高效率：另一种效率较低的方法是在每个语句执行后存储程序状态。为了确保这种方法的合理性，我们假设上下文切换之间的时间是有限的。bool× lasso rLasso（）/* global cfg array P，cfgarray */{hashTblht=0;readylisttready=0;bool×state（f，s）=rInit（）;while（s/∈ ht）{insert（s）;if（f）return（true，lasso（s））;（f，s）= rNext（s）;}return（false，lasso（ht））;}36R. Grosu等人/理论计算机科学电子笔记144（2006）27哈希表。ht哈希表被优化，以便共享全局状态之间的公共信息。它也是分层的，因为属于被调用者的所有状态都相互链接，因此当被调用者返回时，它们可以很容易地从ht中删除。上面给出了rLasso例程的伪代码。第一行将ht和ready设置为空，并通过调用例程rInit来消除违规标记f和当前状态变量s。while循环搜索（违规）套索。如果当前状态s不在ht中，则它是一个新状态并被插入ht中。如果它是一个同样有效的，则通过为真来发信号，找到该无效套索，将其与对应的标签一起返回到GMC2。否则，通过调用rNext生成另一个随机next状态。4.3删除rInit和rNext给定一组类型化变量V，V的赋值（或环境）是V中变量到其类型正确值的映射。如果Γ和ΓJ是列表，并且σ是列表元素，我们分别将通过连接Γ和ΓJ、将σ附加到Γ以及取Γ的其余部分而获得的列表写为concat（Γ， ΓJ）、append（Γ，σ）和rest（Γ），并且将Γ的第i个元素写为Γ（i）如果是一个堆栈，φ是一个堆栈元素，那么我们写push（push，φ），pop（pop）和push.φ分别用于将φ推到堆栈上，弹出堆栈，以及堆栈上最顶层的如果s是一个语句，即，一个CFG的AST，然后是s。a是s的孩子。程序状态。并发C程序的状态f =（χ，Γ）由共享变量（通道和信号量）的赋值χ和进程状态列表Γ组成，每个进程对应一该列表按进程创建的顺序排序一个进程的状态σ=（κ，δ）有两个组成部分：控制状态κ和数据状态δ。控制状态κ=（γ，ν）由函数名γ和γ中的语句号ν组成。 数据状态δ=（π，β，β）由堆π、全局变量β的赋值和帧栈β组成。每个框架φ =（κ，ρ）包含一个返回给调用方CFG的控制状态κ和一个被调用方CFG的局部变量的赋值ρ。常规rInit。P的执行开始于随机状态，定义如下。χ0中的所有通道都是空的，所有信号量都是0。进程状态列表Γ0只包含根进程的状态σ0根过程的控制状态κ0在γ0中主要起P的作用，在ν0中主要起0的作用。R. Grosu等人/理论计算机科学电子笔记144（2006）2737bool× prgState rInit（）/* global cfg array P，cfgarray */{sharedStateχ=χ0;proc Statesr=0;frameStackr=0;cfgNmγ=main;stmNov=0;controlStateκ=（γ，v）;lclEnvρ=ρ0;对于一个ll（x∈dom（P[γ].param））ρ[x]=random（P[γ].param.type）;frameφ=（trap，ρ）;push（push，φ）;dataStateδ=（π0，β0，π）;proc Stateσ=（κ，δ）;append（Γ，σ）;prg StateΣ=（χ，Γ）;如果eval（）return（true，false），则返回（false， false）;}根进程的数据状态δ0由空堆π0、全局变量的值β0和栈帧φ0组成，栈帧φ0只有主进程的帧φ0被推入。这个框架有一个预定义的返回控制状态陷阱（例如停止点）和局部变量的赋值ρ0ρ0中形式参数的取值是在其相应的范围内随机选择的函数eval计算当前状态下的CFG并返回其值。bool× prgState rNext（prgState s）{/*全局cfg数组P，hashTbl h，CFG队列，就绪列表就绪 */int i= random（|准备|int[i] nums = nums;return translate（s，nxt）;}例行程序。例程rNext随机选择一个就绪进程，并通过调用例程interpret对其进行解释，如下所述。 当interpret到达并发语句时，它重新获得控制权，这需要上下文切换。4.4例行解释例程解释器使用语句迭代器succ、tsucc和fsucc遍历P中的CFG，并根据语句的语义解释每个语句特别感兴趣的是进程创建和同步语句，它们在需要上下文切换时强制返回，以及函数调用和返回语句，它们在哈希表上引入层次结构由于interpret在返回之前可能会生成多个状态，因此它必须检查属性numbers是否在所有状态中都为true。要检查的属性也可以插入到程序中，如assert（p）语句。然后解释器检查谓词p在当前状态下是否为真，如果不是，则返回一个违例下面给出了interpret的伪代码。它的主体是一个无限循环，根据当前CFGP[γ]中当前语句ν的类型，它承担定义语句语义的操作由于空间的限制，我们考虑一个有代表性的语句类型子集，其中不包括堆和指针操作语句。38R. Grosu等人/理论计算机科学电子笔记144（2006）27inti（inti，int j）{/* global cfg array P，hashTblht，cfgarray，readylistready*/channel sx= 0. x;proc Statesr= x。r;proc Stateσ=r[i];而（true）{cfgNmγ= σ。κ。γ;stmtN〇v= σ。κ。v;frameStack= σ。δ。globalEnvβ= σ。δ。β;switch（P[γ][ν].type）of if： /* if e gotot */{ν =（eval（P[γ][ν].exp））？t s u c c （P[γ][ν]）：fsucc（P[γ][ν]）;}assert：/* assert（e）*/{如果（！eval（P[γ][ν].exp））return（false，false）;ν=succ（P[γ][ν]）;}分配：/* x = rhs */{如果（P[γ][ν].rhs.type==expr）{/*rhs==e*/v= succ（P[γ][v]）;（？ρ：β）[P[γ][ν].var]=eval（P[γ][ν].rhs）;}else if（P[γ][ν].rhs.fnc==toss）{/* rhs== toss（e）*/νintn = nums（nums）;（注：ρ：β）[P[γ][ν].var]=random（eval（P[γ][ν].rhs.exp））;}else if（P[γ][ν].rhs.fnc==fork）{/* rhs== fork（）*/v= succ（P[γ][v]）;（？p：β）[P[γ][ν].var]= 0;append（Γ，（（γ，ν），（π，β，π）;（π. ρ：β）[P[γ][ν].var]=|Γ|-1;}else if（P[γ][v].rhs.fnc==recv）{/* rhs== recv（c）*/C= P[γ][ν].rhs.chnl;if（empty（x.c））{append（x.c.swait，i）; return（true，i）;}v= succ（P[γ][v]）;（？ρ：β）[P[γ][ν].var]=fst（χ.c.queue））;rest（χ.c.queue）;concat（ready，χ.c.swait）;χ.c.swait=0;}if（a） ==f（a）a=eval（P[γ][ν].rhs.act）;κ=（γ，ν）;γ = P[γ][ν].rhs.fnc）;ν = 0;push（push，（κ，ργ，0））;（push. ρ）[P[γ].fpar]=a;}return：/* return e */{e= eval（P[γ][ν].exp）;（γ，ν）=ε. publicint findDuplicate（intn）;publicintfindDuplicate（int n）;ρ：β）[P[γ][ν].var]=e;}send：/* send（c，e）*/{C= P[γ][ν].rhs.chnl;if（full（x.c））{append（x.c.rwait，i）; return（true，false）;}v= succ（P[γ][v]）; append（χ.c.queue，eval（P[γ][v].rhs.exp））;concat（ready，χ.c.rwait）;χ.c.rwait=numb;}σ=（（γ，ν），（π，β，π））;Γ[i]=σ;π=（χ，Γ）;如果（！return（true，false）;}}对于顺序的过程内语句组，我们讨论if和（简单）赋值的解释。前者计算当前状态下的谓词，并通过修改v分支到适当的位置。后者计算右侧表达式，并相应地更新左侧变量给出的位置上的相应局部环境β.ρ（在帧堆栈顶部的帧内）或全局环境β通过写作.ρ：β，我们意味着两个赋值都被考虑，并且.ρ优先于β;即，我们首先在局部估值中搜索变量。R. Grosu等人/理论计算机科学电子笔记144（2006）2739提出的建模和验证语句是toss和assert。对于toss，解释器首先评估参数表达式以获得值v，然后它随机生成范围[0，v]内的数字。将得到的数字赋给左侧变量给出的位置，以.ρ或β表示。对于assert，解释器检查谓词在当前状态下是否为true。如果不是，则返回false和false。否则，它通过更新ν继续下一个语句。过程间语句是call和return。对于调用，在帧栈的顶部分配新的帧φ=（κ，ρ）;κ是当前控制状态;ρ具有相应地由ργ，0初始化的目标函数γ的局部变量和在当前控制状态状态然后，通过相应地更新γ和ν，控制被移动到被调用方对于返回，解释器执行以下操作。首先，它在一个临时变量中计算返回表达式。然后，它从帧堆栈中恢复控件状态，弹出帧堆栈并从哈希表中擦除与被调用方对应的所有状态。最后，它将临时变量赋值给控制状态所指向的语句的变量所给定的位置，或者在β中，或者在ρ中。到目前为止考虑的并发原语包括进程创建、通道和信号量。为了简单起见，我们只讨论fork，send和recv。其他人也以类似的方式对待。fork语句是通过在Γ中创建一个新的进程（状态）来处理的，除了分配给fork赋值语句左侧变量的值之外，该进程与当前进程相同这对于子进程是零，并且对于父进程是新进程的Γ中的索引send语句按预期处理。如果通道已满，则将进程放入相应通道的发送等待队列中，并将控制返回给rNext。否则，将计算消息表达式并将其追加到通道。此外，在通道的接收队列中等待的进程通过将其移动到就绪列表而被唤醒recv原语的处理方式类似。5实验结果为了评估GMC2的性能和可伸缩性，我们将其与朗讯科技[6]的流行软件模型检查器VeriSoft进行了比较，使用了两个C基准：用餐哲学家和Needham-Schroeder。VeriSoft和GMC2被给予相同的C源文件作为输入，每个源文件都可以从[21]下载。我们还在TCAS基准上运行了GMC2所有的GMC2实验都是在Athlon 2600+ MHz处理器上进行的，该处理器具有1GB RAM，运行Linux2.6.5。40R. Grosu等人/理论计算机科学电子笔记144（2006）27哲学家用餐对于这个经典的同步问题，我们使用了一个错误的对称但公平的变体，其中哲学家的数量从4到16不等。我们检查的安全属性是死锁自由度。我们的实验结果在表1中给出。列标题的含义如下：phi。是哲学家的数量; time是执行时间，单位为min：secs; ce.len是找到的反例的长度; states是VeriSoft在发现错误之前访问的状态数; transitions是VeriSoft遍历的transition数。VeriSoft实验在运行SunOS 5.6的Sun Sparc Ultra-5.10服务器上进行。我们的经验表明，Athlon/Linux环境的执行速度大约是Sparc/SunOS环境的3.4倍GMC2VeriSoftφ的时间样品ce.len.时间国过渡40：00.072120：00.61163760：00.114120：16.60773117180：00.7811202：57.295431844910时间02：173124十点四十一分179083143312时间：0：04.822427>2小时N/AN/A14时间06：222244>2小时N/AN/A160：11.561432>2小时N/AN/A表1对称和公平C实现的死锁自由。李约瑟-施罗德协议这种经典的公钥协议在双方进行交易之前在1995年，Lowe首先报告了协议中的一个错误[14]，展示了一个涉及六个消息交换的攻击假设A是发起者，B是响应者，I是入侵者。那么攻击如下：（i）A向I发送一个随机数。（ii）I将相同的随机数发送给B。(iii)B将上述接收到的随机数及其新的随机数发送给I。（iv）我将上述收到的信息发送给A。(v)A验证I的真实性，并将消息中的第二个随机数发送回I。（vi ）I 将 这个 随机 数 发送 回 B ，B 现 在也 验证 了 I。 我们 在从 PatriceGodefroid获得的协议的C实现中检查了上述攻击的存在，我们非常感谢他。GMC2在检查了10，682，639个套索后，在6小时37分钟内发现了它在[7]中使用了相同的示例和实现来评估一种新的遗传算法。发现3个错误所用的时间为2小时33分钟，在此基准测试中优于GMC2他们还试图R. Grosu等人/理论计算机科学电子笔记144（2006）2741在这个C程序上的穷举和随机搜索算法，这两种算法都不能在8小时内找到错误他们的实验是在Pentium III 700 MHz处理器和256 MB RAM上进行的不幸的是，VeriSoft的基因版本并不公开，我们无法在自己的机器上重现这一结果。其优越的性能可以通过协议实现的顺序性质来解释，它本质上只执行一轮反应式系统。在这一轮中，系统要么死锁，要么产生一个反例，要么行为正确。因此，在这种情况下，套索搜索似乎不如应用遗传算法有用TCAS美国所有商用飞机上都使用交通警报和防撞系统（TCAS）它持续监视雷达信息，以感知邻近飞机是否会因过于接近而成为威胁。这种飞机被称为“入侵者”，正在进入保护区。在这种情况下，TCAS会发出一个交通咨询（TA），并估计两架飞机到达最近进近点的剩余时间。假设受控飞机保持其当前轨迹，这种估计用于计算两架飞机之间的垂直间隔根据所获得的结果，TCAS发出决议咨询（RA），建议飞行员爬升或下降。财产规则GMC2发现的漏洞时间样品安全咨询选择1没有0.2312782是的0.03147最佳咨询选择1没有0.2512782是的0.04206避免不必要的交叉1是的0.01362是的0.03180无交叉咨询选择1是的0.01272是的0.018最优咨询选择1没有0.2312782是的0.06217表2TCAS的GMC2运行时间。我们已根据[3]中的规范每个属性通过检查两个规则的满足性来验证这些规则的细节，值和属性的初始条件，可以在[3]中找到。我们的实验结果如表2所示，其中42R. Grosu等人/理论计算机科学电子笔记144（2006）27列标题的含义如下：属性名称;相应的规则编号; GMC2是否发现反例的指示;发现反例或达到预定数量的样本的时间使用（以秒为单位）;如果发现反例，则最后一列给出到该点采集的样本数量;否则为待采集的预定数量的样本：1，278对应于δ = 0。1，则n = 1。8 ×10−3。6相关工作随着模型检测、静态分析和定理证明等技术的发展，软件模型检测已经成为一个热门的研究领域给定一个软件系统S，软件模型检查器要么直接在S上工作，要么从S中提取一个模型M，然后对M应用更传统的模型检查技术。与GMC2最密切相关的软件模型检查器是那些用于并发过程语言的，例如C/C++，包括VeriSoft[6]，Spin [11]，Blast [10]，Magic [2]和C Wolf [4]。在VeriSoft的情况下，开发了一种基于遗传算法的随机搜索策略，以引导状态空间搜索到错误状态[7]。GMC2和VeriSoft的相对性能比较在第5节中给出。Berkeley的Cooperative Bug Isolation（CBI）项目在许多大型开源项目上执行编译时插装，并分发产生的二进制文件[13]。然后收集有关程序成功或失败的次数的随后的统计分析用于隔离错误的代码段。相比之下，GMC2是一个嵌入在开源GCC编译器的Tree-SSA级别的模型检查器其他研究人员已经开发了用于软件验证和分析的随机方法。随机解释的程序分析技术背后的关键思想[9]是以人为的方式对一些随机输入执行代码片段，其中包括对程序中的运算符进行随机线性条件的两个分支在每次运行时执行，并且在接合点处，执行接合状态的随机随机组合在等式条件的分支中，数据值在等式上进行调整，以反映保护的布尔表达式在[17]中，蒙特卡洛和抽象解释技术被用来分析程序，其输入被分为两类：根据某些固定的概率分布而存在的程序和被认为是不确定的程序。R. Grosu等人/理论计算机科学电子笔记144（2006）27437结论本文介绍了一个基于Monte Carlo模型检测技术的GCC软件模型检测器GMC2。由于是在Tree-SSA级别实现的，GMC2同时是GCCGMC2也是一个开源的模型检查器，因此很容易被开源社区广泛使用，评论和扩展。我们的方法的一个重要优势涉及GMC2中点的处理。基本上，解释指针操作要比静态分析它们容易得多。作为正在进行的和未来的工作，我们正在创建一个软件模型检查分支的GCC的GMC工具套件的公共分发的过程中。此外，我们正在开发自动抽象[1]和插值技术[15]来处理具有无限域变量的程序目前，我们正在手动应用一种形式的有界范围抽象[12]，例如，在TCAS基准上
我的内容管理
展开
