Plangのお勉強

Posted on 2 mins read

P: A programming language designed for asynchrony, fault-tolerance and uncertainty という記事が公開されていた。 OSS化についてはだいぶ前から行われていた けど拾えていませんでした。

この記事でモデル検査を勉強してみたくなったもののP-langのビルドは失敗しました。

(今のところの)P-langのイメージ

P-lang は非同期処理のモデル化が可能な言語でモデル検査器のサポートを受けられる。 また、イベントとして故障をモデル化する事でfault-injectionをサポートしている。 故障モデルを投入できる非同期処理のモデル検査が可能なので分散アルゴリズムの検証を行えるということになる(?)。 そして更に実行可能コードを生成できる。

これらの特徴から、P-lang を用いた開発ではプロトコルの設計時にモデル検査器のサポートを受けられコード自動生成によりバグ混入のない実装を利用することが可能になる。

P-lang は複数の決定性オートマトンを定義してメッセージパッシング(Actor Modelに近そう)でプロトコルを記述する。 メモリ管理はlinear type system を採用しているらしい。

P: A programming language designed for asynchrony, fault-tolerance and uncertainty の抜粋

現在のソフトウェアはクラウド化したリソースやデバイス・物理へのプロセッシングの埋め込み、人工知能の活用などによって開発難易度を増加させている。

これらの現代的なアプリケーションはパフォーマンス改善に非同期処理を活用している。非同期処理の活用は必然的に並行プログラムにたどり着く。 並行プログラムはHeisenbug で知られるような落とし穴がたくさんある。 これら非同期アプリケーションに立ち向かうために、非同期アプリケーションのプロトコルをモデル化し検証するためバークレー校,ロンドン大学と共にP-lang を開発した。

P-lang はプロトコルとその高水準な仕様を記述する。Pコンパイラは自動で非同期処理に関連した競合状態の自動テストを提供する。 P言語は非同期処理のモデリング、安全性・活性の定義、系統だった検索を用いてそれらの仕様が満たされるか検証する事をサポートしている。 これらの機能はLeslie Lamport のTLA+ , Gerard Holzmann のSPIN に似ている。

しかしTLA+ ,SPIN とは実行可能なCを吐き出せる点で異なっている。 この機能により高水準でのモデルと低水準での実装の間のギャップに橋渡しを行い、プログラマーの扱う仕様と受け入れられたモデルの間の巨大な障壁を取り除く。

P-langは、型付けされたメッセージを含むイベント情報を非同期転送する複数の状態マシンを基盤に持つプログラミングモデルに基づいている。 メモリマネージメントはlinear type systems とユニークポインタに基づいていて(Rustなどの)現代的なプログラミング言語に似ている。

既に、USB 3.0 in Windows 8.1, Windows Phoneの開発で使われている。 windows kernel開発によるP-lang はいい結果をもたらしたので状態マシンやテストコードをC#を吐けるP#も開発された。

P-langは現在Azureの置き換えでも利用されている。 Azureは他のクラウドベンダーと同様、レースコンディション・ソフトウェア・ハードウェア障害を原因としたHeisenbugsバグと戦っている。 これらのバグは稼働中のサービスに混乱をきたす。PやP#は、デプロイ済みのサービス・新規投入されるサービス問わずHeisenbugバグを見つけるのに利用されている。

P-langは巨大なAzureを構成するコンポーネントのインタフェースを手頃なモデルに起こせる。 またデスクトップ上で問題の発見・デバッグを行える。

特に重要なPの特徴は、耐障害性のある分散サービスが障害テストを乗り越えて稼働できるか評価するのに適していることだ。 予想外の障害が起きて復旧できるか稼働し続けられるかを評価できる。 通信メッセージがdropされたり各状態マシンが故障したりをイベントとしてモデル化できる。 モデル化された障害は、Pで完全に自動でfault-injectionされて評価できるためプログラマーへの負担は少ない。

Pのシステムテストは並行に振り分けられたイベントの非決定的な実行順序で導ける選択肢を検索する。 しかしこれは入力データが明確である必要となる。 この制約のため、入力ソースが巨大な複雑性を持ち不確定な入力で決定を下すといったロボティクスなどの検証にPを適用するのは難しい。 巨大で不確定な入力は調査・研究領域であり、これらの難問を扱えるように、記号的・確率論の両面で研究を進めている。

出てきた用語で気になるやつ

知らなかった言葉などへの疑問をメモする。 問いにまで整理できてるとは限らないので答えがなかったり的はずれな可能性も多分にある。

linear type systems

部分構造型システムの一部らしい。わからなかった。 ユニークポインタみたいにプログラム中の参照元(?)利用が一箇所なことが保証されるらしい。 何が線形なのかWikipediaには書かれていなかった。 プログラムの状態の和を取って型を評価しても、プログラムの型を評価した後に和をとっても同じとかそういうこと?

