システム設計にAlloyを使ってみる（前篇）

Alloyという形式仕様記述言語の使い勝手も試したくなったので触ってみる。

はじめに

RDSの監査ログをエクスポートするシステムの設計をしている。一応アーキテクチャの概要は浮かんではいるのだが、要求を満たすか客観的に評価しないと「ぼくの考えた〜」止まりになってしまう。少し前に『実践TLA+』を読んで以来、設計の評価にはTLA+を使っているが、Alloyという言語もちらほら耳にして気になっていた。この機会に使い勝手を試してみる。

動作環境

macOS 15.6.1（Apple M1 Max）
Alloy Analyzer 6.1.0.20211119T054551

givenなものを整理する

前提（Assumptions）

要求ID	概要	理由
A001	単一リージョンにある5つのRDSクラスタを処理対象とすること	—
A002	RDS監査ログはCloudWatch Logsへ正常に出力されているものとする	—
A003	エクスポート処理はCloudWatch Logsから実施し、RDSから直接ログを取得しないものとする	エクスポート処理による負荷）をRDSにかけたくないため

要求（Requirements）

要求ID	概要
R001	リアルタイム性よりもインフラコスト抑制を重視すること
R002	エクスポート単位は日次とすること
R003	エクスポート済ログに欠損がないこと
R004	エクスポート済ログに重複がないこと
R005	一つの処理対象に対する自動試行回数が有限であること
R006	自動回復できないエクスポート失敗を運用者が認識できること

制約（Constraints）

ID	概要
C001	1つのAWSアカウントで同時にアクティブにできるCloudWatch Logs export taskは1つである¹
C002	export taskは非同期に実行されるが、export taskの完了イベントは発行されないため成否を確認する必要がある

初期システム要件

前述の前提・要求から、下記の方法は選択肢から除外される:

RDSのDownloadDBLogFilePortion APIを使う方法（A003により）
Amazon Data Firehoseによる方法（R001により）

なので基本的にはこちらのアーキテクチャを基本としたものになる見通しだが、システム要件を一応まとめてみる:

ID	概要	対応元
IR001	各RDSクラスタについて1日を一つの処理対象単位とする	A001, R002
IR002	処理対象単位はクラスタと対象日の組で一意に識別される	R002, R003, R004
IR003	同時にアクティブにするexport taskは最大1つとする	C001
IR004	失敗した処理は規定の上限回数まで再試行する	R003, R005, R006
IR005	試行上限に達したジョブはそれ以上自動試行されない	R005
IR006	試行上限に達したジョブを通知対象として記録する	R006
IR007	成功済みの処理対象単位を再び実行対象にしない	R004
IR008	ある処理対象単位について、成功したexport taskの成果物は高々1つとする	R004
IR009	各処理対象単位は、成功または通知対象のいずれかに到達するまで管理対象から削除しない	R003, R006

Alloyによるモデル検査によって要件の穴が見つかるかもしれないので、システム初期要件（Initial system requirements）としておく。

システム要件をAlloyコードへ

ドメイン構造

本モデルでは下記のエンティティを扱うことにする:

Cluster: 処理対象のRDSクラスタ
Day: 処理対象日
Job: システムによる、ログエクスポートをトリガーするジョブ
ExportTask: CloudWatchがバックエンドで実行する監査ログのエクスポートタスク

Alloyコードとしては下記のようになる:

module RdsAuditLogExport

// Domain model

sig Cluster {}

sig Day {}

sig Job { // 処理対象単位（Cluster × Day）
  cluster: one Cluster, // 各Jobはちょうど一つのClusterを持つ
  day: one Day
}

one sig ExportTask { // AWSの仕様上並行実行不能なのでone
  var job: lone Job // 未使用状態があり得るのでoneではなくlone
}

↑トリガーごとの独立性を示したいjobは、Alloy 6の新機能であるmutable field（var）を使って表現する。

