Go訊息傳遞併發

阿新 • • 發佈：2020-11-04

1.併發缺陷的型別

Go語言基於訊息傳遞機制的併發缺陷大概分為三種：

1.1通道安全性有關的併發缺陷

當一個通道被關閉後，可以任意的向其讀取資料而不會報錯（當通道為空時候會返回通道資料型別對應的0值而不是錯誤,如List 1所示），但是向一個已關閉的通道中傳送資料或者重複關閉已經關閉的通道會引發安全性錯誤（List 2和List 3），這部分併發錯誤在實際的應用程式中幾乎不可能出現，也不是我們研究的重點。

package main

import "fmt"

func main() {
	ch1 := make(chan int,10)
	go func() {
		a:=1
		ch1 <- a
		close(ch1)
	}()
	fmt.Println(<-ch1)
	fmt.Println(<-ch1)
}

1
0

List 1 向已關閉的通道讀取資料程式碼及執行結果

package main
func main() {
	ch1 := make(chan int,10)
	go func() {
		a:=1
		ch1 <- a
		close(ch1)
	}()
	ch1 <- 2
}

panic: send on closed channel

goroutine 1 [running]:
main.main()
        /home/gopath/src/migoinferDemo/demo01.go:14 +0x198

List 2 向已關閉通道中傳送資料

package main

import "time"

func main() {
	ch1 := make(chan int,10)
	go func() {
		a:=1
		ch1 <- a
		close(ch1)
		close(ch1)
	}()
	time.Sleep(time.Second)
}

panic: close of closed channel

goroutine 17 [running]:
main.main.func1(0xc000128000)
        /home/gopath/src/migoinferDemo/demo01.go:11 +0x5a
created by main.main
        /home/gopath/src/migoinferDemo/demo01.go:7 +0x4e

List 3 關閉已關閉的通道

1.2全域性死鎖

如果一個程式在執行的過程中所有goroutine都被阻塞從而引發死鎖，我們就稱之為全域性死鎖，Go語言本身就提供了一個全域性死鎖檢測工具以避免類似情況，然而在實際應用中，一部分Go語言的庫（如net庫）會暫時關閉這個檢測工具從而導致全域性死鎖的發生。

1.3區域性死鎖

區域性死鎖（或者被稱為failure of liveness，具體後面會提到）與全域性死鎖對應，也就是在程式中某些goroutine還能夠正常工作時程式因為某些錯誤發生了死鎖，一個簡單的區域性死鎖例項如List 4所示：

package main

func prod(ch chan int) {
	for i := 0; i < 5; i++ {
		ch <- i // 向ch中傳送資料
	}
	close(ch) // 關閉通道ch
}
func cons(ch1, ch2 chan int) {
	for {
		select {
		case x := <-ch1:
			print(x) // 讀取ch1中的資料
		case x := <-ch2:
			print(x) // 讀取ch2中的資料
		}
	}
}
func main() {
	ch1, ch2 := make(chan int), make(chan int)
	go prod(ch1)
	go prod(ch2)
	cons(ch1, ch1)
}

List 4 區域性死鎖例項

在List 4中的程式碼中，cons方法中select語句表示無傾向的隨機選擇，倒數第二行中由於筆誤使得ch1在cons的引數中出現了兩次，從而使得倒數第三行中"go prod(ch2)"語句中呼叫新goroutine向ch2中傳遞資料操作的結果沒能與cons方法連線起來(實際執行後結果為無限增加的0值），從而破壞了程式的liveness，在這個程式執行過程中不是所有goroutine都被阻塞了，這就是區域性死鎖。

區域性死鎖就是我們研究的重點問題。

lange等人在Go併發缺陷靜態分析方面做了很多工作，他們最新的成果是Godel Checker，該工具的工作流圖為：

2.1對Go語言原始碼進行分析

嘗試使用靜態分析方法對於Go語言併發相關語句進行行為分析，如下：

使用上面型別對List 4中的程式碼進行分析後的結果為：

第一行是對於prod方法的分析，也就是包含一個向通道傳送資料的行為，然後是傳送行為和通道關閉的選擇（傳送行為結束後關閉通道）。

第二行是對於cons方法的分析，包括一個select語句，滿足某一條件就執行對應的語句。

第三行是main函式分析，包含兩個建立通道操作以及三個併發的呼叫方法操作。

對於Go語言原始碼的直接分析看上去能夠對於程式的Liveness進行判斷，然而在實際應用中由於各種不同的輸入或者條件會導致分析的結果unsound。為了解決這個問題，當前的研究大多是從Go語言中間程式碼入手（主要是SSA,static single assignment靜態單賦值），《Fencing off Go:
Liveness and Safety for Channel-Based Programming》中使用Go標準庫中的ssa包將Go原始碼轉換為靜態單賦值（SSA)中間表示（IR),然後從SSA塊中提取通訊結構作為行為型別。該論文中提出了一個名為MiGo的表現形式，具體如圖1所示：

