---
title: ぼくのかんがえたさいきょうの alt TLA+
tags: 
author: [Shoichi Sasaki](https://www.docswell.com/user/ajfAfg)
site: [Docswell](https://www.docswell.com/)
thumbnail: https://bcdn.docswell.com/page/5EGL48LWJL.jpg?width=480
description: 関数型まつり 2026 の発表資料です。  https://fortee.jp/2026fp-matsuri/proposal/29169622-8801-4dd1-8017-59cfff560d89
published: July 12, 26
canonical: https://www.docswell.com/s/ajfAfg/57N917-my-idea-for-ultimate-alt-tlaplus
---
# Page. 1

![Page Image](https://bcdn.docswell.com/page/5EGL48LWJL.jpg)

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


# Page. 2

![Page Image](https://bcdn.docswell.com/page/4JQYG9YQ7P.jpg)

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


# Page. 3

![Page Image](https://bcdn.docswell.com/page/K74W5XWYE1.jpg)

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


# Page. 4

![Page Image](https://bcdn.docswell.com/page/LJ1YWNYNEG.jpg)

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


# Page. 5

![Page Image](https://bcdn.docswell.com/page/GJWG641M72.jpg)

状態数を
減らすのが
大事
モデル検査の仕組み超概説
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


# Page. 6

![Page Image](https://bcdn.docswell.com/page/4EZLY2PM73.jpg)

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


# Page. 7

![Page Image](https://bcdn.docswell.com/page/Y76WDVM57V.jpg)

エラーが出る場合
期待する性質:
キューに詰められたタスクはいつか処理される
反例が出る
（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)


# Page. 8

![Page Image](https://bcdn.docswell.com/page/G75M3DZG74.jpg)

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 の改変


# Page. 9

![Page Image](https://bcdn.docswell.com/page/9J29Z8RDER.jpg)

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あります


# Page. 10

![Page Image](https://bcdn.docswell.com/page/DEY4R6DMJM.jpg)

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書きづらい…


# Page. 11

![Page Image](https://bcdn.docswell.com/page/VJNYDZ6378.jpg)

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


# Page. 12

![Page Image](https://bcdn.docswell.com/page/YE9PGZLPJ3.jpg)

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


# Page. 13

![Page Image](https://bcdn.docswell.com/page/GE8DV1XXED.jpg)

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


# Page. 14

![Page Image](https://bcdn.docswell.com/page/LELM5Q8N7R.jpg)

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


# Page. 15

![Page Image](https://bcdn.docswell.com/page/4JMY316QJW.jpg)

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


# Page. 16

![Page Image](https://bcdn.docswell.com/page/PJR9QLPK79.jpg)

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


# Page. 17

![Page Image](https://bcdn.docswell.com/page/PEXQ5W35JX.jpg)

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


# Page. 18

![Page Image](https://bcdn.docswell.com/page/3EK96VYRED.jpg)

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


# Page. 19

![Page Image](https://bcdn.docswell.com/page/L73W6M9G75.jpg)

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


# Page. 20

![Page Image](https://bcdn.docswell.com/page/87DKV6GNJG.jpg)

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


# Page. 21

![Page Image](https://bcdn.docswell.com/page/VJPKVY3NE8.jpg)

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)


# Page. 22

![Page Image](https://bcdn.docswell.com/page/2EVVZG4YEQ.jpg)

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+、機械語みたいやんけ


# Page. 23

![Page Image](https://bcdn.docswell.com/page/57GL481WEL.jpg)

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


# Page. 24

![Page Image](https://bcdn.docswell.com/page/4EQYG9DQJP.jpg)

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


# Page. 25

![Page Image](https://bcdn.docswell.com/page/KJ4W5XZY71.jpg)

コンパイルしてみる（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


# Page. 26

![Page Image](https://bcdn.docswell.com/page/LE1YWNRN7G.jpg)

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)


# Page. 27

![Page Image](https://bcdn.docswell.com/page/GEWG64YMJ2.jpg)

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


# Page. 28

![Page Image](https://bcdn.docswell.com/page/47ZLY2XMJ3.jpg)

モデル検査してみる
（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


# Page. 29

![Page Image](https://bcdn.docswell.com/page/YJ6WDV45JV.jpg)

モデル検査してみる
（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


# Page. 30

![Page Image](https://bcdn.docswell.com/page/GJ5M3DQGJ4.jpg)

どうやって実現してるの？
• いわゆる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


# Page. 31

![Page Image](https://bcdn.docswell.com/page/9E29Z8PD7R.jpg)

その他の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


# Page. 32

![Page Image](https://bcdn.docswell.com/page/D7Y4R65MEM.jpg)

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


# Page. 33

![Page Image](https://bcdn.docswell.com/page/VENYDZN3J8.jpg)

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


# Page. 34

![Page Image](https://bcdn.docswell.com/page/Y79PGZRPE3.jpg)

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


# Page. 35

![Page Image](https://bcdn.docswell.com/page/G78DV1WX7D.jpg)

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


# Page. 36

![Page Image](https://bcdn.docswell.com/page/L7LM5QNNJR.jpg)

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


# Page. 37

![Page Image](https://bcdn.docswell.com/page/4EMY31XQEW.jpg)

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


# Page. 38

![Page Image](https://bcdn.docswell.com/page/PER9QLNKJ9.jpg)

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


# Page. 39

![Page Image](https://bcdn.docswell.com/page/P7XQ5WN5EX.jpg)

モデル検査の仕組み超概説（再掲）
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


# Page. 40

![Page Image](https://bcdn.docswell.com/page/37K96VNR7D.jpg)

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


# Page. 41

![Page Image](https://bcdn.docswell.com/page/LJ3W6MVGJ5.jpg)

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


# Page. 42

![Page Image](https://bcdn.docswell.com/page/8JDKV68NEG.jpg)

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


# Page. 43

![Page Image](https://bcdn.docswell.com/page/VEPKVY8N78.jpg)

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


# Page. 44

![Page Image](https://bcdn.docswell.com/page/27VVZGNY7Q.jpg)

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


# Page. 45

![Page Image](https://bcdn.docswell.com/page/5JGL48KW7L.jpg)

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


# Page. 46

![Page Image](https://bcdn.docswell.com/page/47QYG9NQEP.jpg)

実験環境
• 共通
•
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


# Page. 47

![Page Image](https://bcdn.docswell.com/page/KE4W5XGYJ1.jpg)

スピンロック
（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


# Page. 48

![Page Image](https://bcdn.docswell.com/page/L71YWNDNJG.jpg)

スピンロック
（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


# Page. 49

![Page Image](https://bcdn.docswell.com/page/G7WG648ME2.jpg)

パン屋のアルゴリズム
（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


# Page. 50

![Page Image](https://bcdn.docswell.com/page/4JZLY28ME3.jpg)

パン屋のアルゴリズム
（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


# Page. 51

![Page Image](https://bcdn.docswell.com/page/YE6WDVP5EV.jpg)

今回施した最適化手法の詳細（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


# Page. 52

![Page Image](https://bcdn.docswell.com/page/GE5M3DKGE4.jpg)

今回施した最適化手法の詳細（２/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


# Page. 53

![Page Image](https://bcdn.docswell.com/page/9729Z8WDJR.jpg)

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