ClusterとJobだけで表現できる要件があるので、さっそく書いてみる:

  one sig ExportTask { // AWSの仕様上並行実行不能なのでone
    var job: lone Job // 未使用状態があり得るのでoneではなくlone
  }
+ /*
+  * 各ClusterとDayの組について、処理対象となるJobがちょうど1つ存在する
+  *
+  * IR001: 各RDSクラスタについて1日を一つの処理対象単位とする
+  *
+  * IR002: 処理対象単位を、ClusterとDayの組で一意に識別する
+  */
+ fact OneJobPerClusterAndDay {
+   all c: Cluster, d: Day |
+     one j: Job | // 条件を満たすJobがちょうど1つ存在する
+       j.cluster = c and j.day = d
+ }

↑sig（signature）で記述したドメインオブジェクトを使って、システム要件をfactとして宣言する。 TLA+はほぼ数式だが、Alloyはほぼプログラミング言語って感じ。ちなみに、ここで使われている=は代入ではなく条件判定の意味。

シンタックスエラー等の早期発見のため、いったんここまででコードをexecuteしておく:

Executing "Run Default for 4 but 4 int, 4 seq expect 1"
   Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=OFF Mode=batch
   689 vars. 64 primary vars. 1444 clauses. 2ms.
   Instance found. Predicate is consistent, as expected. 6ms.

↑まだなにも検査してないが、少なくともコンパイルが通ることはわかった。

状態

続いて、システムがとりうる状態をコード化していく。

下記の概念を扱うことにする:

JobStatus: ジョブの状態
- Pending（実行待ち）
- Running（実行中）
- RetryWaiting（リトライ待ち）
- Succeeded（成功）
- PendingNotification（規定のリトライ数を実行済み、通知待ち）
ExportTaskStatus: CloudWatchによる監査ログエクスポートタスクの状態
- Unused（エクスポート枠が未使用）
- Active（エクスポート中）
- TaskSucceeded（エクスポート成功）
- TaskFailed（エクスポート失敗）

これらをコード化すると下記のようになる:

  fact OneJobPerClusterAndDay {
    all c: Cluster, d: Day |
      one j: Job |
        j.cluster = c and j.day = d
  }
+ 
+ // Status
+ 
+ abstract sig JobStatus {}
+ 
+ one sig Pending,
+         Running,
+         RetryWaiting,
+         Succeeded,
+         PendingNotification
+   extends JobStatus {}
+ 
+ abstract sig ExportTaskStatus {}
+ 
+ one sig Unused,
+         Active,
+         TaskSucceeded,
+         TaskFailed
+   extends ExportTaskStatus {}

↑ここでのoneも前述のものと同じく「ちょうど1つ」の意味で、シングルトンなsigを複数種まとめて宣言しているだけ。 abstractな親と組み合わせることで、実質的にenumとして振る舞う。

また、JobStatusとExportTaskStatusはそれぞれJobとExportTaskが持つべき状態なので、それを明示する:

  sig Job { // 処理対象単位（Cluster × Day）
    cluster: one Cluster,
-   day: one Day
+   day: one Day,
+   var status: one JobStatus
  }
  
  one sig ExportTask { // AWSの仕様上並行実行不能なのでone
-   var job: lone Job // 未使用状態があり得るのでoneではなくlone
+   var job: lone Job, // 未使用状態があり得るのでoneではなくlone
+   var status: one ExportTaskStatus
  }

ここまでをまたexecuteしてみる:

Executing "Run Default for 4 but 4 int, 4 seq expect 1"
   Solver=sat4j Steps=1..10 Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=OFF Mode=batch
   1..1 steps. 849 vars. 101 primary vars. 1704 clauses. 3ms.
   Instance found. Predicate is consistent, as expected. 2ms.

↑問題なし。

状態の定義までできたので、次は初期状態の定義に進む。

初期状態

シミュレーション開始時点のシステムの状態を定義する。

