ぼくのかんがえたさいきょうの alt TLA+

ぼくのかんがえた さいきょうのalt TLA+ Show（@ajfAfg） 関数型まつり 2026

Show（@ajfAfg） プログラミング言語と型が好き 2026/07/12 関数型まつり2026 2

TLA+って何？ • TLA+とは形式仕様記述言語 • 並行・分散システムの振る舞い（あるいはアルゴリズム）を 曖昧なく記述できる • TLA+で書いたシステムは、モデル検査という手法で ある種のバグ（e.g. デッドロック）を検出できる • AWSやAzureで採用事例がある 2026/07/12 関数型まつり2026 テストで見つけづらいバグもOK！ 3

モデル検査って何？ • モデル検査とは、システムが取りうる状態を網羅的に調べ、 期待する性質をシステムが満たすか検査する手法 • 性質の例: 「キューに詰められたタスクはいつか処理される」 • システムは刻々と状態変化するので、検査する性質は 時間の経過を表現可能な論理体系で書きがち • E.g. 時相論理 2026/07/12 今日はあまり触れない 関数型まつり2026 4

状態数を 減らすのが 大事 モデル検査の仕組み超概説 x = 0, y = 0; 1. x++; 2. y++; グラフを走査して期待する 性質を満たすか検査 e.g.「いつかy≥1」 状態遷移グラフに変換 x=2 y=0 x=0 y=0 x=1 y=0 x=1 y=1 x=0 y=0 x=2 y=1 x=1 y=0 x=2 y=2 x=1 y=1 プロセスの数 = 1 2026/07/12 プロセスの数 = 2 関数型まつり2026 5

TLA+でモデル検査 Enqueue(t) == 期待する性質: キューに詰められたタスクはいつか処理される 未完了なタスクを キューに詰める /\ t \in Tasks /\ t \notin q \cup done /\ q' = q \cup {t} /\ UNCHANGED done キューに詰められた Dequeue(t) == タスクを完了 /\ t \in q /\ q' = q \ {t} /\ done' = done \cup {t} Enqueue/Dequeue どちらかを評価 2026/07/12 Next == \/ \E t \in Tasks : Enqueue(t) \/ \E t \in Tasks : Dequeue(t) 関数型まつり2026 6

エラーが出る場合 期待する性質: キューに詰められたタスクはいつか処理される 反例が出る （Tasks = {t1,t2}） Enqueue(t) == /\ t \in Tasks /\ t \notin q \cup done /\ q' = q \cup {t} /\ UNCHANGED done Dequeue(t) == /\ t \in q /\ q' = q \ {t} /\ done' = done \cup {t} キューに詰められた Drop(t) == タスクを削除 /\ t \in q /\ q' = q \ {t} /\ UNCHANGED done 2026/07/12 Next == \/ \E t \in Tasks : Enqueue(t) \/ \E t \in Tasks : Dequeue(t) 関数型まつり2026 7 \/ \E t \in Tasks : Drop(t)

