本系列記錄了我研究JMCR的學(xué)習(xí)筆記和一些自己的想法偿曙，JMCR 是一個(gè)多線程測(cè)試工具的實(shí)現(xiàn)，其源代碼地址為：鏈接屋讶。歡迎大家一起探討交流~
系列文章：
1. JMCR 簡(jiǎn)介
2. JMCR 字節(jié)碼插樁（一）
3. JMCR 字節(jié)碼插樁（二）
4. JMCR 約束求解原理
5. JMCR 線程調(diào)度

簡(jiǎn)述

本文介紹了多線程測(cè)試相關(guān)概念辞友、JMCR 的簡(jiǎn)介和 JMCR 的使用。

一溃睹、多線程測(cè)試

多線程程序的錯(cuò)誤往往是不易被發(fā)現(xiàn)的而账。而每當(dāng)我們想復(fù)現(xiàn)這個(gè)錯(cuò)誤的時(shí)候，我們重新運(yùn)行這個(gè)程序或者使用 JUnit 框架進(jìn)行測(cè)試因篇，這個(gè)錯(cuò)誤往往又會(huì)消失不見(jiàn)（或者概率性出現(xiàn)）泞辐。因此我們需要一個(gè)工具來(lái)幫我們排查多線程程序中的錯(cuò)誤笔横。

多線程程序測(cè)試區(qū)別于單線程程序測(cè)試的地方是，如果我們將一個(gè)程序的運(yùn)行過(guò)程抽象成操作的序列的話咐吼，單線程程序中的每個(gè)操作（包括操作的類型吹缔、操作的值）以及操作的順序是確定的，而多線程程序由于線程調(diào)度的不確定性以及可見(jiàn)性等問(wèn)題锯茄，其操作序列幾乎總是在變化的厢塘。例如，對(duì)于單線程程序1來(lái)講肌幽，其操作序列總是 [(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
    }
}

但是對(duì)于多線程而言晚碾，就沒(méi)有這么簡(jiǎn)單了，對(duì)于如下的程序喂急，其操作序列就是不確定的格嘁，并且有一定的概率觸發(fā)錯(cuò)誤 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 兩個(gè)操作由于調(diào)度的不確定性廊移，其先后順序是無(wú)法確定的糕簿，當(dāng) Operation 2 (Read, a, 0) 發(fā)生在 Operation 1 (Write, a, 1) 之前時(shí)，if 語(yǔ)句進(jìn)入了第一個(gè)分支狡孔，執(zhí)行 (Write, b 2 )懂诗，再執(zhí)行 Operation 3 和 Operation 4；而當(dāng) Operation 1 (Write, a, 1) 發(fā)生在 Operation 2 (Read, a, 1) 之前時(shí)苗膝，if 語(yǔ)句進(jìn)入了第二個(gè)分支殃恒，出發(fā)了錯(cuò)誤，程序輸出錯(cuò)誤信息荚醒，調(diào)用System.exit()芋类，此時(shí)程序崩潰，操作序列中也不會(huì)出現(xiàn) Operation 4界阁。

從上面這個(gè)例子可以看出侯繁，如果要測(cè)試多線程的程序，我們需要“多跑幾遍”，將程序中所有可能的操作序列復(fù)現(xiàn)一遍，看看是否可以觸發(fā)錯(cuò)誤失尖，這樣才能保證我們的測(cè)試不會(huì)漏過(guò)每一種可能。隨之而來(lái)的問(wèn)題是咕别，如何計(jì)算出來(lái)所有可能的操作集合序列？對(duì)于每一次執(zhí)行写穴，怎么驅(qū)動(dòng)程序按照制定操作序列進(jìn)行調(diào)度惰拱，又如對(duì)于多線程程序爆炸性增長(zhǎng)的探索空間進(jìn)行剪枝呢？

How can we do that in Java啊送？—— By JMCR

二偿短、JMCR簡(jiǎn)介

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 是一個(gè)使用高效約簡(jiǎn)算法的無(wú)狀態(tài)的模型測(cè)試工具欣孤。它通過(guò)記錄程序運(yùn)行時(shí)的事件序列并在記錄上構(gòu)建新序列的約束，系統(tǒng)的探索了程序的整個(gè)狀態(tài)空間昔逗。JMCR捕獲寫操作和讀操作的值以去除冗余探索降传。 通過(guò)強(qiáng)制執(zhí)行至少一個(gè)讀操作返回不同的值，它會(huì)生成一個(gè)新的調(diào)度序列勾怒，該調(diào)度序列將驅(qū)動(dòng)程序達(dá)到新的狀態(tài)婆排。

從這份 JMCR 在 Readme 中的簡(jiǎn)短描述，以上提出的幾個(gè)問(wèn)題已經(jīng)初見(jiàn)端倪笔链，同時(shí)也了解到了 JMCR 主要工作可以分為以下三個(gè)部分：

• 程序運(yùn)行時(shí)的操作序列 (trace) 信息捕獲
• 通過(guò)一個(gè)現(xiàn)有的操作序列生成一個(gè)新的操作序列的約束段只，并通過(guò)約束生成新的操作序列信息（線程調(diào)度序列前綴）

• 使程序按照新的（線程調(diào)度）序列執(zhí)行循環(huán)直至不再產(chǎn)生新的狀態(tài)空間序列。

這些內(nèi)容都會(huì)在隨后的文章中有詳細(xì)講解卡乾，此處不再展開(kāi)翼悴。總而言之幔妨，JMCR可以幫我們探尋一個(gè)多線程程序內(nèi)所有的狀態(tài)空間，作為我們多線程測(cè)試的工具谍椅。

三误堡、JMCR 的使用

首先我們需要去 GitHub 上將 JMCR 的源代碼拉到本地，使用 Intelij IDEA 導(dǎo)入功能打開(kāi)這個(gè)項(xiàng)目

使用 Import Project 打開(kāi)項(xiàng)目

pom.xml

文件

隨后點(diǎn)擊 EditConfigure 配置參數(shù)悉抵，為 JUnit 項(xiàng)目添加 vm參數(shù) -ea -javaagent:../libs/agent.jar

vm 參數(shù)配置

運(yùn)行 mcr-test 模塊下 src 中的 TestDeadLock.java 測(cè)試可以得到以下輸出：

或者我們可以自己寫自己的多線程測(cè)試樣例：

1. 在測(cè)試類上加上注解 @RunWith(JUnit4MCRRunner.class)
2. 像 JUnit 一樣編寫測(cè)試樣例

代碼如下：

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
    }
}

運(yùn)行結(jié)果：

TIM截圖20191106002324.png

可以看到，程序執(zhí)行了兩次摘完，覆蓋到了我們提到的兩種情況姥饰，使用成功~