まえがき

システムの信頼性や安全性に対する運用面の取り組みがSREだとすれば、
開発面の取り組みは何にあたるでしょうか。
ペアプロやコードレビューによる人間やAIによって不具合を検査する方法や、
テストコードや静的解析ツール等によるシステム化された検査方法があります。
これらの実装に対するアプローチはどれも馴染み深いですが、
一方で仕様に対するアプローチ、特にシステム化された検証方法を目にする機会はあまりありません。

仕様に対するアプローチには、
形式手法と呼ばれる、システムの仕様を形式的に表現しその妥当性を検証する分野があります。
今回は形式手法のなかでも形式仕様記述のツール、TLA+を用いて、
弊社で運用しているGitHub ActionsのSelf Hosted Runnerのオートスケーリングのロジックの検証をしましたので、形式仕様記述とTLA+活用事例としてご紹介します。

TLA+と形式仕様記述について

すでに解説記事などありますのでそれらの紹介にとどめさせてください。

クラメソさんのやってみた記事

TLA+の公式サイト

後述の「実践TLA+」の著者の解説サイト

「実践TLA+」という技術書もあります。割と最近翻訳されました。

GitHub Actionsのオートスケーリングの検証

背景

弊社はGitHub Enterprise Serverでコード管理を行っているため、
GitHub Actionsを採用するとなると必然的にSelf Hosted Runnerを運用することになります。
現状ではEC2にRunnerを乗せて運用しているケースが多いですが、
各プロダクト/チームごとにRunnerをホストする仮想マシンを用意するのは運用上様々なデメリットが生じるため
Self Hosted Runnerの共通基盤を用意し、各プロダクト共通で利用いただくことを推進しています。

システムの仕様

この共通RunnerはAmazon ECSを基盤としており、Task１つに対してRunnerが1対1対応でホストされる仕様です。
Taskのアイドル時間を最小限にしつつ、開発体験を損なわないようコールドスタートの発生を抑えるため、
常に稼働状態のRunnerを1台用意します。
また、スパイクアクセスに応えるためオートスケールを実装します。

オートスケールの課題

今回Runnerのオートスケーリングロジックの検証にTLA+を採用しました。

Webアプリケーション向けにECSのオートスケーリングポリシーを設定する際は
CloudWatch Metrixで取得可能なメトリックを監視条件に設定することができ、
一般にCPU, メモリの使用量を閾値にするケースが見られます。

今回はRunnerのオートスケールを考える必要がありますが、
RunnerつまりTask１個に対してWorkflow Job１個が占有するため、コンピューティングリソースのメトリックではなく、Runnerの状態遷移がスケーリングの条件に妥当と考えました。

しかしCloudWatchの標準メトリックではRunnerの状態は取得できません。
そのためECSのオートスケーリング機能を採用できず、自前でECSを増減するロジックを実装することにしました。

以下はオートスケールのアイデアになります。

Runnerの起動時にECS ServiceのTask起動数を増やし、Runnerの終了時にTask起動数を減らすというロジックです。ECSTask（Runner）の増減はAPIリクエスト１本投げるだけで済むため実装スクリプト自体は驚くほど簡素となりました。

ただAWSから提供されたものと比べ、悲観的ですが実績がないため信頼性が乏しいです。しかしEC2のRunnerやJenkins, CodePipelineから移行するチーム、Actionsを新規導入するチームに安心して利用いただけるよう、何らかの方法でシステムの品質担保した状態で提供することが望ましいと思いました。

このシステムはECSの状態 x Runnerの状態 x Jobの状態と状態の組み合わせが複雑となるため、状態バグを引き起こしやすい仕様にみえます。
また、複数のRunnerもといECS Taskが平行稼働状態となるため、状態の組み合わせ数が膨大となり動的テストで検査するのは非効率です。
そこで、システムが取りえる状態を網羅的に調べることで、想定から漏れている状態や
仕様から逸脱する振る舞いが発生しないことを確かめるべく、TLA+による仕様記述をおこないました。