fn lock(...) -> LockGuard {
...
for i in 0..NUM_THREADS {
if let Some(t) = ... {
max = max.max(t);
}
}
• いつも書いている言語と
...
for i in 0..NUM_THREADS {
世界観が違いすぎ
if i == idx {continue;}
while ... {}
• 右図のような構造化された
loop {
match ... {
プログラムをTLA+で模倣するの
Some(t) => {if ... {break;}}
しんどい
None => {break;}
}
}
逆によく抽象化されている場合は
}
書きやすいが……
fence(Ordering::SeqCst);
LockGuard { idx }
https://github.com/oreilly}
2026/07/12
関数型まつり2026
8
japan/conc_ytakano/blob/34f4510ed3b41d8ce7929b70deb05

TLA+書きづらい…

e51d15f474f/chap3/3.9/ch3_9_bakery/src/main.rs の改変

• https://github.com/oreilly-japan/conc_ytakano/blob/34f4510ed3b41d8ce7929b70deb05e51d15f474f/chap3/3.9/ch3_9_bakery/src/main.rs

start:
while (loop < NLoop) {
p1:
...
scan: while (j <= N) {
...
};
p2:
...
• PlusCalとは、TLA+の
forj: while (j <= N) {
if (j = self) {
開発チームが開発するalt TLA+
j := j + 1;
} else {
• 擬似コードのような形で
wEnter:
await ~entering[j];
wNumber:
await ~Higher(j, self);
システムの振る舞いを記述できる
j := j + 1;
};
};
cs1: tmp := count;
cs2: count := tmp + 1;
unlock:
...
}
2026/07/12
関数型まつり2026
9

PlusCalあります

start:
while (loop < NLoop) {
p1:
...
scan: while (j <= N) {
...
};
p2:
...
• ラベル多すぎ
forj: while (j <= N) {
if (j = self) {
• PlusCalでは処理の原子性の粒度を
j := j + 1;
ラベルで制御するため、逆に細かく
} else {
wEnter:
await ~entering[j];
制御したいとき大量のラベルが登場 wNumber:
await ~Higher(j, self);
j := j + 1;
};
• レキシカルスコープじゃない
};
cs1: tmp := count;
• 型がない
cs2: count := tmp + 1;
unlock:
...
}
2026/07/12
関数型まつり2026
10

PlusCal書きづらい…

PlusCalは簡潔さを尊ぶ • 公式から「TLA+/PlusCalにリッチな 言語機能を追加しない（超要約）」 と明言されている • 言語機能が多いとそれだけ開発が大変 （モデル検査がバグると困る）なので これは悪い意思決定ではない 2026/07/12 関数型まつり2026 11

あこがれは 止められねぇんだ 2026/07/12 関数型まつり2026 12

爆誕 「私たちが作りました」 • sanpouの役割は主に二つ • sanpouコードからTLA+コードへのコンパイル • コンパイルされたTLA+をモデル検査して見つかったエラーを sanpouの語彙に再翻訳 sanpou コード sanpou コンパイラ TLA+ コード sanpou エラー コンパイル 2026/07/12 sanpou コンパイラ TLA+ エラー 再翻訳 関数型まつり2026 13

今日のゴール • sanpouの解説を通して以下の理解を得る • TLA+/PlusCalの言語仕様 • PlusCalからTLA+へのコンパイルの仕組み • リッチなalt TLA+の開発で生じる問題点と解決方法 2026/07/12 関数型まつり2026 14

お断り • sanpouのモチベーションは、「並行プログラミング入門」で 紹介される手法をTLA+でモデル検査する中で生まれた • 今回のTLA+の用途はモデル検査のみ 2026/07/12 関数型まつり2026 15

目次 1. 背景 2. PlusCalの仕組み 3. sanpouの仕組み 4. 評価 2026/07/12 関数型まつり2026 16

Cでスピンロック • スピンロックとは、 リソースが空くまで ポーリングして確認する ロックの実装 2026/07/12 void lock_acquire(bool *lock) { while (__sync_lock_test_and_set(lock, 1)); } void lock_release(bool *lock) { __sync_lock_release(lock); } bool lock = false; int count = 0; void *worker(void *arg) { for (int i = 0; i < NUM_LOOPS; i++) { lock_acquire(&lock); count++; count--; lock_release(&lock); } return NULL; } 関数型まつり2026 17

variables lock = FALSE, count = 0,
ret = [t \in 1..ThreadNum |-> FALSE];

PlusCalで(ry
void lock_acquire(bool *lock) {
while (__sync_lock_test_and_set(lock, 1));
}
void lock_release(bool *lock) {
__sync_lock_release(lock);
}
bool lock = false;
int count = 0;
void *worker(void *arg) {
for (int i = 0; i < NUM_LOOPS; i++) {
lock_acquire(&lock);
count++;
count--;
lock_release(&lock);
}
return NULL;
}
2026/07/12

procedure testAndSet() {
tas: ret[self] := lock || lock := TRUE; return;
}
procedure lockAcquire() {
acq: call testAndSet();
chk: if (ret[self]) { goto acq; };
fin: return;
}
procedure lockRelease() {
rel: lock := FALSE; return;
}

process (worker \in 1..ThreadNum) {
loop: while (TRUE) {
call lockAcquire();
cs1: count := count + 1;
cs2: count := count - 1;
call lockRelease();
}
}
関数型まつり2026

18

TLA+にコンパイルする（1/3）
variables
lock = FALSE, count = 0,
ret = [t \in 1..ThreadNum |->
FALSE];

VARIABLES pc, lock, count, ret, stack

Init == (* Global variables *)
/\ lock = FALSE
/\ count = 0
/\ ret = [t \in 1..ThreadNum |-> FALSE]
/\ stack = [self \in ProcSet |-> << >>]
pcは評価するアクションの決定に使う
/\ pc = [self \in ProcSet |-> "loop"]

stackはスタックフレームの管理に使う
2026/07/12

関数型まつり2026

19

TLA+にコンパイルする（2/3）
procedure testAndSet() {
tas: ret[self] := lock || lock := TRUE; return;
}

pcを呼び出し元に復帰
stackから先頭の
スタックフレームを破棄

tas(self) == /\ pc[self] = "tas"
/\ /\ lock' = TRUE
/\ ret' = [ret EXCEPT ![self] = lock]
アクション名は
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
ラベルとProcedure名に
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
対応
/\ count' = count
testAndSet(self) == tas(self)
2026/07/12

関数型まつり2026

20

TLA+に
コンパイル
する（3/3）

procedure lockAcquire() {
acq: call testAndSet();
chk: if (ret[self]) { goto acq; };
fin: return;
}

acq(self) == /\ pc[self] = "acq"
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "testAndSet",
pc
|-> "chk" ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "tas"]
/\ UNCHANGED << lock, count, ret >>
chk(self) == /\ pc[self] = "chk"
stackにスタック
/\ IF ret[self]
フレームを積む
THEN /\ pc' = [pc EXCEPT ![self] = "acq"]
pcをProcedureの
ELSE /\ pc' = [pc EXCEPT ![self] = "fin"]
/\ UNCHANGED << lock, count, ret, stack >>
先頭ラベルで更新
fin(self) == /\ pc[self] = "fin"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << lock, count, ret >>
2026/07/12
関数型まつり2026
21
lockAcquire(self) == acq(self) \/ chk(self) \/ fin(self)

TLA+に
コンパイル
する（3/3）

procedure lockAcquire() {
acq: call testAndSet();
chk: if (ret[self]) { goto acq; };
fin: return;
}

acq(self) == /\ pc[self] = "acq"
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "testAndSet",
pc
|-> "chk" ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "tas"]
/\ UNCHANGED << lock, count, ret >>
chk(self) == /\ pc[self] = "chk"
stackにスタック
/\ IF ret[self]
フレームを積む
THEN /\ pc' = [pc EXCEPT ![self] = "acq"]
pcをProcedureの
ELSE /\ pc' = [pc EXCEPT ![self] = "fin"]
/\ UNCHANGED << lock, count, ret, stack >>
先頭ラベルで更新
fin(self) == /\ pc[self] = "fin"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << lock, count, ret >>
2026/07/12
関数型まつり2026
22
lockAcquire(self) == acq(self) \/ chk(self) \/ fin(self)