圖1 MiGo的主要表現形式

這裡需要注意的是select語句和phi語句在轉化為MiGo形式時有其額外的表現形式。

《A Static Verification Framework for Message Passing in Go using

Behavioural Types》中使用圖的形式對MiGo進行分析（目前我還沒找到如何自動生成這種影象，相關工具的readme檔案中沒有提供相關說明，不過在工具原始碼中有block包，後續看看原始碼，這裡直接用論文中的例子）：

package main

func main() {
	ch := make(chan int) // Create channel
	go sendFn(ch)        // Run as goroutine
	x := recvVal(ch)     // Ordinary func call
	for i := 0; i < x; i++ {
		print(i)
	}
	close(ch) // Close channel ch
}
func sendFn(c chan int) {
	c <- 42 // Send on channel c
}
func recvVal(c chan int) int {
	return <-c // Receive from channel c
}

對應的影象為：

圖2 示例SSA圖表示

2.2提取型別定義

對於圖2中的每一個方法（如main,sendFn，recvVal）所表示的每一個塊（block)中都添加了一個型別簽名(type signature),然後使用一個自定義的getFunction演算法對於每一條語句進行遍歷。該演算法如下：

function genFunction(fun, n, k, ρ, Γ)
	switch s ← statement at line k do
		case t =make chan T S do
			genFunction(fun, n, k+1, ρ ; (newS t), Γ[t → t])
		case t=local chan T do
			genFunction(fun, n, k+1, ρ, Γ[t → ⊥])
		case t <−v or <−t or t '= <− t do
			genFunction(fun, n, k+1, ρ ; mkPrefixΓ (s), Γ)
		case close ( t ) do
			genFunction(fun, n, k+1, ρ ; close Γ(t), Γ)
		case return do return ρ; 0
		case jump i do return ρ ; mkJumpΓ (fun, i)
		case i f _ goto i else j do
			return ρ; (mkJumpΓ (fun, i) ⊕ mkJumpΓ (fun, j))
		case select b [д1, ..., дj] do
			ρc ← mkJumpΓ (fun, n+1)
			for i in [1, ..., j] do
				ρi ← mkPrefixΓ (дi ) ρi ← mkJumpΓ (fun, n+2∗i)
			if b = nonblocking then
				ρd ← mkJumpΓ (fun, n+1+2∗j)
				return {ρi ; ρi ; ρc }i∈{1, . . .,j } ∪ {τ ; ρd ; ρc }
			else return {ρi ; ρi ; ρc }i∈{1, . . .,j }
		case F ( x˜ ) or t=F ( x˜ ) do
			if t is a channel then abort
			else genFunction(fun, n, k+1, ρ; mkCallΓ (F, x˜), Γ)
		case go F ( x˜ ) do
			ρ ← genFunction(fun, n, k+1, ◦, Γ)
			return ρ; (mkCallΓ (F, x˜) | ρ)
		case ∗ t0 = t1 or t0 = ∗ t 1 do
			if t 1 is a channel then
				genFunction(fun, n, k+1, ρ, Γ[t0 → Γ(t1)])
			else genFunction(fun, n, k+1, ρ, Γ)
		case phi [Blki :vi ]i∈InEdges do
			if ∃i ∈ InEdges : vi is a channel then abort
			else genFunction(fun, n, k+1, ρ, Γ)
			otherwise do genFunction(fun, n, k+1, ρ, Γ)

演算法1 genFunction

通過使用getFunction方法就可以推匯出某段SSA中間碼對應的行為型別。有一個名為gospal的工具可以實現該方法對應的功能，在第三節中對這個工具會進行例項說明。

2.3 對行為型別進行模型檢查（model checking）

模型檢查主要分為三步。

2.3.1 LTS

LTS是labelled transition system(標記過渡系統)的縮寫，模型檢查的第一步就是從一組操作語義規則（operational semantics rules）中為型別生成一個標記的過渡系統。Lange等人使用了mCRL2進行檢查，mCRL2中有一條規則是：我們無法識別在遞迴環境下的並行組合和通道建立等操作的型別。這是保證狀態空間有限的必要條件。也就是說無限遞迴的通道建立或者方法呼叫等操作在我們的實驗中是無法檢查的。

要研究LTS，需要從型別的語義著手，還是使用類似的標籤來描述各種併發行為，如表1所示。