すべての（今回はたまたま並行実行が最大一つの想定だが）、JobとExportTaskの初期状態はそれぞれPendingとUnusedであってほしい:

  one sig Unused,
          Active,
          TaskSucceeded,
          TaskFailed
    extends ExportTaskStatus {}
+  
+ pred init {
+   all j: Job | j.status = Pending and j.attempts = 0
+   ExportTask.status = Unused
+   no ExportTask.job
+ }

↑one sigであるExportTaskと、ふつうのsigであるJobの違いがシンタックスによく表れている。

ここまでの定義がうまくいっているか、いったん確認しておきたい。検査を実行するために下記を追加する:

  pred init {
    all j: Job | j.status = Pending and j.attempts = 0
    ExportTask.status = Unused
    no ExportTask.job
  }
+ 
+ run init for
+   exactly 2 Cluster,
+   exactly 1 Day,
+   exactly 2 Job

executeしてみる:

Executing "Run init for exactly 2 Cluster, exactly 1 Day, exactly 2 Job"
   Actual scopes: exactly 2 Cluster, exactly 1 Day, exactly 2 Job, exactly 1 ExportTask, 5 JobStatus, exactly 1 Pending, exactly 1 Running, exactly 1 RetryWaiting, exactly 1 Succeeded, exactly 1 PendingNotification, 4 ExportTaskStatus, exactly 1 Unused, exactly 1 Active, exactly 1 TaskSucceeded, exactly 1 TaskFailed
   Solver=sat4j Steps=1..10 Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20 Mode=batch
   1..1 steps. 127 vars. 23 primary vars. 202 clauses. 9ms.
   Instance found. Predicate is consistent. 4ms.

状態遷移

ここまでに出てきた状態に関する各概念について、足りないものを補っていく。

システムのJobがとる状態（var status）は、下のように遷移してほしい:

stateDiagram-v2
    [*] --> Pending: 初期状態
    Pending --> Running: 開始
    Running --> Succeeded: 終了
    Running --> RetryWaiting: 失敗（規定の試行回数未満）
    Running --> PendingNotification: 失敗（規定の試行回数に到達）
    RetryWaiting --> Running: 再開

    classDef idle fill:#f5f5f5,stroke:#9e9e9e,stroke-width:1px,color:#212121
    classDef active fill:#bdbdbd,stroke:#616161,stroke-width:2px,color:#212121
    classDef waiting fill:#e0e0e0,stroke:#757575,stroke-width:1px,color:#212121
    classDef done fill:#424242,stroke:#212121,stroke-width:2px,color:#ffffff

    class Pending idle
    class Running active
    class RetryWaiting waiting
    class Succeeded done
    class PendingNotification done

↑リトライ上限（var attempts）も定義する必要がある。

またCloudWatchのExportTaskの状態は、下のように遷移する意図で定義したものである:

stateDiagram-v2
    [*] --> Unused: 初期状態
    Unused --> Active: 開始
    Active --> TaskSucceeded: 成功
    Active --> TaskFailed: 失敗
    TaskSucceeded --> Unused: 実行枠を解放
    TaskFailed --> Unused: 実行枠を解放

    classDef idle fill:#f5f5f5,stroke:#9e9e9e,stroke-width:1px,color:#212121
    classDef active fill:#bdbdbd,stroke:#616161,stroke-width:2px,color:#212121
    classDef result fill:#757575,stroke:#424242,stroke-width:1px,color:#ffffff

    class Unused idle
    class Active active
    class TaskSucceeded result
    class TaskFailed result

↑Jobとは違って、こちらはリクエストを受けて淡々と実行するだけの形にモデリングしているので、再実行のような概念はない。

Alloyで状態遷移を表すには、これらの状態遷移図の矢印で発生するイベントを述語（pred）として定義する必要がある。以下で、それぞれの関数を個別のブロックで示していく。すべてrds-audit-log-export.alsへの追記である。

