はじめに

go言語には、「スレッドの生成・起動」、「スレッド間の通信」といった、いわゆる「並列処理」を意識した言語要素があります。
このような言語要素を使って書く並行処理は、多くの場合振る舞いが複雑で正しいことを保証するのが難しくなります。

本記事では、そのような複雑な振る舞いになりがちなgoで書かれた「並行処理」の振る舞い設計をCSP(Communicating Sequential Process)という形式言語を使った記述と対応させます。そうする事で、並行処理を含むgo言語のコードの振る舞い検証をするための第一歩、「記述」についての説明を試みます。

尚、本記事で「遷移図」として利用した図は、PAT(Process Analysis Toolkit)というCSPベースのモデル検査のシミュレーション機能を使って表示した絵をキャプチャしたものを使いました。

CSPモデルとして解釈できるgoの制御構造

CSPで記述する並列プログラムのモデルの基本は、通常のプログラムの
基本構造「順次」、「分岐」、「繰り返し」に加えて「並行」「同期」「通信」と
いったものが追加されたものの表現になります。

• 順次 ＝「イベント列」or「逐次合成」
• 繰り返し ＝「再帰」
• 分岐
• 並行動作 = 並行合成
• イベント同期
• 同期通信
• 選択

順次 ＝「イベント列」or「逐次合成」

イベント列

a,b,cというイベントを順番に実行し、止まるプロセスPは以下のように書きます。

P = a->b->c->Skip;

イベント実行に代入などの処理を伴わせたい場合には、以下の様に書きます：

P = a{x=1}->b{y=2}->c{z=x+y}->Skip;

go言語では、プロセス定義は関数定義と対応するので、以下の様に書けます：

func P() { a;b;c; }

ただ、CSPの「イベント」が上記のようなa,b,cという文の順次実行にそのまま対応するかどうかは場合によります（※）。。イベントの実行は以下の図のようにa,b,cの順となります。

※場合によっては後述する同期通信の同期タイミングとして対応させるのが良いかもしれません

逐次合成

3つのプロセスP,Q,Rが以下の様に定義されているとします。

P = a->Skip;
Q = b->Skip;
R = c->Skip;

これらを、逐次合成演算子「;」で結合したSysというプロセス

Sys = P; Q; R;

は、「Pの実行後、Q、Qの実行後、Rを実行」する。イベント実行は、先ほどのイベント列の場合と同様、以下になります。

繰り返し

上の例で、a,b,cのあとに止まらずにまたはじめから実行する（ループする）プロセスは以下のように書きます。

P = a->b->c->P;

これも、go言語のイメージで書くと、直接的には、

func P() { a;b;c;P(); }

となりますが、CSPの再帰はいわゆる再帰呼び出し（スタックを積んで呼び出し、処理が終わったら呼び出し元に戻ってくる）ではありません(※)。
なので、以下のほうが近いです：

func P() { for {a;b;c;} }

遷移図は以下になります。

※再帰呼び出しを使う場合、言語の処理系が「末尾再帰最適化」を行っていれば、スタックは積まれず、無限ループを表現している事になります。

条件分岐

goに限らず、プログラミング言語の分岐では、

if(条件)  <真の時の処理> else <偽の時の処理>

CSPでもほぼ同様の表現が使えます：

if(x>2) { a->Skip } else { b->Skip } ;

これは、$x>2$という条件が成り立っているので、a->Skipが動作します。

「並行動作」

以下のように２つのプロセスP,Qが定義されていたとします：

P = a->b->c->Skip;
Q = d->e->f->Skip;

この２つを「並行合成」したプロセスSysは以下のように書きます。

Sys = P || Q;

C言語にはこれを直接表す言語要素はないのでgo言語で書くと以下のようになります：

func P() { a;b;c; }
func Q() { d;e;f; }
func Sys() {
   go P();
   go Q();
}

goという命令を使って関数呼び出しをするという構文で、「go routine」と呼ばれる、メインスレッドと並行に動作するスレッドを生成・起動しています。
合成されたプロセスSysの実行パターンはそれぞれのイベントの実行順番のありうる組み合わせすべて表現したのが以下の遷移図です。

・・・ちょっとした並行動作部分を持つプログラムの動作がいかに複雑になりがちか、この絵をみただけで怖くなります。

