文件标题：使用随机调度的并发Java程序的错误检测方法

142理论计算机科学电子笔记70第4期（2002）网址：http://www.elsevier.nl/locate/entcs/volume70.html16页使用随机调度Scott D. Stoller1计算机科学系，美国纽约州立大学石溪分校摘要在并发程序中发现由意外的线程交织引起的错误的困难是众所周知的。模型检查器可以精确定位这些错误并验证正确性，但不容易扩展到大型程序。这里讨论的方法更具可扩展性，但系统性较差。我们通过在选定的点插入对调度函数的调用来转换给定的Java程序。调度函数要么什么也不做，要么导致上下文切换。最简单的调度函数使用伪随机数生成器盲目地做出选择;更复杂的调度函数使用算法来加权选择。 我们尝试插入尽可能少的调用，同时仍然确保对于每个可到达的死锁和断言违规，调度函数有一系列的选择导致它;因此，通过测试转换后的程序，无论底层Java虚拟机的调度策略如何，都有非零的概率找到它。1介绍在并发程序中，由于线程的意外交织而导致的错误很难发现。这促使开发强大的工具来帮助发现此类错误。由于Java中并发编程的日益普及，我们在这里重点介绍可以应用于Java编写的程序的工具，尽管其他语言也存在类似的工具。Java语言规范[15]基本上没有提供关于线程调度器的保证。因此，要使并发Java程序在面对变化的负载条件（这可能会干扰运行）时保持健壮，并在所有操作系统和Java运行时环境（可能具有不同的线程调度策略）之间保持可移植性，它必须工作1作者感谢NSF在Grant CCR-9876058下的支持，ONR在赠款N 00014 -01-1-0109和N 00014 -02-1-0363下的支持。电子邮件：stoller@cs.sunysb.edu网址：http：//www.cs.sunysb.edu/2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。n.托勒143不管由不同线程执行的指令的任意交织。模型检查器是一种功能强大的工具，可以帮助查明并发程序中的错误模型检查器的目标是控制所有的非确定性（包括调度中的非确定性），并彻底探索系统的可能行为。现有的Java模型检查器包括最初的JavaPathlogic [16]，第二代Java Pathlogic [3]，它部分建立在Spin [18]的思想上，以及Javalogic [24]，它部分建立在VeriSoft [12]的思想上。模型检查器的系统性和详尽性很有吸引力，但它限制了它们的可伸缩性。本文描述了正在进行的工作，探索一种更具可扩展性但系统性较低方法是在被测程序中的选定点插入对一个函数的调用调度函数要么什么也不做，要么导致上下文切换。最简单的调度函数使用伪随机数生成器盲目地进行选择。伪随机数生成器在执行开始时被播种。通常，种子基于当前时间并被记录。更复杂的调度函数将随机性与加权选择的随机性相结合。分析师可以只考虑当前状态，也可以考虑历史。历史记录是关于当前执行和可能的先前执行的存储信息。调度函数可以通过调用Thread.yield或Thread.sleep来引起上下文切换。转换后的程序会被反复执行以进行测试。如果在某个特定的种子中发现了错误，则会用同一个种子重新执行该程序，以帮助重现错误。通过这种简单的方法，再现性是可能的，但不能保证。保证再现性需要一个捕获和重放机制，如[5]。我们在一个名为rstest（随机抽样测试）的工具中实现了这种方法。为了证明它的可扩展性，我们将其应用于ArgoUML [1]，一个开源的基于UML的图形化软件设计环境。ArgoUML包含4 MB的类文件和7 MB的库（不包括标准的在相当短的时间内，我们发现了一个明显与并发相关的错误。实验描述见第7.4节。还需要做更多的工作来评估这种方法在大型系统中发现错误的有效性。我们还将其应用到一些较小的系统与已知的错误，这是很容易发现的rstest。[9]与[9]相似，[8]与[9]相似。我们在了解他们的工作之前，用了大约一个人月的时间设计和实现了rstest。ConTest是由IBM海法研究实验室的一个团队在过去的2到3年中开发的。当然，ConTest是一个更加成熟和全面的系统。例如，ConTest包含一个捕获和重放机制和一个死锁检测组件，并且它在调度功能中使用了一个新的覆盖度量。这些有用的功能目前还没有n.托勒144已在rstest中实现，但可以添加。我们的设计的一个显着特点是用于选择程序的克点调用调度功能插入的方法。与ConTest相比，它插入更少的调度函数调用，而不会降低发现广泛错误的概率，也不会损害概率完整性。概率完备性属性是：对于每个可达死锁和断言违反，调度函数都有一系列的选择导致了它。因此，通过测试转换后的程序来找到它的概率是非零的，即使在相同的运行时环境中通过测试原始程序来找到它的概率是零，这是由于该运行时环境中的特定线程调度程序。我们只假设线程调度器是公平的。 减少调度函数的调用次数有两个好处。首先，它减少了调用调度函数所导致的速度减慢。其次，它减少了反例中上下文切换的平均次数（即，其中发生错误的执行）。这使得反例更容易理解。我们设计的另一个特点是在调度函数中使用循环，而不是条件，这样一个调用就可以产生多个[2]在没有循环的情况下，如果yield用于引起上下文切换，那么该技术缺乏概率完整性。如果睡眠被用来引起欺骗-文本切换时，会出现类似的问题，并且可以通过使用循环或随机化睡眠持续时间来解决。许多模型检查器，包括Spin [18]和Java Pathquest [3]，都有一个随机测试模式，在功能上与rstest相似，但是在实现策略上的差异有着重大的实际后果：将Spin或Java Pathquest应用到ArgoUML大小的应用程序中需要大量的手动操作来开发系统的可管理抽象，而rstest可以很容易地应用。VeriSoft [12]和JavaServer [24]是执行系统无状态搜索的模型检查器[12]。它们在实现策略上与rstest相似：这三个工具都将对调度程序的调用插入到给定程序中。VeriSoft已成功应用于工业规模的系统（例如，，[13]）。VeriSoft旨在控制多进程系统中的非确定性。通常，识别进程间通信语句是简单的，并且在所有这些语句处插入对调度程序的调用是合理的。rstest的目标是（单进程）多线程程序。识别共享存储位置并不简单，在每次访问每个共享位置时插入对调度器的调用通常会比仅在我们的方法识别的位置插入这些调用引入更高的开销。JavaBean也针对多线程系统，但它更复杂，2最后一分钟注意：ConTest也这样做（Shmuel Ur，私人通信），尽管这在[9，8]中没有提到。n.托勒145比RSTEST更高的开销，因为它完全控制调度以便执行系统搜索。未来的工作很多。最重要的任务是完成第3节中描述的设计，将算法纳入调度功能，并进行更多的实验来评估该方法的有效性。在实践中，逻辑学[9，7，14]对于有效地发现大型系统中的错误至关重要。虽然我们当前的实现没有使用任何调度，但我们减少调度函数调用次数的方法与调度的使用是兼容的本文的其余部分组织如下。第2节提供Java字节码中同步的背景知识。第3节描述了如何选择插入调度函数调用的程序点。第4节讨论调度功能。第5节陈述了概率完备性。第6节介绍了执行情况。第7节描述了一些初步的实验结果。2Java字节码同步概述Java字节码中的基本同步操作基于监视器上的经典操作[20]。因此，Java中的每个对象隐式地包含一个唯一的锁和一个唯一的条件变量。 锁是递归的，即线程可以重新获取它持有的锁，并且如果每次获取都与释放匹配，则锁是空闲的monitorenter和monitorecenter是分别获取和释放与指定对象关联的锁的指令。对声明为synchronized的方法的调用隐式地获取与目标对象相关联的锁（即，这一论点）。退出这样的调用会隐式地释放锁。holdsLock（o）是一个静态本机方法，如果当前线程持有o的锁，则返回true这是JDK 1.4中的一个新特性wait、notify和notifyAll是Object的最终原生方法。它们被所有对 象 继 承 如 果 由 不 拥 有 目 标 对 象 的 锁 的 线 程 调 用 ， 则 抛 出IllegalSystemorStateException;否则，它们的行为如下。wait（）将调用线程t添加到o的等待集（即，等待O的线程集），释放O当另一个线程通知t时，t会争用重新获取o当t获取锁时，调用o.wait（）返回。o.notify（）在o的等待集中非确定性地选择线程t，从集合中移除t，并通知t ;如果o的等待集为空，则o .notify（）没有效果。 o.notifyAll（）从o的等待集中删除所有线程并通知它们。等待对象的线程t也可以通过调用t.interrupt（）来唤醒，其中interrupt是java.lang.Thread的一个方法。wait的有界时间变量是，如果等待线程在指定的时间间隔内没有得到通知，n.托勒1463在何处调用调度函数ConTest在所有并发事件中插入对调度函数的调用，根据定义，这些事件的顺序决定了程序的结果具体来说，所有同步操作（在第2节中描述），所有对象访问指令，以及所有getstatic和putstatic指令（读取和写入类的静态字段）都被视为并发事件。对象访问指令是getfield和putfield（读取和写入对象的实例字段）和数组访问指令（Java字节码有几条指令用于访问数组的元素;不同的指令用于不同类型的元素）。此外，ConTest静态分析可以直接用于减少对调度函数的插入调用的数量。例如，我们使用转义分析，并且在对对象的访问（根据分析）尚未从创建它们的线程转义时，不插入对调度函数的调用。 这并不会降低检测断言的可能性- 违规行为和僵局。为此，我们设计并实现了一个简单的逃逸分析;可以使用更复杂的逃逸分析，如[4，25]。本节的其余部分将描述一种更强大的方法，以减少对调度函数的插入调用的数量。 存储位置 被分类为非共享、受保护或不受保护（定义如下）。这为将操作分类为可见或不可见提供了基础。可见操作（类初始化除外）是ConTest并发事件的子集。对调度函数的调用被插入到可见操作之前 这是概率完备性的一个例子，在第5. 插入的调度函数调用较少，因为调用如下：(1) 未 插 入 在 monitoring 之 前 ， 从 synchronized 方 法 返 回 ， 或notifyAll，（2）仅插入在ConTest视为并发事件的其他指令的某些出现之前，以及（3）未插入在ConTest视为并发事件的任何指令之后这一办法只得到部分执行。我们当前的实现在第6节中描述。存储位置的分类。如果一个存储位置被最多一个线程访问，则该存储位置是非共享的。在Java中，所有变量（局部变量和参数）都是非共享的。堆位置（即，对象的实例字段）和静态位置（即，类的静态字段）可以是共享的或非共享的。如果（1）初始化后对x的每次访问都是读，或者（2）存在锁l，使得对于初始化后对x的每次访问，l在访问发生时由访问线程持有，则（堆或静态）位置x（由锁）受到保护“初始化”的定义n.托勒147位置X的初始化必须在多个线程对X的并发访问成为可能之前结束。具体来说，我们定义初始化如下。当对x的引用从分配x的线程中逃逸时，堆位置x的遍历结束。C类中的静态位置x（即，，x是C的静态字段）在C的类初始化器终止时结束。回想一下，JVM自动为类初始化提供同步，以确保在C的类初始化器终止之前，其他线程无法访问x[15，2.17节]。这种“保护”的定义未保护类别用于共享但不受保护的存储位置然而，任何位置都可以安全地归类为不受保护的，即。第5节中的概率完备性结果仍然成立。如将变得明显的，为了最小化对调度功能的调用的数量，位置应尽可能被分类为非共享或受保护Java的基本同步操作在下面的操作分类中被特别对待，所以上面的存储位置分类不适用于那些操作访问的存储位置（例如，、指示哪个线程持有对象的锁的位置业务分类一个操作是可见的，如果它（1）访问一个未受保护的位置，或（2）是一个潜在的阻塞同步操作或对Thread.interrupt的调用，或（3）是不确定的。可能访问未受保护位置的操作是对象访问指令、getstatic和putstatic。潜在阻塞的同步操作是monitorenter、同步方法的调用、两个等待操作（初始阻塞操作和在线程之后重新获取锁的操作已经被通知），以及可能隐式地导致类被初始化的操作（具体地，在类C未完全初始化的状态下，访问类C的所有操作都是可见的，即访问C的静态字段，调用C的静态方法，创建C的实例，以及调用java. lang. Class和java.lang.reflect中的某些方法）。非正式地说，类初始化是可见的，因为它涉及获取锁，即与类关联的锁 。 该 锁 保 护 包 含 类 的 初 始 化 状 态 的 共 享 存 储 位 置 （ 例 如 ， ,“initialization in progress by thread我们认为唯一不确定的操作是notify。notifyAll不可见而Thread.interrupt可见似乎令人惊讶，因为这两个操作都是确定性的，并且对 等待的线程。区别的根源在于，o.notifyAll只有在调用线程持有o的锁时才n.托勒148约束。在JDK1.4中新的同步原语Thread.holdsLock是不可见的.直观地说，这是因为其他线程的执行不能改变它的返回值。3.1转型通过将对象分类为上述三个类别来参数化变换。对象按其类型分类。具体地说，转换是由一个非共享类列表参数化的（即，，这些类的所有实例都被归类为非共享的）和受保护类的列表（即，这些类的所有实例都被归类为受保护的）。默认情况下，其他类被视为不受保护。第3.2节描述了如何获得这些列表。基于对象的这种分类，在每个可见操作之前插入对调度函数的调用。对于大多数字节码指令，很容易静态地确定指令是否执行可见操作。然而，由于动态方法分派，静态地确定调用指令是调用同步方法还是非同步方法是不可能的（通常）。3这不是一个大问题，因为插入在不可见操作之前调用调度函数是无害的，例如，除了开销 因此，在每个“invokevirtual C.m“指令之前插入对调度函数的调用类型签名。类似地，在每个“invokeinterface I.m“指令之前插入对调度函数的调用3.2获取对象对象的分类可以通过静态分析、运行时监视或两者的组合来获得。静态分析转义分析可以用来保守地确定哪些对象是非共享的。无竞争程序的类型系统[10，2]被设计成表明类型注释中指定的锁保护某些对象。类型系统的可靠性定理粗略地说，在一个良好类型的程序中，所有对象都是非共享或受保护的。 推广这个结果并不困难 声明，如果程序的某些部分是良好类型的，那么某些类（的所有实例）是非共享的或受保护的。3通过在每个同步方法的开始插入对调度函数的调用，而不是在调用位置，可以避免这种困难。但是对调度函数的调用发生在可见操作之后，而不是之前。这不满足第5节中概率完备性结果n.托勒149通常，用户提供类型注释，这些注释会被自动检查。通过精心选择的默认值和试错类型推断的组合，即使很少或没有手动提供类型注释，大多数程序通常也会通过类型检查器，允许许多非共享或受保护的类被分类为这样。运行时监控。运行时监控也可以用于通过迭代修正获得概率正确的分类。（正确性将在第5节中讨论。）初始分类可以是任意的;一个简单的选择是将所有类初始分类为非共享类。除了插入对调度函数的调用之外，程序被转换为检查分类的偏离，如下所述。如果在任何执行中发生违反分类的情况，则自动修改分类以消除它。涉及非共享类C的违反会导致C被重新分类为受保护类。涉及受保护类C的违规会导致C被重新归类为未受保护类。然后程序被重新转换，测试恢复。为了检查C类是否违反了非共享的分类，每个访问C类对象o的对象访问指令都被检测到对静态方法checkUnshared（o）的调用，该方法维护一个哈希映射firstAccessed，该映射将每个对象引用o映射到访问o的第一个线程。当第一次访问o时，在h中创建一个将o映射到Thread.currentThread（）的条目。对o的后续访问检查Thread.currentThread（ ） 是 否 等 于 firstAccessed.get （ o ） ; 如 果 不 等 于 ， 则 报 告 违 规 。firstAccessed 应 该 是 一 个 弱 散 列 映 射 （ 请 参 见 java.util.-WeakHashMap）;这意味着哈希映射中的o条目不会阻止被垃圾收集起来。它也应该是一个身份哈希映射（参见JDK 1.4中的java.util.IdentityHashMap）;这意味着在查找过程中，相等性测试是用==而不是equals完成的。依赖于equals是不合适的，也是危险的，因为应用程序员可以用任意代码覆盖它。要检查是否违反受保护类的分类，可以使用锁集算法[21]。它被设计用来检测数据竞争。它为每个对象o维护在执行期间到目前为止对o的所有访问中持有的锁的集合，不包括初始化期间的访问。为了适应我们对初始化的定义，转义分析用于确定何时可以从创建线程中转义对新创建对象的引用，并在适当的点插入代码以将锁集算法为对象维护的状态从初始化更改为初始化后。请注意，锁集算法只对被分类为受保护的类的实例运行。n.托勒150结合静态分析和运行时监控。无竞争程序的类型系统很有吸引力，因为它们在转换后的程序中不会产生运行时开销。然而，类型系统是不完整的（即，，程序可能包含类型检查器无法验证的受保护类），特别是在没有手动提供类型注释的情况下。这表明了以下混合方法。 使用类型系统（或其他静态分析）来识别一些绝对非共享或绝对受保护的类;运行时监视对于这些类是不必要的。使用基于运行时监控的迭代精化来获得剩余类的概率正确的分类3.3讨论使用静态分析来减少对调度函数的插入调用的数量似乎没有缺点。对于运行时监控，收益是否超过开销还不清楚。对于监视类是否是非共享的，答案更可能是肯定的，因为它的开销比锁集算法少得多。仅仅为了减少对调度函数的插入调用的数量而运行锁集算法是不值得的，但是锁集算法通常是出于其他原因运行的，在这种情况下，我们也可以利用它来达到这个目的。例如，ConTest包含一个竞赛检测组件[8，第3节]，并试图强制竞赛中涉及的操作以不同的顺序执行 在随后的处决中。4调度功能的设计Java的语义并不限制上下文切换后下一个运行的线程。因此，该方法的概率完整性要求对调度函数的调用具有将控制转移到每个可运行线程的非零概率。根据测试期间使用的JVM，对yield的单个调用可能无法实现这一点。例如，考虑一个有三个线程的程序。设a1、b1、a2和a3表示对共享存储位置的访问。让sched 1 a，sched 2等，表示对调度功能的调用（后缀不是实际呼叫的一部分;它们仅用于为每个呼叫站点提供不同的名称，以供下图使用）。主线程t1启动其他两个线程。他们的行动是：n.托勒151t2.startsched1ardy=[t2]B1sched3rdy=[t2]a1t3.startsched1brdy=[t3，t2]A3sched3rdy=[t2，t1]sched2rdy=[t1，t3]A2A1t3.startsched1brdy=[t3]sched2rdy=[t1]B1a1t3.startsched1brdy=[t3，t2]sched3rdy=[t2，t1]A3sched2sched2rdy=[t3]A2A3sched2rdy=[t1]A2 B1A2 B1rdy=[t3，t2]b1 a3B1sched3 a3sched3rdy=[t1]B1sched3 a3a2 rdy=[t2]a3 a2 a2 b1rdy=[]rdy=[t3]rdy=[t2]rdy=[t3] rdy=[t2]rdy=[]rdy=[t3]A2 A3a2 b1a2A3 A2a3 b1 a3a2a3 b1 a3Fig. 1.示例程序的可能调度，在JVM就绪列表的值显示在选定的点处。线程t1线程t2线程t3t2.startsched2sched3sched1aA2A3A1t3.startsched1bB1假设调度函数的每次调用都随机执行零次或一次yield调用。假设底层JVM的调度程序是循环的;因此，它维护一个准备运行的线程列表（“就绪列表”），当当前线程阻塞或用完其当前CPU时间量时，调度程序将当前线程放在列表的尾部并运行在列表的顶部的线程。 进一步假设调度器将新启动的线程放在就绪列表的头部，并且其调度量足够大，以至于在执行该短程序期间不会引起上下文切换。图1显示了在这些假设条件下该计划的所有可能的时间表。存在一种根据语言的语义是可能的但在这些假设下不能发生的调度，即，其中对共享位置的访问以a1、a2、a3、b1的顺序发生的调度。如果yield用于引起上下文切换，则避免此问题的一个简单方法是使用调度函数，其中对yield的调用在循环内，例如。、static java.util.Random prng=.;static float contextSwitchProb=.;public static void run（）{while（prng.nextFloat（）contextSwitchProb）Thread.yield（）;}n.托勒152其中prng是伪随机数生成器，并且contextSwitchProb是确定执行上下文切换的概率的参数。很容易看出，在添加这些循环之后，假设线程调度器是公平的，每个可运行线程都有非零的概率4成为下一个退出循环的线程。继续上面的示例，在a1和a2执行之后，t1可以第二次执行调度函数中的循环，从而执行允许a3在b1之前发生的附加上下文切换。如果使用休眠来引起上下文切换，则会出现类似的问题，并且可以通过使用循环或随机化休眠的持续时间5概率完全性下列结果是文[24]中约化定理的推论假设对象的分类是正确的（例如，通过静态分析确定）。考虑一个按照3.1节所述进行了变换的程序。对于每个可达死锁和断言违反，调度函数都有一系列选择导致它。这意味着通过测试转换后的程序发现它的概率假设静态分析不能保证对象分类的正确性。考虑一个如3.1节所述的程序，它包含对调度函数的调用，并监视违反分类的情况。概率完备性适用于发现错误分类以及死锁和断言违规。具体地说，如果存在一个违反分类的可达状态，那么调度函数会有一系列当一个错误的分类被发现，它应该被纠正，因为可能有其他的错误分类，将不会被发现，直到这样做，并重新转换程序这些结果仅依赖于调度函数引起的上下文切换。底层运行时系统的线程调度程序可能在任何时候引起额外的上下文切换。我们只假设线程调度器是公平的。这些结果不适用于（在转换之前）使用实时原语的程序，例如Thread.sleep，Thread的有限时间版本。系统.currentTimeMillis。实际上，将该工具应用于此类方案并不存在任何障碍。 这可能是有用的，如果开销不会太影响时间。 我们的设计减少了对调度函数的调用次数，从而减少了开销，使该方法对此类系统更有用4 通过对调度函数的这种简单改变，这些概率是不相等的。这是可以补救的，代价是一些并发症。n.托勒1536执行rstest是使用字节码工程库[6]作为字节码转换实现的。回想起来，Soot编译器基础设施[22]可能是更好的选择。Soot的中间表示比字节码更容易分析和操作。 例如，使用BCEL，插入对调度或监控函数的调用是一件麻烦的事，这些函数将被访问的对象作为参数，因为对该对象的引用不一定在访问之前的操作数堆栈的顶部（例如，对于同步方法的调用，其锁被获取的对象位于该方法的其他参数下面的操作数堆栈上）。使用Soot，添加这样的调用应该很容易。在当前的实现中，每个对象都必须被视为非共享或不受保护。我们的工具在可见的操作中插入对调度函数的调用（除了可能导致类初始化的操作;这仍然需要实现），并监视是否违反了对象的非共享分类。基于一个简单的转义分析，它通常避免在访问构造函数中的this参数时插入对调度函数的调用。支持将物体视为受保护的物体是今后的工作。我们计划为无竞争程序集成一个类型系统[2]，也许还有锁集算法（最简单的方法是在JavaPathExplorer中实现）。7实验结果对于每个应用程序，我们都将每个类视为非共享类。如果rstest发现违反了这一点，则将对象类重新分类为不受保护的。只转换了应用程序类，而不是Java运行时库中的类。除非另有说明，调度函数包含一个类似于第4节中所示的循环，除了使用sleep而不是yield，睡眠时间为1毫秒，上下文切换概率为1/8。大多数实验，包括所有报告运行时间的实验，都是在具有440 MHz UltraXP CPU的Sun Ultra 10上使用Sun JDK 1.3执行的;少数是在Windows XP上使用Sun JDK 1.3执行的。报告的运行时间是用户+系统时间，除非另有说明。“代码行”的计数7.1清洁Clean示例基于NASA的Remote Agent中的代码代码为57行，与[3，图1]中的代码大致相同。线程在无限循环中运行，反复交互，但在不恰当的时间切换上下文会导致死锁。没有rstest，就没有死锁n.托勒154发生在行刑的10分钟内 对于rstest，死锁发生在0.5秒（这是10次运行的平均值）。7.2基金经理基金经理的例子来自[19]。它涉及多个“基金经理”线程，重复在账户之间转移资金。这些转移不应改变资金总额。然而，如果在转账过程中发生了不恰当的上下文切换，钱可能会消失或被创造出来。代码是123行。我们对代码做了两个小的修改：我们将基金经理的数量从150个减少到2个，因为在进行压力测试之前，我们希望用一个小的配置进行测试和调试，我们删除了对Thread.setPriority的调用，它最初只是作为一个人工设备包含进来，以使错误更有可能出现。程序的每次执行都执行几千次传输。如果没有rstest，这个bug在10次执行中从未出现过。使用rstest时，bug在每次执行中都会多次出现。7.3Xtango动画库Xtango动画库[23]提供了绘制几何对象和文本以及移动它们的方法我们使用S。Hartley它附带了一个演示程序，该程序创建了两个圆c1和c2，并 调 用 exchangePosAsync （ c1 ， c2 ） ， 然 后 调 用 exchangePos（c1，c2）。这两种方法都通过在屏幕上滑动来使两个圆交换位置exchangePosAsync创建一个单独的线程来滑动它们，而原始线程继续执行下一个命令。exchangePos让调用线程完成工作。交换位置在概念上是一个对称操作，因此一个天真的用户可能只是写了exchangePos（c 2，c 1）作为第二个命令。这可能会导致死锁，因为exchangePos和exchangePosAsync都会锁定第一个参数，然后锁定第二个参数。我们对演示程序进行了此更改。在没有rstest的情况下，在200个执行中没有发生死锁。使用rstest，每17次执行就会发生一次死锁。在睡眠时间为1毫秒和2毫秒的情况下也得到了相同的结果我们还将rstest应用于Xtango附带的快速排序和用餐哲学的动画。 它们分别包含大约230和340行额外的代码。调度的扰动导致了快速排序动画中的一些暂时特性，快速排序绘制了一系列框，通常在绘制下一个框之前擦除每个框。使用rstest，擦除一个盒子的一个边缘有时会被延迟到下一个盒子被绘制之后。吃饭的哲学家表现正常。插入的代码对动画的速度有明显的影响。对于快速排序，经过时间（即，一次执行的时间从原始程序的大约7秒增加到了31秒，而在睡眠状态下则增加到了37秒n.托勒155时间分别为1和2毫秒。这些运行时间是为调用调度函数而转换的程序准备的，但不是为了监视违反非共享对象分类的情况。在Xtango和ArgoUML中，插入代码来监视违反非共享对象分类的行为导致了大约15%的速度下降7.4ArgoUMLArgoUML [1]是一个开源的基于UML的图形化软件设计环境。ArgoUML0.10的核心是4 MB的类文件，它使用GEF图形编辑框架（0.8 MB的类文件）和用于解析和数据交换的库（6 MB的类文件）。我们目前还没有合适的软件来捕获和重放用户输入，所以我们用半随机的手动输入测试了转换后的程序。我们在调度函数中使用了yield，因为yield比sleep造成的减速要小得多。首先，我们只转换了核心类。大约30分钟的输入只产生了一些警告消息，这些警告消息也出现在原始程序中。 不到5分钟的输入导致java.lang.ClassCastException：org.tigris.gef.presentation.FigRectat org.argouml.uml.diagram.static_structure.ui.FigClass.图结构eIn（FigClass.java：716）[省略了几行]在java.awt.EventDispatchThread.run（EventDispatchThread.java：85）ArgoUML捕获了异常并继续，尽管图形编辑窗口中的鼠标点击暂时不能正常工作。在对原始程序进行类似输入的大约30分钟内没有发生错误。这表明（但远不是结论性的），错误是由于rstest的扰动调度。为了进行更系统的实验，需要一种用于用户输入的捕获和重放机制。致谢。我感谢Han Li实现了rstest的大部分内容，Leena Unnikrishnan实现了逃逸分析，Shmuel Ur回答了关于ConTest的问题。引用[1] ArgoUML。 http://argouml.tigris.org。[2] 作者声明：Dr.里纳德一个用于无竞争Java程序的参数化类型系统。 在proc第16届ACM面向对象编程、系统、语言和应用会议（OOPSLA），SIGPLAN通告第36卷（11），第56-69页。ACM Press，November 2001.n.托勒156[3] Guillaume Brat，Klaus Havelund，Seung-Joon Park，and Willem Visser.模型 检 查 程 序 。 IEEEInternational Conference on Automated SoftwareEngineering（ASE），第3-12页[4] J. - D.崔，M。古普塔，M。Serrano、V. Sreedhar和S. Midki Java的转义分析ACM面向对象编程、系统、语言和应用会议（OOPSLA）ACM Press，October 1999.出现在ACM SIGPLAN Notices34（10）中。[5] 崔钟德和哈里尼·斯里尼瓦桑Java多线程应用程序的确定性重放。ACMSymposium on Parallel and Distributed Tools（SPDT），第48ACM Press，1998.[6] Markus达姆字节码工程库（BCEL）。http://bcel.sourceforge.net的网站。[7] Stefan Edelkamp，Alberto Lluch Lafuente，and Stefan Leue.使用HSF-SPIN进行定向显式模型检查。在Proc. 8th Int'l. SPIN软件模型检测研讨会，计算机科学讲义第2057卷，第57-79页。Springer-Verlag，2001年5月。[8] Orit Edelstein，Eitan Farchi，Evgeny Goldin，Yarden Nir，Gil Ratsaby，andShmuel Ur.测试多线程Java程序的框架，2002年。可从ur@il.ibm.com获得。这是一个扩展版本：ConTest -用户的角度来看。 2002年第五届软件质量国际会议论文集[9] Orit Edelstein，Eitan Farchi，Yarden Nir，Gil Ratsaby，and Shmuel Ur. 多线程Java程序测试生成。IBM Systems Journal，41（1），2002.[10] 科马克·弗拉纳根和斯蒂芬·弗罗因德。Java中基于类型的竞争检测。在Proc.ACM SIGPLAN编程语言设计和实现会议（PLDI）上，第219-232页。北京：人民出版社，2000年。[11] 科马克·弗拉纳根和斯蒂芬·弗罗因德。检测大型程序中的竞争条件。 软件工具和工程程序分析研讨会（PASTE），第90-96页。ACM Press，June2001.[12] 帕特里斯·戈德弗鲁德使用VeriSoft对编程语言进行模型检查在Proc.24thACM Symposium on Principles of Programming Languages （ POPL ），第174ACM Press，1997.[13] 放大图片作者：Robert S.汉默和拉丽塔·贾加德桑没有模型的模型检查：使用VeriSoft分析电话交换机的心跳监视器。ACM International Symposium onSoftware Testing and Analysis（ISSTA），第124-133页。ACM Press，1998.[14] 帕特里斯·戈德弗鲁德和萨尔弗拉兹·库尔希德使用遗传算法探索非常大的状态空间。在Proc. 8th Intl. Conf. on Tools and Algorithms for the Construction andAnalysis of Systems （ TACAS ） ， 卷 2280 计 算 机 科 学 讲 义 ， 页 266-280.Springer-Verlag，2002年4月。n.托勒157[15] 詹姆斯·高斯林、比尔·乔伊、盖伊·斯蒂尔和吉拉德·布拉查。Java语言规范。Addison Wesley，第2版，2000年。[16] 克劳斯·哈夫隆和托马斯·普莱斯伯格。使用Java Path对Java程序进行模型检查 。 International Journal on Software Tools for Technology Transfer ， 2（4），April 2000.[17] 克劳斯·哈夫隆和格里戈尔·罗苏。使用Java PathExplorer监视Java程序。在Proc. First Workshop on Verification（RVElsevier，2001年。[18] 杰拉德·J·霍尔茨曼。Spin模型检查器。IEEE软件工程学报，23（5）：279-295，1997年5月。[19] 2000 年 3 月 28 日 的 Java 开 发 人 员 连 接 技 术 提 示 。http://developer.java.sun.com/developer/TechTips/2000/tt0328.html 的 网站。[20] 巴 特 勒 ·W Lampson 和 David D. 雷 德 尔 在 Mesa 有 工 艺 和 监 控 经 验 。Communications of the ACM，23（2）：106[21] Stefan Savage、Michael Burrows、Greg Nelson、Patrick Sobalvarro和ThomasE.安德森Eraser：多线程程序的动态数据竞争检测器。ACM Transactions onComputer Systems，15（4）：391-411，1997年11月。[22] 煤烟 http://www.sable.mcgill.ca/soot/。[23] 约翰T.斯塔斯科动画算法与XTANGO。SIGACTNews，23（ 2 ） ： 67-71 ， 1992.S. Hartley 的 Java 版 本 可 以 在 http ：//www.mcs.drexel.edu/jumsha