以下は、P 言語 のチュートリアル https://github.com/p-org/P/blob/master/Doc/Manual/pmanual.pdf の、２０１７年６月時点の、kanda.motohiro@gmail.com による抄訳です。MIT License の下で公開します。P#プログラミングガイド も参照。
P言語を紹介してくださった kuenishi さんに感謝します。P言語の素晴らしさについて - kuenishi
P tutorial
Ethan Jackson
ejackson@microsoft.com
Shaz Qadeer
qadeer@microsoft.com
１．はじめに
Pは、非同期なイベント駆動型システムを実装するためのドメイン固有言語です。Pのゴールは、非同期システムのコンポーネント間の通信につきもののプロトコルを簡潔かつ正確にとらえる言語プリミティブを提供することです。Pプログラムのもととなる計算モデルは、メッセージを使って通信する状態マシンです。それは、組み込みの、ネットワーク接続された、分散システムを作るのに一般的に使われるアプローチです。それぞれの状態マシンは入力キュー、状態、遷移、イベントハンドラ、そして変数の集まりのためのマシンローカルな記憶域を持ちます。状態マシンは、お互いに並行して走ります。それぞれはイベントハンドラのループを実行します。それは、入力キューからメッセージをデキユーし、ローカル記憶域を調べ、そして操作のシーケンスを実行することができます。それぞれの操作は、ローカル記憶域を更新したり、メッセージを他のシステムに送ったり、新しいマシンを作ったりします。Pにおいては、送信操作はノンブロッキングです。メッセージは単純に、目的マシンの入力キューにエンキューされます。
このチュートリアルの以下では、いくつかの例を使って P の機能を紹介します。まず、状態マシンプログラミングモデルの基本を示す単純なプログラム（２節）を紹介します。次に、障害検知プロトコル（３節）という、より洗練された例を紹介します。これはP言語の高度な機能を示します。Pは、非同期アプリケーションにおいてプロトコルを実装するためのドメイン固有言語です。プロトコル以外のアプリケーションの部分は、Cのようなホスト言語で書かれることが期待されます。Pコードと、Cで書かれた外部コードとの相互運用性に重要な、外部コードインタフェースを説明します（４節）。最後に、Pプログラムを処理するツールの概要を示します（５節）。最後は、P言語の全ての機能の用語集です（６節）。
２．ピンポンプログラム
Pプログラムは、イベントとマシン宣言の集まりです。これはクライアントマシンとサーバマシンがお互いに PING と PONG というイベントを使って通信する基本的なPプログラムです。
// PingPong.p
event PING assert 1:machine;
event PONG assert 1;
event SUCCESS;
main machine Client {
var server:machine;
start state Init {
entry {
server = new Server ();
raise SUCCESS;
} on SUCCESS goto SendPing;
}
state SendPing {
entry {
send server, PING, this;
raise SUCCESS;
} on SUCCESS goto WaitPong;
}
state WaitPong {
on PONG goto SendPing;
}
}
machine Server {
start state WaitPing {
on PING goto SendPong;
}
state SendPong {
entry (payload:machine) {
send payload, PONG;
raise SUCCESS;
} on SUCCESS goto WaitPing;
}
}
さて、このプログラムのイベントとマシン宣言をもっと詳しく見ましょう。PINGイベントの宣言は、それが machine 型のデータ値を伴うことを示します。machine 型は全てのダイナミックに作られたPマシンのアドレスを持ちます。この宣言はまた、どのマシンの入力キューにおいても最大でも１つのPINGイベントしか存在してはいけないことを示します。
マシン宣言は、変数と状態の宣言をいくつか持ちます。例えば、Client マシンはserver変数と、Init, SendPing, and WaitPong の三つの状態をその中に宣言します。server変数のための記憶域はそれぞれのClient マシンインスタンスにローカルです。Init 状態は start state と宣言されていて、Client のインスタンスは Init 状態に入ることで実行を始めることを示します。
state 内には、多くの異なる宣言をすることができます。entry { ...} で示されるコードブロックは、その state に入った時に実行されます。同様に、exit { ... } で示されるコードブロック（この例では使われません）は、その state が終わるときに実行されます。この二つの宣言以外の state 内の全ての宣言は、イベントのハンドリングに関係あります。
state Init にある、on SUCCESS goto SendPing の宣言は、そのような宣言の例です。それは、SUCCESS イベントは、SendPing 状態に移動することで処理されなくてはいけないことを示します。特定のイベントを、異なる状態は、異なるように処理することができます。
例えば、 Init 状態は、 SUCCESS を、 SendPing 状態に移動することで処理しますが、SendPing 状態は、SUCCESS を、 WaitPong 状態に移動することで処理します。
次は、Client マシンの、 Init 状態にある、entry コードブロックの中身を見ましょう。このコードブロックには、二つの文があります。最初の文は、Server マシンのインスタンスを作って、このインスタンスのアドレスを、 server 変数に格納します。次の文は、SUCCESS イベントをレイズして、その結果、制御は Init を抜けて SendPing に入ります。Pでは、あるマシンがイベントを他のマシン（あるいは自分）に投げた時に、そのイベントは目的マシンの入力キューにエンキューされます。しかし、レイズされたイベントはキューを通りません。その代わり、それはそれを取り囲むコードブロックの実行を中止して、すぐに処理されます。
SendPing 状態の entry コードブロックは、PING イベントを送るための send 文の使い方を示します。送信先マシンのアドレスは、 server 変数に格納されています。this キーワードは、現在の文を実行中のマシンのアドレスに評価されます。
最後に、Server マシンの SendPong 状態の entry コードブロックは、受信したイベントに関連するデータ値は、そのイベントハンドラの、適切な型のパラメータを通じて取得できることを示します。このコードブロックでは、 payload パラメータは、制御が SendPong に入る原因となった PING イベントにアタッチされたデータに評価されます。このデータ値は、 PING イベントを送った Client マシンのインスタンスのアドレスです。新しく作られたマシンのコンストラクタがその start 状態の entry ブロックの実行を始めるときに、それに対する引数を取得するためにも、パラメータは同様に使われます。
注意深い読者は、 PingPong プログラムがどのように実行を始めるか疑問に思っているかもしれません。Client マシンは、 main とアノテートされており、これが、プログラムが Client の単一のインスタンスにおいて Init 状態に入ることからプログラムの実行を始めることを示します。このマシンを、X と呼びましょう。マシンXは、Server インスタンスを作って、SUCCESS をレイズして、SendPing 状態に入ります。この Server インスタンスをYと呼びましょう。それは、Server の WaitPing 状態で実行を始めます。この点から、XとYは PING と PONG メッセージを交換します。Xは、SendPing と WaitPong を回り、Yは WaitPing と SendPong を回ります。
Pプログラムの最も重要な安全性仕様は、マシンがデキューした全てのイベントが処理されることです。そうでない場合、Pランタイムは、UnhandledEvent 例外を投げます。PingPong プログラムはこの仕様を満足します。イベントデキューが可能な全ての状態において、 Server マシンはPING イベントを処理し、 Client マシンは PONG イベントを処理するからです。
状態マシンをクリーンに終わらせるために、特別の halt イベントがあります。halt イベントを処理しないことによるマシンの終了は、正常な振る舞いであり、UnhandledEvent 例外を投げません。なので、マシンは、halt イベントをそれにキューすることで終わらせることができます。形式的操作セマンティクスの観点からは、終了したマシンは完全に応答可能で、それに送られる全てのイベントを消費します。Pランタイムはこのセマンティクスを、終了するマシンに確保された資源をクリーンアップして、そしてそのマシンが終了したことを記録することによって、効率的に実装します。終了したマシンに送られたイベントは、単純にドロップされます。終了したマシンは再開始できません。それは、永遠に、終了したままです。
３．障害検知プログラム
P言語の他の機能を示すために、もっと洗練されたプログラムを見ましょう。このプログラムは、障害検知プロトコルを実装します。障害検知状態マシンには、マシンのリストが与えられます。それぞれは、分散システムのノードで動くデーモンを表します。障害検知器はリストのそれぞれのマシンに、PINGイベントを送って、それが決められた時間内にPONGイベントで応答しない場合、マシンが障害であると判断します。障害検知器はPONGイベントの有限時間の待ちを実装するために、OSタイマーを使います。
３．１ Timer マシン
Timer マシンのコードを示すことから始めましょう。Timer マシンはキーワード model を使って宣言されます。これは、OSタイマーの抽象化を表すことを示します。この抽象化は、障害検知器プロトコルの、OSに対する相互作用をテストするために使われます。プロトコルを実行するには、その Timer マシンとの相互作用をスタブと置き換えます。スタブは、プログラマが手で書いたCコードを提供しなくてはいけません。
// Timer.p
// events from client to timer
event START:int;
event CANCEL;
// events from timer to client
event TIMEOUT:machine;
event CANCEL_SUCCESS:machine;
event CANCEL_FAILURE:machine;
// local event for control transfer within timer
event UNIT;
model Timer {
var client:machine;
start state Init {
entry (payload:machine) {
client = payload;
raise UNIT; // goto handler of UNIT
}
on UNIT goto WaitForReq;
}
state WaitForReq {
on CANCEL goto WaitForReq with {
send client, CANCEL_FAILURE, this;
};
on START goto WaitForCancel;
}
state WaitForCancel {
ignore START;
on CANCEL goto WaitForReq with {
if ($) {
send client, CANCEL_SUCCESS, this;
} else {
send client, CANCEL_FAILURE, this;
send client, TIMEOUT, this;
}
};
on null goto WaitForReq with {
send client, TIMEOUT, this;
};
}
}
Timer マシンのそれぞれのインスタンスは、クライアントを持ち、そのアドレスは、 client 変数に格納されます。クライアントはタイマーマシンに START と CANCEL イベントを送り、こちらは、TIMEOUT, CANCEL_SUCCESS, あるいは CANCEL_FAILUREを応答します。
Timer マシンは三つの状態を持ちます。それは、Init 状態で実行を開始し、client 変数を、payload から得て、初期化します。それはクライアントからの要求を WaitForReq 状態で待ち、CANCEL イベントには CANCEL_FAILURE を返し、STARTイベントの場合、 WaitForCancel 状態に移動します。
WaitForCancel 状態では、全てのSTARTイベントはデキューされ、何のアクションも無くドロップされます(これは、ignore キーワードで示されます)。CANCELイベントへの応答は非決定論的で、クライアントからのCANCELイベントの到着と、タイマーの満了との競合をモデルします。この非決定論は、$ を持つ if 文で示されます。then の分岐は、CANCELイベントがタイマーが満了する前に到着する場合をモデルします。その場合, CANCEL_SUCCESS がクライアントに送り返されます。else の分岐は、CANCELイベントが届くより先にタイマーが発火する場合をモデルします。この場合、CANCEL_FAILURE と TIMEOUT が、順にクライアントに送り返されます。最後のイベントハンドラである、on null goto WaitForReq with { ... } は、制御を WaitForReq に移します。これは、 WaitForCancel にある他のイベントハンドラがどれも実行できないでタイマーが満了したことをモデルします。null は特別なイベントであり、この場合、ランタイムが内部的に生成します。
３．２ 障害検知プロトコル
障害検知プロトコルはTimerマシンに依存し、二つの種類のマシンの相互作用をもととします。以下で示す、 FailureDetector と Node です。FailureDetector のコードはP言語のより多くの機能を示します。それには、コンテナ型、関数、doアクション、push 遷移とpop 文、遅延イベント、そしてモニタです。
Pはコンテナ型をサポートします。それには、タプル、名前付きタプルあるいは構造体、シーケンス、そしてマップが含まれます。型 (t1,...,tn) は、 n 個の要素を持つタプルで、型は t1 から tn です。型 (f1:t1,...,fn:tn) は構造体で、型 t1 から tn を持つフィールド f1 から fn です。型 seq[T] は、型 T の値の拡張可能シーケンスです。例えば、変数 nodes は、型 seq[machine] です。型 map[K,V] は、型 K のキーから、型 V の値へのマップです。例えば、変数 clients は型 map[machine,int] です。Pは現在、セット型はサポートしません。しかし、set[T] の代わりに、map[T,bool] を使うことができます。Pはまた、関数をサポートし、それは、任意のコードブロックから呼ぶことができます。関数はそのボディにローカルの、名前付きパラメタを持つことができます。
Init 状態は、push 遷移の使い方を示します。entry ブロックで適切に変数を初期化した後、レイズされたUNITイベントは、現在のInit状態の上にSendPing状態をプッシュすることで処理されます。このようにして、push 遷移の使用は、状態マシンの制御をエンコードした状態のスタックを作ります。Init状態がスタックの上にある間は、そこで、定義されたイベントハンドラは前記の制御状態の変化があっても実行されます。イベントハンドラ REGISTER_CLIENT と、UNREGISTER_CLIENT はそのようなハンドラです。Init から SendPing への push 遷移は、(goto 遷移とは違って)このようなハンドラを一カ所で宣言して、FailureDetector のどこからでも再使用することを許します。イベントハンドラの再使用を提供するほかに、 push 遷移は、他のマシンとの特定の相互作用を処理するプロトコル論理の再使用も可能とします。後で、FailureDetector とTimerの間の相互作用を処理する時の、push 遷移のこのような使い方を説明します。
SendPing状態は、Pの新しい機能をいくつか示します。この状態に入った時、その entry ブロックはまだPONGで応答していない全ての生きているノードにPINGイベントを送ります。そして、１００ミリ秒のタイムアウト値のタイマーを始めます。このマシンは、全ての生きているノードが応答するかあるいはTIMEOUTイベントがデキューされるまで、PONG応答を集めながらこの状態にとどまります。TIMEOUTがデキューされる前に全ての生きているノードがPONG応答をしたら、タイマーはキャンセルされ、TIMER_CANCELED イベントがレイズされます。そうでない場合、TIMEOUTのハンドラが実行され、潜在的に生きているノードへの到達をもう一度試みるべきかを決めます。試みの回数が、試みの最大数(このコードでは２です)に達したら、障害通知が送られます。
// FailureDetector.p
訳注。コードは原文を見て下さい。
SendPing状態は do アクションの使い方を示します。SendPingにあるPONGのハンドラは、on PONG do { … } のコードで示されます。これは、PONG がデキューされた時、かっこの中のコードブロックが実行されなくてはいけないことを示します。この実行の後、コードはSendPing状態にとどまります。この制御プリミティブは、ある状態でのイベント駆動ループを実行するのに便利です。ここで、SendPingがPONG応答を集めるのと同様に。
SendPing状態はまた、push 遷移の使い方も示します。これは、タイマーキャンセルを処理する論理をファクターアウトするためです。全ての生きているノードがPONG応答を返した結果、タイマーをキャンセルした後、TIMER_CANCELEDがレイズされた時、on TIMER_CANCELED push WaitForCancelResponse のハンドラは、SengPing 状態の上に、WaitForCancelResponse状態をプッシュします。WaitForCancelResponse状態は、タイマーをキャンセルした後のタイマーとの相互作用を処理します。それが終わったら、SendPingに制御を戻します。タイマーは、CANCEL_SUCCESS あるいは CANCEL_FAILURE のどちらかで応答します。前者の場合、ROUND_DONE イベントがレイズされます。それは、TIMER_CANCELED 状態では処理されないので、ポップされて、SendPing がそのイベントを処理することになります。後者の場合、pop 文が実行され、TIMER_CANCELED がポップされ、SendPing状態で新しいイベントがデキューされます。
WaitForCancelResponse状態は、defer TIMEOUT, PONG というコードを使います。これは、この状態は TIMEOUT と PONG イベントを処理しないことを示します。なので、マシンがこの状態でブロックしている間は、Pランタイムはこれら二つのイベントはデキューしません。その代わりに、それらを飛ばして、入力キューにある他のイベントを取得します。
FailureDetector マシンが WaitForCancelResponse状態でブロックしている時は、そのスタックは三つの状態を持ちます。スタックの底から言って、それらは、Init, SendPing, そして、WaitForCancelResponse です。Init 状態は、REGISTER_CLIENT と、UNREGISTER_CLIENT の do ハンドラを指定します。SendPing 状態は、PONG と、TIMEOUT の do ハンドラを指定します。そして、WaitForCancelResponse状態 は TIMEOUT と PONG イベントを遅延させます。Pのデキュー論理は、スタックの任意のところにある do ハンドラの実行を、それがそれより上の状態で遅延されていない限り、許します。なので、WaitForCancelResponse状態では、REGISTER_CLIENT と、UNREGISTER_CLIENT はデキューされることが可能ですが、TIMEOUT と PONG はそうではありません。
Pは、プログラマがコードブロック内にアサーションを書くことを許します。それは、マシンにローカルな状態についての不変量を表現します。プログラムにおいて、複数のマシン間の状態についてアサーションを書くことができると、便利なことが多いです。Pは、そのような指定を書くためのモニタを提供します。いかなるノードに対しても、それに送った PING イベントの数は、そのノードが送った PONG イベントの数よりも三つ以上多いことはありえないことを指定する問題を考えましょう。この指定は、Safety 状態マシンを使ってコードできます。このマシンは、マップを使って、ノードごとに、PING と PONG イベントの数の差を維持します。そして、この値が最大でも３であることを保証します。指定をする状態マシンは、それがモニタするイベントを明示的に表す必要があります。例えば、Safety specification は、M_PING と PONG イベントをモニタします。あるマシンから他へ、 send 文を使って送られたイベントは、自動的に、それをモニタする全ての specification にルートされます。最も一般的な場合、モニタされるイベントは、ある状態マシンから他に送られるプログラムイベントですが、モニタリング専用のイベントを作成することが重要な時もあります。M_PING はそのようなイベントです。このイベントは、障害検知器によって、それがnodes[i] にPING イベントを送るちょうど前に、monitor M_PING, nodes[i] 文を使って生成されます。PING イベントの場合、そのペイロードは障害検知器の識別子ですが、M_PING イベントのペイロードは、目的ノードの識別子です。M_PING と PONG のペイロードを使って、Safety マシンは、自分の、ノードごとのチェックを実装できます。
３．３ テストドライバ
Driverマシンは、障害検知プロトコルをテストするためのテストドライバの書き方を示します。このマシンは、プロトコルのクライアントをモデルします。このクライアントは、監視するためのノードをいくつか作り、Safety モニタのインスタンスと、Liveness モニタ(後で説明します)のインスタンスと、FailureDetectorのインスタンスを作り、今作ったFailureDetectorインスタンスに自分を登録し、そして自分が作ったノードにそれぞれ、特別の halt イベントをエンキューします。halt イベントは、特別です。処理されない halt イベントによるマシンの終了は期待される動作で、UnhandledEvent例外をレイズしないからです。Nodeマシンは halt イベントを処理しないので、それは終了します。このようにして、Driverマシンは障害検知プロトコルのための有限のテストプログラムを作ります。
// TestDriver.p
include "FailureDetector.p"
main model Driver {
var fd:machine;
var nodeseq:seq[machine];
var nodemap:map[machine, bool];
start state Init {
entry {
Init (0, null);
monitor M_START, nodemap;
fd = new FailureDetector (nodeseq);
send fd, REGISTER_CLIENT, this;
Fail (0);
} ignore NODE_DOWN;
}
fun Init (i:int, n:machine) {
i = 0;
while (i < 2) {
n = new Node ();
nodeseq += (i, n);
nodemap += (n, true);
i = i + 1;
}
}
fun Fail (i:int) {
i = 0;
while (i < 2) {
send nodeseq[i], halt;
i = i + 1;
}
}
}
event M_START:map[machine, bool];
spec Liveness monitors M_START, NODE_DOWN {
var nodes:map[machine, bool];
start state Init {
on M_START goto Wait;
}
hot state Wait {
entry (payload:map[machine, bool]) {
nodes = payload;
} on NODE_DOWN do (payload:machine) {
nodes -= payload;
if (sizeof (nodes) == 0)
raise UNIT;
};
on UNIT goto Done;
}
state Done { }
}
Driverマシンがコーディングするテストプログラムは有限ですが、それは、膨大な数のふるまいを生成する可能性があります。それは主に、多くの状態マシン(一つのDriverマシン、二つのNodeマシン、一つのFailureDetectorマシン、そして一つのTimerマシン)が並列実行するためです。実行のそれぞれのステップで、ローカルでないアクション(マシンを作ったり、あるマシンから他に、イベントを送ったり)が実行される前に、これらのマシンのどれを選んで実行するかという選択肢があります。Pの基礎にあるテストツールは、これらのふるまいをシステマチックに列挙します。例外がレイズされたり、アサーションが発火した場合、エラーに至るパスがプログラマに報告されます。
これまで述べたような方法でテストプログラムを指定するスタイルは、テスト実行の巨大なセットの、簡潔な記述につながります。プログラマがそれらを指定し、生成する労力を大いに減らします。例えば、DriverマシンはNodeマシンを作るとすぐに、それらに halt イベントを送りますが、この送信アクションは、非決定論的なスケジューラがその代りにプログラム内の他のマシンを実行することを選んだならば「任意の長さ」遅延させられることがあります。Pの基礎にあるシステマチックなテストツールはそういうふるまいを列挙する能力があります。
安全性の指定に加えて、Pはプログラマが、テストプログラムにデッドロックやライブロックがないことを表現できる、ライブネスの指定を許します。デッドロックを最も簡単に表現すると、いかなるマシンもイネーブルされていないことになる有限の実行です。つまり、全てのマシンは終了したかあるいは、イベントを待っています。しかしそのような実行の全てが、特に誤りであるとは考えることはできません。悪いふるまいの指定をさらに詳しくするために、ライブネスモニタは、特定の状態を hot 状態とマークするのを許します。もしモニタがデッドロック実行の後でホット状態にいるならば、この実行はエラーと報告されます。
例えば、前図の Livenessモニタを考えましょう。このモニタは Init状態で始まり、M_START イベントを受けたら Wait状態に遷移します。Wait の entry 関数で、nodes 変数にあるマシンは、このプログラムの全ての Node マシンのアドレスのセットに初期化されます。Driver マシンがFailureDetector マシンから、NODE_DOWN イベントを受けた時には必ず、それはそのイベントをLivenessモニタに送ります。Liveness モニタは、障害が検知されたそのマシンをnodes のセットから除きます。モニタは、全てのnodes が空になったとき、つまり、全ての Node マシンの障害が検知されたとき、に限り、ホット Init 状態を抜けます。このようにして、このモニタは、Node マシンの全ての障害は最終的に検知されなくてはいけないという仕様を表現します。それは、Driver マシンが halt イベントを全ての Node マシンに投げることから、合理的な期待です。
時には、ライブネスの違反が、有限の実行の中でのデッドロックからではなくて、無限の実行から起きることがあります。そこでは、一つ以上のマシンがそれぞれ、進行をしますが、プログラム全体としては進行がありません。ホット状態を持つライブネスモニタは、そのような無限の誤ったふるまいを、指定することもできます。もしモニタが、実行中に、無限にしばしば、ホット状態にあるならば、無限実行は誤りです。ホット状態だけで、モニタは「結果的な」性質を指定できます。例えば、最終的に、何か良いことが起きるとか。ライブネスモニタを一般化して、「無限にしばしば」、例えば、なにか良いことが、繰り返し起きる、という、ふるまいを指定できるようにするために、Pは cold 状態という概念もサポートします。ホットとコールド状態の両方を持つモニタは誤った、無限の実行を、あるホット状態を無限にしばしば訪れ、かつ、コールド状態を有限にしばしばしか、訪れないものであると指定します。
ホットとコールド状態の意味を理解するには、実行の温度というものを考えてみるのが便利です。実行のステップで、その後に、ライブネスモニタがホット状態にあるものは、少量、実行の温度を上げます。コールド状態に入ることは、温度を、ゼロにします。（無限の）実行は、もしその温度が無限になるならば誤りです。
４． 外部コード
３節では、障害検知プロトコルを紹介しましたが、その実装は、タイムアウトを実装するためにOSタイマーを使っていました。システマチックなテストのために、私達はOSタイマーを、Timerという名のマシンにモデルしました。しかし、障害検知プロトコルを実行するためには、Timerの背後にあるCコードを書かなくてはいけません。このコードを外部コードと呼びます。
Pコンパイラは、Timerマシンのために、以下のC関数プロトタイプを出力します。
void P_CTOR_Timer_IMPL(PRT_MACHINEINST *context, PRT_VALUE *value);
void P_DTOR_Timer_IMPL(PRT_MACHINEINST *context);
void P_SEND_Timer_IMPL(PRT_MACHINEINST *context, PRT_VALUE *evnt, PRT_VALUE *payload);
P_CTOR_Timer_IMPL と P_DTOR_Timer_IMPL 関数は、それぞれ、Timerのインスタンスを表すCデータ構造のコンストラクタとデストラクタです。コンストラクタは、new Timer(this) 文が実行された時に呼ばれます。デストラクタは以前に作られたTimerマシンが終了した時に呼ばれます。P_SEND_Timer_IMPL 関数は、Timerマシンにイベントをキューする操作を実装します。以下のコードは、Win32 API を使ってTimerを実装する例を示します。
// P runtime library APIs used in this code
PRT_API PRT_VALUE *PRT_CALL_CONV PrtCloneValue (_In_ PRT_VALUE * value);
PRT_API void PRT_CALL_CONV PrtFreeValue (_Inout_ PRT_VALUE * value);
PRT_API PRT_VALUE *PRT_CALL_CONV PrtMkEventValue (_In_ PRT_UINT32 value);
PRT_API void PRT_CALL_CONV PrtSend (_Inout_ PRT_MACHINEINST * machine,
_In_ PRT_VALUE * evt,
_In_ PRT_VALUE * payload);
PRT_API void PRT_CALL_CONV PrtAssert (_In_ int condition,
_In_opt_z_ PRT_CSTRING message);
// Timer.c
typedef struct TimerContext {
PRT_VALUE *client;
HANDLE timer;
} TimerContext;
void
P_CTOR_Timer_IMPL (PRT_MACHINEINST * context, PRT_VALUE * value)
{
printf ("Entering P_CTOR_Timer_IMPL\n");
TimerContext *timerContext =
(TimerContext *) malloc (sizeof (TimerContext));
timerContext->client = PrtCloneValue (value);
timerContext->timer = CreateWaitableTimer (NULL, TRUE, NULL);
PrtAssert (timerContext->timer != NULL, "CreateWaitableTimer failed");
context->extContext = timerContext;
}
void
P_DTOR_Timer_IMPL (PRT_MACHINEINST * context)
{
printf ("Entering P_DTOR_Timer_IMPL\n");
TimerContext *timerContext;
timerContext = (TimerContext *) context->extContext;
PrtFreeValue (timerContext->client);
CloseHandle (timerContext->timer);
free (timerContext);
}
VOID CALLBACK
Callback (LPVOID arg, DWORD dwTimerLowValue, DWORD dwTimerHighValue)
{
PRT_MACHINEINST *context = (PRT_MACHINEINST *) arg;
TimerContext *timerContext = (TimerContext *) context->extContext;
PRT_VALUE *ev = PrtMkEventValue (P_EVENT_TIMEOUT);
PrtSend (PrtGetMachine (context->process, timerContext->client), ev,
context->id);
PrtFreeValue (ev);
}
void
P_SEND_Timer_IMPL (PRT_MACHINEINST * context, PRT_VALUE * evnt,
PRT_VALUE * payload)
{
printf ("Entering P_SEND_Timer_IMPL\n");
PRT_VALUE *ev;
BOOL success;
TimerContext *timerContext = (TimerContext *) context->extContext;
LARGE_INTEGER liDueTime;
liDueTime.QuadPart = -10000 * payload->valueUnion.nt;
if (evnt->valueUnion.ev == P_EVENT_START) {
printf ("Timer received START\n");
success =
SetWaitableTimer (timerContext->timer, &liDueTime, 0, Callback,
context, FALSE);
PrtAssert (success, "SetWaitableTimer failed");
} else if (evnt->valueUnion.ev == P_EVENT_CANCEL) {
printf ("Timer received CANCEL\n");
success = CancelWaitableTimer (timerContext->timer);
if (success) {
ev = PrtMkEventValue (P_EVENT_CANCEL_SUCCESS);
PrtSend (PrtGetMachine (context->process, timerContext->client),
ev, context->id);
} else {
ev = PrtMkEventValue (P_EVENT_CANCEL_FAILURE);
PrtSend (PrtGetMachine (context->process, timerContext->client),
ev, context->id);
}
PrtFreeValue (ev);
} else {
PrtAssert (FALSE, "Illegal event");
}
}
それぞれのタイマーインスタンスは、TimerContext型のオブジェクトで表されます。それは、クライアントマシンに戻るポインタと、Win32タイマーを表すOSハンドルを持ちます。コンストラクタはこのオブジェクトを作成、初期化して、コンストラクタの最初の引数として渡された PRT_MACHINEINST の extContext フィールドに、それへのポインタをしまっておきます。デストラクタは、確保されたOSとメモリリソースを解放します。PRT_MACHINEINST 型や、前記コードで参照されている多くの他の型と関数は、Pランタイムライブラリで定義されます。これらの定義は、Pコンパイラが自動で生成する “program.h” を引くことで得られます。P_SEND_Timer_IMPL 関数は、STARTやCANCELのようなPのイベントをOSタイマーAPIの適切な呼び出しに変換します。それはまた、これらAPIが返す全ての値を、クライアントにエンキューバックされるイベントに変換します。
５． ツール
上図に、Pプログラミングシステムを使うことに関係する、典型的なワークフローを示します。プログラマは、Pコンパイラへの入力として、Pプログラム(図の左にあります)を、与えます。コンパイラは軽量の静的解析を動かします。エラーメッセージが出ることがあります。プログラマが、全ての静的に見つかったエラーを直したら、コンパイラは二つの出力を生成します。実行するCコードと、システマチックなテストのための Zing モデルです。後者の出力は、Zingモデルと、その .NET アセンブリ形式のコンパイル済みバージョンからなります。次に、プログラマはこの .NET アセンブリを Zingerツールに与えます。それは、このプログラムを、いろいろなインタリーブした実行にわたってテストします。もし、ダイナミックなエラーが見つかったら、プログラムの始めの状態からの完全なエラートレースがテキストファイルの形で、ディスクにダンプされます(Zingerの、 -et オプションを参照)。プログラマはバグを直し、修正したプログラムに対してコンパイラとZingerを再び実行します。このプロセスのいつでも、プログラマは、生成されたCコードを外部コードとともにコンパイルして実行するのを選ぶことができます。
コンパイラとテストツールの他に、Pディストリビューションは、Pコードの状態マシンの構造をグラフィカルに表示する可視化ツールも含みます。可視化は、プログラムを理解するのに便利な助けとなります。特に、状態と遷移の数が大きくなった時は。
Pディストリビューションは、{ Debug, Release } x {x86, x64 }のマトリックスで与えられる四つの構成で入手可能です。例えば、x86 の下にある、Debug ツールのためのフォルダは、Plang_Debug_x86 と呼ばれます。このフォルダの中には、二つのサブフォルダがあります。Compiler と Runtime です。Compiler フォルダは、Pプログラムを可視化、コンパイル、そしてテストするための全てのツールを持ちます。Runtime フォルダは、Pランタイムライブラリのためのバイナリとヘッダファイルを持ちます。Pプログラムの実行可能バイナリを生成するためには、標準のCコンパイラを使って、自動生成されたコードと手で書いたコードを、ヘッダファイルを参照してコンパイルし、Pランタイムライブラリとリンクします。
５．１ 可視化
可視化ツールは、コマンドラインから、PVisualizer.exe を実行して動かします。一番上にあるドロップダウンメニューから、Pファイルをロード（そしてリフレッシュ）できます。
５．２ コンパイル
コンパイラ実行形式ファイルは、pc.exe と呼ばれます。それは入力に、Pファイルと、オプショナルな引数を取ります。オプションは、コマンドラインで、pc.exe /? とすると、わかります。pc.exe foo.p コマンドを実行すると、foo.dll, program.h, program.c, そして stubs.c の４つのファイルが生成されます。最初のファイルは、foo.p の、（潜在的に非決定論的な）実行をシステマチックにテストするためのものです（５．３節で議論します）。残りの三つのファイルは、foo.p を実行するためのものです（５．４節で議論します）。
５．３ システマチックなテスト
Pプログラムを、異なる実行パスにわたってシステマチックにテストするためには、プログラマはPコンパイラが生成した dll に対して、Zinger.exe を実行しなくてはいけません。例えば、 Zinger.exe foo.dll. Zinger.exe /? とすると、Zingerのオプションの完全なリストが得られます。デフォルトのオプションの適切なセットは、以下です。
`-s -delayB:<PlangDist>\Compiler\RunToCompletionDelayingScheduler.dll -et:trace.txt`
このオプションで、Zinger は、定期的に探索統計を表示し、(-s オプション)、探索で、 Run-To-Completion 遅延スケジューラを使い、(-delayB オプション)、そして見つかった全てのエラーのトレースをファイル trace.txt に書きます(-et オプション)。無限の誤った実行の検出(ライブネスモニタがいる時に)は、高価なので、デフォルトでは有効になりません。その機能を有効にするには、 -liveness オプションを使って下さい。
５．４ 実行
ランタイムフォルダは二つのサブフォルダを持ちます。Headers と Lib です。Headers フォルダは、出力である、program.h, program.c, stub.c をコンパイルするために必要なヘッダファイルを持ちます。LibフォルダはPランタイムのダイナミックにロードされる dll を持ちます。あなたのアプリケーションを実行するには、stub.c の欠けている関数(モデルマシンと関数を使ったことから生じます)をうめて、標準のCコンパイラを使ってアプリケーションをコンパイルして下さい。
６． 用語集
略。
ライセンス
以下は、原文のライセンス https://github.com/p-org/P/blob/master/LICENSE.txt です。インラインで置きます。
The MIT License
Copyright (c) 2015 Microsoft Corporation
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED,
INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A
PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
おまけ
以下は、私が動かしたことのご紹介です。
サンプルソースは、ここにあります。
C:\Users\kanda_000\git\P>dir /b Tutorial
CoarseGrainedLocking
CoffeeMachine
Failover
Hello
P-tutorial.pptx
PingPong
Timer
C:\Users\kanda_000\git\P>dir /b src\Samples
FailureDetector
FaultTolerantDistributedSystems
ForeignTypes
LivenessBenchmarks
PingPong
PingPongFast
PingPongSimple
RefinementChecking
regressions
SimplePaxos ＜＝おお、paxos だって。
Timer
https://github.com/p-org/P/wiki/Build-P-on-Windows
に従って、 Windows でビルドした。
C:\Users\kanda_000\git\P>bld\build.bat release x64
ものすごくいろいろ、ダウンロードしてくる。
なんで、ここで止まってしまうの？メモリが無いとか？
CompileP:
########## compiling p files test.p;events.p ##################
C:\Users\kanda_000\git\P\Bld\Targets\..\Drops\Release\x64\Binaries\pc.exe /generate:C /t:PingPongSimple.4ml /shared /outputDir:C:\Users\kanda_000\git\P\Src\Samples\PingPongSimple\PGenerated /r:C:\Users\kanda_000\git\P\Src\Samples\Timer\PGenerated\Timer.4ml C:\Users\kanda_000\git\P\Src\Samples\PingPongSimple\test.p C:\Users\kanda_000\git\P\Src\Samples\PingPongSimple\events.p
バイナリはできたみたいだから、いいや。
C:\Users\kanda_000\git\P\Bld\Drops\Release\x64\Binaries>pc.exe /?
------------ Compiler Phase ------------
USAGE: Pc.exe file1.p [file2.p ...] [/t:tfile.4ml] [/r:rfile.4ml ...] [options]
Compiles *.p programs and produces .4ml summary file which can then be passed to PLink.exe
/t:file.4ml -- name of summary file produced for this compilation unit; if not supplied then file1.4ml
/r:file.4ml -- refer to another summary file
/outputDir:path -- where to write the generated files
/shared -- use the compiler service
/profile -- print detailed timing information
/generate:[C,C#,Zing]
C : generate C without model functions
C# : generate C# with model functions
Zing: generate Zing with model functions
/liveness[:sampling] -- controls compilation for Zinger
/shortFileNames -- print only file names in error messages
/dumpFormulaModel -- write the entire formula model to a file named 'output.4ml'
------------ Linker Phase ------------
USAGE: Pc.exe [linkfile.p] /link /r:file1.4ml [/r:file2.4ml ...] [options]
Links *.4ml summary files against an optional linkfile.p and generates linker.{h,c,dll}
/outputDir:path -- where to write the generated files
/shared -- use the compiler service
/profile -- print detailed timing information
Profiling can also be enabled by setting the environment variable PCOMPILE_PROFILE=1
C:\Users\kanda_000\git\P\Bld\Drops\Release\x64\Binaries>zinger /?
Usage: zinger [options] <ZingModel>
-h | -? display this message (-h or -?)
===========================
Iterative Bounding Options:
---------------------------
-fBound:<int>
Final Cutoff or Maximum bound in the case of depth or delay bounding. Default value is (int max)
-iBound:<int>
Iterative increment bound in the case of depth or delay bounding. Default value is 1
===========================
Zinger Configuration:
---------------------------
-p | -p:<n>
Degree of Parallelism during Search. -p would create no_of_worker_threads = no_of_cores.
You can control the degree of parallelism by using -p:<n>, in that case no_of_worker_threads = n
-m | -multiple
Find all bugs in the model. Dont stop exploration after finding first bug.
-s | -stats
Print Search Statistics after each Iterative Bound
-et:<filename>
Dump the generated (only trace statements) Zing error trace in file.
-entireZingTrace
Genererates detailed Zing Stack Error trace.
-timeout:<time in seconds>
Maximum amount of time to run zinger. Zinger will be terminated after time-out period
===========================
Zinger Optimizations:
---------------------------
-ct
Use trace compaction, steps from states that have single successor are not stored.
-frontiersToDisk
Dump frontier states after each iteration into files on disk.
This option should be used when you dont want store frontiers in memory.
The search will be severely slowed down because of disk access but memory consumption is minimal
-co:n
Fingerprint states having single successor with probability n/1000000 <default n = 0>.
-maxMemory:<double>GB
Maximum memory consumption during stateful search. After process consumes 70% ofmax_size (e.g. 2GB).
States are randomly replaced from the state table and frontiers are stored on disk.
===========================
Zinger Search Strategy:
---------------------------
-maxDFSStack:<int>
Maximum size of the DFS search stack. A counter example is generated if size of the stack exceeds the bound.
-randomsample:(numOfSchedulesPerIteration,maxDepth)
Zinger performs random walk without DFS stack. default is (1000,600).
-pb
Perform preemption bounding
-sched:<scheduler.dll>
Zinger performs delay bounding using the deterministic scheduler (scheduler.dll).
-bc:<int>
Bound the choice operations or bound the number of times choose(bool) returns true.
The default value is "false" for choose(bool), choice budget is used each time true is returned.
-depthb
Perform iterative depth bounding (default is delay bounded search)
===========================
Zinger Search Strategy For Liveness:
---------------------------
-NDFSliveness
To perform liveness search using NDFS <use only with sequential and non-iterative>
-randomliveness
This option uses random search based liveness algorithm.
It performs random search untill it finds a cycles in the execution.
===============================
Zinger Plugin:
-------------------------------
-plugin:<plugin.dll>
C:\Users\kanda_000\git\P>Bld\Drops\Release\x64\Binaries\pt.exe /?
---------------------------------------------
Options ::
---------------------------------------------
-h Print the help message
-v or -verbose Print the execution trace during exploration
-ns:<int> Number of schedulers <int> to explore
-lhs:<LHS Model Dll> Load the pre-computed traces of RHS Model and perform trace containment
-rhs:<RHS Model Dll> Compute all possible trace of the RHS Model using sampling and dump it in a file on disk
Hello を動かす
C:\Users\kanda_000\git\P\Tutorial\Hello>build.cmd
..
Finished generating code
Hello.vcxproj -> C:\Users\kanda_000\git\P\Tutorial\Hello\x64\Release\Hello.exe
ビルドに成功しました。
C:\Users\kanda_000\git\P\Tutorial\Hello>..\..\bld\drops\Release\x64\Binaries\pc.exe /generate:C# /shared ..\Timer\Timer.p /t:Timer.4ml /outputDir:..\Timer
ここで、止まっている。exe を msbuild で作った後、C#ソースを生成しようとして止まる。
exe は、面白いものではない。
C:\Users\kanda_000\git\P\Tutorial\Hello>x64\Release\Hello.exe
Continue (Y/N): Y
Hello
Continue (Y/N): ?
Illegal input
Continue (Y/N): N
main は、手で書いたこのファイル Main.cpp にある。
int main(int argc, char *argv[])
{
。。
ContainerProcess = PrtStartProcess(processGuid, &P_GEND_PROGRAM, ExceptionHandler, LogHandler);
PRT_MACHINEINST* machine = PrtMkMachine(ContainerProcess, P_MACHINE_Hello, 1, PRT_FUN_PARAM_CLONE, payload);
。。
これらは、生成されたファイル。
C:\Users\kanda_000\git\P\Tutorial\Hello>dir /b PGenerated
hello.4ml
hello.c
hello.h
linker.c
linker.h
hello.c を見る。
マシンの宣言。
PRT_MACHINEDECL P_MACHINE_Hello_STRUCT =
{
0U,
"Hello",
1,
4,
15,
4294967295,
P_STATE_Hello_Init,
P_GEND_VARS_Hello,
P_GEND_STATES_Hello,
P_GEND_FUNS_Hello,
0U,
NULL
};
状態の宣言。
PRT_STATEDECL P_GEND_STATES_Hello[] =
{
{
"PrintHello",
1,
0,
&P_GEND_EVENTSET,
&P_GEND_EVENTSET_TIMEOUT,
&P_GEND_EVENTSET,
P_GEND_TRANS_Hello_PrintHello,
NULL,
&P_FUN_Hello_ANON0_STRUCT,
&P_FUN_Hello_ANON7_STRUCT,
0U,
NULL
},
。。
ここの状態に対応しているらしい、 main.p のソース
state PrintHello {
entry {
StartTimer(timer, 100);
}
on TIMEOUT goto GetInput with {
print "Hello\n";
}
}
これが、上記 entry のブロックらしい。
PRT_FUNDECL P_FUN_Hello_ANON0_STRUCT =
{
0U,
NULL,
&P_FUN_Hello_ANON0_IMPL, これが、実装関数。
1U,
1U,
1U,
&P_GEND_TYPE_4,
NULL,
0U,
NULL,
0U,
NULL
};
static PRT_VALUE *P_FUN_Hello_ANON0_IMPL(PRT_MACHINEINST *context)
{
{
PRT_FUNSTACK_INFO p_tmp_frame;
PRT_MACHINEINST_PRIV *p_tmp_mach_priv;
PRT_VALUE *p_tmp_expr_0;
PRT_VALUE *p_tmp_expr_1;
PRT_VALUE *p_tmp_expr_2;
PRT_VALUE *p_tmp_funstmt_ret;
PRT_VALUE *p_tmp_ret;
p_tmp_mach_priv = (PRT_MACHINEINST_PRIV *)context;
p_tmp_ret = NULL;
PrtPopFrame(p_tmp_mach_priv, &p_tmp_frame);
if (p_tmp_frame.returnTo == 2U)
{
goto L2;
}
P_EXPR_2(P_SEQ(PrtPushNewFrame(p_tmp_mach_priv, PRT_FALSE, P_FUN_StartTimer, PRT_FUN_PARAM_CLONE, p_tmp_expr_0, PRT_FUN_PARAM_CLONE, p_tmp_expr_1), NULL), PRT_FALSE, &P_GEND_VALUE_0, PRT_FALSE, p_tmp_mach_priv->varValues[P_VAR_Hello_timer], PRT_FALSE);
L2:
p_tmp_funstmt_ret = PrtWrapFunStmt(&p_tmp_frame, 2U, p_tmp_mach_priv, P_FUN_StartTimer);
if (p_tmp_mach_priv->receive != NULL)
{
return p_tmp_funstmt_ret;
}
if (p_tmp_mach_priv->lastOperation != ReturnStatement)
{
goto P_EXIT_FUN;
}
if (p_tmp_funstmt_ret != NULL)
{
PrtFreeValue(p_tmp_funstmt_ret);
}
goto P_EXIT_FUN;
P_EXIT_FUN:
PrtFreeLocals(p_tmp_mach_priv, &p_tmp_frame);
return p_tmp_ret;
}
}
いかにも状態マシン。
タスクマネージャーで見ると、 CompilerService が、メモリを５００MBくらい使って、CPU ０％で止まっている。
これを、「タスクの終了」して、もう一度、 pc.exe を動かすと、うまくいく。なぜかは不明。メモリ４GBの、 Windows 10 です。
C:\Users\kanda_000\git\P\Tutorial\Hello>%pc% /generate:C# /shared Main.p /t:Hello.4ml /r:..\Timer\timer.4ml
Writing hello.cs ...
Writing hello.4ml ...
生成されたソース。
C:\Users\kanda_000\git\P\Tutorial\Hello>more hello.cs
#pragma warning disable CS0162, CS0164, CS0168, CS0649
namespace P.Program
{
using P.Runtime;
using System;
using System.Collections.Generic;
public partial class Application : StateImpl
。。
C:\Users\kanda_000\git\P\Tutorial\Hello>%pc% /generate:C# /link /shared TestScript.p /r:Hello.4ml /r:..\Timer\timer.4ml
Writing Test0.cs ...
Writing Test0.dll ...
これが、探索と検証らしい。一瞬で終わった。
C:\Users\kanda_000\git\P\Tutorial\Hello>%pt% /psharp Test0.dll
... Task 0 is using 'Random' strategy (seed:).
..... Iteration #1
。。
..... Iteration #100
Bugs found: 0
Dumping coverage information
... Writing coverage.txt
... Writing coverage.dgml
C:\Users\kanda_000\git\P\Tutorial\Hello>more coverage.txt
Total event coverage: 100.0%
Machine: Hello
***************
Machine event coverage: 100.0%
State: Hello_PrintHello
State event coverage: 100.0%
Events Received: TIMEOUT
Events Sent: START
Previous States: Hello_GetInput
Next States: Hello_GetInput
。。
ピンポンに、バグを入れてみる。
C:\Users\kanda_000\git\P\Tutorial\PingPong>git diff .
diff --git a/Tutorial/PingPong/PingPong.p b/Tutorial/PingPong/PingPong.p
index 42c9341..55fda66 100644
--- a/Tutorial/PingPong/PingPong.p
+++ b/Tutorial/PingPong/PingPong.p
@@ -74,6 +74,7 @@ sends PONG, START;
on TIMEOUT goto WaitPing with {
print "Server sending PONG\n";
send client, PONG;
+ send client, PONG; // BUG!
}
C:\Users\kanda_000\git\P\Tutorial\PingPong>%pt% /psharp Test0.dll
... Task 0 is using 'Random' strategy (seed:).
..... Iteration #1
Bugs found: 1
<CreateLog> Created spec Machine Safety
<CreateLog> Created Machine TestMachine0-1
<StateLog> Machine TestMachine0-1 entering State TestMachine0_Init
<CreateLog> Created Machine Client-1
<StateLog> Machine Client-1 entering State Client_Init
<PrintLog> Client created
。。
<PrintLog> Server sending PONG
<EnqueueLog> Enqueued Event <PONG, null> in Client-1 by Server-1
<AnnounceLog> Enqueued Event <PONG, null> to Spec Machine Safety
<StateLog> Machine Timer-1 entering State Timer_WaitForReq
<EnqueueLog> Enqueued Event <PONG, null> in Client-1 by Server-1
ERROR: < Exception > Attempting to enqueue event PONG more than max instance of 1\n
すげえ。
疑問点
raft, 二相コミットのサンプルを読んでいます。
ディスクに書く操作が無い。落ちて、メモリを失って、最初から動く操作が書けない。
うーん。これで、分散システムの完全なモデルが書けて、状態を網羅できるのだろうか。
以上