以下は、P# 言語 のマニュアル https://github.com/p-org/PSharp/wiki/Walkthrough-and-Samples の、２０１７年６月時点の、kanda.motohiro@gmail.com による訳です。MIT License の下で公開します。P言語のチュートリアル も参照。
P# は、Roslyn コンパイラ https://github.com/dotnet/roslyn の上に構築されます。それは、マシンを作り、あるマシンから他にイベントを送り、システムの属性に関して、アサーションを書くための、新しい C# 言語プリミティブ(それらはほぼ、マイクロソフトの P プログラミング言語 https://github.com/p-org/P をもとにします)を提供します。
それぞれのマシンは、入力キュー状態、状態遷移、イベントハンドラ、フィールド、そしてメソッドを持ちます。マシンはお互いに、並列に走ります。それぞれのマシンは、入力キューからイベントをデキューして、操作のシーケンスを実行してそれを処理するという、イベントループを実行します。操作は、フィールドを更新し、新しいマシンを作り、他のマシンにイベントを送ったりします。
P# では、マシンを作る操作と、送信操作はノンブロッキングです。送信操作の場合、メッセージは単に、目的マシンの入力キューにエンキューされます。
P# のいろいろな使い方
P# を使って、既存システムをテストしたり、新しい高信頼システムを構築するには多くの異なる方法があります。
・P# は、既存のメッセージパッシングシステムの環境(例えば、クライアント)そして/あるいはそのシステムのコンポーネントをモデリングすることによって、 それをシステマチックにテストするために、単純に使うことができます。
・P# の surface syntax を使って、システム全体をスクラッチから書くために使うことができます(この例 https://github.com/p-org/PSharp/blob/master/Samples/PingPong/PingPong.PSharpLanguage/Server.psharp を参照下さい)。surface P# シンタックスは、ラピッドプロトタイプに適した新しい言語要素を使って、直接、C# を拡張します。しかし、surface syntax を使うには、開発者は、Roslyn の上に構築された P# コンパイラを使う必要があります。このアプローチの主な欠点は、P# がまだ、Visual Studio 統合開発環境（IDE)と完全に統合されていないことです。このため、IntelliSense のような生産性を高める機能（例えば、自動補完や自動リファクタリング）がサポートされません。なお、私たちは活発にこの作業を行なっています（ここ https://github.com/p-org/PSharp/issues/128 を参照下さい）。
・P# を、C# ライブラリとして使って、システム全体をスクラッチから書くことができます(この例 https://github.com/p-org/PSharp/blob/master/Samples/PingPong/PingPong.PSharpLibrary/Server.cs を参照下さい)。このアプローチは、前項よりも少し冗長ですが、Visual Studio との完全な統合ができます。このガイドのほとんどの例は、冗長性が低いので、 P# surface syntax を使うことに注意下さい。
このガイドでは、高レベルの P# シンタックスを使ったプログラムの書き方を示しますが、P# を C# ライブラリとして使う時にも、同じ原理が適用されます(P# ライブラリを使ったプログラムの例を、以下で示します)。
P# プログラムの基本機能
P# プログラムは、event と machine 宣言の集まりです。オプショナルで、class と struct のような、C# のトップレベル宣言も含みます。C# と同様に、全てのトップレベル宣言は、namespace の中で宣言されなくてはいけません。P# 高レベルシンタックスを使うならば、イベントとマシンは .psharp ファイル内に宣言されなくてはいけません。そして、C# トップレベル宣言は、.cs ファイル内に宣言されなくてはいけません。一方、P# を C# ライブラリとして使うならば、全てのコードは、.cs ファイル内に書かなくてはいけません。
状態マシンは、P# 言語の一級市民であり、このように宣言します。
machine Server { ... }
上記コード断片は、Server という名の P# マシンを宣言します。マシン宣言は、C# のクラス宣言と似ており、任意の数のフィールドとメソッドを持つことができます。例えば、以下のコード断片は、machine 型のフィールド client を宣言します。この型のオブジェクトは、マシンインスタンスへの参照を持ちます。
machine Server {
machine client;
}
クラスとマシン宣言の主な違いは、後者は一つ以上の状態も宣言しなくてはいけないことです。
machine Server {
machine client;
start state Init { ... }
state Active { ... }
}
上記は、Server マシンに二つの状態、 Init と Active を宣言します。P# 開発者は、初期状態を宣言するときに、start モディファイアを使わなくてはいけません。それは、マシンが、インスタンス化した時に、遷移する最初の状態です。この例では、Init 状態が、Server の初期状態であると宣言されています。マシンあたり、一つだけの状態を、初期状態と宣言できることに注意ください。state 宣言は、オプショナルで、多くの状態固有のアクションを含むことができます。以下のコード断片を参照。
state SomeState {
entry { ... }
exit { ... }
}
entry { ... } で示されるコードブロックは、マシンがその状態に遷移したときに実行されるアクションを示します。またexit { ... } で示されるコードブロックは、マシンがその状態を抜けるときに実行されるアクションを示します。P# のアクションは、要するに、入力パラメタがなく、void 戻り値の C# メソッドです。P# のアクションは、任意の P# と C# の文を含みます。しかし、私たちは、非同期の源を全て、P# を使って明示的に宣言したいため、P# マシン内では、シーケンシャルな C# コードだけを使うことができます。例外 https://github.com/p-org/PSharp/wiki/Object-Sharing-in-P%23 もあります。実際は、私たちは、C# コードがシーケンシャルであると推定するだけです。現実世界のプログラムでこの規則を強制するのはとても難しいでしょうから。
以下は、entry アクションの例です。
entry {
this.client = create(Client);
send(this.client, Config, this);
send(this.client, Ping);
raise(Unit);
}
前記アクションは、三つの最も重要な P# 文を含みます。create 文は、Client マシンの新しいインスタンスを作るために使います。このインスタンスへの参照が、client フィールドに格納されます。次に、 send 文は、イベント（この場合、イベントは、 Config と Ping）を目的マシン（この場合、client フィールドに格納されているアドレスを持つマシン）に送るために使います。
イベントが送られたらそれは、目的マシンのイベントキューにエンキューされます。そのマシンは次に、受信したイベントをデキューして、送信マシンとは非同期にそれを処理します。最後に、 raise 文は、コール元マシン（つまり、自分自身）にイベントを送るために使います。send を呼ぶのと同じように、マシンがイベントをレイズすると、それはそれを囲むコードブロックをまだ、実行し続けます。
訳注。あれ、raise の次の文は実行されるのだっけ。
しかし、現在のマシンアクションが終わったら、インボックスからデキューする代わりに、マシンは直ちに、レイズされたイベントを処理します。
P# では、イベント (例えば、上の例の Ping, Unit と Config ）はこのように宣言します。
event Ping;
event Unit;
event Config (target: machine);
P# マシンは、イベントのペイロードとして、データ（スカラー値あるいは参照）を、目的マシンに送ることができます。そのようなイベントは、ペイロードの型を、その宣言に指定しなくてはいけません（上記の Config イベントのように）。マシンは、raise を使って、自分自身にイベントを送ることもできます（例えば、後の状態で処理するために）。
上記の例で、Server マシンは client マシンに、 this (つまり、現在のマシンインスタンスへの参照)を送ります。受信者(この場合 client)は、送られたデータを、trigger キーワード(あるいは P# を C# ライブラリとして使う時は、ReceivedEvent )、それは受信したイベントへのハンドルです、を使って取り出すことができます。triggerを、期待されるイベント型(今の場合、Config)にキャストして、受信したイベントのフィールドとしてペイロードをアクセスできます。
前に述べたように、createと send 文はノンブロッキングです。P# ランタイムは、隠された非同期性の全てを、Task Parallel Library を使って面倒をみます。なので、開発者が明示的にタスクを作ったり管理する必要はありません。
P# 状態内で、entry と exit 宣言以外のすべての他の宣言は、イベント処理に関係します。それは P# の鍵となる特徴です。イベントハンドラは、P# マシンがどのように受信したイベントに応答するべきかを宣言します。あり得る応答は、一つ以上のマシンインスタンスを作る、一つ以上のイベントを送る、あるいは、いくらかのローカルデータを処理する、などです。以下は、P# で最も重要な二つのイベント処理宣言です。
state SomeState {
on Unit goto AnotherState;
on Pong do SomeAction;
}
on Unit goto AnotherState 宣言は、このマシンが、SomeState で Unit イベントを受けたら、それは Unit を、その状態から抜けて、AnotherState に遷移することで処理しなくてはいけないことを示します。on Pong do SomeAction 宣言は、Pong イベントは、SomeAction を呼ぶことで処理しなくてはいけないことを示します。そのマシンは、SomeState に留まります。
P# はまた、無名のイベントハンドラもサポートします。例えば、 on Pong do { … } の宣言は無名のイベントハンドラで、Pong イベントがデキューされた時に、かっこの中の文のブロックが実行されなくてはいけないことを示します。あるマシンの特定の状態では、それぞれのイベントは最大でも一つのイベントと関連付きます。もし P# マシンが SomeState 状態にあり、SomeEvent をデキューしたけれど、SomeState には、SomeEvent のためのイベントハンドラが何も宣言されていない時は、P# は適切な例外を投げます。
上記のイベント処理の宣言以外に、P# は特定の状態でイベントを遅延あるいは無視する能力も提供します。
state SomeState {
defer Ping;
ignore Unit;
}
defer Ping の宣言は、マシンが、SomeState にある間は、Ping イベントはデキューされるべきでないことを示します。その代わり、マシンは Ping イベントを飛び越えて(Ping をキューからドロップすることもなく)、遅延されていない次のイベントをデキューするべきです。ignore Unit の宣言は、マシンが、SomeState にある間は、Unit がデキューされたら必ず、そのマシンは Unit を、アクションを何も呼ばないでドロップするべきであることを示します。
P# はまた、マシンのローカル状態に関して、不変量(つまり、アサーション)を指定することもサポートします。開発者は、assert 文を使って、それができます。それは、その特定のプログラム地点で、常に成立しなければいけない述語を入力に取ります。例えば、assert(k == 0) は、整数 k がゼロに等しい時に成立します。
単純なプログラム例
以下の P# プログラムは、Ping と Pong イベントを使って非同期に通信する Client マシンと Server マシンです。
namespace PingPong {
event Ping; // Client sends this event to the Server
event Pong; // Server sends this event to the Client
event Unit; // Event used for local transitions
// Event used for configuration, can take a payload
event Config (target: machine);
machine Server {
machine client;
start state Init {
entry {
// Instantiates the Client
this.client = create(Client);
// Sends event to client to configure it
send(this.client, Config, this);
raise(Unit); // Sends an event to itself
}
on Unit goto Active; // Performs a state transition
}
state Active {
on Ping do {
// Sends a Pong event to the Client
send(this.client, Pong);
};
}
}
machine Client {
machine server;
start state Init {
on Config do Configure; // Handles the event
on Unit goto Active; // Performs a state transition
}
void Configure() {
// Receives reference to Server
this.server = (trigger as Config).target;
raise(Unit); // Sends an event to itself
}
state Active {
entry {
SendPing();
}
on Pong do SendPing;
}
void SendPing() {
// Sends a Ping event to the Server
send(this.server, Ping);
}
}
public class HostProgram {
static void Main(string[] args) {
PSharpRuntime.Create().CreateMachine(typeof(Server));
Console.ReadLine();
}
}
}
上記の例では、プログラムはServer マシンのインスタンスを作ることから始めます。それぞれの P# マシンの、暗黙的なコンストラクタは、そのマシンの、P# ランタイムの内部的なデータを初期化します。それには、イベントキュー、使用可能な状態のセット、そして状態ごとの、イベントからイベントハンドラへのマップが含まれます。
Server マシンが初期化されたら、P# ランタイムは、Server の初期 (Init) 状態の entry アクションを実行します。それはまず、Client マシンのインスタンスを作り、Config イベントを Client マシンに送ります。ペイロードには、this 参照を置きます。次に、Unit イベントをレイズします。以前述べたように、マシンが raise を呼ぶと、それはキューをバイパスし、まず、レイズされたイベントを処理します。この場合、Server マシンは、Active 状態に遷移することで、Unit を処理します。
Client は、Server に作られると、(非同期に)実行を始めます。Client マシンは、受け取ったペイロード(それは Server マシンへの参照です)を、server フィールドに格納して、Unit をレイズして、Active 状態に遷移します。新しい状態で、Client は、SendPing メソッドを呼んで、Ping イベントを Server に送ります。次に、Server マシンは、Ping をデキューして、Client に Pong イベントを送ることでそれを処理します。次にまた、Client は新しい Ping イベントを Server に送ることで応答します。この、Ping と Pong の非同期の交換は、無限に続きます。
P# プログラムのエントリポイント
P# は、C# 言語の上に構築されているので、P# プログラムのエントリポイント(つまり、P# ランタイムが最初にインスタンス化し、実行するマシン)は、ホスト C# プログラム内(典型的には、Main メソッド中)に、以下のように明示的に宣言される必要があります。
using Microsoft.PSharp;
public class HostProgram {
static void Main(string[] args) {
PSharpRuntime.Create().CreateMachine(typeof(Server));
Console.ReadLine();
}
}
開発者はまず、P# ランタイムライブラリ (Microsoft.PSharp.dll) をインポートして、PSharpRuntime インスタンスを作り、最後に、CreateMachine ランタイムメソッドを呼んで、最初の P# マシン(上の例では、Server)をインスタンス化します。
CreateMachine メソッドは、PSharpRuntimeが公開する、.NET interoperability API (ネイティブ C# コードから P# を呼ぶためのメソッドのセット)の一部です。このメソッドは、インスタンス化するマシンの型をパラメタに取り、MachineId 型のオブジェクトを返します。それは、作成された P# マシンの参照を持ちます。CreateMachine は非同期なメソッドですから、私たちは、Console.ReadLine メソッドを呼びます。それは、コンソール入力があるまで、メインスレッドを止めます。そうして、ホスト C# プログラムが勝手に終わらないようにします。
PSharpRuntimeの、.NET interoperability API はまた、ネイティブ C# から P# マシンにイベントを送るための、SendEvent メソッドを提供します。このメソッドは、パラメタとして、MachineId 型のオブジェクトと、イベント、そしてオプショナルのペイロードを取ります。開発者はネイティブ C# から P# コードを呼ぶためには、CreateMachine と SendEvent を使わなくてはいけません。しかしその逆は、簡単です。P# コードから、C# オブジェクトをアクセスするだけですから。
P# を C# ライブラリとして使う
前記の例は、P# を C# ライブラリとして使って、このように書くことができます。
using System;
using Microsoft.PSharp;
namespace PingPong {
class Unit : Event { }
class Ping : Event { }
class Pong : Event { }
class Config : Event {
public MachineId Target;
public Config(MachineId target) : base() {
this.Target = target;
}
}
class Server : Machine {
MachineId Client;
[Start]
[OnEntry(nameof(InitOnEntry))]
[OnEventGotoState(typeof(Unit), typeof(Active))]
class Init : MachineState { }
void InitOnEntry() {
this.Client = this.CreateMachine(typeof(Client));
this.Send(this.Client, new Config(this));
this.Raise(new Unit());
}
[OnEventDoAction(typeof(Pong), nameof(SendPing))]
class Active : MachineState {
protected override void OnEntry() {
(this.Machine as Server).SendPing();
}
}
void SendPing() {
this.Send(this.Client, new Ping());
}
}
class Client : Machine {
MachineId Server;
[Start]
[OnEventGotoState(typeof(Unit), typeof(Active))]
[OnEventDoAction(typeof(Config), nameof(Configure))]
class Init : MachineState { }
void Configure() {
this.Server = (this.ReceivedEvent as Config).Trigger;
this.Raise(new Unit());
}
[OnEventDoAction(typeof(Ping), nameof(SendPong))]
class Active : MachineState { }
void SendPong() {
this.Send(this.Server, new Pong());
}
}
public class Program {
static void Main(string[] args) {
PSharpRuntime.CreateMachine(typeof(Server));
Console.ReadLine();
}
}
}
プログラマは、Microsoft.PSharp.dll ライブラリをインポートすることで、P# をライブラリとして使うことができます。P# マシンを宣言するには、Machine 型（P# ライブラリが提供します）を継承する C# クラスを作ります。状態は、 MachineState 型を継承する C# クラスを作ります。この状態クラスは、マシンクラスの中にネストしなければいけません（状態以外の他のクラスを、マシンクラスの中にネストすることはできません）。start 状態は、[Start] 属性を使って宣言します。
状態遷移は、[OnEventGotoState(...)] 属性を使って宣言します。属性の最初の引数は受信したイベントの型で、二つ目の引数は、目的状態の型です。オプショナルの三つ目の引数は、今の状態を抜けた後、新しい状態に入る前に実行されるべきメソッドの名前を示す文字列です。同様に、アクションのハンドラは、[OnEventDoAction(...)] 属性で宣言します。属性の最初の引数は受信したイベントの型で、二つ目の引数は、実行するアクションの名前です。全ての P# 文（例えば、 send と raise）は、Machine と MachineState クラスのメソッド呼び出しとして公開されます。
P# の高度な機能
以下は、P# のより高度な機能の議論です。それには、明示的なマシンの終了、システムのコンポーネントと環境のモデリング、そして安全性とライブネス属性の指定が含まれます。
P# マシンの明示的な終了
P# マシンを明示的に終わらせるためには、それは、P# ランタイムが提供する、halt という名の特別なイベント(ユーザはそれを宣言できません）をデキューしなくてはいけません。halt イベント（P# をライブラリとして使う時には Halt）は、レイズしたり、あるいは他のマシンに送ることができます。処理されない halt イベントによるマシンの修了は、有効なふるまいです（P# ランタイムはエラーを報告しません）。形式的操作セマンティクスの観点からは、終了したマシンは完全に応答可能で、それに送られる全てのイベントを消費します。P# ランタイムはこのセマンティクスを、終了するマシンに確保された資源をクリーンアップして、そしてそのマシンが終了したことを記録することによって、効率的に実装します。終了したマシンに送られたイベントは、単純にドロップされます。終了したマシンは再開始できません。それは、永遠に、終了したままです。
システムコンポーネントを P# を使ってモデリングする
上記の図は、私達の P# テスト技法を説明する目的で作り上げた、単純な分散ストレージシステムの擬似コードです。このシステムは、クライアント、サーバ、そして３つのストレージノード（SN)からなります。クライアントはサーバに、ClientReq メッセージを投げます。それには、複製されるべきデータ (DataToReplicate) が含まれます。クライアントは次の要求を投げる前に、アクノリッジメントを（receive メソッドを呼んで）待ちます。サーバは ClientReq を受けたとき、まずそのデータをローカルに（Data フィールドに）格納し、ReplReq メッセージを全ての SN にブロードキャストします。SN は ReplReq を受けた時、そのメッセージを、受け取ったデータをローカルに格納する（store メソッドを呼ぶことで）ことで処理します。それぞれの SN にはタイマーがあり、定期的に Timeout メッセージを送ります。Timeout を受けたら、SN はサーバに、Sync メッセージを送ります。それは、ストレージログを持ちます。サーバは、isUpToDate メソッドを呼んで、SN のログがアップトゥーデートであるかをチェックすることで、Sync メッセージを処理します。そうでない場合、サーバは、古くなった SN に、繰り返しの ReplReq メッセージを送ります。SN ログがアップトゥーデートならば、サーバは、複製カウンタを一つ加算します。最後に、三つの複製が使用可能な時、サーバはクライアントに Ack メッセージを送ります。
この例には、二つのバグがあります。最初のは、サーバが、一意の複製を追跡しないことです。複製カウンタは、アップトゥーデートな Sync ごとに加算されます。同期する SN が既に複製に数えられていてもです。これは、サーバは、三つより小さい複製しか存在しない時に Ack メッセージを送る可能性があることを意味します。これは誤ったふるまいです。二つ目のバグは、サーバが、Ack メッセージを送ったときに、複製カウンタをゼロにリセットしないことです。これは、クライアントが次の ClientReq メッセージを送った時に、それは決して Ack を受け取らず、無限にブロックすることを意味します。この例をシステマチックにテストするために、開発者はまず、P# テストハーネスを作らなくてはいけません。そして次に、システムの正しさの属性を指定します。
以下の図は、前記二つのバグを見つけるためのテストハーネスです。
図のそれぞれの箱は、並列に実行する P# マシンで、矢印は、あるマシンから他に送られるイベントを示します。箱には三種類あります。(i) 角が丸で、ふちが太い箱は、P# マシンにラップされる実際のコンポーネントを示します。(ii)ふちが細い箱はモデルされたコンポーネントを示します。 (iii)破線のふちの箱は、安全性あるいはライブネスのチェックのために使われる特別の P# マシンを示します（以下を参照）。
サーバコンポーネントはモデルしません。私たちはその実際の実装をテストしたいからです。サーバは、P# マシン内にラップされます。それは、(i)システムメッセージを、実際のネットワークの代わりに、（P# イベントのペイロードとして）P# の send(...) メソッドを使って送り、 (ii) 受信したメッセージをラップされたコンポーネントに届ける役割を果たします。私たちは SN をモデルします。それは、データを、ディスクでなく、メモリに格納します（テストのためにはそのほうが、効率的です）。私たちはまた、クライアントもモデルします。クライアントは、繰り返し、非決定論に生成された ClientReq を送り、Ack イベントを待つことによって、システムをドライブすることができます。最後に、私たちはタイマーをモデルします。P# が、システム内の、時間に関連する非決定論的ふるまいの全てを制御するためです。これにより、P# テストエンジンはテストの間、Timeout イベントがいつ、SN に送られるかを制御でき、（システマチックに）異なるスケジュールを探索できます。
P# は、実際のコードとモデルされたコードをつなぐために、インタフェースと、ダイナミックメソッドディスパッチなどのオブジェクト指向言語の機能を使います。産業界の開発者はそのような機能を使うことに慣れており、本番システムをテストする時には大いにそれを活用しています。私達の経験によると、これは、マイクロソフト内の技術者チームが、テストに P# を受け入れるための障壁を大いに低くしました。
安全性属性を書く
安全性属性の指定は、ソースコードアサーションの概念を一般化します。安全性属性の違反は、誤った状態に至る、有限のトレースです。P# は、ある P# マシンにローカルな安全性属性を指定するための通常のアサーションをサポートします。そしてさらに、安全性モニタの形で、グローバルなアサーションを指定する方法も提供します。それは、イベントを受信し、送信しない特別な P# マシンです。
安全性モニタは、通常の(モニタではない)マシンから受信したイベントに応じて変更されるローカルな状態を維持します。このローカル状態は、指定された属性に関連する計算の履歴を維持するために使われます。誤ったグローバルなふるまいは、安全性モニタのプライベートな状態に対してのアサーションを使ってフラグされます。このようにして、モニタは、指定のために必要なインストゥルメンテーション状態(モニタの内の)と、プログラム状態(モニタの外の)をクリーンに分離します。
前記の例の最初のバグは、安全性バグです。それを見つけるために、開発者は一意の SN id からブール値へのマップを持つ安全性モニタを書くことができます。それは、その SN が複製かどうかを示します。SN が最新データを複製する時に毎回、それはモニタに、マップを更新するように通知します。サーバが Ack を発行する時に毎回、それはまた、モニタに通知します。もしモニタが、三つの複製が実際に存在しないのに Ack が送られたことを検出したら、安全性違反が発火します。以下のコード断片は、この安全性モニタの P# ソースコードです。
monitor SafetyMonitor {
// Map from unique SNs ids to a boolean value
// that denotes if a node is replica or not
Dictionary<int, bool> replicas;
start state Checking {
entry {
var node_ids = (HashSet<int>)payload;
this.replicas = new Dictionary<int, bool>();
foreach (var id in node_ids) {
this.replicas.Add(id, false);
}
}
// Notification that the SN is up-to-date
on NotifyUpdated do {
var node_id = (int)payload;
this.replicas[node_id] = true;
};
// Notification that the SN is out-of-date
on NotifyOutdated do {
var node_id = (int)payload;
this.replicas[node_id] = false;
};
// Notification that an Ack was issued
on NotifyAck do {
// Assert that 3 replicas exist
assert(this.replicas.All(n => n.Value));
};
}
}
ライブネス属性を書く
ライブネス属性の指定は、終わらないことを一般化します。ライブネス属性の違反は、進行の見られない無限のトレースです。典型的には、ライブネス属性は、時相論理の形式を使って指定されます。私たちは異なるアプローチを取り、開発者がライブネスモニタを書けるようにします。安全性モニタと同様、ライブネスモニタはイベントを受信しますが、送信しません。
ライブネスモニタは二つの特別の状態を持ちます。ホットとコールド状態です。ホット状態は、進行が必要であるが、まだそれが起きていない、実行内の地点を示します。例えば、ノードが落ちて、新しいノードがまだ起動していない時です。ライブネスモニタは、システムが進行をしないといけないことを通知された時にホット状態に遷移します。ライブネスモニタは、システムが進行したことを通知された時に、ホット状態を抜けてコールド状態に入ります。ライブネスモニタが、無限に長い期間、ホット状態に留まるならば、その無限実行は誤りです。私たちのライブネスモニタは、任意の時相論理属性をエンコードできます。
ライブネス属性の違反は、全ての並列実行する P# マシンが公平にスケジュールされている、無限の実行によって発見されます。プログラムを有限時間、動かして、無限の実行時間を生成するのは不可能なので、私たちの P# でのライブネスのチェックの実装は、いくつかのヒューリスティクスを使って、無限実行を近似します。ここでは私たちは、ユーザが提供した最大値よりも長い実行を「無限」実行と考えます。このヒューリスティクスを使う時には、公平性のチェックは無関係であることに注意ください。それは、私達が、大きな最大値を現実的に使うためです。
上記の例の二つ目のバグは、ライブネスのバグです。それを検出するために、開発者は、ライブネスモニタを書きます。モニタは、クライアントが ClientReq を送って、Ack を待っていることを示すホット状態から、サーバが、最後の ClientReq への応答として、Ack を送ったことを示すコールド状態へと遷移します。サーバが ClientReq を受け取るたびに、それは、モニタに、ホット状態へと遷移するように通知します。サーバが Ack を送るたびに、それはモニタに、コールド状態へと遷移するように通知します。もしモニタが、無限実行の最大値が終わってもホット状態にあるならば、ライブネスの違反が発火します。以下のコード断片は、このライブネスモニタの P# ソースコードです。
monitor LivenessMonitor {
start hot state Progressing {
// Notification that the server issued an Ack
on NotifyAck do {
raise(Unit);
};
on Unit goto Progressed;
}
cold state Progressed {
// Notification that server received ClientReq
on NotifyClientRequest do {
raise(Unit);
};
on Unit goto Progressing;
}
}
サンプル P# プログラム
私たちはサンプルのコレクションを提供します。それは、非同期でイベントドリブンのアプリケーションを、P# フレームワークを使ってどのように構築し、システマチックにテストするかを示します。P# サンプルは Git リポジトリの、Samples ディレクトリの下にあります。
詳しくは、ここ https://github.com/p-org/PSharp/tree/master/Samples を参照。
ライセンス
以下は、原文のライセンス https://github.com/p-org/PSharp/blob/master/LICENSE.txt です。インラインで置きます。
The MIT License
Copyright (c) 2017 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.
おまけ
VS2015 IDE で、PSharp.sln を開き、 Restore Nuget Packages をやって、Build Solution をした。Binaries に PSharpCompiler.exe、PSharpTester.exe などができる。
C:\Users\kanda_000\git\PSharp\Binaries>PSharpCompiler.exe /?
--------------
Basic options:
--------------
/? Show this help menu
/s:[x] Path to a P# solution
/p:[x] Name of a project in the P# solution
/o:[x] Path for output files
/timeout:[x] Timeout for the tool (default is no timeout)
/v:[x] Enable verbose mode (values from '1' to '3')
/warnings-on Show warnings
/debug Enable debugging
--------------------
Compilation options:
--------------------
/t:[x] The compilation target ('exe', 'lib' or 'test')
--------------------
Analysis options:
--------------------
/dfa Enables data-flow analysis
/check-races Enables race-checking analysis
C:\Users\kanda_000\git\PSharp\Binaries>PSharpTester.exe /?
--------------
Basic options:
--------------
/? Show this help menu
/test:[x] Path to the P# program to test
/method:[x] Suffix of the test method to execute
/timeout:[x] Timeout in seconds (disabled by default)
/v:[x] Enable verbose mode (values from '1' to '3')
/o:[x] Dump output to directory x (absolute path or relative to current directory)
---------------------------
Systematic testing options:
---------------------------
/i:[x] Number of schedules to explore for bugs
/parallel:[x] Number of parallel testing tasks ('1' by default)
/sch:[x] Choose a systematic testing strategy ('random' by default)
/max-steps:[x] Max scheduling steps to be explored (disabled by default)
---------------------------
Testing code coverage options:
---------------------------
/coverage-report Print code coverage statistics
Samples\PingPong\README.md に従って、ピンポンサンプルの一番簡単なやつをビルドした。
C:\Users\kanda_000\git\PSharp\Samples\PingPong\PingPong.PSharpLanguage>msbuild /p:configuration=release
。。
CopyFilesToOutputDirectory:
"obj\release\PingPong.PSharpLanguage.exe" から "..\Binaries\Release\PingPong.PSharpLanguage.exe" へファイルをコピーしています。
プロジェクト "C:\Users\kanda_000\git\PSharp\Samples\PingPong\PingPong.PSharpLanguage\PingPong.PSharpLanguage.csproj" (既定のターゲット) のビルドが完了しました。
動かす。
C:\Users\kanda_000\git\PSharp\Samples\PingPong\Binaries\Release>PingPong.PSharpLanguage.exe
<CreateLog> Machine 'PingPong.PSharpLanguage.NetworkEnvironment(1)' is created.
Press Enter to terminate...
<StateLog> Machine 'PingPong.PSharpLanguage.NetworkEnvironment(1)' enters state 'PingPong.PSharpLanguage.NetworkEnvironment.Init'.
。。
<PopLog> Machine 'PingPong.PSharpLanguage.Client(3)' popped with unhandled event 'Microsoft.PSharp.Halt'.
<HaltLog> Machine 'PingPong.PSharpLanguage.Client(3)' halted.
テストする。
C:\Users\kanda_000\git\PSharp\Samples\PingPong\Binaries\Release>C:\Users\kanda_000\git\PSharp\Binaries\PSharpTester.exe /test:PingPong.PSharpLanguage.exe /i:100
. Testing PingPong.PSharpLanguage.exe
... Created '1' testing task.
... Task 0 is using 'Random' strategy (seed:967).
..... Iteration #1
。。
..... Iteration #100
... Testing statistics:
..... Found 0 bugs.
... Scheduling statistics:
..... Explored 100 schedules: 100 fair and 0 unfair.
..... Number of scheduling points in fair terminating schedules: 23 (min), 23 (avg), 24 (max).
... Elapsed 3.8724914 sec.
. Done
ピンポンにバグを入れる。
C:\Users\kanda_000\git\PSharp\Samples\PingPong\PingPong.PSharpLanguage>git diff .
diff --git a/Samples/PingPong/PingPong.PSharpLanguage/Server.psharp b/Samples/PingPong/PingPong.PSharpLanguage/Server.psharp
index f1bb511..57a69aa 100644
--- a/Samples/PingPong/PingPong.PSharpLanguage/Server.psharp
+++ b/Samples/PingPong/PingPong.PSharpLanguage/Server.psharp
@@ -28,7 +28,7 @@
// the 'Ping' event).
var client = (trigger as Client.Ping).client;
// Sends (asynchronously) a 'Pong' event to the client.
- send(client, Pong);
+ send(client, Client.Ping, this); // BUG!
}
}
C:\Users\kanda_000\git\PSharp\Samples\PingPong\Binaries\Release>\Users\kanda_000\git\PSharp\Binaries\PSharpTester.exe /test:PingPong.PSharpLanguage.exe /i:100
. Testing PingPong.PSharpLanguage.exe
... Created '1' testing task.
... Task 0 is using 'Random' strategy (seed:374).
..... Iteration #1
... Task 0 found a bug.
... Emitting task 0 traces:
..... Writing .\Output\PingPong.PSharpLanguage_0_0.txt
..... Writing .\Output\PingPong.PSharpLanguage_0_0.pstrace
..... Writing .\Output\PingPong.PSharpLanguage_0_0.schedule
... Testing statistics:
..... Found 1 bug.
... Scheduling statistics:
..... Explored 1 schedule: 1 fair and 0 unfair.
..... Found 100.00% buggy schedules.
..... Number of scheduling points in fair terminating schedules: 10 (min), 10 (avg), 10 (max).
... Elapsed 2.5383851 sec.
. Done
C:\Users\kanda_000\git\PSharp\Samples\PingPong\Binaries\Release\Output>more PingPong.PSharpLanguage_0_0.txt
<TestHarnessLog> Running test method 'PingPong.PSharpLanguage.Program.Execute'.
。。
<PopLog> Machine 'PingPong.PSharpLanguage.Client(4)' popped with unhandled event 'PingPong.PSharpLanguage.Client+Ping'.
<ErrorLog> Machine 'PingPong.PSharpLanguage.Client(4)' received event 'PingPong.PSharpLanguage.Client+Ping' that cannot be handled.
<StrategyLog> Found bug using 'Random' strategy.
すげえ。
以上。