Communication Sequential Process

Java や C++ とかでマルチスレッドを使った並列プログラムとかやっていると、訳の分からん、デッドロックやリソーススタベーションなどにぶつかって、苦労する事がある。そしてそれをどうやって論理的に把握するかって所で、さらに訳分からん事になり、苦労する事になる。今までなら、直感的に状態遷移図やタイミングチャート書いてみて、状況を整理しようとしていたが、描いた状態遷移モデルやタイミングチャートに妥当性があるという保証はどこにも無く、結局、プログラムとモデルの両方を修正しながら、螺旋階段を進むがごとく、試行錯誤して解決していた。

こうした問題に対して、形式的仕様記述の方法が使えないかと考えていた。以前、mixi のソフトウェア工学のコミュでその辺の情報交換を進めていた際に、長いやり取りの後で、形式的仕様記述を学ぶためにと勘違いして、プロセス代数の入門書として「仕様記述言語LOTOS―分散システム設計の先端技法 (コンピュータ通信シリーズ)」を勧められて読んだ事がある。が、やはりまだなんか全然取っ掛かりの部分でしっくり来なくて、形式的仕様記述手法の理解の道は遠いもんだと思った。その LOTOS の本にプロセス代数の基本として、紹介してあったのが、「ホーアCSPモデルの理論」である。
ずっと気に留めてはいたのだが、最近、IBM の developers works で Java プログラマーのための CSPとかいった記事*1が出ていたりして、なんか、実際に自分の仕事への適用する上での、敷居みたいな物が下がった気がした。そう思い、一度、プロセス代数の基礎から学ぼうという気にもなったので「ホーアCSPモデルの理論」を購入して読み始めた。全７章からなるが、今現在、ようやく基本部分である１．プロセス、２．並行性、３．非決定性の３章を読み終えた所である。

表記法は多くの場合不満の種となる。ロシア語を学生が学ばねばならなくなると、不慣れなロシアアルファベットが最初の障害となる。特に、この多くは奇妙な発音をしていることもある。ほとんど慰めにならないが、こんなことは心配しても始まらない。文字の書き方を学んだ後、文法を学び語彙も増やさなければならぬし、慣用句と文体を習得せねばならない。この後この言葉をを流暢に操ることを訓練し、ようやく自らのアイデアが表現できるようになる。このことは全て学習と訓練と時間とを必要とし、決して短時間では解決できない。数学においても同様である。あらたな記号は、最初は深刻な障害に映る。しかし本当の問題は、これら記号の意味と特性、および操作法を理解し、これを用いて新たな問題を記述し、それを解きそして証明を与える力をつけることである。
「ホーアCSPモデルの理論」 まえがき 醞ページ より引用

この手の理論を学ぶ際に障害になる、記号群、表記法の嵐に対しても、初出の章も添えた記号要約を最初のページに沿えて有ったりと、分かりやすく伝えようとする姿勢、丁寧な作りに好感を覚えたし、実際に理解しやすいと思う。*2 読んでみて思うに、今まで漠然と考えていた、プロセス、並行性や非決定性などについて、ちゃんとした考え方を提供しており、CSP の理論で語られている枠組みは、今まで悩んできた並列システムの品質をどう確保するかという課題に対して強力な手法を提供してくれそうな期待が持てそうな気がする。ただ、まだこの本の中では、実時間応答（リアルタイム）に関する記述は出てきていないので、その辺は差し引いて考える必要が有るかもしれない。

最後には、読者は数学的エレガントさスタイルに対する鑑識眼を養うことになろう。ときそこに至れば、もはや記号は目に入らなくなる、すなわち読者は記号を通じてその意味するところだけをみるのである。数学の最大の利点は、使用される規則が自然言語よりよほど単純でありまた語彙も少ないということである。結果として何か不案内なことにぶつかっても、ほかの本や専門書に頼ることなく、独力で理論的演算と創意をもって解を得ることができる。

これがプログラミング同様、数学のかくも愉しい所以である。しかし、必ずしも容易だと言うわけではない。例えば数学者といえども、自分の専門領域から派生した新しい分野について学ぶことは難しい。通信するプロセスの理論は数学の新しい分野である。しかしそれを学ぶプログラマは数学者に対して何ら不利な点はない。それどころか結局は習得した知識を実際の問題に使用するという明らかな利点すらある。

「ホーアCSPモデルの理論」 まえがき 醬ページ より引用

割りに古い本であるし*3、もっと早く手にしていればよかったのにと少し悔やまれる。こうした本には滅多に出会わない。大学の教科書のような本のつくりであるが、見た目が分かりやすい割りに内容がマニュアルのような事が多い、今時の情報システム関連の本よりは、ちゃんと考えないと理解できないこの手の本のほうが個人的には好きだ。古いけど、developers works の JCSP の記事を見ると、内容の先進性はまだ十分に普及していないのだろう。当面はこれの勉強で通勤時間をつぶせそうである。*4

ホーアCSPモデルの理論

*1:ただし、この記事、結局、JCSP という Java のパッケージの紹介が主体で、CSP を使う事のメリットと、Java に適用する際のミソについてはあまり語ってくれていない。

*2:まーそれでも、通勤中の電車内で読んでいるんで、進みは遅いのですが。

*3:1992年である。本書内での実装例は主に Common Lisp であり、巻末の広告に Common Lisp や Smalltalk に並んで ADA の本もあった。ADA って今でも使われているのだろうか。

*4:但し、体調が悪い時はむりであるが。