TLA+、機械語みたいやんけ

目次 1. 背景 2. PlusCalの仕組み 3. sanpouの仕組み 4. 評価 2026/07/12 関数型まつり2026 23

sanpouで
スピンロック

var lock = false; var count = 0;
procedure testAndSet() {
var old = false;
old = lock, lock = true;
return old;
}
procedure lockAcquire() {
• なんとラベルなし
while (testAndSet()) {}
return ();
• <stmt>{,<stmt>};
}
という単位でコンパイル時に
procedure lockRelease() {
lock = false; return ();
ラベルを自動挿入
}
procedure worker() {
• while文の前にも入る
while (true) {
lockAcquire();
count = count + 1; count = count - 1;
• Procedureは返り値を持つ
lockRelease();
}
return ();
}
2026/07/12
関数型まつり2026
24

コンパイルしてみる（1/3） PlusCalと同じ仕組み var lock = false; var count = 0; Init == /\ lock = FALSE /\ count = 0 /\ stack = [self \in ProcSet |-> << >>] /\ pc = [self \in ProcSet |-> "__w_workers_entry__"] 2026/07/12 関数型まつり2026 25

procedure testAndSet() {
var old = false;
old = lock, lock = true;
return old;
}

コンパイルしてみる（2/3）

L3(self) ==
/\ pc[self] = "L3"
/\ stack' = [stack EXCEPT ![self] = [stack[self] EXCEPT ![1].old__1 = FALSE]]
/\ pc' = [pc EXCEPT ![self] = "L2"]
/\ UNCHANGED << lock, count >>
L2(self) ==
ローカル変数はスタックフレームで管理
/\ pc[self] = "L2"
/\ lock' = TRUE
/\ stack' = [stack EXCEPT ![self] = [stack[self] EXCEPT ![1].old__1 = lock]]
/\ pc' = [pc EXCEPT ![self] = "L1"]
/\ UNCHANGED << count >>
返り値をスタックフレームに積む
L1(self) ==
/\ pc[self] = "L1"
/\ stack' = [stack EXCEPT ![self] = << [value |-> Head(stack[self]).old__1] >> \o
Tail(stack[self])]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).return_pc]
/\2026/07/12
UNCHANGED << lock, count >>
関数型まつり2026
26
testAndSet(self) == L3(self) \/ L2(self) \/ L1(self)