イベント同期

２つのプロセスを並行合成したとき、それぞれのプロセスのイベントに「同じ名前」のイベントがある場合、そのイベントの実行は「同時」に起こっている事を表します。

P = a->x->c->Skip;
Q = d->x->f->Skip;
S = P || Q;

この実行の組み合わせを表す以下の図を見るとイメージがはっきりすると思います。「同時」というよりは、イベント実行自体が１つになっています。

同期通信

CSPでの通信表現は「同期通信」です。

つまり、同期したタイミングでグローバル変数などを介してデータを受け渡せばよいのです。それ自体はすでに説明したようにイベント同期を使えば同期が表現できるのですが、CSPではそのためのチャネルという概念があります。

チャネル

chというチャネル変数を使って、プロセスPからプロセスQへ５という数値を送信するには以下のように書きます。

channel ch 0;
P = a->ch!5->c->Skip;
Q = d->ch?data->f->Skip;
S = P || Q;

go言語にも、このチャネルに対応する概念があります。送信には <- という二項演算子、受信には <-という単項演算子を用意しています。
チャネルは、「チャネル型の変数」として表現されます。

func P() { a; ch<- 5; c; }       // チャネルchに5を送信
func Q() { d; data := <-ch; f; } // チャネルchから値を受信し、dataに代入
func S() {
   go P();
   go Q();
}

※channel変数の宣言や関数への引き渡しの部分は省略しています。

尚、図を眺めると、チャネルによる同期通信と、イベントによる同期の構造は（前者にはデータの送受信が伴う事を除き、）ほぼ同じであるというのが理解できると思います。

「選択」

cspでの「選択」は、一般的には、

[処理Aを実行するためのガード条件]<処理A> []  [処理Bを実行するためガード条件]<処理B>;

と書きます。ifと違って、２つの「ガード条件」は必ずしも「排他的」ではありません。

真ん中の [] が、選択を表すCSPの演算子です。

条件が排他的でないため、一般的には、分岐は、確率的にどちらかへ、という事になりますがこれを「非決定的」な選択動作といいます。

goのselect

goには、「select」という言語表現があります。ただ、CSPでいうところの選択とは若干異なり、チャネルによる受信
タイミングが非決定的な場合に利用します。
CSPで、

Sender1 = ch!5 -> Skip;
Sender2 = ch!4 -> Skip;
Receiver = ch1?x->Skip [] ch2?x->Skip;
Sys = Sender1 || Sender2 || Receiver;

Sender1, Sender2とReceiverは並行動作しているので、Receiverがch1とch2のどちらを先に受け取るのかは「非決定的」になります。
goで同様の処理を表現すると以下になります。

// test_selector.go
package main
import "fmt"
func sender1(ch1 chan int) {
  ch1 <- 3;
}
func sender2(ch2 chan int) {
  ch2 <- 4;
}
func receiver(ch1, ch2 chan int) {
  select {
    case x := <-ch1:
      fmt.Printf("x = %d\n", x);
    case x := <-ch2:
      fmt.Printf("x = %d\n", x);
  }
}
func main() {
  ch1 := make(chan int)
  ch2 := make(chan int)
  go sender2(ch2)
  go sender1(ch1)
  go receiver(ch1, ch2)
}

receiverのselect文の中でch1の受信とch2の受信が同時に開始可能になった場合でも、どちらかが
「非決定的」に選択されて実行されます。

なお、ここまでにでてきた goのコードはイメージをつかむための不完全なコードでしたが、今回は動作可能です。以下の様なコマンドで動かせます。

$ go run test_selector.go
x = 4

この結果は、sender2がch2を使って送った数値4を「たまたま」receiverが受け取った結果、xに４が代入されていたという事になります。

おわりに

今回は、goで記述する「並行処理」、それに伴って必要になってくる「同期通信」のためのチャネル、「選択」といった概念を並行処理プロセスの振る舞い記述の言語「CSP」ではどのように表現するのか（またはその逆）を説明しました。
記述ができたら、それを使った「検証」を行う事ができるようになります。検証には、いわゆる数学の証明的な方法を使う方法と、モデル検査ツールを利用する方法があります。今後はそれについても説明できればと思います。

今回は以上、です。