BT

Your opinion matters! あなたのご意見でInfoQが変わる!

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

| 作者: Sergio De Simone フォローする 6 人のフォロワー , 翻訳者 猪股 健太郎 フォローする 0 人のフォロワー 投稿日 2016年10月26日. 推定読書時間: 2 分 |

あなたのリクエストに応じて、ノイズを減らす機能を開発しました。大切な情報を見逃さないよう、お気に入りのトピックを選択して、メールとウェブで通知をもらいましょう。

原文(投稿日: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

このスレッドのメッセージについてEmailでリプライする
コミュニティコメント

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

このスレッドのメッセージについてEmailでリプライする

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

このスレッドのメッセージについてEmailでリプライする

ディスカッション

InfoQにログインし新機能を利用する


パスワードを忘れた方はこちらへ

Follow

お気に入りのトピックや著者をフォローする

業界やサイト内で一番重要な見出しを閲覧する

Like

より多いシグナル、より少ないノイズ

お気に入りのトピックと著者を選択して自分のフィードを作る

Notifications

最新情報をすぐ手に入れるようにしよう

通知設定をして、お気に入りコンテンツを見逃さないようにしよう!

BT