並行プログラミング concurrent programming

並行プログラミング
concurrent programming
分散,並列,並行
いずれも複数の処理を行う。おおよその違いは
• 分散(distributed): 複数の処理主体が空間的
に分散している。厳密には同時性とは別。
• 並列(parallel): （物理的に）複数の処理主体が
同時に処理を行う。
• 並行(concurrent): 処理主体の数は問わない。
純粋に論理的。
並行プログラミングの要素
• プロセス：処理主体
– プロセスは停まるとは限らない。
• 通信と計算
– 各プロセスが受け持つ処理の粒度によって通信
と計算の比重が変わる。
オブジェクト指向との類似性に注意
並行プログラミングの例
• Communicating Sequential Process(CSP)
(Hoare, 1978)
• Concurrent Prolog (Shapiro, 1986)
• Guarded Horn Clauses(GHC) (Ueda, 1988)
• p-calculus (Milner, 1989)
近年はセキュリティ関連で。
GHC
GHCの構文
factorial(X,Y) :- X>0 | X1:=X1, factorial(X1,Y1),Y:=X＊Y1.
factorial(0,Y) :- true | Y=1.
構文
各行はガード付ホーン節(guarded Horn clause)
factorial(X,Y) ゴール（プロセスを表す）
節の左辺はヘッド
右辺の縦棒|（コミット演算子）の左をガード、右をボディ
GHCの動作
• ゴールの変数に節のヘッドとのパタンマッチが成功する
ような結合（binding）が生じ、ガードの条件を満たせば、
（非同期、並行して）そのゴールを具体化された節のボ
ディに書き換える（ゴール書き換え規則）
• :=は右辺を評価して代入。=は評価せず項として代入
• 後戻り（バックトラック）はしない！
GHCにおけるストリーム
factorials([X|Xs1],Ys1) :- true |
factorial(X,Y),Ys=[Y|Ys1],factorials(Xs1,Ys2).
factorials([],Ys) :- true | Ys=[].
factorial(Xs,Ys)
Xs←[5|Xs1] とすると Ys←[120|Ys1]となる。
Xs1←[7|Xs2] とすると Ys1←[5040|Ys2]となる。
並行計算
Xs←[150, 3 | Xs2]とすると、
Y1←150! より Y2←3!のほうが早く得られる可
能性がある。
GHCの特徴
• 通信は（節で共有する）変数を通じて行う。
– 結合(binding)の生成と観測
• I/Oもプロセス
– outstream([write(‘hello’),nl|X1])
• 通信は非同期
p(X,Y) :- true | X=5,q(Y).
q(Y) :- true | Y=6.
プロセスX=5とY=6の実行順序は不定
GHCによる記述例1
• 双方向通信
ストリームXを未完成メッセージ
[write(‘more?’), nl, read(T) | X1]
に結合すれば、受信側によるTの結合が送信側で
観測可能。
cf. Cにおけるポインタ渡し（代入通知なし）
記述例２
• 履歴のあるオブジェクト
stack(Xs) :- true | stk(Xs, []).
stk([push(T) | Xs1], Ls) :- true | stk(Xs1,[T|Ls]).
stk([pop(T) |Xs1],[L|Ls1]) :- T=L, stk(Xs1,Ls1).
stk([pop(T) |Xs1],[]) :- true | T=error, stk(Xs1,[]).
stk([], Ls) :- true | ture.
πcalculus
π計算の要素
• x,y,z, ‥‥ （チャネル
の）名前
• P,Q,R ‥‥ プロセス
P ::

iI i
p i .P | P | Q | ! P | (x) P
π計算の構文と意味
P
:: 
|
|
|
|
|
|
|
0
x y.P
x ( y ).P
PQ
P|Q
( x) P
[ x  y ]P
A
（停止したプロセス）
（出力ポートｘから引数ｙを送信）
（入力ポートｘから値または通信ポート名をｙで受信）
（PまたはQとして振る舞う）
（PとQが並行に動作できる）
（通信ポートｘをPのスコープ内に制限する）
（ｘとｙが一致したときのみPとして振る舞う）
（A=Pとなるとき、AをPで置換）
動作
xˉy.0 | x(u).uˉv.0 | xˉz.0
略記：
xˉy | x(u).uˉv | xˉz
は次のようにリダクションされる
0 | yˉv | xˉz
または xˉy | zˉv | 0
π計算の性質
• λ計算を模倣できる
• 計算＝通信
• チャネルが動的に生成消滅
文献
The Polyadic -Calculus: A Tutorial, (by
Robin Milner).
http://lampwww.epfl.ch/mobility/papers/ECSLFCS-91-180.ps.gz
リンク
http://move.to/mobility

Download Report