エクスポート処理をシステムのJobがトリガーする様子:

// Events

pred startExport[j: Job] {
  // guard
  j.status in Pending + RetryWaiting
  ExportTask.status = Unused

  // effect
  j.status' = Running
  ExportTask.status' = Active
  ExportTask.job' = j
}

↑枠が空いていて、かつ実行待ちまたはリトライ待ちのJobがあるときに実行される。

CloudWatchのエクスポートタスク作成に失敗したり、エクスポートタスクが失敗したときには有限回リトライしてほしいので、Jobで試行回数を管理することにする:

  sig Job { // 処理対象単位（Cluster × Day）
    cluster: one Cluster, // 各Jobはちょうど一つのClusterを持つ
    day: one Day,
-   var status: one JobStatus
+   var status: one JobStatus,
+   var attempts: one Int
  }

初期状態ではもちろん試行回数は0回:

  pred init {
-   all j: Job | j.status = Pending
+   all j: Job | j.status = Pending and j.attempts = 0
    ExportTask.status = Unused
    no ExportTask.job
  }

試行回数は有限にしたいので、ひとまず3回を上限としておく:

+ /*
+  * 1つの処理対象単位（Job）に許される試行回数の上限
+  * 初回実行とリトライを合算した回数とする（3ならリトライは最大2回）
+  */
+ fun MaxAttempts: Int { 3 }

  pred startExport[j: Job] {
    // guard
    j.status in Pending + RetryWaiting
+   j.attempts < MaxAttempts
    ExportTask.status = Unused
  
    // effect
    j.status' = Running
+   j.attempts' = add[j.attempts, 1]
    ExportTask.status' = Active
    ExportTask.job' = j
  }

重要なポイントとして、このシステムでは一つのExportTask枠をクラスタ数 × 日付個のJobが譲り合って（？）利用する必要がある。現時点の書き方だと、すべてのJobの状態がそれぞれ同時に変化するようになってしまっている。 Alloyのドキュメントで説明されている通り、変化してはならないものについてはそれを明示する必要がある。この制約を明示するには、ジョブが変化しない場合を表現した関数を追加したうえで、startExportを下記のようにする:

  pred init {
    all j: Job | j.status = Pending and j.attempts = 0
    ExportTask.status = Unused
    no ExportTask.job
  }
+ 
+ // Frame conditions
+ 
+ pred noJobChange[js: set Job] {
+   all j: js | j.status' = j.status and j.attempts' = j.attempts
+ }
+ 
  // Events
  
  pred startExport[j: Job] {
    // guard
    j.status in Pending + RetryWaiting
    j.attempts < MaxAttempts
    ExportTask.status = Unused
  
    // effect
    j.status' = Running
    j.attempts' = add[j.attempts, 1]
    ExportTask.status' = Active
    ExportTask.job' = j
+ 
+   // frame
+   noJobChange[Job - j]
  }

また、エクスポートタスクは時間がかかるため、システムのタイムステップが進んでも、タスク状態が変わっていない状況がありえる。そのためエクスポートタスクについても、状態を変化させないフレーム関数をつくる:

  pred noJobChange[js: set Job] {
    all j: js | j.status' = j.status and j.attempts' = j.attempts
  }
+   
+ pred noTaskChange {
+   ExportTask.status' = ExportTask.status
+   ExportTask.job' = ExportTask.job
+ }

この調子で、状態遷移に必要な他のpredを追加していく²。

エクスポートタスクの成功・失敗:

pred taskSucceed {
  // guard
  ExportTask.status = Active
  one ExportTask.job

  // effect
  ExportTask.status' = TaskSucceeded
  ExportTask.job' = ExportTask.job

  // frame
  noJobChange[Job]
}

pred taskFail {
  // guard
  ExportTask.status = Active
  one ExportTask.job

  // effect
  ExportTask.status' = TaskFailed
  ExportTask.job' = ExportTask.job

  // frame
  noJobChange[Job]
}

