文件标题：并发Java程序中的错误检测

理论计算机科学电子笔记144（2006）45-58www.elsevier.com/locate/entcs并发Java程序中的错误检测格雷厄姆·休斯1加州大学伯克利分校Santa Barbara，CA 93106，美国斯雷兰加山口Rajan，Tom Sidle，Keith Swenson汤姆·西德勒基思·斯文森2，3，4Fujitsu Laboratories ofAmerica美国加利福尼亚州森尼韦尔摘要多线程程序中的并发性在软件验证和测试中引入了额外的复杂性我们提出了一个案例研究中，一个专门的模型检查器被用来发现并发错误在一个大的预先存在的代码库。结果揭示了导致数据损坏错误的竞争条件，使用传统的测试和QA方法检测这些错误将是非常昂贵的我们描述了我们的方法，并强调部分的方法，可以自动化。关键词：并发，模型检查，软件验证和确认1引言随着软件项目变得越来越大和复杂，检测其中错误的技术变得越来越重要。并发错误被认为是特别令人烦恼的。最常用的检测1电子邮件地址：graham@cs.ucsb.edu2电子邮件地址：sree@us.fujitsu.com3电子邮件地址：tsidle@us.fujitsu.com4电子邮件地址：kswenson@us.fujitsu.com1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.01.00446G. Hughes等人/理论计算机科学电子笔记144（2006）45当然，大型商业系统中的并发错误是测试; 2然而，创建好的测试用例是非常困难的，并且并发错误的测试可能是非常令人沮丧的。我们提出了一个案例研究中，一个专门的模型检查器被用来发现并发错误在一个大的预先存在的代码库。我们还讨论了如何减少使这成为可能所需的劳动力。在本文中，我们讨论了在第2节中将模型检查器应用于代码库的一般问题，在第3节中我们检查的代码库，在第4节和第5节中我们通过将模型检查应用于该代码库而获得的结果，以及对第6节中我们使用的方法的反思。在我们之前，其他人已经将模型检查器应用到程序中。在[13]中，Yang，Twohey等人将CMC模型检查器[7]应用于Linux内核，特别是三个文件系统，并在文件系统中发现了许多可能导致数据损坏或丢失的错误。在[1]中，Ball，Majumdar等人提出了一种在C程序上执行谓词抽象的方法，SLAM工具包的一部分，目的是对产生的布尔程序进行模型检查;他们提到在NT设备驱动程序和其他程序中使用这种技术。Java Path团队被要求在NASA的远程代理系统中我们的工作在以下几个方面不同于这些工作。首先，我们在一个大型并发程序上工作，寻找并发错误。Yang，Twohey等人的Linux系统主要关注崩溃恢复。虽然该引擎模拟了硬件级别的并发性，例如使用写缓冲器重新排序，但它并没有寻找死锁、竞争等。Ball，Majumdar et al.的SLAM工具包不考虑并发程序。我们与远程代理系统的区别在于运行的系统的大小，并且因为我们尽可能多地保留了原始系统;远程代理被重新编码为Java，以便可以应用分析。2模型检查程序作为一种技术，将模型检验应用于程序中值得简要说明。模型检查最初应用于硬件验证，然后应用于程序或协议行为的小型，自包含，故意简化的模型。在这里，每一个可行的状态都将被检查--无论是先验的，还是借助于数学形式主义，允许一次检查多个状态--并且关于模型行为的各种属性都可以被验证。最近，直接在程序本身而不是提取的工件上运行模型检查器已经变得可行;G. Hughes等人/理论计算机科学电子笔记144（2006）4547Verisoft [2]、CMC [7]和Java Pathview [9]是设计用于在代码上运行的模型检查器的示例在我们的工作中，我们使用了Java Path，我们经常将其名称称为JPF。作为一个实用的工具，JPF可以被看作是一个不确定的Java虚拟机。所有的控制不确定性都必须显式化，但并发不确定性会自动得到处理。因此，虽然JPF在实际模型检查问题上不如SPIN [4JPF处理几乎所有的纯Java代码;例外包括文件输入/输出或网络传输。JPF也不能处理本机方法，尽管用户可以为模拟提供纯Java版本。JPF模拟程序能力中的这些漏洞可以使用相关类的简化版本来修补。这种替换可以在不修改正在检查的代码的情况下完成，这是有用的。我们发现JPF很有用，因为它能够运行我们的目标软件，这是用Java编写的。因为我们正在研究并发错误，所以它尝试并发代码的每个序列化的能力非常有吸引力。如果我们正确地运行代码，那么任何死锁、竞争或其他错误都应该被注意到，即使它们很难被发现。3代码库概述我们将第2节中讨论的技术应用于大型客户机服务器代码库的开发树。该系统具有许多不同的用户界面，必须与几个第三方数据库产品进行通信。用户界面可以实现为基于Java的胖客户端、Java小程序或浏览器中的网页。浏览器由Web层提供服务，Web层由运行在Web服务器中的JSP和servlet组件组成。主流程逻辑和分析引擎位于第三层。第四层包含底层存储库，如数据库、目录和文档管理，以及使用各种机制与其他系统的连接。该结构如图1所示。各个模块通过Java RMI进行通信[11]。我们检查的系统版本包括超过1000个类和470，000行Java代码。由于它的模块化设计，以及模块之间的接口通过RMI接口很好地描述的事实，48G. Hughes等人/理论计算机科学电子笔记144（2006）45Fig. 1.代码库结构设计我们使用这些划分来控制我们在模型检查时必须检查的软件数量RMI的使用还有一个额外的效果。Sun的Java开发工具包附带的RMI版本（代码库使用的版本）是隐式并发的默认的RMI服务器为每个客户端创建一个新线程。任何基于它的软件都必须能够处理这种并发性的能力。同样，在这种情况下，并发性也是为了可伸缩性而开发的。这种并发性可能会在开发过程中产生问题;调试复杂的并发代码是非常困难的，并且重新生成死锁和竞争条件可能非常复杂。即使在许多情况下只需要少数几个线程就可以引发问题，这也是正确的。4应用模型检查因此，分析阶段已经准备好了;我们有一个大型并发程序，解决并发错误有一定的难度，还有一个工具应该很好 可靠地重现这些并发错误。当我们开始分析时，开发团队告诉我们，有一个在压力测试中很少出现的死锁，我们可以看看吗？在此分析之前，我们都没有见过或使用过该系统。项目的规模令人生畏，而且由于状态爆炸问题，我们当时不相信我们能够分析代码库的实质部分我们认为死锁可能与数据库接口代码有关。由于代码库的结构，数据库接口运行在RMI服务器之后，与主代码完全分离马绍尔群岛共和国G. Hughes等人/理论计算机科学电子笔记144（2006）4549接口似乎是一个逻辑起点，我们手动编写了启动数据库服务器并准备好服务请求所需的最小环境。这个环境是通过一个迭代过程开发的：数据库服务器将运行，它将立即失败（在我们的例子中，经常是由于一些未设置的全局变量），环境将相应地修改当时，我们认为这将是一个很好的方法来探索系统，并找到它的哪些部分，我们必须手工模拟，以避免状态爆炸。有必要替换一些Java系统类，以便在JPF下启动数据库服务器。这些课程包括：• RMI包必须替换为不会尝试连接到网络的包。• 系统日志机制使用的Date类被修改为始终给出完全相同的时间。这避免了程序状态的扩散，这些状态除了时间戳之外完全相同• 本地化类被认为是超级复杂的，因此被淘汰了。• JDBC和相关的数据库访问类需要被替换为一个对代码库足够高的版本，以便代码可以正确工作，但不存储任何不必要的数据。我们发现这个阶段需要投入最多的时间，部分原因是我们不熟悉代码库。4.1数据库并发环境生成完成后，我们开始使用RMI接口驱动数据库服务器.标称方案的相关部分如下：(i) 客户端代码使用RMI获取子系统(ii) 客户端 代码 电话 getConnection（）on 的 DbAdapter， 得到一个DbConnection。(iii) 客户端代码通过DbConnection使用数据库。(iv) 客户端代码释放连接;返回步骤2。该协议在图2中被写成状态机。这个协议，正如所写的那样，对于实际使用来说太简单了。创建DbConnection对象的速度非常慢，数据库服务器试图保持一个已分配但未使用的连接池。这个池子带来了另一个问题.如果客户端由于任何原因没有执行步骤4-客户端50G. Hughes等人/理论计算机科学电子笔记144（2006）45图二. 在没有网络断开连接的情况图三. 假定已实现崩溃、网络错误、挂起的客户端-它正在使用的DbConnection对象将永远不会返回到池中这将导致资源泄漏。为了解决这个问题，数据库服务器在步骤2中检查它的每个连接，以确定原始客户端是否仍然存在。如果服务器确定客户端已经死亡，那么它将向新客户端分发已经分配的连接。代码库声称要实现的修改后的协议如图3所示。如果网络连接实际上已经断开，则此行为或多或少是正确的。然而，用于确定客户端是否死亡的方法是查看连接是否是五分钟前的。如果由于任何原因-数据库行锁定，数据库备份，网络延迟，重负载，客户端上的长时间计算-客户端需要超过五分钟来处理事务，它就会冒着它的DbConnection将被提供给其他客户端的风险。图4描述了所实施的方案。G. Hughes等人/理论计算机科学电子笔记144（2006）4551见图4。 实际实施的如果一个客户端超时，然后它的连接被放弃，那么两个客户端的事务可能会交叉。此外，JDBC标准并不要求java.sql.Connection对象是线程安全的。这对线程安全和数据库正确性都有灾难性的后果此错误仅在存在并发行为的情况下才会出现，虽然它可以在只有两个客户端的情况下出现，但客户端的合法事务不太可能使用传统的测试方法可靠地捕捉这样的故障是很困难的。为了检测这个问题，我们创建了一个存根客户端，它获取一个名为getConnection的DbAdapter，使用一段时间，然后释放连接。我们实例化了几个这样的客户机，以并发地访问服务器。我们没有等待5分钟超时，而是用调用JPF的randomBool函数来替换超时代码因此，我们实现了任何客户端可以在任何时候断开连接的所有情况的覆盖。最后，我们插入断言来检查是否任何两个客户端都可以获得相同的DbConnection。JPF在几分钟内证明了这个错误是可能的，考虑到正在运行的代码量，这是一个令人惊讶的结果。 我们预料到了一场国家爆炸，但没有观察到在这种情况下。52G. Hughes等人/理论计算机科学电子笔记144（2006）45为了解决这个问题，我们建议数据库团队使用更确定的方法来确定客户端是否已死亡，或者重新构建协议以避免这种行为。4.2缓存验证在分析了这部分代码之后，应开发团队的要求，我们开始分析对象缓存，其目标是确保尽可能少地发生数据库访问。这段代码包含许多简单的并发错误和糟糕的设计决策;一个简单的静态检查器，如FindBugs [5]，可以检测到其中的大部分或全部。然而，其中是否有任何一种可能导致数据损坏的问题仍然悬而未决。因此，我们使用JPF运行系统，使用多个线程处理不同的对象。在运行这个过程中，我们发现所有的线程都在尝试处理同一个数据库对象（对象#0）。困惑的是，我们花了一些时间试图确定我们的环境是如何出错的，相信系统不可能以这种方式行为不端毕竟，它已经运行了多年的测试用例和生产跟踪错误，我们发现当对象缓存从数据库中读取进程定义时，对象缓存将进程定义的唯一对象标识符存储在本地字段中。当创建新的过程定义时，标识符尚未确定。在过程定义被保存到数据库中，并因此被分配了一个唯一的对象标识符之后，对象缓存应该更新其对象标识符的副本。相反，对象缓存将其副本设置为默认值0。这个bug几乎是在压力运行期间立即被发现的，但是测试显然没有被编写来捕捉这样的错误。如果我们没有发现几个线程从完全独立的进程定义开始，最终都以相同的进程定义结束，我们就不会发现它，这违反了缓存契约。我们将在第7节中进一步分析这种行为。5结果我们在4.1节中提到了证明数据库适配器通信协议中存在一个细微的错误，在4.2节中也提到了并发缓存中存在错误的证明，但没有给出结果;我们在这里这样使用通信协议，修复错误的过程非常困难，我们无法提供验证时间;然而，错误的识别在108秒内完成有关该运行的进一步数据是G. Hughes等人/理论计算机科学电子笔记144（2006）4553在表1中可用。使用并发缓存，我们在56秒内发现了错误，表2中有进一步的数据。不幸的是，对固定但未调优的缓存的验证没有在合理的时间内完成。然而，通过手动切片和插入适当的同步来删除一些良性竞争，我们在21小时内实现了两个线程的验证;更多细节见表3。通过非常严格的同步-具体来说，缓存的每个公共方法都锁定了缓存类对象，确保所有缓存操作都是同步的-在16小时内实现了两个线程的同步验证，表4中有更多细节。受访国家4,710执行的过渡4,710执行的指令113,666最大堆栈深度4,509中间步骤45使用的存储器128.83 MBGC后使用的内存110.37 MB存储存储器0.0 B收集的物体2,186标记和扫描运行3,784执行时间108.404秒速度43 tr/s表1数据库适配器Bug6方法正如我们在第4节中简要讨论的那样，我们的方法如下：(i) 找一个不变量来检查。(ii) 尝试运行程序来检查它。(iii) 如果由于环境不太忠实于原始系统而发生故障，请提高环境的忠实性并返回到54G. Hughes等人/理论计算机科学电子笔记144（2006）45受访国家18,997执行的过渡35,776执行的指令206,759最大堆栈深度718中间步骤26使用的存储器22.62 MBGC后使用的内存14.56 MB存储存储器0.0 B收集的物体10,284标记和扫描运行30,160执行时间55.648秒速度642 tr/s表2并发缓存Bug步骤2.(iv) 如果系统运行的时间太长，那么找出是什么占用了所有的时间，并用具有更抽象行为的存根来替换它返回第2步。(v) 如果不变量被违反，检查以确保它可能发生在原始系统中，如果是这样，报告违反。如果不是，通过提高系统的可靠性来纠正问题，然后返回步骤2。(vi) 如果没有违反不变量，请检查以确保您的驱动系统足够忠实。如果是，报告成功。否则，相应地提高系统的可靠性并返回步骤2。这种方法不是一种算法，因为这些步骤不是机械的过程;正确的做法需要模型检查和系统的经验。此外，该方法是否会终止也值得怀疑。几乎所有的支出都花在了相当于产生环境的事情上，而不是检查本身。我们必须用存根替换的一些类要么是JPF限制的逻辑结果，例如RMI;要么是因为与第三方产品的链接，例如JDBC。对这个代码库的任何分析几乎都必须排除这两类中的类，因为JPF当前没有也不能直接处理网络代码。G. Hughes等人/理论计算机科学电子笔记144（2006）4555受访国家19,941,239执行的过渡56,126,468执行的指令316,141,092最大堆栈深度1,234中间步骤191,058使用的存储器511.16 MBGC后使用的内存462.51 MB存储存储器0.0 B收集的物体10,922,272标记和扫描运行45,082,614执行时间20：54：55.075秒速度745 tr/s表3并发缓存正确性验证（适当的同步）形式，并且因为模拟关系数据库可能会导致分析花费太长时间。这将是非常有帮助的，如果这整个过程可以自动化，实际上，第1节中提到的SLAM引擎确实自动化了一个类似的过程，为单线程C程序。他们使用谓词抽象，这有一些吸引人的理论品质，但目前还不清楚如何将他们的技术扩展到多线程程序。一个自动化这个环境生成的工具将是非常有用的。这是一个积极的研究问题。在[8]中，Tkachuk，Dwyer等人，描述一种自动推导驱动系统的在[6]中，Khurshid et al.描述了一种使用JPF生成测试用例的技术。在[12]中，Xie等人描述了一种类似的技术，使用穷举运行来生成测试用例。这些技术非常有趣，但以它们目前的形式，它们对我们来说没有价值，因为它们只在程序调用树的有限深度上探索程序。由于我们的系统一个不同但同样重要的问题是“我们如何知道去哪里看？”以及相关的问题“什么样的问题56G. Hughes等人/理论计算机科学电子笔记144（2006）45受访国家10,616,063执行的过渡28,743,772执行的指令178,827,220最大堆栈深度1,232中间步骤193,554使用的存储器285.28 MBGC后使用的内存254.47 MB存储存储器0.0 B收集的物体9,913,584标记和扫描运行23,655,230执行时间15：54：04.732秒速度502 tr/s表4并发缓存正确性验证（严格同步）是否适合使用模型检查？”在我们的案例中，我们被开发团队引导到问题上，在一种情况下，他们指定了一个他们一直很难找到的问题，在另一种情况下，要求验证一个特定的模块是健全的。在这两种情况下，我们都提取了一个状态机来描述所讨论的模块的输入，然后探索该状态机，寻找违反简单属性的情况;例如以及由于所讨论的系统广泛地使用并发性，或者像任何RMI客户机那样直接使用，或者在缓存的情况下显式地使用，测试这些属性是困难的，并且易于计时。测试也有麻烦回答- ing活动属性-属性，如因此，我们认为，一个适当的使用模型检查器是系统的探索接口的模块，同时检查重要的不变量。模型检测程序在今天的可行性如何？目前，需要专家以一种充分探索其行为但不会导致模型检查器爆炸的方式关闭系统。然而，正如我们所展示的，使用当前形式的JPF，甚至可以检查大型模块，或者与大型系统的其余部分G. Hughes等人/理论计算机科学电子笔记144（2006）45577结论我们已经证明，可以在已有的软件上使用模型检查进行重要的分析，即使软件不是为模型检查而设计的。我们期望遇到困扰使用模型检查分析大型程序的主要问题状态爆炸问题，但在很大程度上没有。另一方面，环境的产生代表了大部分的排放。我们相信有两个主要的原因可以解释为什么我们没有遇到国家爆炸的问题。第一个原因是我们的系统是商业软件，特别是将几乎所有可变状态存储在数据库中的商业软件。因为我们抽象了数据库，所以我们也抽象了程序中几乎所有的mu- table状态，这意味着我们探索的不同状态的数量。 并没有想象中的那么大第二个原因是，我们的大多数分析都是为了检测错误的存在。有可能只有一个或两个可能的状态配置中存在错误，所以搜索整个状态空间以证明正确性是必要的。然而，我们发现了几个错误，这些错误会沿着许多不同的状态配置被触发，因此找到其中一个并不需要像搜索整个状态空间那样多的工作。事实上这种并发错误的例子包括简单的数据竞争，或者我们对通信协议的分析。为了测试通信协议而不发现问题，所有的线程都必须在不触发断开连接的情况下完成它们的整个操作集。这在测试中是很有可能的，但是因为我们探索了任何线程可能断开连接的状态空间，所以我们几乎立即发现了错误。我们的分析的一个积极的属性是，我们对原始系统的忠实性是故意高的。我们已经尽可能少地删除了组件，而且我们删除的组件基本上都是像JDBC和RMI这样的通信库，它们同时独立于代码库，并且很容易建模。如前所述，我们在执行这项工作时遇到的最大障碍是生成环境所需的大量电子邮件。我们已经讨论了最近在这方面的几项进展，希望不久这将是一项需要更少体力劳动的我们感谢dr.Willem Visser对JPF非常有帮助58G. Hughes等人/理论计算机科学电子笔记144（2006）45引用[1] T. 鲍 尔 河 Majumdar ， T.D. Millstein 和 S.K. 拉 贾 马 尼 C 程 序 的 自 动 谓 词 抽 象 SIGPLANConference on Programming Language Design and Implementation，第203-213页，2001年[2] P. Godefroid。使用VeriSoft对编程语言进行模型检查。在第24届ACM SIGPLAN-SIGACT专题讨论会上，编程语言的原则，第174-186页ACM Press，1997.[3] K. Havelund，M. Lowry，S.帕克角，澳-地Pecheur，J. Penix，W. Visser和J. White。形式化分析了远程代理在授权之前和之后的情况第五届NASA兰利正式方法研讨会论文集，2000年6月。[4] G. 霍尔茨曼计算机协议的设计与验证。普伦蒂斯·霍尔1991年[5] D. Hovemeyer和W.Pugh. 发现bug很容易。 ACM SIGPLAN 2004年编程语言设计与实现会议论文集，2004年12月。地出现。[6] S. K hurshid，C. P. 维瑟为建模和测试提供了通用的系统执行在第九届国际会议的工具和算法的建设和分析系统，华沙，波兰，2003年4月。[7] M. Musuvathi，D.帕克A. Chou，D. R. Engler和D. L.迪尔CMC：一种实用的模型检查方法。第五届操作系统设计与实现研讨会论文集，2002年12月。[8] O. TKACHUK，M. B. 是的，还有C。 S. Pasarea nu. 用于软件模型检测的自动化工程图生成第18届IEEE自动化软件工程国际会议论文集，2003年10月。[9] W. Visser，K.Havelund，G.Brat和S.公园Java PathFinder-第二代Java模型检查器。在Proc.后CAV讲习班在验证的进展，芝加哥，2000年7月。[10] W. Visser，K.Havelund，G.Brat和S.公园模型检查程序。在第十五届IEEE自动化软件工程国际会议（ASE '00）的会议记录中IEEE计算机学会，2000年。[11] J·沃尔多远程过程调用和Java远程方法调用。IEEE Concurrency，6（3）：5[12] T. Xie，黄胸拟谷盗D. Marinov，W. Schulte和D.诺特金Symstra：一个使用符号执行生成面向对象单元测试的框架. 工具和算法的建设和分析系统，第11届国际会议，TACAS 2005年，2005年。[13] J. Yang，P.图黑，D.恩格勒和M。穆苏瓦提 使用模型检查来发现严重的文件系统错误。2004年，第六届操作系统设计与实现研讨会论文集