fault injection

fault-injection(故障注入?)は、故障をテストのコードパスに入れ込む事でテストのカバレッジを上げる技術を指す。 Web界隈だとJepsen が有名なフレームワークで、このフレームワークをメンテしてるJepsen って分散システムの改善を目指したプロジェクトもある(もともとは個人的なPJだったみたい)。 (coockroachの記事もあったので要チェックだ)

Fault injection Techniques and Tool(1997) で環境変化に強い(ロバストな)ソフトウェア開発で重要だとされたらしい(Wikipedia曰く )。

Wikipediaの参考文献でみると'95あたりから具体的なシステムの提案論文が掲出されてる。

Fault injection Techniques and Tool(1997) の部分的な紹介はQiitaの記事 になっていたので参考に読んだ。 ただFault-Injectionの図でコンポーネント間の接続がグラフとしては正しいけど紛らわしい繋がり方をしてるので原文に目を通した方が良い。

Pの入門記事

ドキュメントは割りと充実していた。 特にチュートリアル を読むとモデルを書くのが手軽で直感的な事がわかる。 実際にP-lang環境をビルドできなかったのでマニュアルを根拠に列挙する。

チュートリアルに出てきた最初のサンプルは下の通り。

event PING assert 1; machine;
event PONG assert 1;
event SUCCESS;

main machine Client {
  var server: machine;
  tart state Init {
    entry {
      server = new Server();
      raise SUCCESS;
    }
    on SUCESS goto SendPing;
  }
  state SendPoing {
    entry {
      send server, PING, this;
      raise SUCCESS;
    }
    on SUCCESS goto WaitPong;
  }
  state WaitPong {
    on PONG goto SendPing;
  }
}
machine Server {
  tart state WaitPing {
    on PING goto SendPong;
  }
  state SendPong {
    entry (payload: machine) {
      send payload, PONG;
      raise SUCCESS;
    }
    on SUCCESS goto WaitPing;
  }
}

解説がされている。 プログラムは状態を持つオートマトンを定義してイベントを自分や他のオートマトンに投げる形で実装している。

オートマトンと状態に関わるキーワード

キーワード 意味
machine オートマトンを定義(設計対象)
model 非決定性オートマトンを定義(外部環境)
state オートマトンの状態
main プログラム開始時に存在する事をアノテート
start 初期状態をアノテート
goto 状態遷移
push 状態遷移を行う際にスタックに積み上げる
pop 状態スタックを巻き戻す
hot 無限回の実行・デットロックに陥らない事をアノテート(?)
cold 無限回の実行・終了状態でも問題ない事をアノテート(?)

イベント通知・ハンドルに関わるキーワード

キーワード 意味
event イベント定義
send イベントをメッセージを伴い対象へ送る
raise イベントを自分自身へ送る
on, do パターンマッチによるイベントハンドル
with 状態遷移に伴って行う処理を記述(atomic?)
ignore 無視するイベントでdropする
defer 無視するイベントで別の状態になったら受理される可能性がある
halt 処理されず停止する特別なイベント

その他

他にもmap, seqなどのデータ構造に関わるキーワードやfunなどの関数定義もある。 SPINは関数定義がないのでこれは嬉しい。 monitor, specキーワードがまだ理解できなかった。

OSや外部環境を表現するのにmodelが使われる

故障検知プロトコルで利用されるTimerは以下の様に書かれていた。

model Timer {
  var client: machine;
  tart state Init {
    entry (payload: machine) {
      client = payload;
      raise UNIT;
    }
    on UNIT goto WaitForReq;
  }
  state WiatForReq {
    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;
    };
  }
}

紹介されている論文

公式には3報リンクが貼られていた

P: Safe asynchronous event-driven programming.;2013

Pがイベント駆動プログラムの設計・開発に向けたDSLであることが宣言されている。 非同期システムが稼働する環境をモデルに含めて全体を閉じた系として記述できる。 この時、環境を表現した状態機械をghoset machine と呼び、ghost machine は非決定的な状態遷移が許される。

2章でコンセプトと構文が説明されている。3章で操作的意味論が定義されている。 4章で実行についてでコード生成・ランタイム・インタフェース・外部関数などの説明がなされている。 5章ではシステムテストについて書かれておりZing によるモデル検査が言及されていた。 6章以降は具体例や関連研究の紹介になっている。

Systematic Testing of Asynchronous Reactive Systems;2015

非同期アプリケーションのテストは困難で、探索対象となる状態が莫大になる。 そこで、caching, partialorder reductionなどが開発されてきたが、探索に時間が掛かりすぎる状態の探索を諦めたり刷るため最悪になるケースを逃したりする。 この論文では遅延スケジューラを利用した効率的な状態探索を提案する、的な感じだった。 インタリーブの戦略を変えると効率的にバグを拾える感じ。

comments powered by Disqus