簡述
本文將會介紹 JMCR 中約束求解的算法。
提綱
- 約束求解的定義
- 約束求解的目的
- JMCR 中基本的概念
- JMCR 中約束的實(shí)現(xiàn)
本文中的圖片和文字參考于源碼在 github Readme中提供的論文囊咏。本文僅供學(xué)習(xí)參考使用倘核，如有侵權(quán)，請聯(lián)系刪除栈拖。
系列文章：
1. JMCR 簡介
2. JMCR 字節(jié)碼插樁（一）
3. JMCR 字節(jié)碼插樁（二）
4. JMCR 約束求解原理
5. JMCR 線程調(diào)度
一趾盐、什么是約束求解
約束求解是通過一個(gè)已知的程序運(yùn)行記錄（以下簡稱 trace）搬泥，生成約束并通過 smt 求解技術(shù)得出新的線程可行的調(diào)度序列的過程辅搬。
二唯沮、約束求解的目標(biāo)
回顧一下在 JMCR 學(xué)習(xí)筆記 中的內(nèi)容
如果要測試多線程的程序，我們需要 “多跑幾遍”堪遂，將程序中所有可能的操作序列復(fù)現(xiàn)一遍介蛉，看看是否可以觸發(fā)錯(cuò)誤，這樣才能保證我們的測試不會漏過每一種可能溶褪。隨之而來的問題是币旧，如何計(jì)算出來所有可能的操作集合序列？對于每一次執(zhí)行猿妈，怎么驅(qū)動(dòng)程序按照制定操作序列進(jìn)行調(diào)度吹菱，又如對于多線程程序爆炸性增長的探索空間進(jìn)行剪枝呢？
首先于游，為了保證測試的 completeness 毁葱，要覆蓋程序過程中每一個(gè)可能的狀態(tài)。其次贰剥，由于多線程程序的測試具有隨著測試規(guī)模增長而爆炸性增長的趨勢，對于不合法的和冗余的測試樣例在約束階段就刪除掉筷频，提高測試程序的運(yùn)行效率
三蚌成、一些基本的概念
- trace：程序調(diào)度序列前痘，由一系列 event 組成。
- event：多線程程序中發(fā)生的事件担忧，包括：
- begin(t)/end(t)：線程 t 中的第一個(gè)/最后一個(gè)事件
- read(t, x, v)/write(t, x, v)：線程 t 讀到/寫變量 x 值為 v
- lock(t, l)/unlock(t, l)：線程 t 獲取/釋放鎖 l
- fork(t, t')：線程 t 創(chuàng)建新線程 t'
- join(t, t')：線程 t 阻塞直到 t' 運(yùn)行結(jié)束
運(yùn)行程序芹缔，通過之前提到過的字節(jié)碼插裝技術(shù)，我們可以獲取到整個(gè)測試程序中的變量瓶盛、線程以及trace 信息最欠。
四、約束
程序中每一行都是一個(gè) event惩猫，我們對其進(jìn)行了標(biāo)號芝硬，在本小節(jié)將對以下程序增加約束來產(chǎn)生新的調(diào)度序列
（一）保證生成合法的調(diào)度序列
合法在這里有三個(gè)部分：讀一致性、鎖互斥以及 Must Happens-Before 原則轧房。
- 讀一致性
A read event contains the value written
by the most recent write event on the same memory location.
指的是每一個(gè) read(t, x, v0) 事件和之前距離其最近的 write(t, x, v1) 事件拌阴，v0 = v1。
2.鎖互斥原則
Each release event is preceded by an acquire event on the same lock by the same thread, and each pair is not interleaved by any other acquire or release event on the same lock
每個(gè) unlock(t, l) 事件之前都應(yīng)該有一個(gè) lock(t, l) 事件奶镶，且兩個(gè)不同線程對于同一個(gè)鎖 l 的 lock unlock 對之間不能有交錯(cuò)的時(shí)間序列迟赃。
- Must Happens-Before 原則
A begin event can happen only as a first event in a thread and only after the thread is forked by another thread. An end event can happen only as the last event in a thread, and a join event can happen only after the end event of the joined thread.
begin 事件只能作為線程中的第一個(gè)事件發(fā)生，并且只能在該線程被另一個(gè)線程 fork 之后發(fā)生厂镇。 end 事件只能作為線程中的最后一個(gè)事件發(fā)生纤壁，而 join 事件只能在被 join 線程的 end 事件之后發(fā)生。
線程內(nèi)串行
對于線程內(nèi)的事件順序捺信，序號為n的事件一定 happens-before 于序號 n+1 的事件摄乒。線程間的順序以及 happens-before 傳遞性
這里借用了 Lamport 算法思想：因?yàn)閎egin 事件只能在該線程被另一個(gè)線程 fork 之后發(fā)生。所以 fork 是因残黑，begin是果馍佑。而 end 事件只能在被 join 線程的 end 事件之后發(fā)生，所以 end 是因梨水，join 是果拭荤。而每個(gè)線程內(nèi)的事件可以把前一個(gè)事件作為因，后面的是果疫诽， 這樣一來舅世，我們可以參照分布式系統(tǒng)因果一致性，來對于程序的線程之間的通信（fork奇徒、start雏亚、end、join）進(jìn)行建模摩钙。而因果關(guān)系是具有傳遞性的罢低，同樣的happens-before 也具有傳遞性。
（二）程序狀態(tài)模型
來給程序執(zhí)行的過程建立一個(gè)模型：
- 程序狀態(tài)：
程序的狀態(tài)是由當(dāng)前的所有線程的局部變量和所有線程的共享的全局變量的集合。特別的网持，每個(gè)線程的 pc 計(jì)數(shù)器也是局部變量的一部分宜岛。 -
程序執(zhí)行：
程序執(zhí)行的過程就是程序從初始狀態(tài)經(jīng)過一系列的事件，也就是 trace功舀，程序的狀態(tài)狀態(tài)不斷地變化的一個(gè)過程萍倡。
程序執(zhí)行模型
當(dāng)一個(gè)事件的操作對象是局部變量的時(shí)候，取決于當(dāng)前程序的狀態(tài)辟汰，事件所在線程的局部變量到達(dá)了一個(gè)新的狀態(tài)列敲，而不會改變?nèi)肿兞浚欢?dāng)一個(gè)時(shí)間的操作對象是全局變量 s 的時(shí)候帖汞，取決于當(dāng)前程序的狀態(tài)戴而，s 和事件所在線程的局部狀態(tài)會發(fā)生改變。
（三） Race 約束
基于之前的程序狀
態(tài)模型和之前提出的程序合法性涨冀。
不同的程序狀態(tài)會導(dǎo)致程序中某些直接判斷語句if 和間接判斷 (例如全局變量 x 作為數(shù)組的下標(biāo)) 產(chǎn)生不一樣的新的程序狀態(tài)填硕。所以，我們的目標(biāo)就是探究所有可能的程序狀態(tài)序列鹿鳖。提出了 Race 約束
定義：COP(a,b) 是不同線程中對于同一個(gè)全局變量的讀-寫對扁眯。
對于每一個(gè)存在 COP 的變量，對于該變量的每一個(gè)讀事件R翅帜，定義以下約束：
- 所有 happens-before 于
R的讀事件讀到和之前一樣的值 - 讀事件
R讀到和之前不一樣的值姻檀。
以下面這個(gè)程序?yàn)槔?/p>
圖中的每一個(gè)線程中的代碼都會循環(huán)兩次執(zhí)行，給出了事件的編號涝滴，以及事件在 trace 中的表示方法绣版，其中 中上標(biāo)
表示的是第幾次循環(huán)，而下標(biāo)
給出的是在圖中的行號(1-14)歼疮。
假設(shè)我們第一次運(yùn)行中讀寫的狀態(tài)如圖：
這個(gè)圖的含義為：第一個(gè)黑點(diǎn)表示 T2 線程中第八行第一次循環(huán)
if(x>0) 讀到的值是 T2 線程第一次循環(huán)第六行寫 x = 0 的值杂抽。第二個(gè)黑點(diǎn)表示T2 線程第二次循環(huán)中第八行 if(x>0) 讀到的值是 T2 線程第二次循環(huán)第六行寫 x = 0 的值。后面兩個(gè)黑點(diǎn)表示 T3 線程第一次循環(huán)和第二次循環(huán)中第十一行 if(x>1) 都是讀到的T2 線程第二次循環(huán)第六行寫 x = 0 的值韩脏。同時(shí)缩麸，由于兩次 T3 中 if(x>1) 的判斷結(jié)
果都是false，因此沒有對于 y 的讀時(shí)間赡矢，y 的讀寫表為空杭朱。
接下來對于，添加 Race 約束吹散，使
讀到一個(gè)與之前不同的值 1弧械。并保證所有 happens-before 于這個(gè)事件的讀事件（此處為空集合）都可以讀到。運(yùn)行的程序可得到以下的讀寫表空民。
不斷讀到一個(gè)新值刃唐，可以獲得一顆樹。
這顆樹便覆蓋了程序中所有可能的程序狀態(tài)。
（四）示例的約束求解：
- 鎖互斥
- Must Happens-Before 與線程內(nèi)串行
- Race 約束（滿足其中之一即可）
使第八行的讀到 0
或
使第十行的讀到 0
通過這一系列約束唁桩，我們可以通過 z3 來進(jìn)行求解闭树，得到新的事件順序（這里滿足了 Race 約束中的第二個(gè)）：
轉(zhuǎn)換到線程耸棒，我們也得到了一個(gè)調(diào)度序列前綴：