↑ただ一つのJobと紐づくようにガードを入れている。

ジョブの終了:

pred completeJob {
  // guard
  ExportTask.status = TaskSucceeded
  one ExportTask.job

  let j = ExportTask.job {
    j.status = Running

    // effect
    j.status' = Succeeded
    j.attempts' = j.attempts

    // frame
    noJobChange[Job - j]
  }

  // ExportTask実行枠を解放
  ExportTask.status' = Unused
  no ExportTask.job'
}

↑エクスポートが成功したらエクスポートタスク実行枠を解放する。

失敗のハンドリング:

pred handleFailure {
  ExportTask.status = TaskFailed
  one ExportTask.job

  let j = ExportTask.job {
    j.status = Running

    j.attempts < MaxAttempts implies
      j.status' = RetryWaiting

    j.attempts >= MaxAttempts implies
      j.status' = PendingNotification

    j.attempts' = j.attempts
    noJobChange[Job - j]
  }

  ExportTask.status' = Unused
  no ExportTask.job'
}

ここまでのAlloyコードの全体は下記のようになる:

module RdsAuditLogExport

// Domain model

sig Cluster {}

sig Day {}

sig Job { // 処理対象単位（Cluster × Day）
  cluster: one Cluster, // 各Jobはちょうど一つのClusterを持つ
  day: one Day,
  var status: one JobStatus,
  var attempts: one Int
}

one sig ExportTask { // AWSの仕様上並行実行不能なのでone
  var job: lone Job, // 未使用状態があり得るのでoneではなくlone
  var status: one ExportTaskStatus
}

/*
 * 各ClusterとDayの組について、処理対象となるJobがちょうど1つ存在する
 *
 * IR001: 各RDSクラスタについて1日を一つの処理対象単位とする
 *
 * IR002: 処理対象単位を、ClusterとDayの組で一意に識別する
 */
fact OneJobPerClusterAndDay {
  all c: Cluster, d: Day |
    one j: Job | // 条件を満たすJobがちょうど1つ存在する
      j.cluster = c and j.day = d
}

// Status

abstract sig JobStatus {}

one sig Pending,
        Running,
        RetryWaiting,
        Succeeded,
        PendingNotification
  extends JobStatus {}

abstract sig ExportTaskStatus {}

one sig Unused,
        Active,
        TaskSucceeded,
        TaskFailed
  extends ExportTaskStatus {}
  
pred init {
  all j: Job | j.status = Pending and j.attempts = 0
  ExportTask.status = Unused
  no ExportTask.job
}

// Frame conditions

pred noJobChange[js: set Job] {
  all j: js | j.status' = j.status and j.attempts' = j.attempts
}

pred noTaskChange {
  ExportTask.status' = ExportTask.status
  ExportTask.job' = ExportTask.job
} 

// Events

/*
 * 1つの処理対象単位（Job）に許される試行回数の上限
 * 初回実行とリトライを合算した回数とする（3ならリトライは最大2回）
 */
fun MaxAttempts: Int { 3 }

pred startExport[j: Job] {
  // guard
  j.status in Pending + RetryWaiting
  j.attempts < MaxAttempts
  ExportTask.status = Unused

  // effect
  j.status' = Running
  j.attempts' = add[j.attempts, 1]
  ExportTask.status' = Active
  ExportTask.job' = j

  // frame
  noJobChange[Job - j]
}

/*
 * CloudWatch Logsのエクスポート処理が成功する。
 *
 * JobはまだRunningのままであり、completeJobによって
 * 成功確認後にSucceededへ遷移する。
 */
pred taskSucceed {
  // guard
  ExportTask.status = Active
  one ExportTask.job

  // effect
  ExportTask.status' = TaskSucceeded
  ExportTask.job' = ExportTask.job

  // frame
  noJobChange[Job]
}

