BT

InfoQ ホームページ ニュース 安全な非同期イベント駆動プログラミングのためのP言語をMicrosoftがオープンソース化

安全な非同期イベント駆動プログラミングのためのP言語をMicrosoftがオープンソース化

ブックマーク

原文(投稿日:2016/10/12)へのリンク

Microsoftが最近オープンソースとして公開したP言語は、非同期イベント駆動プログラムを安全に書くことができ、Linux、macOSWindows上で動作する。

P言語とは、組み込みシステム、ネットワークで結ばれたシステム、分散システムといった非同期システムにおける構成要素間の通信をモデル化するドメイン特化言語であるとMicrosoftは解説している。Pのプログラムは並行動作する有限ステートマシンとして定義される。それぞれが入力キュー、状態、状態遷移、ローカルストアを持ち、互いに非同期メッセージを送信し合うことができる。Pにおける基本操作は、ローカルストアの更新、メッセージの送信、新しいステートマシンの生成のどれかである。下記の部分的なコードスニペットは、状態とその遷移をPで定義する方法を示している。また、メッセージの送信と新しいマシンの生成も併せて記述している。

...
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;
}
...

Microsoftによれば、Pのプログラムはモデル検査によって検証可能である。開発者は、システムがすべてのイベントを適時に処理できることを保証できる。あるPのプログラムがレスポンシブであるためには、ステートマシンはどの状態においても、キューから取り出される可能性があるすべてのイベントを処理できなければならない。それは必ずしも実用的とは言えないため、一部のイベントについては先送りすることも可能である。そのような場合には、P言語はあるイベントが永遠に先送りされるようなことがないことを保証する。Pコンパイラーは、後からCコンパイラーに与えて実行することができるCのコードを生成するのに加え、プログラムの属性を検証できるように、システムのテストに利用可能なZingモデルを出力するだろう。Zingはオープンソースの並行プログラム用モデルチェッカーであり、モデルがとりうるすべての状態を体系的に調査する(PPT)ことができる。

MicrosoftはP言語を使用してWindows 8のUSBデバイスドライバースタックの中核を実装し検証した。Microsoftによれば、ハードウェアやOSやファンクションドライバーやそのほかのドライバーコンポーネントにおいてばらばらに発生する多くのイベントを、エンジニアがPを利用することで直列化することができ、信頼性と性能を向上させることができたとのことである。特に、新しいUSBハブドライバーでは不正メモリーアクセスや競合状態に起因するクラッシュが非常に少なくなった一方で、列挙時間は30%高速化され、ワーカーアイテムの飢餓状態は観測されることがなかったと主張している(PDF)

この記事に星をつける

おすすめ度
スタイル

こんにちは

コメントするには InfoQアカウントの登録 または が必要です。InfoQ に登録するとさまざまなことができます。

アカウント登録をしてInfoQをお楽しみください。

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

コミュニティコメント

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

BT

あなたのプロファイルは最新ですか?プロフィールを確認してアップデートしてください。

Eメールを変更すると確認のメールが配信されます。

会社名:
役職:
組織規模:
国:
都道府県:
新しいメールアドレスに確認用のメールを送信します。このポップアップ画面は自動的に閉じられます。