表1 語義標籤

前面提到按照mCRL2規則需要排除無限遞迴建立通道的情況，因此可以直接將通道建立語句放到最外層，也就是：

這樣T就不包括通道建立語句了，也可以將它們都寫成並行建立的形式，即

這樣我們就可以得到型別的語義，也就是各種操作前後狀態的變化，如圖3所示，箭頭左邊就是操作之前的狀態，箭頭所指就是操作後狀態，比如說第二行第二個就是一個已經建立好的快取為n的通道經過關閉操作後狀態變為關閉的狀態。

圖3 型別的語義

根據以上資訊可以構造有限的LTS，該LTS可以代表t<>所有可能的操作，它是一個元組

S是由行為型別術語（behavior type terms)隱式標記的一組狀態,t₀<>就是初始狀態，A是標籤的集合，箭頭就代表轉換的過程。

2.3.2行為型別狀態的屬性（這部分目前原理清楚，就是示意圖還沒完全搞明白）

對於前面得到的LTS，在它們的基礎上定義謂詞，以分析在某一狀態時可以執行哪些操作。具體來說就是定義了一個謂詞族，如果T準備執行族中的某一個動作，則謂詞成立，謂詞的示意圖如4所示：

圖4 謂詞的定義

2.3.3 Go程式的liveness和安全性（不太懂，準備看μ-calculus相關文獻）

我們在μ-calculus中對Go程式的liveness進行編碼，並在2.3.2的狀態標籤上進行擴充套件。

在2.3.1中定義的LTS上對μ-calculus進行解釋，如果T在LTS T中滿足ϕ，則我們可以定義

也就是說公式⊤對於每個T成立（而⊥永遠不成立）。構造[α]ϕ是模態運算子，如果對於T的每個α導數T'（即，通過執行動作α可以從T到達T'），公式ϕ滿足T'，則滿足該條件。對偶模態是<α>ϕ，如果存在T的α導數T^'使得ϕ在T^'中成立，則對偶模態成立。構造νx. ϕ（resp.µx.ϕ）是標準最大定點運算子（fixpoint operator)。圖5是μ-calculus的公式

圖5 μ-calculus的公式

根據圖5中公式可以描述能夠使用mCRL2進行驗證的幾個屬性，給定一個

µ-calculus公式ϕ，如果ϕ對於所有可能達到的狀態都滿足，那麼第一行的公式就總是成立。而如果ϕ只能滿足某些可達狀態，那麼第二行的公式就成立。下面各個公式所對應的情況都在每行末尾的方括號內說明了，也就是說µ-calculus公式可以覆蓋幾乎所有已知的Go語言併發情況。

Model checking這部分總的來說就是根據從Go原始碼中推斷出的行為型別，將其轉換為mCRL2語言，然後生成儘量小的（通過LTS等方式）µ-calculus公式，最後為每一個公式執行mCRL2檢查器，並將結果返回給使用者。

2.4 終止檢查（Termination checking)

這一步就是為了解決2.1中提到的程式行為型別分析結果與程式實際之間不匹配的情況，使用了KITTeL終止分析器，該分析器原本是用於C語言的，因為Go語言結構與C語言類似所以也可以用於Go迴圈的終止分析，簡單地說就是將Go語言中的所有迴圈（也就是for迴圈，Go語言中沒有while迴圈）單獨提取出來，忽略其他語句，然後檢查迴圈的引數是否能使每個迴圈終止，如List 5所示。

func f(n int) {
	for i := 0; i < n; i++ {
		for j := 0; j < 10; j++ { ... }
    } 
}

List 5 終止檢查迴圈例項

可以看到在這個巢狀的迴圈中有一個靜態未知值n，它將作為各個C函式的引數生成，終止檢查器KITTeL會強制檢查這一類未知值所有可能的結果。

3.一部分工具

3.1 Go併發語句行為型別的分析

Lange等提出了一個名為gospal的工具包來分析Go併發語句的行為型別。List6展示了這個工具的使用情況。

package main

func main() {
	ch := make(chan int) 
	go sendFn(ch)        
	x := recvVal(ch)    
	for i := 0; i < x; i++ {
		print(i)
	}
	close(ch) 
}
func sendFn(c chan int) {
	c <- 42 
}
func recvVal(c chan int) int {
	return <-c 
}

def main.main():
    let t0 = newchan main.main0.t0_chan0, 0;
    spawn main.sendFn(t0);
    call main.recvVal(t0);
    call main.main#3(t0);
def main.sendFn(c):
    send c;
def main.recvVal(c):
    recv c;
def main.main#1(t0):
    call main.main#3(t0);
