并发程序的源转换方法及其在并发分析中的应用

理论计算机科学电子笔记141（2005）57-75www.elsevier.com/locate/entcs用于并发分析的源转换放大图片作者：James R.托马斯·科迪Dean，Juergen Dingel于尔根·丁格尔院长1，2加拿大金斯敦皇后大学计算机学院摘要并发编程对质量保证提出了一系列独特的问题。这些困难包括死锁、活锁和发散的复杂性，这可能非常难以检测和调试。已经开发了各种工具来帮助并发应用程序的设计者和开发者。其中一些工具，如VeriSoft，是特定于特定的实现语言，如C++。Java远程方法调用（Java RMI）包促进了并发应用程序的实现，包括那些进程驻留在不同主机上并通过网络进行通信的应用程序。不幸的是，它并没有使开发人员从控制对远程对象的并发访问的潜在陷阱中解脱出来，事实上，可能会使并发问题更加难以发现。本文提出了一种方法，允许VeriSoft的状态探索系统被用来分析Java RMI程序的死锁，活锁，分歧，断言违规。该系统通过将JavaRMI程序转换为C++程序来实现，其中Java的语法、结构、并发性和内存管理都被C++等效程序所取代，JavaRMI通信也被转换为VeriSoftC ++进程间通信。 我们提出了这种转变的细节，并讨论了一些小的例子的初步结果保留字：源转换，静态分析，并发1引言并发程序的开发对质量保证提出了一系列独特的问题这些困难包括死锁、活锁和1电邮地址：蒂姆cassidy@tricolour.queensu.ca，（cordy，dean，dingel）@cs.queensu.ca2这项工作得到加拿大自然科学和工程研究理事会的支持。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.05.012T. Cassidy等人理论计算机科学电子笔记141（2005）5758发散，这可能是非常难以检测和调试。因此，各种静态和动态分析工具已经被开发出来，以帮助设计师和开发人员的并发应用程序。特别是，VeriSoft[10]提供了一个用于C++程序中进程间通信的并发分析系统Java远程方法调用（Java RMI）包[24]促进了为网络环境（例如客户端-服务器系统）设计的并发应用程序的实现，并广泛用于电子商务和其他分布式环境中的生产应用程序。Java RMI通过隐藏低级并发实现细节提供了更高级别的抽象。然而，它并没有使开发人员从控制对远程对象的并发访问的潜在陷阱中解脱出来，事实上可能会使并发问题更加难以发现。虽然已经开发了许多工具来帮助设计和开发正确的Java并发应用程序，但这些工具都没有解决Java RMI。这部分是因为Java RMI而不是重新定位现有的分析工具，以了解Java RMI直接，这提出了一些困难的新的分析问题，将在最好的昂贵和耗时的过程中，在本文中，我们提出了一个实验，在提供并发分析的Java RMI程序使用不同的解决方案：语义保持源到源的转换，从Java程序使用Java RMI到C++程序使用VeriSoft进程间通信。2动机并发程序设计必须处理在顺序程序中不存在的困难。这些问题中的三个是死锁、活锁和发散。死锁是指两个或多个进程都被阻塞，等待其他进程的资源或结果，从而导致它们都无法继续。当两个进程/线程能够改变它们的状态（即它们没有被阻塞）但无法进行任何有用的进展时，就会发生活锁。当两个线程或进程之间在给定的时间段之后没有通信时，就会发生发散任何使用同步的消息协议都容易发生死锁。更常见的是，这些协议容易出现分歧。在多用户环境中，分歧可能T. Cassidy等人理论计算机科学电子笔记141（2005）5759public class PeerA extends UnicastRemoteObjectimplements PeerAInterface，Serializable {public void onDestroy（）{//never make it into here}public void run（）{ try {String name =“PeerB”;PeerB接口peerB =（）; document. writeln（）;document.writeln（）;}catch（exception_）{exception_.printStackTrace（）;}}public static void main（String strategy[]）{String name =“PeerA”; PeerAInterfacepeerA = new PeerA（）; String.rebind（name，peerA）; peerA.run（）;}catch（exception_）{exception_.printStackTrace（）;public class PeerB extends UnicastRemoteObjectimplements PeerBInterface，Serializable {public void run（）{String name =“PeerA”;PeerA接口peerA =（）; document. writeln（）;document.writeln（）}catch（exception_）{exception_.printStackTrace（）;}}public static void main（String[] args）{ String name =“PeerB”;尝试{public int findDuplicate（）; int findDuplicate（）;}catch（exception_）{exception_.printStackTrace（）;}}}}}}图1.一、一个总是死锁的Java RMI程序的简单例子随着用户数量的增加，使应用程序完全不可用。因此，防止分歧和死锁变得非常重要已经开发了各种工具来帮助设计和开发正确的并发应用程序[4，15，21]。其中一些是基于抽象模型的，代码可以从这些模型中生成（全部或部分），其他的则基于对源代码的分析。最新的工具之一是VeriSoftState Space Exploration System [10]。VeriSoft提供了一组库和一个执行引擎，用于探索使用进程间通信在C++中实现的并发程序的状态空间。除了死锁、活锁和发散之外，开发人员还可以指定在整个程序执行过程中必须保持Java远程方法调用（Java RMI）通常用于现代分布式网络系统（如电子商务应用）的开发。Java RMI的吸引力在于它使开发人员不必担心网络通信的细节，例如打开，连接和关闭套接字。不幸的是，JavaRMI在正确处理并发控制的复杂细节方面几乎没有提供什么帮助。当并发元素的数量增加时，这个问题会加剧，因为开发人员可能很容易忽略在远程对象之间引入可能导致死锁的循环依赖关系。例如，考虑图1中的JavaRMI代码，它总是会导致死锁。在图1中，PeerB首先启动。一旦它将自己绑定到RMI注册表（使用Roll.rebind方法），就可以启动PeerA。PeerA绑定到RMI注册表（也使用Roll.rebind方法），然后T. Cassidy等人理论计算机科学电子笔记141（2005）5760进入它的run方法，使用RMI注册表定位PeerB，并调用PeerBPeerB然后尝试调用PeerAVeriSoft被明确设计为使用进程间通信分析C++程序，不能直接与其他语言和并发方法一起使用。VeriSoft网站描述了一种分析Java的可能方法然而，这种方法将Java程序简单地视为一个黑盒，并严重限制了对Java程序本身的分析。特别是，它没有解决使用VeriSoft进程间通信表示JavaRMI的并发性的问题，因此不允许Java RMI的并发性分析。此外，JavaRMI系统本质上是分布式的，通常包括几个独立通信的Java程序，而不仅仅是一个。作为弥合这一差距的实验，我们已经开发出一种不同的方法，允许Java RMI程序进行分析VeriSoft：一套正式的源代码转换从Java到C++，保留Java RMI并发行为使用VeriSoft进程间通信库。可以使用VeriSoft分析产生的C++程序的死锁、发散和活锁，并且可以使用方法名称轻松地将分析结果与原始Java源代码相关联。我们使用自动源代码转换，因为它比手动转换更不容易出错，因为它（至少在理论上）适合于形式验证 ， 并 且 因 为 它 很 容 易 扩 展 到 处 理 实 际 大 小 的 程 序 。 例 如 ，java.util.Hashtable及其依赖类由超过14，000行Java代码组成，我们的系统在10秒内就将其转换为C++代码。2.20 GHz Pentium PC，不可能出现笔误。我们选择在这个实验中使用VeriSoft的主要原因是它直接使用源代码。能够直接在源代码上执行分析有两个优点。首先，由于不需要构建模型，因此降低了由于建模不准确而导致的虚假分析结果其次，将分析输出（如错误跟踪或反例）与C++源代码关联起来更简单，并通过方法名称与转换它的Java源代码关联起来更简单。VeriSoft的第三个优点是它是无状态的，也就是说，它执行分析时没有程序变量值的显式表示。无状态分析特别适合于分析具有大量复杂数据的软件系统，例如电子商务应用程序。VeriSoft优于其他分析工具的最后一个好处是它使用了部分T. Cassidy等人理论计算机科学电子笔记141（2005）5761降阶偏序约简背后的基本前提是，并不是所有并发事件的交织都必须被检查。也就是说，对应于状态空间中相同并发执行的交织不需要单独探索[10]。正是由于这个原因，部分降阶已被证明是一个有效的手段，以保持在检查状态爆炸问题。2.1论文大纲本文的其余部分将致力于解释如何将使用RMI的Java代码转换为VeriSoft可分析的C++代码。第3节介绍了我们工作中使用的各种工具和库。第4节详细介绍了转换过程和使用我们的工具的优势。Java使用垃圾收集算法，自动释放不再使用的内存。为了模拟这种行为，我们为C++开发了一个简单的垃圾收集算法，在第5节中详细介绍。我们的变换的最终结果的一个例子在第6节中解释。第7节简要概述了我们进行的其他一些实验最后，第8节描述了相关工作，第9节介绍了我们的结论和未来的工作。3背景3.1VeriSoftVeriSoft [10]是一个可以用来分析并发C++程序的工具。它通过遍历程序的状态空间到开发人员设置的任意深度，直到发现死锁，发散，活锁或直到某些用户定义的断言失败。任何状态空间遍历的深度都是由可见操作的存在决定的。可见操作是VeriSoft库中的任何函数，包括但不限于消息传递操作和非确定性选择点。VeriSoft是一种实用的验证工具，已在工业中用于分析并发应用程序，如朗讯技术CDMA呼叫处理库[3]，并协助调试和测试关键任务系统，如4ESS心跳监视器[11]。3.2源转换有很多种转换系统可用于将一种语言转换成另一种语言。 TXL [8]是十多年前开发的，用作探索编程语言方言的工具由于T. Cassidy等人理论计算机科学电子笔记141（2005）5762同时，它已经被用于各种各样的源代码转换应用程序，从简单的语法替换到复杂的软件工程转换[9]。TXL是一种纯函数式编程语言，专门用于支持结构化源代码转换。要转换的源的结构是使用一个无限制的模糊上下文自由语法，从语法分析器自动派生。通过示例描述了转换，使用一组上下文敏感的形式化转换规则，从中自动推断出应用策略我们这里使用的转换是源迁移，将程序从一种语言翻译成另一种语言，基本上是在相同的抽象级别上。在本例中，更改是从使用Java远程方法调用的Java源代码更改为使用VeriSoft进程间通信的C++源代码。由于多种原因，这种迁移的源转换特别具有挑战性。首先，这两种语言的内存、并发和通信模型是非常不同的，这给语义的保持带来了有趣的问题其次，我们需要的并发行为的转换不是简单的语言翻译，而是在高抽象级别（Java RMI）解释并发库的语义，并使用不同的语义模型和抽象级别（VeriSoft进程间通信）表示。最后，转换涉及最近确定的3.3Java RMIJava远程方法调用的基础非常简单。其思想是，远程对象应该从某种意义上说，注册表就像是远程服务的可通过互联网访问的哈希表。在注册之后，任何Java对象都可以使用远程对象注册自己所使用的唯一名称来当一个对象查询注册表时，它返回一个对存根类对象的引用，该对象与远程对象具有相同的接口，但位于本地上下文中。存根类的方法包含对远程对象的基于套接字的请求（带有参数“marshalled”）和等待接收返回对象（来自相应的远程方法）的阻塞代码。 如果远程方法的返回类型为void，则本地对象将直接阻塞，直到它收到远程方法已完成的确认。图2说明了该过程。T. Cassidy等人理论计算机科学电子笔记141（2005）5763Node1Node2客户端进程服务器存根请求远程对象请求远程对象返回ServerStub返回ServerStub任何方法调用任何方法调用（编组）返回值（编组）返回值远程对象Node3RMI注册图二、Java RMI中远程方法调用的顺序图4我们的解决方案：弥合差距图3显示了使用VeriSoft从JavaRMI到C++转换的总体结构有三个基本步骤。第一个是使用TXL从Java到C++的自动语言转换。一旦原始Java代码所依赖的所有Java库也被转换，就可以编译和执行生成的C++代码第二步需要生成一个类，该类对JavaBean和RMI注册中心的功能进行建 模 ， 包 括 生 成 存 根 类 （ 充 当 远 程 对 象 的 代 理 ） 和 Uni-castRemoteObject类。这一步在组件生成器角色中使用TXL，使用源代码转换生成所需的工件第三步涉及在VeriSoft中编译、链接和执行生成的C++代码，然后可以使用这些代码来分析生成的模型。4.1源转换4.1.1步骤1：从Java到C++的语言迁移图3的第一步虽然庞大而复杂，但相对简单。它包括从Java源代码到C++源代码的语义保持转换。在某些系统中，也可能有Java类方法被声明为本机的，因此是用其他语言编写的。T. Cassidy等人理论计算机科学电子笔记141（2005）5764传奇用户定义类隐式类（由编译器供应商提供）源转换不转型隐式源代码转换（由编译器供应商完成）图三. 模型的转换序列和后续执行。 隐含方面必须作为转换到C++的一部分生成Java（通常是C或C++）。在这种情况下，这些方法可能必须手动处理，因为C或C++源代码并不总是可用的。在此阶段进行的转换类型的一个简单示例是数组的转换。虽然数组是一个简单的结构，数组实际上扩展了java.lang.Object，因此以下是有效的Java代码：1次int[]arrayOfInts;2对象java对象=arrayOfInts;3 int []nums= int []nums;因此，需要转换后的java.lang.Object类和数组（在C++中）支持这种赋值。为了支持这一点，Java命名RMI注册表RMI编译存根（代理）单播远程对象步骤1C++步骤2图书馆存根（代理）步骤3Verisoft软件XML和RMI注册表单播远程对象C++使用Verisoft远程对象客户端单播远程对象存根（代理）远程对象XML和RMI注册表客户端远程对象客户端转型隐式变换隐式类用户定义类J a v ato C++J a v ato C++T. Cassidy等人理论计算机科学电子笔记141（2005）5765rulearrayDeclarationAndArrayDeclarationTransformationreplace[变量声明]Mods [repeatmodifier] TypeName [type_name] '[ OptExpression [optexpression] ']VarName [variable_name] =“new AssignedTypeName [type_name]”[ SizeOfArray [optexpression]通过Mods 'StdVector TypeName >：：'type VarName（SizeOfArray）;结束规则见图4。 将Java数组转换为StdVector它本质上充当C++标准vector类周围的包装类（通过自己的方法提供对另一个类的服务的访问的类这个新类的名称是StdVector。 为了维护Java语义，转换必须识别所有Java数组并将其转换为C++中的StdVector将Java数组转换为C++StdVector类对象的转换规则之一如图4所示。使用它，上面的Java数组赋值示例会自动转换为以下C++代码：1StdVectorint>：：typeOfInts;2SmtObjectPtrjava对象=arrayOfInts;3StdVector：：typeenewArrayOfInts= avaObject.Dynamic_cast（（StdVectorint>：：type）0）;4.1.2步骤2：在C++中生成远程对象注册表第二步的第一部分涉及到Java RMI类的生成，它实现了Java RMI注册表的一个模型。这是必需的，因为C++不支持任何类似于Java的反射库的功能，Java的反射库提供了（除其他外）实例化一个类的能力，该类的名称直到运行时才知道。在这种情况下，我们需要能够使用字符串名称来初始化类。为了在C++中对这种行为建模，在类中生成了一个查找方法，该方法根据作为参数传递的字符串名称返回远程类的存根。下面是为图1的示例程序生成的PHP类中生成的查找方法的示例：1静态Smt RemotePtr查找（SmtStringPtrname_）二{3目标目标 =m_hashtablee->get（name_）;4if（object！= 空值）{5if（instanceOf（object，PeerBInterface））{6返回SmtPeerB_StubPtr（新PeerB_Stub）;T. Cassidy等人理论计算机科学电子笔记141（2005）5766（七）8}9返回NULL;10}上面的代码试图找到一个与name参数相关联的对象。如果它找到了一个与name参数相关联的对象，它将返回一个同名的该类对象的实例，并在该实例的后面附加生成每个存根类（远程对象的代理），使其包含具有相同签名（返回类型，名称和参数）的方法，但其内容实际上向真正的远程对象发送消息并等待确认（即方法是阻塞的）。这需要将Java RMI中的所有网络通信替换为使用进程间通信的VeriSoft方法。存根类的生成是作为原始JavaRMI远程对象类的转换C++版本的副本的源转换实现的（图5）。例如，以下存根方法被生成为图1的示例程序的远程类PeerB的存根类的一部分：1虚拟虚空执行任务（）下一页二{3个字符*消息=新char[100];4sprintf （message，GLOBAL_executeTask_VAR）;5send_to_queue（m_remoteObjectMsgMessageID，QSZ，message）;6删除[]消息;7消息=（char* ）接收自队列（m_msgbaseID，QSZ）;8if（strcmp （message，GLOBAL_executeTask_VAR）==0）{9//收到我等待的确认-远程方法完成10返回;11}12throwSmtRemoteExceptionPtr（“problemintransmissionofmessage“）;13}此存根方法首先将宏GLOBAL executeTask VAR中表示的字符串放入消 息 字 符 数 组 中 。 然 后 ， 它 将 这 些 字 符 发 送 到 名 为mremoteObjectMsgMessageID。 消息队列对象是VeriSoft专用的类，用于在进程之间发送消息。一旦这些字符被发送到队列中，包含它们的缓冲器就会被本地删除。然后，代码将一直阻塞，直到它从队列接收到返回消息。如果接收到的消息是它所期望的（即它发送的相同消息），则它返回，否则抛出RemoteException对象T. Cassidy等人理论计算机科学电子笔记141（2005）5767规则定义函数%make类中所有方法的存根版本替换$[member]%以原始方法的C++版本开头OPTOSIS SpecColon [optaccess_specifier_colon]DeclSpecifiers [decl_specifiers] PointerOperators [repeatpointer_operator]FunctionNameID [id] DeclaratorExtensions [repeatdeclarator_extension+]OptCtorInit [optctor_initializer]OptExceptionSpec[optexception_specification]FunctionBody [function_body]%确保该方法不是我们生成的方法之一解构非FunctionNameID 'AddRefdeconstructnotFunctionNameID“版本%构造全局宏名constructMacroIDFromFunctionNameID [id]FunctionNameID [MacroIDFromID]%现在将原始版本替换为存根版本，%使用进程间通信与真实的东西通过OptSpecColon DeclSpecifiers PointerOperatorsFunctionNameIDDeclaratorExtensions{‘charsprintf（message，MacroIDFromFunctionNameID）;send_to_queue（m_remoteObjectMsgMessageID，QSZ，message）;消息=（char *）rcv_from_queue（m_msgcodeID，QSZ）;'//received the ack I was waiting for-remote method completed}‘throw}结束规则图五.一条TXL规则，用于将C++转换的Java RMI类的每个方法转换为存根方法，该存根方法使用VeriSoft进程间通信JavaRMI框架中的所有远程对象都必须扩展Uni-castRemoteObject类.为了接受来自存根类的传入消息，调用适当的方法，然后将消息发送回存根类，指示方法已完成，需要生成UnicastRemoteObject。与存根类一样，UnicastRemoteObject类是使用源转换生成的，源转换基于原始JavaRMI远程类的转换后C++代码的副本。TXL函数实现了T. Cassidy等人理论计算机科学电子笔记141（2005）5768functionRunMethod Members [repeatmember]%在给定所有存根成员的情况replace[repeatmember]%（生成，所以没有开始）%make selector if语句用于每个远程方法构造SelectionStatements [重复语句]_ [选择条件成员]constructFirstStatementAsRepeat [repeatstatement]通过'public：‘void run ({'char * message;'while（1）{FirstStatementAsRepeat [. 选择声明]}}end function见图6。一个TXL函数，用于为转换后的Java RMI程序生成UnicastRemoteObject类的run方法，该程序的C++转换后的远程方法作为参数给出这个类的run方法部分的生成如图6所示。下面是这个函数生成的run方法，它是图1程序的UnicastRemoteObject的一部分：1例 无效run（）二{3个字符*message;4而那些(1){1}5条留言=（char* ）接收自队列（m_msgbaseID，QSZ）;6if（strcmp （message，GLOBAL_executeTask_VAR）==0）{月7->执行任务 （）的情况;8send_to_queue（m_remoteObjectMsgMessageID，QSZ，message）;（9）10}11}在某些Java RMI应用程序中，参数被发送到远程对象，并从远程对象的方法返回对象。为了实现这一点，必须对对象进行编组和解组。 编组一个对象是创建一个字节数组来表示对象的过程，这样它就可以通过网络发送，而解编组是从另一端接收到的字节数组重新构建对象的过程。我们当前的实现只支持对简单的整数和字符串进行对象的编组和解组。但是，可以相对容易地扩展该实现，以将任何可序列化的对象作为VeriSoft字符串消息参数进行处理。T. Cassidy等人理论计算机科学电子笔记141（2005）57694.1.3步骤3：在VeriSoft中编译、链接和执行最后一步简单地涉及编译和链接转换和生成的C++文件，并使用VeriSoft执行结果。 在执行之前，必须为程序配置VeriSoft系统文件.VS要运行VeriSoft，必须在此文件中指定要执行的进程数、分析深度（即要探索的状态空间的深度）、是否忽略死锁等因素VeriSoft可以在三种模式（手动、引导或自动模拟模式）中的一种手动模式允许用户手动逐步执行代码。 导模如果用户希望指定特定进程何时执行其下一个可见操作，或者在抛出点（代码中可以选择从函数返回的数字范围的点）选择哪个数字，则使用。 自动模式允许VeriSoft自动运行并返回在程序执行的状态空间中的什么点（如果有的话），发现僵局、分歧或活锁。5存储器管理由于Java内置的自动堆恢复，内存管理对我们的实现来说是一个特殊的挑战。这是在Java虚拟机中通过垃圾收集器实现的，当Java程序执行时，垃圾收集器作为一个单独的线程在后台运行。 然而，C++没有这样的内置垃圾收集，默认情况下使用显式的new（）和delete（）调用来管理堆。虽然C++有垃圾收集库[2，23]，但它们对内存的分配和使用制定了规则，这些规则可能与Java模型不完全匹配，或者对于VeriSoft分析来说过于复杂。为了解决这个问题，我们决定使用一个简单的垃圾收集算法，其中包括智能指针和引用计数，以保持转换简单和VeriSoft状态空间小。但是，我们的方法可以很容易地更改为使用其他内存管理库。我们的内存解决方案引入了两个新的Java类。第一个是使用模板的智能指针类这个类用来代替常规的C++指针。它允许动态创建的C++对象保持在堆栈上（像自动对象一样）。当这些指针被复制和赋值时，它们会调整所指向对象的引用计数。智能指针具有解构器，以确保在指针变量超出范围时适当地例如，考虑以下声明和初始化：T. Cassidy等人理论计算机科学电子笔记141（2005）57701TrainCar=newTrainCar（42）;我们到C++的转换为指针引入了一个新的智能指针类型，然后使用该类型声明变量并初始化它：1typedefSmartPtr火车车厢>智能列车车厢2辆智能列车车厢（新列车车厢（42））;为 了 便 于 跟 踪 对 对 象 的 引 用 ， 我 们 设 计 了 另 一 个 类 （ 名 为JTCUVobject），所有其他翻译的类都扩展了这个类。这个类在我们生成的C++代码中扮演Java的java.lang.Object类的角色因此，我们的转换为生成的C++代码构建了与原始Java程序相同的继承层次结构。所有Java类都直接或间接地扩展java.lang.Object，因此为转换后的Java类（未指定父类）生成的C++父类是我们的JTCUVobject类。6最终结果图1的示例Java RMI类的整个转换的最终结果如图7所示。转换添加的AddRef和Release方法是前一节讨论的简单引用计数内存管理策略的工件。我们的系统增加了VeriSoft可以分析的语言的集合，通过使用VeriSoft的li-tool自动化Java RMI代码到C++的转换。此外，我们的系统也能够实现一个小的减少在Java RMI程序中的状态的数量，通过只提取关键的高层次的信息传递的细节。Java RMI的低级网络方面，如套接字和端口，对我们的并发分析也不重要，因此被我们的转换抽象掉了。因此，我们得到的模型能够在一台机器上运行，利用进程间通信，而不需要一个联网的客户端-服务器环境。我们在Java RMI转换系统中演示的策略和方法没有理由不能用于其他语言和并发范例，从而进一步增加了可以使用VeriSoft进行分析的应用程序的范围7实验/结果到目前为止，我们只在一小部分Java RMI示例上使用了我们的转换，并故意添加了并发错误，以便于分析。T. Cassidy等人理论计算机科学电子笔记141（2005）5771#ifndef PeerA_H#define PeerA_H类PeerA;typedef SmartPtr PeerA> SmtPeerAPtr;class PeerA：public UnicastRemoteObject，public String s，publicString {公共场所：public int findDuplicate（）{Duplicate：：Duplicate（）;}公共场所：public void Release（）{public void Release（）;}公共场所：public void callBack（）{DataGuard（*this）;//never make it into here}公共场所：public void run（）{System. out. println（*this）;try {SmtStringPtr name =“PeerB”;SmtPeerBInterfacePtr peerB =（String->lookup（name））.Dynamic_cast（（SmtPeerBInterface Ptr *）0）;return（）;}public int findDuplicate（）{findDuplicate（）;}}公共场所：public static void main（StdVectorSmtStringPtr>：：type args）{尝试{String name =“String”;SmtPeerAPtr peerA（SmtPeerAPtr（new PeerA（）;String->rebind（name，peerA）;peerA->run（）;}#ifndef PeerB_H#定义PeerB_H类PeerB;typedef SmartPtr PeerB> SmtPeerBPtr;class PeerB：public UnicastRemoteObject，public String s，publicString s {公共场所：public int findDuplicate（）{Duplicate：：Duplicate（）;}公共场所：public void Release（）{public void Release（）;}公共场所：public void run（）{SmtStringPtr name =“PeerA”;SmtPeerAInterfacePtr peerA =（String->lookup（name））.Dynamic_cast（（SmtPeerAInterface Ptr *）0）;return（）;}public int findDuplicate（）{findDuplicate（）;}}};int main（int argc，char * args []）{ SmtStringPtr name =“PeerB”;尝试{int n（int n，int n）;return（name，name）;}public int findDuplicate（）{findDuplicate（）;}}#结束public int findDuplicate（）{findDuplicate（）;}}};#结束图7.第一次会议。图1的简单示例Java RMI程序转换为C++。ysis。使用100个不同的C++测试函数测试了java.util.Hashtable及其依赖类（来自第2节）的转换，以确保其行为与原始Java的行为相虽然还没有调整，我们的系统已经相当有效。在图1提供的示例中，非隐式类 （即PeerA 和PeerB ）的 转换在小型PC 上在5 秒内完成 。VeriSoft的分析（其中发现了死锁）也在同一台机器上在5秒内完成。我们的另一个例子是网络金融交易系统的简化版本。系统中的所有客户都共享同一个帐户，将钱存入帐户并获得余额。这个例子使用了10个独立的客户端对一个共享的远程对象进行远程方法调用。在一次执行中，成功地发现了深度为T. Cassidy等人理论计算机科学电子笔记141（2005）5772八个看得见的行动在这种情况下，转换也花了不到5秒，VeriSoft的分析花了大约10秒。8相关工作其他工具所做的许多转换实际上忽略了语言的基本语义[14，7]。一个例子是Bandera [7]在将Java转换为Promela时完成的转换。在这场变革中， 重要的动态I/O功能（套接字、文件等）无法转换，尽管可以对这些服务的行为进行建模（从文件读取或写入，通过端口发送消息等）。通过指示方法是阻塞还是非阻塞、依赖关系等。然而，因为C++是一种（至少在理论上）能够进行Java所能进行的任何I/O活动的语言，所以应该可以在随后使用VeriSoft库的C++程序中精确地模拟Java的动态I/O行为。虽然两者都可以对Java程序进行建模，但Bandera和Java Path都不能将Java RMI转换/翻译成建模语言[22，19]。主要问题在于Java RMI框架中的大量本地通过在更高的抽象层次上自动转换为C++，我们的工作避免了这个问题。与VeriSoft相比，Bandera基本上，这意味着Bandera允许更丰富的属性规范在程序中应该或不应该出现。类似地，Java Pathlogic能够将Java代码转换为支持线性时态逻辑的Promela [14]这些分析工具非常适合于检查类似于我们所处理的程序的各个方面，但是使用的建模语言在I/O能力上比Java更有限。I/O库的行为必须通过确定基本属性（阻塞、非阻塞、依赖关系等）来建模。的I/O功能，并将其编码在建模语言中。然而，如果以这种方式对行为进行建模，则程序的状态空间会显着减少。虽然这些工具必须手动对任何动态I/O库进行建模，但它可以显著节省状态空间，从而减少确定感兴趣属性（如死锁，发散，活锁等）的时间。因此，尽管Bandera和Java Path finder等工具满足了手动构建大多数低级Java I/O库模型的要求，但它们弥补了后续T. Cassidy等人理论计算机科学电子笔记141（2005）5773程序中的状态空间大大减少。我们的系统并不是唯一一个利用源代码转换来辅助分析并发程序的系统。微软研究院[18]探索了一种不同的基于源代码转换的方法.在KISS（“Keep It Simple and Sequential”）项目中通过这种方式，可以使用顺序程序模型检查器（如SLAM [1]）来分析并发行为的某些方面，如设备驱动程序中的竞争条件。虽然这项工作没有跨越语言边界或将用户从建模任务中解放出来，但它在两个方面与我们的相似：它使用源转换来扩展现有模型检查器的功能，并且它将并发的更高级别抽象转换为具有不同语义模型的更低级别表示。Gradara等人[12]提出了另一种分析并发Java程序的转换方法，他们描述了将使用本机Java