JMCR 简介

本系列记录了我研究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

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

最后编辑于
©著作权归作者所有,转载或内容合作请联系作者
  • 序言:七十年代末,一起剥皮案震惊了整个滨河市,随后出现的几起案子,更是在滨河造成了极大的恐慌,老刑警刘岩,带你破解...
    沈念sama阅读 204,732评论 6 478
  • 序言:滨河连续发生了三起死亡事件,死亡现场离奇诡异,居然都是意外死亡,警方通过查阅死者的电脑和手机,发现死者居然都...
    沈念sama阅读 87,496评论 2 381
  • 文/潘晓璐 我一进店门,熙熙楼的掌柜王于贵愁眉苦脸地迎上来,“玉大人,你说我怎么就摊上这事。” “怎么了?”我有些...
    开封第一讲书人阅读 151,264评论 0 338
  • 文/不坏的土叔 我叫张陵,是天一观的道长。 经常有香客问我,道长,这世上最难降的妖魔是什么? 我笑而不...
    开封第一讲书人阅读 54,807评论 1 277
  • 正文 为了忘掉前任,我火速办了婚礼,结果婚礼上,老公的妹妹穿的比我还像新娘。我一直安慰自己,他们只是感情好,可当我...
    茶点故事阅读 63,806评论 5 368
  • 文/花漫 我一把揭开白布。 她就那样静静地躺着,像睡着了一般。 火红的嫁衣衬着肌肤如雪。 梳的纹丝不乱的头发上,一...
    开封第一讲书人阅读 48,675评论 1 281
  • 那天,我揣着相机与录音,去河边找鬼。 笑死,一个胖子当着我的面吹牛,可吹牛的内容都是我干的。 我是一名探鬼主播,决...
    沈念sama阅读 38,029评论 3 399
  • 文/苍兰香墨 我猛地睁开眼,长吁一口气:“原来是场噩梦啊……” “哼!你这毒妇竟也来了?” 一声冷哼从身侧响起,我...
    开封第一讲书人阅读 36,683评论 0 258
  • 序言:老挝万荣一对情侣失踪,失踪者是张志新(化名)和其女友刘颖,没想到半个月后,有当地人在树林里发现了一具尸体,经...
    沈念sama阅读 41,704评论 1 299
  • 正文 独居荒郊野岭守林人离奇死亡,尸身上长有42处带血的脓包…… 初始之章·张勋 以下内容为张勋视角 年9月15日...
    茶点故事阅读 35,666评论 2 321
  • 正文 我和宋清朗相恋三年,在试婚纱的时候发现自己被绿了。 大学时的朋友给我发了我未婚夫和他白月光在一起吃饭的照片。...
    茶点故事阅读 37,773评论 1 332
  • 序言:一个原本活蹦乱跳的男人离奇死亡,死状恐怖,灵堂内的尸体忽然破棺而出,到底是诈尸还是另有隐情,我是刑警宁泽,带...
    沈念sama阅读 33,413评论 4 321
  • 正文 年R本政府宣布,位于F岛的核电站,受9级特大地震影响,放射性物质发生泄漏。R本人自食恶果不足惜,却给世界环境...
    茶点故事阅读 39,016评论 3 307
  • 文/蒙蒙 一、第九天 我趴在偏房一处隐蔽的房顶上张望。 院中可真热闹,春花似锦、人声如沸。这庄子的主人今日做“春日...
    开封第一讲书人阅读 29,978评论 0 19
  • 文/苍兰香墨 我抬头看了看天上的太阳。三九已至,却和暖如春,着一层夹袄步出监牢的瞬间,已是汗流浃背。 一阵脚步声响...
    开封第一讲书人阅读 31,204评论 1 260
  • 我被黑心中介骗来泰国打工, 没想到刚下飞机就差点儿被人妖公主榨干…… 1. 我叫王不留,地道东北人。 一个月前我还...
    沈念sama阅读 45,083评论 2 350
  • 正文 我出身青楼,却偏偏与公主长得像,于是被迫代替她去往敌国和亲。 传闻我的和亲对象是个残疾皇子,可洞房花烛夜当晚...
    茶点故事阅读 42,503评论 2 343

推荐阅读更多精彩内容