JMCR 简介

作者: 毒死预言家的女巫 | 来源:发表于2019-11-06 00:18 被阅读0次

    本系列记录了我研究JMCR的学习笔记和一些自己的想法,JMCR 是一个多线程测试工具的实现,其源代码地址为:链接。欢迎大家一起探讨交流~
    系列文章:
    1. JMCR 简介
    2. JMCR 字节码插桩(一)
    3. JMCR 字节码插桩(二)
    4. JMCR 约束求解原理
    5. JMCR 线程调度

    简述

    本文介绍了多线程测试相关概念、JMCR 的简介和 JMCR 的使用。

    一、多线程测试

    多线程程序的错误往往是不易被发现的。而每当我们想复现这个错误的时候,我们重新运行这个程序或者使用 JUnit 框架进行测试,这个错误往往又会消失不见(或者概率性出现)。因此我们需要一个工具来帮我们排查多线程程序中的错误。

    多线程程序测试区别于单线程程序测试的地方是,如果我们将一个程序的运行过程抽象成操作的序列的话,单线程程序中的每个操作(包括操作的类型、操作的值)以及操作的顺序是确定的,而多线程程序由于线程调度的不确定性以及可见性等问题,其操作序列几乎总是在变化的。例如,对于单线程程序1来讲,其操作序列总是 [(Read, a, 0), (Write, b, 2), (Read, b, 2)]

    单线程程序1:

    public class Test {
        static int a = 0;
        static int b = 1;
        public static void main(String []args){
            if(a == 0){ //Read  a 0
                b = 2;   //Write b 2   
            }  else {
                System.err.println("Error! Read a != 0");
                System.exit(-1);
            }
            System.out.println(b); // Read b 2
        }
    }
    

    但是对于多线程而言,就没有这么简单了,对于如下的程序,其操作序列就是不确定的,并且有一定的概率触发错误 case。

    多线程程序1:

    public class Test {
        static int a = 0;
        static int b = 1;
        public static void main(String []args) throws InterruptedException {
            new Thread(new Runnable() {
                @Override
                public void run() {
                    try {
                        Thread.sleep(10);
                    } catch (InterruptedException e) {
                        e.printStackTrace();
                    }
                    //Operation 1
                    a = 1; //Write a 1 
                }
            }).start();
            Thread.sleep(10);
            //Operation 2
            if(a == 0){ //Read  a ?
                //Operation 3
                b = 2;   //Write b 2
            } else {
                System.err.println("Error! Read a != 0");
                System.exit(-1);
            }
            //Operation 4
            System.out.println(b); // Read b 2
        }
    }
    

    上述代码中 Operation 1 和 Operation 2 两个操作由于调度的不确定性,其先后顺序是无法确定的,当 Operation 2 (Read, a, 0) 发生在 Operation 1 (Write, a, 1) 之前时,if 语句进入了第一个分支,执行 (Write, b 2 ),再执行 Operation 3 和 Operation 4;而当 Operation 1 (Write, a, 1) 发生在 Operation 2 (Read, a, 1) 之前时,if 语句进入了第二个分支,出发了错误,程序输出错误信息,调用System.exit(),此时程序崩溃,操作序列中也不会出现 Operation 4。

    从上面这个例子可以看出,如果要测试多线程的程序,我们需要“多跑几遍”,将程序中所有可能的操作序列复现一遍,看看是否可以触发错误,这样才能保证我们的测试不会漏过每一种可能。随之而来的问题是,如何计算出来所有可能的操作集合序列?对于每一次执行,怎么驱动程序按照制定操作序列进行调度,又如对于多线程程序爆炸性增长的探索空间进行剪枝呢?

    How can we do that in Java?—— By JMCR

    二、JMCR简介

    Maximal-Causality-Reduction (MCR) Java version
    MCR is a stateless model checker powered by an efficient reduction algorithm. It systematically explores the state-space of the program by collecting runtime traces of the program executions and constructing ordering constraints over the traces to generate other possible schedules. It captures the values of the writes and reads to prune redundant explorations. By enforcing at least one read to return a different value, it generates a new schedule which drives the program to reach a new state.

    JMCR 是一个使用高效约简算法的无状态的模型测试工具。它通过记录程序运行时的事件序列并在记录上构建新序列的约束,系统的探索了程序的整个状态空间。JMCR捕获写操作和读操作的值以去除冗余探索。 通过强制执行至少一个读操作返回不同的值,它会生成一个新的调度序列,该调度序列将驱动程序达到新的状态。

    从这份 JMCR 在 Readme 中的简短描述,以上提出的几个问题已经初见端倪,同时也了解到了 JMCR 主要工作可以分为以下三个部分:

    • 程序运行时的操作序列 (trace) 信息捕获
    • 通过一个现有的操作序列生成一个新的操作序列的约束,并通过约束生成新的操作序列信息(线程调度序列前缀)
    • 使程序按照新的(线程调度)序列执行循环直至不再产生新的状态空间序列。

    这些内容都会在随后的文章中有详细讲解,此处不再展开。总而言之,JMCR可以帮我们探寻一个多线程程序内所有的状态空间,作为我们多线程测试的工具。

    三、JMCR 的使用

    首先我们需要去 GitHub 上将 JMCR 的源代码拉到本地,使用 Intelij IDEA 导入功能打开这个项目

    使用 Import Project 打开项目
    随后点击项目根目录下的pom.xml进行导入。
    pom.xml
    随后一路确认,进入项目后,将根目录下的 default.properties 文件拷贝到 mcr-test 模块下的 \target\classes 文件夹内。 文件

    随后点击 EditConfigure 配置参数,为 JUnit 项目添加 vm参数 -ea -javaagent:../libs/agent.jar

    vm 参数配置

    运行 mcr-test 模块下 src 中的 TestDeadLock.java 测试可以得到以下输出:


    或者我们可以自己写自己的多线程测试样例:

    1. 在测试类上加上注解 @RunWith(JUnit4MCRRunner.class)
    2. 像 JUnit 一样编写测试样例

    代码如下:

    package edu.tamu.aser.tests;
    
    import edu.tamu.aser.reex.JUnit4MCRRunner;
    import org.junit.Test;
    import org.junit.runner.RunWith;
    
    
    @RunWith(JUnit4MCRRunner.class)
    public class MyTest {
        static int a = 0;
        static int b = 1;
    
        @Test
        public void test() throws InterruptedException {
            new Thread(new Runnable() {
                @Override
                public void run() {
                    try {
                        Thread.sleep(10);
                    } catch (InterruptedException e) {
                        e.printStackTrace();
                    }
                    a = 1;
                    System.out.println("b : " + b);
                }
            }).start();
            Thread.sleep(10);
            if(a == 0){ //Read  a 0
                b = 2;   //Write b 2
            } else {
                System.err.println("Error! Read a != 0");
                System.exit(-1);
            }
            System.out.println(b); // Read b 2
        }
    }
    

    运行结果:


    TIM截图20191106002324.png

    可以看到,程序执行了两次,覆盖到了我们提到的两种情况,使用成功~

    相关文章

      网友评论

        本文标题:JMCR 简介

        本文链接:https://www.haomeiwen.com/subject/gnnebctx.html