ステートマシンによるTLA+仕様の合成
原文は Hillel Wayne により に公開されました。 このブログを購読する
昨年、あるクライアントから相談を受けました。より大きなシステムの一部として、2つの大規模なTLA+仕様を合成したいというのです。通常はそうすべきではないとされていて、両方のシステムをハードコードした1つの大きな仕様を書くのが定石ですが、これらの仕様は巨大で、それぞれが多くの内部不変条件を抱えていました。彼らが必要としていたのは、2つの仕様を独立に開発し、最小限の手間で統合する方法でした。
そこで私が考えたのが、今回紹介する方法です。注意：これは上級のTLA+ユーザー向けの複雑な手法です。もっと（ずっと）やさしい入門をお探しなら、私のサイトlearntlaをご覧ください。
具体例
まずは動機となるシステムから始めましょう。WorkerがServerに認証リクエストを送ります。パスワードがサーバーの内部パスワードと一致すればサーバーは「valid」を、一致しなければ「invalid」を返します。Workerが「invalid」という応答を受け取ると、エラー状態に遷移します。Workerはその状態からリトライし、新たな認証リクエストを送ることができます。
WorkerとServerはrequest/responseを通じて状態を共有しています。さらに厄介な要素として、ServerにWorkerからは見えない内部状態として、リクエストのログを追加します。
この例を使って、合成における問題点と私の解決策を示していきます（ただし、この例は手法の有用性を示すには少し単純すぎることは断っておきます）。
合成における問題
私たちが求めているのは、できる限りシンプルで手間のない合成です。仕様がWorkerSpecとServerSpecだとすれば、最も簡単な合成は単に
CombinedSpec == WorkerSpec /\ ServerSpecとするだけでしょう。この問題についてはこちらで詳しく論じていますが、要するに、ServerSpecとWorkerSpecが「通常の」仕様である場合、共有変数に対して矛盾する制約を課してしまうということです。
例えば、WorkerSpecはおそらくサーバーの応答を読み取りますが、変更はしません。したがってWorkerSpecを合成とは独立に実行するには、応答は決して変化しないと記述しなければなりませんが、これは応答を変更できないと言っているのと同じであり、ServerSpecが応答を送ることを不可能にしてしまいます！
この問題を回避する通常の方法は、WorkerSpecとServerSpecの両方をアクションの集合に分解し、それらを矛盾が生じないように慎重に縫い合わせることです。聞いた通りの複雑さで、2つの仕様を合成する作業は、それらを最初から書き直すのと同じくらいの手間がかかることもあります。
だからこそ、もっと良い方法を探しているのです。
中心となるアイデア
やるべきことは、世界のある部分を表すことを意図した仕様を書き、それを「世界全体」のメイン仕様に組み込むことです。そのために、TLA+の最も強力な機能の1つを使います。x'を使って、xの次の値を代入すると同時に次の値が取りうるものを制約することができるのです。例えば次のような仕様があるとします。
VARIABLE x, y
Foo ==
/\ x' \in {0, 1}
/\ y' \in {0, 1}
Bar == x' < y'
Next == Foo /\ BarTLCがNextを評価するとき、Fooの中のx'とy'は代入として読み取られます。4通りの代入が考えられるため、モデル検査器はそれらすべてを評価します。
そして、x'とy'がすでに選ばれているため、TLCはBarの中の文を制約として読み取ります。4通りのうち3つはその制約を破るため、TLCはそれらを除外し、唯一の次状態が残ります。
これは、仕様Qが2つの仕様XとYを取り込み、互いに制約し合うことができることを意味します。Xがx_logをインクリメントするアクションIncを持っているとき、QはIncはy_flagが真のときにのみ起こり得ると言えます。同様に、Qはある代入が別の代入を引き起こすようにもできます。
Inc ==
/\ x_log' = x_log + 1
Sync ==
IF ~y_flag /\ y_flag'
THEN Inc
ELSE TRUE
Next == (X!Next \/ Y!Next) /\ Syncこれで、y_flagを真に変更することがx_logのインクリメントを強制します。Qは一方の仕様を使ってシステム内の副作用を駆動しているのです。
これはまさにステートマシンです！遷移に対する制約は単なるガード節であり、遷移における代入は単なるエフェクトです。これらは、ステートマシンが知らない他の仕様に対して強制できるのです。
このアイデアを実際に機能させる手順は次の通りです。
- コアコンポーネントの高レベルな状態遷移すべてについて、抽象的なステートマシンを書く
- 他のコンポーネントを、次の状態を完全には記述しない「オープン」な仕様として書く
- リファインによりコアコンポーネントをメイン仕様へと展開し、状態遷移にガードと副作用を追加する
Syncアクションを加える
解決策
これを3つの別々の仕様でモデル化します。workerSM.tla、server.tla、そしてsystem.tlaです。
ステートマシン
システム全体がWorkerのステートマシンを中心に構築されているので、まずはworkerSM.tlaから始めましょう。これはWorkerが状態遷移する際に何が起こるかを表すのではなく、どのような遷移が存在するかだけを表します。
------------------- MODULE workerSM -------------------
EXTENDS Integers
VARIABLES state
Transitions == {
[from |-> "init", to |-> "ready"]
, [from |-> "ready", to |-> "requesting"]
, [from |-> "requesting", to |-> "done"]
, [from |-> "requesting", to |-> "error"]
, [from |-> "error", to |-> "ready"]
}
Init == state = "init"
Valid(t) == state = t.from
ValidTransitions == {t \in Transitions: Valid(t)}
ValidOutcomes == {t.to : t \in ValidTransitions}
Done ==
state = "done"
Next ==
\E t \in ValidOutcomes:
state' = t
Fairness ==
/\ WF_state(Next)
/\ SF_state(state' = "done")
Spec == Init /\ [][Next]_state /\ Fairness
Liveness == <>Done
=========================================================Transitionsは有効な遷移の集合を表します。3つのValid-演算子は単なるヘルパーです。これらを追加するのは良い慣習です。ほとんどのTLA+仕様はヘルパーが不足しています。
Fairness制約は少し複雑ですが、言っていることは単に、requestingからerrorへ常に遷移するわけではない、ということです。そこに十分な回数到達すれば、最終的には代わりにdoneへ遷移します。
それ以外、この仕様は遷移に何の条件も課しません。doneに移るために「何かをする必要」はないのです。それはsystem.tlaの役割です。
設定を表示
これはWorkerを直接テストするために使いました。
SPECIFICATION Spec
PROPERTY Liveness
CHECK_DEADLOCK FALSEこれは成功し、この仕様が<>Doneを保証することを意味します。
次に、Workerと統合する外部コンポーネントです。
サーバー
------------------- MODULE server -------------------
CONSTANTS Password, NULL
VARIABLE req, resp, log
internal == <<log>> \* (a)
external == <<req, resp>> \* (a)
vars == <<external, internal>> \* (a)
Init ==
/\ req = NULL
/\ resp = NULL
/\ log = {}
CheckRequest ==
/\ req # NULL
/\ log' = log \union {req}
/\ IF req = Password THEN
resp' = "valid"
ELSE
resp' = "invalid"
/\ req' = NULL
Next == \* (b)
CheckRequest
Spec == Init /\ [][Next]_internal \* (c)
====この仕様では3つの変わったことをしています。1つ目は、変数をinternalとexternalに分割していることです(a)。externalな変数は合成された仕様の他の部分と共有される状態を表し、internalな変数はserverの性質にのみ関わります。ここではサーバーへのリクエストをreqで、レスポンスをrespで表しています。
2つ目は、この仕様は自明にデッドロックすることです(b)。NextはCheckRequestアクションのみを含み、CheckRequestはreqがnullでない場合にのみ有効ですが、仕様内の何もreqを非nullにしません。この仕様は「自己完結」しておらず、他の仕様と組み合わされて初めて意味を持ちます。
3つ目は、Specがinternal変数に関してのみスタッタリング不変であることです。これは[][Next]_varsの代わりに[][Next]_internalと書くことで実現しています(c)。これは最も見落としやすい点ですが、後々の仕様の合成とリファインメントの両方を容易にします。
では、サーバーとWorkerを組み合わせましょう。
システム
これが群を抜いて最も複雑な部分です。まずは仕様全体を示し、その後で最も重要な部分を詳しく見ていきます。
システム仕様
---- MODULE system ----
EXTENDS TLC, Integers, Sequences
CONSTANT NULL
VARIABLES ws \* worker state
, server_req \* requests to server
, server_resp \* server response
, server_log \* log (internal to server)
Strings == {"a", "b", "c"}
comm_vars == <<server_req, server_resp>>
vars == <<ws, server_log, comm_vars>>
Worker == INSTANCE workerSM WITH state <- ws
Server == INSTANCE server WITH
req <- server_req,
resp <- server_resp,
log <- server_log,
Password <- "a"
Sync ==
LET i == <<ws, ws'>> IN
/\ CASE
i = <<"ready", "requesting">> ->
/\ \E x \in Strings:
/\ server_req' = x
/\ server_resp' = NULL
[] i = <<"requesting", "error">> ->
/\ server_resp = "invalid"
/\ UNCHANGED comm_vars
[] i = <<"requesting", "done">> ->
/\ server_resp = "valid"
/\ UNCHANGED comm_vars
[] OTHER -> UNCHANGED comm_vars
Init ==
/\ Worker!Init
/\ Server!Init
Done == \* No deadlock on finish
/\ Worker!Done
/\ UNCHANGED vars
ServerNext ==
/\ Server!Next
/\ UNCHANGED ws
WorkerNext ==
/\ Worker!Next
/\ Sync
/\ UNCHANGED server_log
Next ==
\/ WorkerNext
\/ ServerNext
\/ Done
Fairness ==
/\ WF_vars(Next)
Spec == Init /\ [][Next]_vars /\ Fairness
RefinesServer == Server!Spec
RefinesWorker == Worker!Spec
====VARIABLES ws \* worker state
, server_req \* requests to server
, server_resp \* server response
, server_log \* log (internal to server)
Strings == {"a", "b", "c"}
comm_vars == <<server_req, server_resp>>
vars == <<ws, server_log, comm_vars>>私はvarsを目的や仕様ごとにグループ化するのが好きです。サーバーとWorkerの両方がserver_reqと_respを使うので、それらを別のcomm_varsグループにまとめました。
Worker == INSTANCE workerSM WITH state <- ws
Server == INSTANCE server WITH
req <- server_req,
resp <- server_resp,
log <- server_log,
Password <- "a"教育上の都合で、サーバーのPassword定数はハードコードしました。NULL定数はsystem.tlaとserver.tlaの両方で同じ名前なので、自動的に伝播するため、インスタンス化する必要はありません。
Sync ==
\* See next section
Init ==
/\ Worker!Init
/\ Server!Init
ServerNext ==
/\ Server!Next
/\ UNCHANGED ws
WorkerNext ==
/\ Worker!Next
/\ Sync
/\ UNCHANGED server_log
Done == \* No deadlock on finish
/\ Worker!Done
/\ UNCHANGED vars
Next ==
\/ WorkerNext
\/ ServerNext
\/ DoneInitはWorker!InitとServer!Initの両方に委譲して、それぞれの変数を初期化するだけです。ここでは変数を共有していないので簡単です。もし両方が使うものがあったり、systemが追加のbookkeeping変数を必要とする場合は、ここで特別に扱います。ServerNextは単に「サーバーは自身の状態更新を自前で処理できる」と言っているだけで、wsのスタッタリングを考慮しています（すべての変数はすべてのステップで値を割り当てられる必要があるため）。サーバーはシステム内で独立して動作し、その振る舞いはWorkerに同期的に依存しません。コンポーネントを分離しておくことは合成において常に可能なわけではありませんが、可能な場合には物事をより便利にします。WorkerNextも同様で、ServerNextとは独立に振る舞います。ただし、ここで「システム」が役割を果たし始めます。それがSyncです。
Sync
Syncこそが面白いところです。
Sync ==
LET i == <<ws, ws'>> IN
CASE
i = <<"ready", "requesting">> ->
/\ \E x \in Strings:
server_req' = x
/\ server_resp' = NULL
[] i = <<"requesting", "error">> ->
/\ server_resp = "invalid"
/\ UNCHANGED comm_vars
[] i = <<"requesting", "done">> ->
/\ server_resp = "valid"
/\ UNCHANGED comm_vars
[] OTHER -> UNCHANGED comm_vars先ほどの説明を振り返ると、プライム付き変数は代入された後、他の式で使うことができます。つまり、あるアクションで遷移を試み、その遷移が有効かどうかを後のアクションでチェックできるのです。これがすべてを機能させる鍵です。これがなければ、ガードや副作用を遷移と同じアクションの中に置かなければなりません。例えば次の行では、
[] i = <<"requesting", "error">> ->
/\ server_resp = "invalid"
/\ UNCHANGED comm_vars私たちはrequesting -> errorへの遷移を、サーバーの応答が「invalid」だった場合にのみ可能であるように制約しています。それはServer!Nextがパスワードを拒否した場合にのみ起こり得ます。しかしWorkerはこれを知る必要はありません。私たちはそれらを独立に開発し、Syncがそれらの振る舞いを正しく合成してくれることに頼ることができます。
これを使ってシステム上のエフェクトを駆動することもできます。
[] i = <<"ready", "requesting">> ->
/\ \E x \in Strings:
server_req' = x
/\ server_resp' = NULLこれにより、ready -> requestingへの遷移がリクエストをトリガーし（ついでに未処理のレスポンスをクリアし）ます。するとServer!CheckRequestが有効になり、ServerNextが有効になるため、サーバーはシステムに反応できるようになります。
リファインメント
思い出してください、私たちはそもそも2つの複雑な仕様を合成するために、この仕組みを追加しました。どちらの仕様の性質も破らない形で合成していることを確認する必要があります。それを担うのが次の行です。
RefinesServer == Server!Spec
RefinesWorker == Worker!Specこれらはリファインメント特性です。大まかに言えば、system.tlaがServerやWorkerに通常ではできないことをさせていないかをチェックします。例えば、logから何かを削除すれば、この特性は失敗します。なぜならそれはServer!Specでは不可能だからです。1
TLA+では、リファインメントは推移的です。workerSM.tlaはライブネス特性である<>Doneを持っていました。workerSM.cfgですでに検証済みなので、system.tlaでそれをテストする必要はありません。RefinesWorkerが通れば、Worker!Livenessも必ず通ることが保証されるのです！
なぜリファインメントは推移的なのか
RefinesWorkerをテストするとき、私たちが検証しているのは次のことです。
Spec => Worker!Spec
(S) (WS)workerSM.tlaのモデル検査から、私たちはすでに次のことを知っています。
Worker!Spec => Worker!Liveness (2)
(WS) (WL)含意は推移的です。S => WSかつWS => WLならば、S => WLです。
そして現状では、これは失敗します。
設定を表示
SPECIFICATION Spec
CONSTANTS
NULL = NULL
PROPERTY
RefinesServer
RefinesWorker
問題は、Workerが間違ったパスワードを選び続ける可能性があるため、サーバーがそれを拒否し続け、Workerが決して完了しないことです。1つの修正方法は、システムは同じパスワードを再試行しない、とすることです。
Sync ==
\* ...
/\ \E x \in Strings:
/\ x \notin server_log
/\ server_req' = xこれで仕様は通るようになります。サーバーの内部ログがシステムに漏れることが気になる場合は、Worker側にもログを追加できます。system.tla内に置いても、Syncに含める別のコンポーネントとして置いても構いません。2別の修正方法として、強公平性制約を使う方法もあります。
Sync ==
\* ...
/\ \E x \in Strings:
/\ server_req' = x
Fairness ==
/\ WF_vars(Next)
/\ SF_vars(WorkerNext /\ server_req' = "a")これは、正しいパスワードを送る形でWorkerNextを実行することが常にいつかは可能であるなら、仕様はいずれそうする、ということを意味します。これにより、システムの本質的なロジックを変えずに仕様を通すことができます。
オープンワールドを閉じる
最後にもう1つやるべきことがあります。server.tlaをモデル検査可能にすることです。これは「クローズド」な仕様ではないため、直接テストできません。リクエストを送るために他の仕様に依存しているからです。より複雑な仕様では、合成とは独立に、その仕様の特性をテストできるようにしたいものです。
幸い、これはTLA+コミュニティでは「すでに解決された問題」です。オープンな仕様をクローズドなものへリファインするのです。新しいファイルMCserver.tlaでそれを行います。
---- MODULE MCserver ----
EXTENDS TLC, server
Strings == {"a", "b", "c"}
ASSUME Password \in Strings
MCInit == Init
WorldNext ==
/\ \E x \in Strings:
req' = x
/\ UNCHANGED <<log, resp>>
MCNext ==
\/ Next
\/ WorldNext
MCSpec == MCInit /\ [][MCNext]_vars
====これはサーバーを、リクエストを送ることができる外部のWorldで拡張します。これでMCserver.tlaをモデル検査することでserver.tlaの振る舞いをテストできます。
設定を表示
SPECIFICATION MCSpec
CONSTANT
NULL = NULL
Password = "b"VSCodeのTLA+拡張のnightly版を使っているなら、server.tlaに対して「Check model with TLC」コマンドを実行すると、自動的にMCserver.tlaでモデル検査が実行されます。TLA+デバッガも付属しています。VSCode拡張は素晴らしいです。
利点と欠点
これはかなりの作業です！では、なぜ1つの大きな仕様を書くのではなく、わざわざこれを行うのでしょうか？
そもそも仕様を合成する目的は、それらを独立に作業できるようにすることです。各仕様が30行程度なら大した問題ではありませんが、それぞれが200行以上になると、単に1つの仕様として書き直すわけにはいきません。
そこで、より一般的な合成アプローチと比較してみましょう。MongoDB Raftの合成を例に取ります。これはMurat Demirbasがこちらで分析しています。独立した仕様はMongoStaticRaftとMongoLoglessDynamicRaftで、それらがMongoRaftReconfigで合成されています。MongoStaticRaftのNextは次のようになっています。
\* MongoStaticRaft
Next ==
\* (a)
\/ \E s \in Server : ClientRequest(s)
\* etc
\* (b)
\/ \E s \in Server : \E Q \in Quorums(config[s]) : BecomeLeader(s, Q)
\* etc一方、合成されたNextは次のようになっています。
\* MongoRaftReconfig
Next ==
\/ OSMNext /\ UNCHANGED csmVars
\/ CSMNext /\ UNCHANGED osmVars
\/ JointNext
OSMNext ==
\* (a)
\/ \E s \in Server : OSM!ClientRequest(s)
\* etc
JointNext ==
\* (b)
\/ \E i \in Server : \E Q \in Quorums(config[i]) :
/\ OSM!BecomeLeader(i, Q)
/\ CSM!BecomeLeader(i, Q)
\* etc(a)の下のアクションはOSMNextで手作業で繰り返す必要があり、(b)の下のアクションはJointNextの下で他の仕様と慎重に織り交ぜる必要があります。これは2つの仕様を合成する標準的な方法ですが、統合する仕様が増えるほど次第に難しくなります。また、このパラダイムではリファインメントのチェックも困難です。
私はSyncベースのアプローチで、これら両方の問題を回避しようとしています。各コンポーネントはすでに独自のNextを持っており、それをそのまま変更せずに使えます。共有変数に影響するものはすべて、追加のSync演算子で処理します。
この仕様が私のアプローチの恩恵を受けるかどうかは、正直わかりません。このアプローチは、外部コンポーネントと対話する主要な「マシン」を想定して設計したもので、ここでは2つの仕様が対等の立場にあるからです。変換がどうなるかのスケッチはありますが、必ずしも優れているかどうかはわかりません。
変更のスケッチ
これは追加のステートマシンを加えずに行う場合です。1つの「プライマリ」な仕様、例えばCSMを選びます。するとSpecは次のようになります。
Next ==
\/ OSMNext
\/ CSMNext
OSMNext ==
/\ OSM!Next
/\ UNCHANGED <<csmVars>>
/\ UNCHANGED <<sharedVars>> \* new op
CSMNext ==
/\ CSM!Next
/\ Sync
/\ UNCHANGED <<osmVars>>OSM!BecomeLeaderを単独で呼び出さないように、OSMNextにsharedVarsを追加する必要があります。それはSync経由で起こる必要があるからです。sharedVarsはcsmVarsやosmVarsといくつかの変数を共有することになります。
SyncはJointNextと似た形になります。
Sync ==
\/ \E i \in Server : \E Q \in Quorums(config[i]) :
/\ OSM!BecomeLeader(i, Q)
/\ CSM!BecomeLeader(i, Q)
\/ \* ...
\/ UNCHANGED <<sharedVars>>CSM!BecomeLeaderをCSMNextとSyncの両方で繰り返しているのは正直気に食わないのですが、OSMとCSMの両方がiとQに同じ値を使うことを保証する最も直接的な方法なのです。重複をなくす方法もいくつか考えましたが、どれもTLA+のセマンティクスを創造的に悪用するものになってしまいます。
私の予測では、従来の合成はより幅広いケースで機能しますが、Syncの方がそれが機能するケースではより保守しやすく、スケールしやすいということです。
どちらのアプローチも「1対多」のケースをうまく扱えません。これは単一のWorkerの仕様があり、それを使ってN個のWorkerを追加しようとするケースで、Nはモデルパラメータです。なぜこれがこれほど難しいのかは、私の記事Using Abstract Data Types in TLA+で論じています。
結論
これは強力なテクニックですが、経験を要し、複雑さも増します。非常に大きな仕様を書く必要がある場合や、再利用可能なコンポーネントのライブラリが必要な場合には適しています。より小さな仕様であれば、すべてのコンポーネントを1つの仕様にまとめる標準的な手法をお勧めします。
これはコンサルティングのクライアントのために開発したもので、見事にうまくいきました。皆さんと共有できることを嬉しく思います！気に入っていただけたなら、こちらで他の高度なTLA+テクニックも読むことができます。例えばモデル検査を高速化する方法などです。
Murat Demirbas氏とAndrew Helwer氏にフィードバックに感謝します。この記事を気に入っていただけたら、ぜひ私のニュースレターにもご登録ください！毎週新しいエッセイを書いています。
私は企業向けに形式手法のトレーニングを行い、ソフトウェア開発をより速く、安く、安全にしています。詳しくはこちらをご覧ください。
付録: プライムなしのSync
一部の企業のスタイルガイドでは、後のアクションでプライム付き変数を式として使うことが禁じられています。その場合は、次のようにして同じ効果を得ることができます。
-Sync ==
- LET i == <<ws, ws'>> IN
+Sync(t) ==
+ LET i == <<t.from, t.to>> IN
+Do(t) ==
+ /\ ws = t.from
+ /\ ws' = t.to
WorkerNext ==
- /\ Worker!Next
- /\ Sync
+ /\ \E t \in Worker!ValidTransitions:
+ /\ Do(t)
+ /\ Sync(t)
/\ UNCHANGED server_logDo(t)は実質的にWorker!Nextの振る舞いをエミュレートしているだけですが、使った遷移を「保存」してSyncに渡すことができる点が異なります。
これはアクションに渡されたパラメータを保持するのにも役立ち、合成の際に必要になることがあります。
コメント
ログインしてコメントする