/*
 * CloudWatch Logsのエクスポート処理が失敗する。
 *
 * JobはまだRunningのままであり、handleFailureによって
 * RetryWaitingまたはPendingNotificationへ遷移する。
 */
pred taskFail {
  // guard
  ExportTask.status = Active
  one ExportTask.job

  // effect
  ExportTask.status' = TaskFailed
  ExportTask.job' = ExportTask.job

  // frame
  noJobChange[Job]
}

/*
 * ExportTaskの成功を確認し、対応するJobを完了させる。
 */
pred completeJob {
  // guard
  ExportTask.status = TaskSucceeded
  one ExportTask.job

  let j = ExportTask.job {
    j.status = Running

    // effect
    j.status' = Succeeded
    j.attempts' = j.attempts

    // frame
    noJobChange[Job - j]
  }

  // ExportTask実行枠を解放
  ExportTask.status' = Unused
  no ExportTask.job'
}


pred handleFailure {
  ExportTask.status = TaskFailed
  one ExportTask.job

  let j = ExportTask.job {
    j.status = Running

    j.attempts < MaxAttempts implies
      j.status' = RetryWaiting

    j.attempts >= MaxAttempts implies
      j.status' = PendingNotification

    j.attempts' = j.attempts
    noJobChange[Job - j]
  }

  ExportTask.status' = Unused
  no ExportTask.job'
}

run init for
  exactly 2 Cluster,
  exactly 1 Day,
  exactly 2 Job

さてこの状態でexecuteしても、前回の実行時からの違いはattemptsを示す0が追加されただけで、その他のシステムの状態には全く変化がない:

これは、現在のrunコマンドが、初期状態を表すinit predicateだけを満たすトレースを探索しているためだ:

pred init {
  all j: Job | j.status = Pending and j.attempts = 0
  ExportTask.status = Unused
  no ExportTask.job
}

run init for
  exactly 2 Cluster,
  exactly 1 Day,
  exactly 2 Job

そこで、探索対象にstartExport predicateを含めてみる:

- run init for
+ run {
+   init
+   some j: Job | startExport[j]
+ } for
  exactly 2 Cluster,
  exactly 1 Day,
- exactly 2 Job
+ exactly 2 Job,
+  3 Int

↑some j: Job | startExport[j]は、「少なくとも1つのJobについて、startExport[j]という状態遷移が成立する」という意味³。

また、ややわかりにくいが、runコマンド最後の3 Intは、この検証で使いたい整数の範囲を符号付きビット数で指定したもの。いまは最大でも試行回数用に3まで表現できれば足りるので、3ビットの符号つき整数（-4〜3）でOK。

探索範囲にstartExportを含めた実行結果を示したのが下図:

↑statusがRunningとなったJob0のattemptが1になり、それがActiveになったExportTaskと紐づいている。

ここまでで、ひとまず検証ループを一周回せた。

Alloyコードとシステム初期要件との照合

システムに対する理解のモデル化を一通り終えたつもりなので、ここでシステム初期要件を見直し、モデル定義で保証できている要件と、追加で検証が必要な要件とを分類する。

ID	概要	対応元	現在の対応状況
IR001	各RDSクラスタについて1日を一つの処理対象単位とする	A001, R002	`Day`としてモデル化済⁴
IR002	処理対象単位はクラスタと対象日の組で一意に識別される	R002, R003, R004	`OneJobPerClusterAndDay` factで構造的に保証済 ✅
IR003	同時にアクティブにするexport taskは最大1つとする	C001	単一のエクスポートタスク実行枠として構造的に保証済 ✅
IR004	失敗した処理は規定の上限回数まで再試行される	R003, R005, R006	モデル化済み・追加で検証が必要 ⚠️
IR005	試行上限に達したジョブはそれ以上自動試行されない	R005	モデル化済み・追加で検証が必要 ⚠️
IR006	試行上限に達したジョブを通知対象として記録する	R006	PendingNotificationとしてモデル化済み・追加で検証が必要⁵ ⚠️
IR007	成功済みの処理対象単位を再び実行対象にしない	R004	`startExport`のガードでモデル化済み・追加で検証が必要 ⚠️
IR008	ある処理対象単位について、成功したexport taskの成果物は高々1つとする	R004	成果物または実行履歴の追加モデル化と検証が必要 ⚠️
IR009	各処理対象単位は、成功または通知対象のいずれかに到達するまで管理対象から削除しない	R003, R006	signatureである`Job`は消えない点は構造的に保証済。ただし終端状態への到達は追加で検証が必要 ⚠️