def main.main#2(t0):
    close t0;
def main.main#3(t0):
    ifFor (int t5 = 0; (t5<t1); t5 = t5 + 1) then call main.main#1(t0); else call main.main#2(t0); endif;

List 6 gospal分析Go語言語句的行為型別

3.2對於Go語言併發缺陷的檢測工具

3.2.1 Gong

該工具是在《Fencing off Go:
Liveness and Safety for Channel-Based Programming》中提出的，github上的網址為https://github.com/nickng/gong 。它是本文主要描述的方法的前一步工作，該工具是對於行為型別分析的結果（.migo檔案）進行程式liveness和安全性的分析。該工具是用Haskell語言寫的，安裝完成後在命令列中輸入

Gong --help

可以看到該工具的一系列方法：

The checker program

checker [OPTIONS] FILE [INT (optional bound)]
  Go-Types liveness and safety checks

Common flags:
  -A --all       Check liveness and behavioural safety (default)
  -L --liveness  Check liveness
  -S --safety    Check behavioural safety
  -D --debug     Show liveness/safety error terms (debug)
  -N --list      Show list of k-reachable terms (debug)
  -? --help      Display help message
  -V --version   Print version information

使用一個簡單的程式（List 7）驗證一下該工具

package main

type S struct {
	ch chan int // nilchan
	v  int
}

func set(s *S, v int) {
	s.v = v
}

func main() {
	s := new(S)
	set(s, 10)
	set(s, 10)
	<-s.ch

	n := new(S)
	set(n, 11)
	n.ch = make(chan int)
	<-n.ch
}

List 7 Gong demo code

使用gospal分析後得到的行為型別為

def main.main():
    let t0_0 = newchan nilchan, 0;
    let t0_0 = newchan nilchan, 0;
    let t3 = newchan nilchan, 0;
    recv t3;
    let t6_0 = newchan nilchan, 0;
    let t9 = newchan main.main0.t9_chan0, 0;
    recv t9;

對其應用Gong進行分析，得到的結果如下，可知該程式是有併發錯誤的。

Go訊息傳遞併發

1.併發缺陷的型別

1.1通道安全性有關的併發缺陷

1.2全域性死鎖

1.3區域性死鎖

2.1對Go語言原始碼進行分析

2.2提取型別定義

2.3 對行為型別進行模型檢查（model checking）

2.3.1 LTS

2.3.2行為型別狀態的屬性（這部分目前原理清楚，就是示意圖還沒完全搞明白）

2.3.3 Go程式的liveness和安全性（不太懂，準備看μ-calculus相關文獻）

2.4 終止檢查（Termination checking)

3.一部分工具

3.1 Go併發語句行為型別的分析

3.2對於Go語言併發缺陷的檢測工具

3.2.1 Gong

Go訊息傳遞併發

go語言基礎(併發--goroutine+channel)

DGL學習(三): 訊息傳遞教程

ndroid訊息傳遞 EventBus 使用

Android訊息傳遞 Handler 訊息機制

Go語言 | CSP併發模型與Goroutine的基本使用

吳裕雄--天生自然ANDROID開發學習：3.3 Handler訊息傳遞機制淺析

C# 利用SendMessage實現winform與wpf之間的訊息傳遞

洛谷 P2018 訊息傳遞

洛谷P2018 訊息傳遞

TCP實現訊息傳遞

go的WaitGroup併發問題，多次執行結果不相等

1.3 Go語言為併發而生

C++第五十二篇 -- 多執行緒之訊息傳遞

MVVMLight ViewModel to View 訊息傳遞

CSP201903-4 訊息傳遞介面（模擬）

#點分樹#洛谷 6626 [省選聯考 2020 B 卷] 訊息傳遞

python 模擬SIP訊息傳遞

go切片支援併發嗎？

客戶端和服務端的訊息傳遞

Go訊息傳遞併發

1.併發缺陷的型別

1.1通道安全性有關的併發缺陷

1.2全域性死鎖

1.3區域性死鎖

2.訊息傳遞相關併發缺陷檢測相關思路（related works）

2.1對Go語言原始碼進行分析

2.2提取型別定義

2.3 對行為型別進行模型檢查（model checking）

2.3.1 LTS

2.3.2行為型別狀態的屬性（這部分目前原理清楚，就是示意圖還沒完全搞明白）

2.3.3 Go程式的liveness和安全性（不太懂，準備看μ-calculus相關文獻）

2.4 終止檢查（Termination checking)

3.一部分工具

3.1 Go併發語句行為型別的分析

3.2對於Go語言併發缺陷的檢測工具

3.2.1 Gong

相關推薦