procedure lockAcquire() {
while (testAndSet()) {}
return ();
}

コンパイルしてみる（3/3）

L6(self) ==
/\ pc[self] = "L6"
/\ stack' = [stack EXCEPT ![self] = << [procedure |-> "testAndSet", return_pc |->
"L7", old__1 |-> defaultInitValue] >> \o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "L3"]
/\ UNCHANGED << lock, count >>

先頭スタックフレーム削除 & 返り値取得

L7(self) ==
/\ pc[self] = "L7"
/\ stack' = [stack EXCEPT ![self] = [Tail(stack[self]) EXCEPT ![1].callRet__1 =
Head(stack[self]).value]]
/\ pc' = [pc EXCEPT ![self] = "L5"]
/\ UNCHANGED << lock, count >>
2026/07/12

関数型まつり2026

27

モデル検査してみる （1/2） 期待する性質: 常にcount <= 1 2026/07/12 var lock = false; var count = 0; procedure testAndSet() { var old = false; old = lock; lock = true; return old; } procedure lockAcquire() { while (testAndSet()) {} return (); } procedure lockRelease() { lock = false; return (); } procedure worker() { while (true) { lockAcquire(); count = count + 1; count = count - 1; lockRelease(); } return (); } 関数型まつり2026 28

モデル検査してみる （2/2） var lock = false; var count = 0; procedure testAndSet() { var old = false; old = lock; lock = true; return old; } $ sanpou trace spinlock.out Step 1: Initial state lock = FALSE count = 0 Step 2: ... Step 3: ... Step 4: ... Step 5: lockAcquire (process 1): [call testAndSet] (frame: old = null) Step 6: testAndSet (process 1): var old = false old = FALSE 2026/07/12 関数型まつり2026 sanpouの 語彙に 再翻訳 29

どうやって実現してるの？ • いわゆるSourcemap L3: proc: “testAndSet” desc: “var old = false;” L3(self) == ... L2(self) == ... L1(self) == ... L2: proc: “testAndSet;” desc: “old = lock, lock = true” L1: proc: “testAndSet” desc: “return old” 2026/07/12 関数型まつり2026 procedure testAndSet() { var old = false; old = lock, lock = true; return old; } 30

