TL;DR
- PlusCal の不足（ラベルの手書き、レキシカルスコープがない、型がない）を補う alt TLA+ として、言語 sanpou を作った。
- 言語機能を豊かにするとモデル検査の状態数が増えるので、コンパイル時の最適化で状態数を抑えることが alt TLA+ では重要になる。
内容
TLA+ と PlusCal の課題
TLA+ は、並行・分散システムの振る舞いを曖昧さなく記述できる形式仕様記述言語である。モデル検査では、システムが取りうる状態を網羅的に調べるので、テストでは見つけにくいデッドロックなどのバグを見つけられる。モデル検査では状態数を減らすことが大事になる。
TLA+ は普段書くプログラミング言語と書き方が大きく違い、構造化されたプログラムを TLA+ で写すのは大変である。TLA+ の開発チームが作った PlusCal は、疑似コードに近い書き方ができる。しかし、原子性の粒度をラベルで制御するので細かく制御したいとラベルが大量に要り、レキシカルスコープも型もない。公式は TLA+ と PlusCal に豊かな言語機能を足さないと明言している。言語機能が多いと開発が大変で、モデル検査器にバグがあると困るので、発表者はこれを悪い判断ではないとしていた。
PlusCal から TLA+ への変換
スピンロックを例に、PlusCal を TLA+ に変換する過程を示していた。各ラベルは状態を表す pc の値に対応し、アクションはラベルごとに定義される。Procedure の呼び出しは stack 変数でのフレームの積み下ろしで表される。変換後の TLA+ は機械語に近い低レベルな記述になる。
sanpou の設計
sanpou は、疑似コードとして書けることを保ちつつ言語機能を豊かにする。ラベルはコンパイル時に自動で挿入される。Procedure が返り値を持ち、レキシカルスコープを持つ。静的型付けで Hindley-Milner 型推論を使い、α 変換で名前の重複をなくす。
コンパイルは、構文解析、意味解析（型推論と α 変換）、AST の正規化、単純な命令列への変換（Lowering）、TLA+ コードの生成の順に進む。生成時にソースマップを作り、モデル検査で見つかった反例を sanpou の語彙に戻して表示する。
評価と最適化
最適化前に検査時間を測ると、パン屋のアルゴリズムほど大きな例では、言語機能を豊かにした弊害で状態数が増えていた。ラベルの自動挿入はコードが大きいほど役に立つはずなのに、逆効果になっていたので、2 つの最適化を入れた。1 つはプロセスの外から観測できない連続したアクションを、制御フローグラフの縮約で 1 つにまとめるものである。もう 1 つは生存変数解析で、参照されなくなったローカル変数にデフォルト値を入れて状態の差分を減らすものである。最適化後は、スピンロック（N=6）で状態数が約 97%、パン屋のアルゴリズム（N=3）で約 94% 減り、検査時間は PlusCal の倍程度に収まった。
Quint との比較
発表者の見方では、Quint は型付きの TLA+ という位置づけで、疑似コードのように書けることは目指していない。sanpou は PlusCal と同じく疑似コードの書き味を目指す点が違う。
まとめ
PlusCal から TLA+ へのコンパイルは、高級言語から機械語へのコンパイルとよく似た構造を持つ。alt TLA+ では、言語機能の豊かさと状態数の削減の両方が重要になる。