TLA+の記述と検証

以下はTLA+と、その糖衣構文のPlusCal言語による仕様記述です。
すみませんがTLA＋の構文の説明は割愛します。

---- MODULE ecs_ghactions_scaling ----
EXTENDS Sequences, FiniteSets, Integers, TLC
CONSTANTS NumRunners
ASSUME NumRunners \in Int
Runners == 1..NumRunners

(*--algorithm ecs_ghactions_scaling
\* システムの状態を記述します。
variables
    desire_count = Cardinality(Runners);
\*  state kind {"pending", "running", "completed", "failed"}
    workflow_run = [r \in Runners |-> "pending"];
\*  state kind {"registrate", "offline", "idle", "active", "terminate"}
    runner_state = [r \in Runners |-> "registrate"];
    connected_ghserver = [r \in Runners |-> FALSE];
    ecs_task_state = [r \in Runners |-> [ state |-> "running" ] ];

\*  defineにはシステムが満たすべき性質を記述します。
define 
    \* 常にECS desire countが0より大きいこと
    AlwayNeedRunner == desire_count > 0
end define;

\* システムの状態遷移を定義します。
process Registration \in Runners
begin
    \* Runner登録時
    Registration:
        await ~connected_ghserver[self];
        await runner_state[self] = "registrate";
        \* runner registration
        connected_ghserver[self] := TRUE;
        runner_state[self] := "idle";
    \* RunnerIdle時
    Idle:
        await connected_ghserver[self];
        await runner_state[self]  = "idle";
        either \* workflowがstarted
            await workflow_run[self] = "pending";
            workflow_run[self] := "running";
            runner_state[self] := "active";
            desire_count := desire_count + 1;
        or     \* trouble 何かしらの理由で落ちた
            connected_ghserver[self] := FALSE;
            runner_state[self] := "offline";
            ecs_task_state[self].state := "stop";
            workflow_run[self] := "failed";
            goto Done
        end either;
    \* Runner Active時
    Active:
        await connected_ghserver[self];
        await runner_state[self] = "active";
        await workflow_run[self] = "running";
        either \* workflowがcomplited/failed
            with picked_runner \in Runners do
                connected_ghserver[self] := FALSE;
                desire_count := desire_count - 1;
                ecs_task_state[picked_runner].state := "stop";
                runner_state[picked_runner] := "terminate";
                workflow_run[self] := "completed";
            end with;
        or     \* runner disconnected
            connected_ghserver[self] := FALSE;
            ecs_task_state[self].state := "stop";
            runner_state[self] := "offline";
            desire_count := desire_count - 1;
            workflow_run[self] := "failed";
        end either;
    \* Runner終了時
    Terminate:        
        runner_state[self] := "terminate";
        workflow_run[self] := "failed";
        goto Done
end process;

end algorithm; *)
=======================

仕様のリファインメント

このコードをモデル検査にかけたところ、
RunnerがActive中にECSによって停止させられるモデルを発見しました。
Actionsのジョブ実行中にECSのタスク数調整によってRunnerを停止させられることを防がなければいけません。

ECSのドキュメントを調査したところ、scale in_protectionというパラメーターを発見しました。
こちらを有効化すると、ECS Taskが正常終了されるまでECS Serviceによって強制停止させられないようになります。
https://docs.aws.amazon.com/ja_jp/AmazonECS/latest/developerguide/task-scale-in-protection-endpoint.html

これによりジョブ実行が中断させられる課題を解決できそうなため、仕様に組み込みこんで再度検証してみることにしました。

以下は修正したシーケンス図になります。

また、修正したTLA＋コードは以下になります。
scalein_protectionの状態と、Runnerが中断させられるモデルを発見するため、
NoSuddenlyStopActiveRunnerの検査項目を追加しました。

---- MODULE ecs_ghactions_scaling ----
EXTENDS Sequences, FiniteSets, Integers, TLC
CONSTANTS NumRunners
ASSUME NumRunners \in Int
Runners == 1..NumRunners