…うーん。各要件を意識しながらモデル化したつもりだったが、あらためてなぞってみると、複数の制約の組み合わせによって表現されていて、“構造的に保証済"と言い切れるものはほとんどなかった⁶。ちなみにAlloyの動作原理は有限範囲を探索するだけなので、構造的に保証したもの以外は「探索した範囲内では反例は見つかりませんでした」という意味でしかないらしい。ただそれでも、人間の根気ではとても列挙できない多数の状態や組み合わせを機械的に探索してくれるし、境界条件や複数の状態遷移が組み合わさったときの欠陥を発見してくれる点に、やはり大きな価値があると思う。

追加検証

事前準備

追加の検証でassertとcheckを利用するため、システムが取り得る状態遷移をTraces factとして定義する:

pred stutter {
  noJobChange[Job]
  noTaskChange
}

fact Traces {
  init

  always {
    (some j: Job | startExport[j])
    or taskSucceed
    or taskFail
    or completeJob
    or handleFailure
    or stutter
  }
}

↑alwaysの内部では、各時点から次の時点への遷移が、列挙したpredicateのいずれかに一致することを要求している。しかし、すべてのジョブが状態遷移の終端に到達した場合や、外部処理の完了を待っている場合など、実質的に状態が変化しない時点もあり得る。そこで、すべての可変フィールドを現在の値のまま維持するstutter遷移を追加する。これにより、実行可能なイベントがない状態でも、同じ状態にとどまるトレースを表現できる。

準備ができたので、IR0004に対応するassertを追加してみる。

IR004: 失敗した処理は規定の上限回数まで再試行される

assert FailedJobIsEventuallyRetried {
  always all j: Job |
    j.status = RetryWaiting and
    j.attempts < MaxAttempts
    implies
    eventually startExport[j]
}

上記のassertを8ステップ内でcheckしてみる:

check FailedJobIsEventuallyRetried for
  exactly 2 Cluster,
  exactly 1 Day,
  exactly 2 Job,
  3 Int,
  8 steps

反例が見つかった:

Executing "Check FailedJobIsEventuallyRetried for 3 int 8 steps, exactly 2 Cluster, exactly 1 Day, exactly 2 Job"
   Actual scopes: exactly 2 Cluster, exactly 1 Day, exactly 2 Job, exactly 1 ExportTask, 5 JobStatus, exactly 1 Pending, exactly 1 Running, exactly 1 RetryWaiting, exactly 1 Succeeded, exactly 1 Exhausted, 4 ExportTaskStatus, exactly 1 Unused, exactly 1 Active, exactly 1 TaskSucceeded, exactly 1 TaskFailed
   Solver=sat4j Steps=1..8 Bitwidth=3 MaxSeq=3 SkolemDepth=1 Symmetry=20 Mode=batch
   1..4 steps. 9201 vars. 372 primary vars. 24717 clauses. 33ms.
   Counterexample found. Assertion is invalid. 7ms.

状態を見てみる:

↑ジョブがRetryWaitingのまま動かないケースが見つかった。これは、連続でstutter predicateが選ばれている状態らしい。確かに、startExportが選ばれる条件としてRetryWaitingを書いたが、startExportを選ばなければならないとは書かなかった⁷。