その他のsanpouの特徴 逆にこれら以外は 大体PlusCalと同じ • レキシカルスコープ • 型推論時は普通（？）に型環境を引き回してるだけ • コンパイル時はα変換して名前の重複を排除 • Hindley-Milner型推論 • 破壊的単一化による多相型推論 • varによる変数代入は単相 • mutableなので 2026/07/12 procedure f() { var x = 0; // 1. x : int x = x + 1; // 2. OK var x = (x == 1); // 3. x : bool await x; // 4. OK return (); } 関数型まつり2026 31

sanpouの仕組みの全体像（１/2） Procedure呼び出し を巻き上げ 型推論はここ 意味解析 + α変換 Parse sanpou コード AST 正規化 AST’ 単純な命令の列に 変換 コード 生成 Lowering AST’’ 中間 表現 TLA+ コード source map コンパイル 2026/07/12 関数型まつり2026 32

sanpouの仕組みの全体像（2/2） 気合いで 翻訳 sanpou エラー 気合いで Parse sanpou コンパイラ TLA+ エラー 再翻訳 2026/07/12 関数型まつり2026 33

目次 1. 背景 2. PlusCalの仕組み 3. sanpouの仕組み 4. 評価 2026/07/12 関数型まつり2026 34

sanpou最強説 もう全部あいつ一人で いいんじゃないかな 2026/07/12 関数型まつり2026 35

仮説「状態数が爆発してない？」 • 言語機能をリッチにした弊害で状態数が爆発してる可能性 • 状態数が爆発するとモデル検査が現実的な時間で 終わらなくなる • とても困る • モデル検査にかかる時間を計測してみよう！ 2026/07/12 関数型まつり2026 実験の詳しい条件は 付録 36

スピンロックの場合 まだ慌てるような 時間じゃない 2026/07/12 関数型まつり2026 37

パン屋のアルゴリズムの場合 終わった 2026/07/12 関数型まつり2026 38

モデル検査の仕組み超概説（再掲） x = 0, y = 0; 1. x++; 2. y++; 状態数を 減らすのが 大事 グラフを走査して期待する 性質を満たすか検査 e.g.「いつかy≥1」 状態遷移グラフに変換 x=2 y=0 x=0 y=0 x=1 y=0 x=1 y=1 x=0 y=0 x=2 y=1 x=1 y=0 x=2 y=2 x=1 y=1 プロセスの数 = 1 2026/07/12 プロセスの数 = 2 関数型まつり2026 39

反省会 • パン屋のアルゴリズムほど巨大な例になってくると 言語機能をリッチにした弊害が目に見えてくる • ラベルの自動挿入はコードが大きいほど嬉しいのに本末転倒 • 最適化しよう • ローカル変数の操作列のような、プロセス外から観測できない一連の アクションを一つのアクションにまとめる • 参照されなくなったローカル変数にデフォルト値を代入 2026/07/12 関数型まつり2026 詳しくは付録 40

スピンロックの場合（最適化後） 約97%減！ （N=6） 2026/07/12 関数型まつり2026 41

パン屋のアルゴリズムの場合（最適化後） 約94%減！！ （N=3） 2026/07/12 関数型まつり2026 42

教訓 • alt TLA+は言語機能のリッチさだけではなく、状態数にも気を 配る必要がある • モデル検査する対象言語へのコンパイラ一般について言えそう 2026/07/12 関数型まつり2026 43

まとめ • PlusCalからTLA+へのコンパイルの仕組みは、高級言語から 機械語へのコンパイルの仕組みとよく似ていた • レキシカルスコープとProcedureの返り値をサポートする、 PlusCal的なalt TLA+のモデル検査にかかる時間は、PlusCalと 比較して倍程度（ただし最適化を施せば） • alt TLA+は言語機能のリッチさの他に状態数削減がとても大事 2026/07/12 関数型まつり2026 44

付録 2026/07/12 関数型まつり2026 45

実験環境 • 共通 • PC: Apple M5 Pro, 48 GB • Java: openjdk 26.0.1, TLA+: v1.7.4 • 実行コマンド • スピンロック: java -XX:+UseParallelGC -jar tla2tools.jar -workers auto -metadir <tmpdir> -config <.cfg> <.tla> • パン屋のアルゴリズム: java -XX:+UseParallelGC -Xmx6g -jar tla2tools.jar -workers auto -metadir <tmpdir> config <.cfg> <.tla> • sanpou改修前 • コミットハッシュ: ca2545f66ec79eb31ef29b18793daee5270a2854 • sanpou改修後 • コミットハッシュ: 7c3b814331ed1f9291d0af7dca1f0fccd62db0d5 2026/07/12 関数型まつり2026 46

スピンロック
（PlusCal）

---- MODULE spinlock_pluscal ---EXTENDS Naturals, Sequences

spinlock.tla

CONSTANT N
(* --algorithm spinlock {
variables lock = FALSE, count = 0, ret = [p \in 1..N |-> FALSE];
define {
MutexOk == count <= 1
}
procedure testAndSet()
variable old = FALSE;
{
tas: old := lock;
lock := TRUE;
tasR: ret[self] := old;
return;
}

spinlock.cfg
SPECIFICATION Spec
CONSTANT N = 2
CHECK_DEADLOCK FALSE
INVARIANT MutexOk

2026/07/12

procedure lockAcquire()
{
acq: call testAndSet();
acqC: if (ret[self]) { goto acq; } else { return; };
}

procedure lockRelease()
{
rel: lock := FALSE;
return;
}
process (w \in 1..N)
{
loop: while (TRUE) {
call lockAcquire();
cs1:
count := count + 1;
cs2:
count := count - 1;
relC:
call lockRelease();
}
}
関数型まつり2026
} *)
====

47

スピンロック
（sanpou）

mod spinlock {
def threadNum = 2;

spinlock.snp

var lock = false;
var count = 0;
def mutexOk = count <= 1;
procedure testAndSet() {
var old = false;
old = lock, lock = true;
return old;
}

spinlock.json

{
"checks": {
"deadlock": false,
"termination": false
},
"properties": [],
"invariants": ["mutexOk"]
}

2026/07/12

procedure lockAcquire() {
while (testAndSet()) {}
return ();
}
procedure lockRelease() {
lock = false;
return ();
}
procedure worker() {
while (true) {
lockAcquire();
count = count + 1;
count = count - 1;
lockRelease();
}
return ();
}
process workers(self in 1..threadNum) = worker;
関数型まつり2026
}

48

パン屋のアルゴリズム
（PlusCal）

CONSTANT defaultInitValue = defaultInitValue
SPECIFICATION Spec
CONSTANTS
numThreads = 2
numLoop = 2
CHECK_DEADLOCK TRUE
INVARIANTS
MutexOk
TicketValid
PROPERTIES
Termination

2026/07/12

bakery.tla
---- MODULE bakery_pluscal ---EXTENDS Integers, Sequences

CONSTANTS numThreads, numLoop
(* --algorithm bakery {
variables
entering = [x \in 1..numThreads |-> FALSE],
tickets = [x \in 1..numThreads |-> -1],
cs = 0;
define {
MutexOk == cs <= 1
TicketValid == \A j \in 1..numThreads : tickets[j] = -1 \/ tickets[j] >= 1
}
procedure lockAcquire(idx)
variables max = 0, i = 1, tmp = 0, ticket = 0;
{
la1: entering[idx] := TRUE;
max := 0;
i := 1;
scan: while (i <= numThreads) {
tmp := tickets[i];
if (max < tmp) { max := tmp; };
i := i + 1;
};
ticket := max + 1;
pub: tickets[idx] := ticket;
la2: entering[idx] := FALSE;
i := 1;
wait: while (i <= numThreads) {
if (i = idx) {
i := i + 1;
} else {
we:
while (entering[i]) { skip; };
wt:
while (TRUE) {
tmp := tickets[i];
if (tmp # -1) {
if (ticket < tmp \/ (ticket = tmp /\ idx < i)) { goto adv; };
} else {
goto adv;
};
};
adv:
i := i + 1;
};
};
return;
}

bakery.cfg

procedure lockRelease(idx)
{
rel: tickets[idx] := -1;
return;
}

関数型まつり2026

fair process (t \in 1..numThreads)
variable k = 1;
{
loop: while (k <= numLoop) {
call lockAcquire(self);
csI:
cs := cs + 1;
csO:
cs := cs - 1;
relC:
call lockRelease(self);
inc:
k := k + 1;
};
}
} *)
====

49

パン屋のアルゴリズム
（sanpou）

mod bakery_algorithm {
def null = -1;
def numThreads = 2;
def numLoop = 2;

bakery.snp

var entering = {
x in 1..numThreads -> false
};
var tickets = {
x in 1..numThreads -> null
};
// 検証用のゴースト変数: クリティカルセクションの同時占有数
var cs = 0;
// 相互排除: クリティカルセクションに同時に入れるのは高々 1 スレッド
def mutexOk = cs <= 1;
// チケットは未使用 (null) か 1 以上。max 走査で tickets[i] の読みが
// 複数アクションに分かれていると 0 が生まれる(退行の検知用)
def ticketValid = forall (j in 1..numThreads) {
tickets[j] == null || tickets[j] >= 1
};
procedure lockAcquire(idx) {
entering[idx] = true;

var max = 0;
var i = 1;
while (i <= numThreads) {
var tmp = tickets[i];
if (max < tmp) {
max = tmp;
}
i = i + 1;
}
var ticket = max + 1;
tickets[idx] = ticket;
entering[idx] = false;
var i = 1;
while (i <= numThreads) {
if (i == idx) {
i = i + 1;
continue;
} else {
while (entering[i]) {}

bakery.json

{

while (true) {
var tmp = tickets[i];
if (tmp != null) {
// スレッド i のチケット番号より自分の番号の方が若いか、
// チケット番号が同じでかつ、自分の方がスレッド番号が若い場合に待機終了
if ((ticket < tmp) || (ticket == tmp && idx < i)) {
break;
}
} else {
// スレッド i が処理中でない場合は待機終了
break;
}
}

"checks": {
"deadlock": true,
"termination": true
},
"properties": [],
"invariants": ["mutexOk", "ticketValid"]

}
i = i + 1;

}

}

return ();

}
procedure lockRelease(idx) {
tickets[idx] = null;
return ();
}
procedure thread() {
var i = 1;
while (i <= numLoop) {
lockAcquire(self);
cs = cs + 1;
cs = cs - 1;
lockRelease(self);

i = i + 1;
}

2026/07/12

関数型まつり2026

return ();
}

fair process t(self in 1..numThreads) = thread;
}

50

今回施した最適化手法の詳細（1/2）
１つ目「ローカル変数の操作列のような、プロセス外から観測できない一連のアクション
を一つのアクションにまとめる」
L3(self) ==
/\ pc[self] = "L3"
/\ stack' = [stack EXCEPT ![self] = [stack[self] EXCEPT ![1].old__1 = FALSE]]
/\ pc' = [pc EXCEPT ![self] = "L2"]
/\ UNCHANGED << lock, count >>
L2(self) ==
/\ pc[self] = "L2"
/\ lock' = TRUE
/\ stack' = [stack EXCEPT ![self] = [stack[self] EXCEPT ![1].old__1 = lock]]
/\ pc' = [pc EXCEPT ![self] = "L1"]
/\ UNCHANGED << count >>
L1(self) ==
/\ pc[self] = "L1"
/\ stack' = [stack EXCEPT ![self] = << [value |-> Head(stack[self]).old__1] >> \o
Tail(stack[self])]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).return_pc]
/\ UNCHANGED << lock, count >>

