Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
Speaker Deck
Features
Speaker Deck
PRO
Sign in
Sign up for free
Search
Search
形式手法特論:位相空間としての並行プログラミング #kernelvm / Kernel VM ...
Search
y_taka_23
August 09, 2025
Technology
3
240
形式手法特論:位相空間としての並行プログラミング #kernelvm / Kernel VM Study Tokyo 18th
Kernel/VM 探検隊@東京 No.18 で使用したスライドです。
y_taka_23
August 09, 2025
Tweet
Share
More Decks by y_taka_23
See All by y_taka_23
AWS と定理証明 〜ポリシー言語 Cedar 開発の舞台裏〜 #fp_matsuri / FP Matsuri 2025
ytaka23
10
3k
問 1:以下のコンパイラを証明せよ(予告編) #kernelvm / Kernel VM Study Kansai 11th
ytaka23
3
820
AWS のポリシー言語 Cedar を活用した高速かつスケーラブルな認可技術の探求 #phperkaigi / PHPerKaigi 2025
ytaka23
10
2.6k
NilAway による静的解析で「10 億ドル」を節約する #kyotogo / Kyoto Go 56th
ytaka23
4
690
形式手法の 10 メートル手前 #kernelvm / Kernel VM Study Hokuriku Part 7
ytaka23
7
1.4k
普通の Web エンジニアのための様相論理入門 #yapcjapan / YAPC Hakodate 2024
ytaka23
11
3.2k
kcp: Kubernetes APIs Are All You Need #techfeed_live / TechFeed Experts Night 28th
ytaka23
1
520
サーバーレスアーキテクチャの数理的理解と分析 #devsumi / Developers Summit 2023 Summer
ytaka23
9
5.4k
形式手法による分散システムの検証 〜S3 の一貫性モデルを例として〜 #ourdevday2023 / Our DevDay 2023
ytaka23
2
1.5k
Other Decks in Technology
See All in Technology
大規模イベントに向けた ABEMA アーキテクチャの遍歴 ~ Platform Strategy 詳細解説 ~
nagapad
0
190
Amazon Q と『音楽』-ゲーム音楽もAmazonQで作成してみた感想-
senseofunity129
0
110
LIFF CLIとngrokを使ったLIFF/LINEミニアプリのお手軽実機確認
diggymo
0
230
Findy Freelance 利用シーン別AI活用例
ness
0
310
Claude Codeが働くAI中心の業務システム構築の挑戦―AIエージェント中心の働き方を目指して
os1ma
9
1.5k
僕たちが「開発しやすさ」を求め 模索し続けたアーキテクチャ #アーキテクチャ勉強会_findy
bengo4com
0
2k
ホリスティックテスティングの右側も大切にする 〜2つの[はか]る〜 / Holistic Testing: Right Side Matters
nihonbuson
PRO
0
590
Strands Agents & Bedrock AgentCoreを1分でおさらい
minorun365
PRO
6
240
S3 Glacier のデータを Athena からクエリしようとしたらどうなるのか/try-to-query-s3-glacier-from-athena
emiki
0
190
解消したはずが…技術と人間のエラーが交錯する恐怖体験
lamaglama39
0
190
LLM 機能を支える Langfuse / ClickHouse のサーバレス化
yuu26
5
430
✨敗北解法コレクション✨〜Expertだった頃に足りなかった知識と技術〜
nanachi
1
540
Featured
See All Featured
Making the Leap to Tech Lead
cromwellryan
134
9.5k
Refactoring Trust on Your Teams (GOTO; Chicago 2020)
rmw
34
3.1k
Bash Introduction
62gerente
614
210k
How to Create Impact in a Changing Tech Landscape [PerfNow 2023]
tammyeverts
53
2.9k
Building a Modern Day E-commerce SEO Strategy
aleyda
43
7.4k
Responsive Adventures: Dirty Tricks From The Dark Corners of Front-End
smashingmag
251
21k
Agile that works and the tools we love
rasmusluckow
329
21k
Side Projects
sachag
455
43k
Build The Right Thing And Hit Your Dates
maggiecrowley
37
2.8k
実際に使うSQLの書き方 徹底解説 / pgcon21j-tutorial
soudai
PRO
182
54k
Sharpening the Axe: The Primacy of Toolmaking
bcantrill
44
2.4k
Building Flexible Design Systems
yeseniaperezcruz
328
39k
Transcript
形式手法特論 位相空間としての 並行プログラミング #kernelvm チェシャ猫 (@y_taka_23) Kernel/VM 探検隊@東京 No.18 (9th
Aug. 2025)
本日お話ししたいこと • 並行システムの仕様をテストしたい ◦ 仕様にはいくつかの類型があり、特性が異なる ◦ しかしそれを自然言語のまま扱うのは難しい • 仕様や実装をシステム状態の列として捉える ◦
状態遷移を位相空間の言葉で特徴づけできる ◦ 数学的な操作が可能になる
夏休みといえば排他制御
スレッドが一つの場合 赤:スレッドが排他区間内 Enter / Leave を繰り返す
スレッドが二つの場合 左側が赤:スレッド 1 が区間内 右側が赤:スレッド 2 が区間内 1 と 2
が独立に Enter / Leave 排他性違反
排他制御の仕様 • いくつかの仕様が考えられる ◦ 二つのスレッドが同時に排他区間に入らない ◦ スレッド 1 も 2
も、いつかは排他区間に入れる ◦ スレッド 1 と 2 が、必ず交互に排他区間に入る • それぞれの仕様はなんとなくタイプが異なる ◦ 本質的な違いや相互関係について分析したい
安全性と活性 • 安全性 (safety) ◦ 「悪いことが決して起こらない」タイプの仕様 ◦ 例:二つのスレッドが同時に排他区間に入らない • 活性
(liveness) ◦ 「いつか必ず良いことが起こる」タイプの仕様 ◦ 例:スレッド 1 も 2 も、いつか排他区間に入れる
振る舞い:状態からなる無限列全体 • ランダムなパターン全体 • 実際の挙動としてあり得ない すべて白 全て赤 交互に などの列も「すべて」含む …
… … 振る舞い
• 仕様を表すパターン全体 • 例えば排他性の場合なら i違を含まない すべて白 全て赤 などの列が含まれる 仕様:条件を満たす無限列全体 …
仕様 仕様 … 振る舞い
実装:実際に発生する無限列全体 • 実装を表すパターン全体 • プログラムを実行した時に 実際に発生しうる すべて白 全て赤 などの列が含まれる …
… 仕様 仕様 実装 振る舞い
違 反 違反:実装に属すが仕様に属さない … … … … … 1: 2:
3: 4: 5: 1 2 3 4 5 仕様 実装 振る舞い
仕様そのものに対するエンジニアリング
仕様を集合で表現するメリット • 仕様の強弱や包含関係が比較できる ◦ 広い集合はゆるい条件、狭い集合は厳しい条件 • 部分集合として、仕様のモジュール化や合成ができる • 仕様の各モジュールに対しテストを分割統治できる ◦
P ∪ Q なら、P と Q をテストしてどちらか Pass ◦ P ∩ Q なら、P と Q をテストして両方 Pass
さらに集合に構造を追加
位相空間 Topology Space
を全部解説すると半期 15 コマ必要なので 今回は必要なワードだけ取り上げる
閉集合 集合 A が「A に属さない任意の点を選んだとき、 その十分近くにある点はやはり A に属さない」という条件を 満たす場合、A は閉集合
(closed set) であるという 定義
閉集合の例、閉集合でない例 • A = { x : 0 ≤ x
≤ 1 } は閉集合 ◦ 0 未満の x の十分近くは 0 未満 • A = { x : 0 < x < 1 } は閉集合ではない ◦ 0 自身は A に属さないが、 0 のどんなに近くの点を考えても プラス側が A にかぶってしまう 0 0 - ε 0 + ε A 0 x - ε A x - ε x
稠密集合 集合 A が「A 以外も含む全体から任意の点を選んだとき、 その十分近くに必ず A に属す点が存在する」という条件を 満たす場合、A は稠密集合
(dence set) であるという 定義
稠密集合の例 • A = { x : x は有理数 }
は稠密集合 ◦ どんな実数を取ってきても、小数点 N 桁までの 近似値を考えれば、どこまでも近い有理数が存在 • A = { x : x は i / 2^j の形の分数 } は稠密集合 ◦ 有理数の中でも限られた形の分数しか取れないが、 分母 2^j はどこまでも細かく刻める
「近さ」を用いて定義されている
振る舞い同士の距離 • 状態列が 2 つあるとき、その「近さ」が定義できる ◦ 冒頭部分が長く一致するほど「近い」とする ◦ N 個目まで一致するなら「レベル
N」の近さ • 数直線上の通常の距離と同じような扱いができる ◦ 数学的にいえば位相空間(特に距離空間)になる ◦ 閉集合や稠密集合を考えることが可能
振る舞い同士の距離の例 … … … … … 1: 2: 3: 4:
5: • 4-5 はこの中で最も近い (2 個目まで一致) • 1-4 や 1-5 は次点で近い (1 個目まで一致) • 2 や 3 はどれとも遠い (1 個目で既に不一致)
安全性(位相版) • 安全性 (safety) ◦ 閉集合で表されるタイプの仕様 ◦ 例:無限列のどこにも違反が現れない • 違反の例として、N
個目で両側が現れる列を取る ◦ その列と「レベル N 以上近い列」は全部両側を持つ ◦ 違反に十分近い点は違反:閉集合の特徴
活性(位相版) • 活性 (liveness) ◦ 稠密集合で表されるタイプの仕様 ◦ 例:無限列のどこかで最低一回左側と右側が現れる • 任意の列と、十分大きい
N を選ぶ ◦ 列の N + 1 個目から先を交互に排 で置き換え ◦ 元の列の「レベル N 近似」が可能:稠密集合の特徴 …
そういえば残る三つ目の仕様の例は?
一般の仕様に対する分析 • 実際の仕様は普通、純粋な安全性でも活性でもない • 例:右側と左側が両側を挟みつつ交互に出現し続ける ◦ 安全性でない:永遠に両側が続く場合も違反 ◦ 活性でない:両側から 両側が出たら即違反 •
一般的な仕様をうまく扱う方法が欲しい ◦ 単純なモジュールの組み合わせに還元したい
安全性 - 活性分解定理 任意の仕様 P が与えられたとき、ある安全性 S と活性 L が
存在して P = S ∩ L という分解が成り立つ 定理 (Alpern-Schneider, 1985) • 任意の仕様を安全性と活性に分解できる広範な主張 • 定式化の勝利で、位相空間の初歩のみで証明可能 https://doi.org/10.1016/0020-0190(85)90056-0
本日のまとめ • 仕様は状態列の集合とみなせる ◦ 仕様から実装がはみ出さないことを検証すればよい ◦ 仕様自体を分析や操作の対象にできる • 仕様の特徴は、位相空間を用いて定式化できる ◦
安全性とは閉集合、活性とは稠密集合 ◦ 任意の仕様は、安全性と活性の共通部分になる
It’s Only Logical to Go Topological! Presented By チェシャ猫 (@y_taka_23)