このことから、IR004 は状態遷移の正しさだけでは満たすことができず、スケジューリングに関する要件が足りていないことがわかった。追加要件（Additional Requirement）が見つかったので、IDをふって記録することにする。

ID	概要	関連要件
AR001	システムは実行を待っているJobを無期限に保留しない	IR004

追加要件がもっと出てきそうなので、ここでいったん一区切りとする。

所感

本記事は、RDS監査ログのエクスポートシステムの設計について検討した（しきれなかった）。監査ログアーキテクチャが頭に浮かんではいるが⁸、モデルには具体的なアーキテクチャの構成要素は登場させず、あくまでも要求から導かれる仕様を検証してみた。

まだちょっと触ってみただけだが、Alloyの使い勝手を（TLA+の使い勝手を思い出しながら）メモしておく。

良さが感じられた点 ☀️
- ドメイン構造を第一級市民として書けるところ
  - “処理対象単位が Cluster × Day で一意” という制約を一行でone j: Job | j.cluster = c and j.day = dと書けた
  - 多重度（one / lone）が言語に組み込まれているので、ExportTaskに関する「未使用状態があり得る」をvar job: lone Jobと簡潔に書けた
- モデルを探索的に育てられるところ
  - 「そういう状態がありうるか」をrunですぐ確認できるので、今回はvacuityの検出に多用した
  - 結果の可視化機能が素晴らしい。初学者にとっては「自分のモデルが何を意味しているのか」を視覚的に確認しながら進める助けになる
戸惑った点 ⛅
- フレーム条件を自分で書かないといけないところ
  - 本記事で扱った題材では、noJobChange[Job - j] のような述語を自前で用意し、全イベントで呼ばないといけなかった。呼び忘れると、その変数が次状態で任意の値を取れるようになるので、他のsignatureの状態が意図せず勝手に変わるようになる
- stutterを遷移の選択肢に明示的に足す必要があるところ
  - 今回のモデルでは、全JobがSucceeded/PendingNotificationに到達し、ExportTaskがUnusedの状態でどのアクションもEnabledにならない。この状態は意図された終了状態なので必ず到達するべきだが、stutterを書き忘れるとシミュレーションが先に進めず、有効な無限トレースが1本も存在しなくなってしまう。厄介なのは、同じ原因が問いの向きによって逆の表示になること: 「存在するか」を問うrunでは「インスタンスなし」と出るため問題に気付けるが、一方で「反例が存在するか」を問うcheckはでは「反例なし」（= 検証成功）になってしまうため気付けない

追加要件も見つかったので、別記事で続きをやりたい。

参考文献

CloudWatch Logs quotas | docs.aws.amazon.com ↩︎
ここまででいったんexecuteしてみたが、必要なpredを全てを定義し切らないと解決しない状態遷移系の違反が起きてしまうため ↩︎
ちなみにall j: Job | startExport[j]を探索しても、No instance found. Predicate may be inconsistentとなる。これはone sig ExportTaskであり、またExportTaskではvar job: lone Jobなことによる ↩︎
Day sigによって対象日をモデル化したが、それが暦上の1日単位で生成されることは実装側で保証する必要がある ↩︎
PendingNotificationステータスと、その状態へ移行する遷移をモデル化する。ただし、試行上限到達時に必ず移行することはassertで検証する必要がある ↩︎
まぁでもそれは普通のことだと思うし、だからこそassertやcheckの存在意義があるのだけど ↩︎
ちなみに、ここで注意が必要なのは、「反例になっているのは連続stutterなのだからstutterを禁止すればよい」はNGであること。これをやってしまうと、意図された終了状態（全Jobが終端状態に達し、ExportTaskがUnusedの状態など）で無限トレースが構成できず、有効なトレースが1本も存在しなくなってしまう。というか、これが起こると困るからstutterが必要なのだ ↩︎
アーキテクチャ例出てるし。 ↩︎