(*--algorithm ecs_ghactions_scaling
\* システムの状態を記述します。
variables
    desire_count = Cardinality(Runners);
\*  state kind {"pending", "running", "completed", "failed"}
    workflow_run = [r \in Runners |-> "pending"];
\*  state kind {"registrate", "offline", "idle", "active", "terminate"}
    runner_state = [r \in Runners |-> "registrate"];
    connected_ghserver = [r \in Runners |-> FALSE];
    ecs_task_state = [r \in Runners |-> [ state |-> "running", scalein_protection |-> FALSE] ];

\*  defineにはシステムが満たすべき性質を記述します。
define 
    \* 常にECS dire countが0より大きいこと
    AlwayNeedRunner == desire_count > 0

    \* ECS Task scalein protectionが有効のときECS Serviceによって強制終了させられないこと
    NoSuddenlyStopActiveRunner == ~\E runner \in Runners: 
        runner_state[runner] = "active" 
        /\ ecs_task_state[runner].state = "stop"
        /\ ecs_task_state[runner].scalein_protection
end define;

\* システムの状態遷移を定義します。
process Registration \in Runners
begin
    \* Runner登録時
    Registration:
        await ~connected_ghserver[self];
        await runner_state[self] = "registrate";
        \* runner registration
        connected_ghserver[self] := TRUE;
        runner_state[self] := "idle";
    \* RunnerIdle時
    Idle:
        await connected_ghserver[self];
        await runner_state[self]  = "idle";
        either \* workflowがstarted
            await workflow_run[self] = "pending";
            workflow_run[self] := "running";
            runner_state[self] := "active";
            ecs_task_state[self].scalein_protection := TRUE;
            desire_count := desire_count + 1;
        or     \* trouble 何かしらの理由で落ちた
            connected_ghserver[self] := FALSE;
            runner_state[self] := "offline";
            ecs_task_state[self].state := "stop";
            workflow_run[self] := "failed";
            goto Done
        end either;
    \* Runner Active時
    Active:
        await connected_ghserver[self];
        await runner_state[self] = "active";
        await workflow_run[self] = "running";
        either \* workflowがcomplited/failed
            with picked_runner \in Runners do
                connected_ghserver[self] := FALSE;
                desire_count := desire_count - 1;
                await ~ecs_task_state[picked_runner].scalein_protection;
                ecs_task_state[picked_runner].state := "stop";
                runner_state[picked_runner] := "terminate";
                workflow_run[self] := "completed";
            end with;
        or     \* runner disconnected
            connected_ghserver[self] := FALSE;
            ecs_task_state[self].state := "stop";
            runner_state[self] := "offline";
            desire_count := desire_count - 1;
            workflow_run[self] := "failed";
        end either;
    \* Runner終了時
    Terminate:        
        runner_state[self] := "terminate";
        workflow_run[self] := "failed";
        goto Done
end process;


end algorithm; *)

再度モデル検査を実行した結果、
期待通りActive状態のRunnerが中断させられるモデルがないことを確認できました。

おわりに

TLA＋によってロジックの仕様を厳密に記述することで、
隠れていた不具合を発見し、設計の妥当性を検証することができました。

また、仕様のコーディングを通して考慮が漏れていたケースに気づくこともできました。
このような気づきはアプリを実装する際にも得られますが、
仕様記述はアプリの実装時よりマクロに考えさせられるため異なる観点でレビューできる点は面白いです。

今回は小さい仕様でしたが、例えばより規模が大きいシステムなどで完成に時間を要する場合や、仕様ミスによる実装の手戻りを防ぎたい場など、完成前の段階でアイデアの検証ができる点が魅力的です。

今回はTLA＋を採用しましたが、その他様々なツール/言語がありますので、
形式手法を導入される際は用途に合わせて検討するのがよさそうです。

形式手法の全体像の把握にはこちらが役立ちました。