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
1.6k
形式手法特論:位相空間としての並行プログラミング #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
3.2k
問 1:以下のコンパイラを証明せよ(予告編) #kernelvm / Kernel VM Study Kansai 11th
ytaka23
3
850
AWS のポリシー言語 Cedar を活用した高速かつスケーラブルな認可技術の探求 #phperkaigi / PHPerKaigi 2025
ytaka23
11
2.7k
NilAway による静的解析で「10 億ドル」を節約する #kyotogo / Kyoto Go 56th
ytaka23
4
710
形式手法の 10 メートル手前 #kernelvm / Kernel VM Study Hokuriku Part 7
ytaka23
7
1.4k
普通の Web エンジニアのための様相論理入門 #yapcjapan / YAPC Hakodate 2024
ytaka23
11
3.3k
kcp: Kubernetes APIs Are All You Need #techfeed_live / TechFeed Experts Night 28th
ytaka23
1
540
サーバーレスアーキテクチャの数理的理解と分析 #devsumi / Developers Summit 2023 Summer
ytaka23
9
5.5k
形式手法による分散システムの検証 〜S3 の一貫性モデルを例として〜 #ourdevday2023 / Our DevDay 2023
ytaka23
2
1.5k
Other Decks in Technology
See All in Technology
キャリアを支え組織力を高める「多層型ふりかえり」 / 20250821 Kazuki Mori
shift_evolve
PRO
2
300
Go で言うところのアレは TypeScript で言うとコレ / Kyoto.なんか #7
susisu
5
1.4k
OpenAPIから画面生成に挑戦した話
koinunopochi
0
150
Goss: Faiss向けの新しい本番環境対応 Goバインディング #coefl_go_jp
bengo4com
0
1.4k
JOAI発表資料 @ 関東kaggler会
joai_committee
1
260
株式会社ARAV 採用案内
maqui
0
340
Product Management Conference -AI時代に進化するPdM-
kojima111
0
220
Webアクセシビリティ入門
recruitengineers
PRO
1
220
Preferred Networks (PFN) とLLM Post-Training チームの紹介 / 第4回 関東Kaggler会 スポンサーセッション
pfn
PRO
1
180
あなたの知らない OneDrive
murachiakira
0
230
実践データベース設計 ①データベース設計概論
recruitengineers
PRO
2
190
Gaze-LLE: Gaze Target Estimation via Large-Scale Learned Encoders
kzykmyzw
0
310
Featured
See All Featured
Bash Introduction
62gerente
614
210k
What's in a price? How to price your products and services
michaelherold
246
12k
Docker and Python
trallard
45
3.5k
A designer walks into a library…
pauljervisheath
207
24k
Building Flexible Design Systems
yeseniaperezcruz
328
39k
Responsive Adventures: Dirty Tricks From The Dark Corners of Front-End
smashingmag
251
21k
A better future with KSS
kneath
239
17k
Save Time (by Creating Custom Rails Generators)
garrettdimon
PRO
32
1.4k
Testing 201, or: Great Expectations
jmmastey
45
7.6k
Music & Morning Musume
bryan
46
6.7k
[RailsConf 2023 Opening Keynote] The Magic of Rails
eileencodes
30
9.6k
Building Adaptive Systems
keathley
43
2.7k
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 は稠密集合
(dense 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)