before

L3(self) ==
/\ pc[self] = "L3"
/\ lock' = TRUE
/\ stack' = [stack EXCEPT ![self] = << [value |-> lock] >> \o
Tail([stack[self] EXCEPT ![1].old__1 = FALSE, ![1].old__1 = lock])]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).return_pc]
/\ UNCHANGED << count >>
testAndSet(self) == L3(self)

testAndSet(self) == L3(self) \/ L2(self) \/ L1(self)

2026/07/12

中間表現（Control-flow graph; CFG）を
対象に、隣接する頂点を繰り返し縮約する。
ただし、縮約後のCFGに含まれる任意の頂
点はグローバル変数に高々１回アクセスす
る（違反するなら縮約しない）。

関数型まつり2026

after

51

今回施した最適化手法の詳細（２/2）
２つ目「参照されなくなったローカル変数にデフォルト値を代入」

L5(self) ==
/\ pc[self] = "L5"
/\ pc' = [pc EXCEPT ![self] = IF Head(stack[self]).callRet__1 THEN "L8" ELSE "L4"]
/\ UNCHANGED << stack, lock, count >>

そもそもモチベは、ローカル変数だけの差分
による状態数増加の抑制
（グローバル変数は同じなのにローカル変数
だけ異なり状態が増えるケースがままある）

before

生存変数解析してローカル変数が
死んだタイミングでデフォルト値
を代入
2026/07/12

L5(self) ==
/\ pc[self] = "L5"
/\ stack' = [stack EXCEPT ![self] = [stack[self] EXCEPT ![1].callRet__1 = defaultInitValue]]
/\ pc' = [pc EXCEPT ![self] = IF Head(stack[self]).callRet__1 THEN "L8" ELSE "L4"]
/\ UNCHANGED << lock, count >>

after
関数型まつり2026

52

vs Quint • Quintは「疑似コードっぽく書ける」体験を目指していない （と思っている） • 型付きTLA+という印象 • sanpouはPlusCalと同じように、「疑似コードっぽく書ける」 体験を目指している点でQuintと異なる • 静的型付けな点は同じ 2026/07/12 関数型まつり2026 53