CSP に入門してみた

programming

java

softwareengineering

並行システムの検証と実装: 形式手法CSPに基づく高信頼並行システム開発入門 (トップエスイーシリーズ実践講座)

最近少し CSP (Communicating Sequential Processes) をかじり始めています。

CSP というのはプロセス代数と呼ばれる並行システムを記述して解析するための分野の言語の1つで、クイックソートを発明したことでも知られている C.A.R. Hoare が考案したものです。個人的に形式手法には懐疑的な印象を持っているので、ちょっとどうなのかなという感じでしたが、使えるところだけでうまく切り取れば面白そうな気がしてきました。

日本語の文献は多くないので、詳しく知りたい場合にはトップエスイーシリーズの「並行システムの検証と実装形式手法CSPに基づく高信頼並行システム開発入門」が役に立ちます。形式手法なので、当然のことながら数学的な臭いが強く、手続き的な記述に慣れた一般的なプログラマーにとって、敷居が高いことは否めません。通常のビジネスアプリであれば、並行化して高速化する恩恵よりも、厄介なバグが増えてしまうリスクの方が大きいという現実があるので普及はゆっくりとしか進まないでしょうが、自前で分散処理をやりたいという場合には役に立ちそうです。僕は昔仕事で、TP モニタをいじっていた時期があるので、こういうのも面白いなと感じました。

どうやって入門するかということになりますが、Occam-pi などの専用のプログラミング言語だと敷居が高いので、簡単に使うためには Java 向けに作られている JCSP を使うのが一番簡単なようです。

Communicating Sequential Processes for Java (JCSP)

以下、プログラミングメモ。

† とりあえずスレッドを書き換えてみる

チャネルを使ってスレッド間（CSPでいうとプロセス間？）通信するのが本筋だろうと思いますが、まずは簡単なスレッドプログラミングを、JCSPで書き換えてみるところからスタートしてみます。

MultiThreadTest.java

package sample;

public class MultiThreadTest {
	public static void main(String[] args) {
		Thread t1 = new Thread(){
			@Override
			public void run() {
				for (int i = 0; i < 10; i++) {
					System.out.println("a:"+i);
					try {
						Thread.sleep(1);
					} catch (InterruptedException e) {}
				}
			}
		};
		Thread t2 = new Thread(){
			@Override
			public void run() {
				for (int i = 0; i < 10; i++) {
					System.out.println("b:"+i);
					try {
						Thread.sleep(1);
					} catch (InterruptedException e) {}
				}
			}
		};
		Thread t3 = new Thread(){
			@Override
			public void run() {
				for (int i = 0; i < 10; i++) {
					System.out.println("c:"+i);
					try {
						Thread.sleep(1);
					} catch (InterruptedException e) {}
				}
			}
		};
		t1.start();
		t2.start();
		t3.start();
	}
}

上記と等価なプログラムを書くと、こんな感じでしょうか。
Thread と書いていないので、マルチスレッドに見えませんが動かすと並行に動くというのが確認できます。

JCSPTest.java

package sample;

import org.jcsp.lang.CSProcess;
import org.jcsp.lang.CSTimer;
import org.jcsp.lang.Parallel;

public class JCSPTest {
	public static void main(String[] args) {
		final CSTimer t = new CSTimer();
		CSProcess[] procs = new CSProcess[]{
			new CSProcess() {
				@Override
				public void run() {
					for (int i = 0; i < 10; i++) {
						System.out.println("a:"+i);
						t.sleep(1);
					}
				}
			},
			new CSProcess() {
				@Override
				public void run() {
					for (int i = 0; i < 10; i++) {
						System.out.println("b:"+i);
						t.sleep(1);
					}
				}
			},
			new CSProcess() {
				@Override
				public void run() {
					for (int i = 0; i < 10; i++) {
						System.out.println("c:"+i);
						t.sleep(1);
					}
				}
			},
		};
		new Parallel(procs).run();
	}
}

記述はシンプルになりましたが、単にガリゴリ書いていっただけだと Thread と BlockingQueue を使ったのとあまりかわりませんね。
ちゃんと使いこなすには CSP モデリングして、モデル検証するところまでマスターするのが必須のようです。

唯一のマイナスポイントは JCSP がジェネリクスに対応してないことでしょうか。