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.9k
形式手法特論:位相空間としての並行プログラミング #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
4.6k
問 1:以下のコンパイラを証明せよ(予告編) #kernelvm / Kernel VM Study Kansai 11th
ytaka23
3
900
AWS のポリシー言語 Cedar を活用した高速かつスケーラブルな認可技術の探求 #phperkaigi / PHPerKaigi 2025
ytaka23
12
3.2k
NilAway による静的解析で「10 億ドル」を節約する #kyotogo / Kyoto Go 56th
ytaka23
7
850
形式手法の 10 メートル手前 #kernelvm / Kernel VM Study Hokuriku Part 7
ytaka23
7
1.4k
普通の Web エンジニアのための様相論理入門 #yapcjapan / YAPC Hakodate 2024
ytaka23
12
3.5k
kcp: Kubernetes APIs Are All You Need #techfeed_live / TechFeed Experts Night 28th
ytaka23
1
590
サーバーレスアーキテクチャの数理的理解と分析 #devsumi / Developers Summit 2023 Summer
ytaka23
9
5.6k
形式手法による分散システムの検証 〜S3 の一貫性モデルを例として〜 #ourdevday2023 / Our DevDay 2023
ytaka23
2
1.5k
Other Decks in Technology
See All in Technology
もう外には出ない。より快適なフルリモート環境を目指して
mottyzzz
13
11k
AIとともに歩んでいくデザイナーの役割の変化
lycorptech_jp
PRO
0
890
激動の時代を爆速リチーミングで乗り越えろ
sansantech
PRO
1
110
OPENLOGI Company Profile for engineer
hr01
1
45k
SRE × マネジメントレイヤーが挑戦した組織・会社のオブザーバビリティ改革 ― ビジネス価値と信頼性を両立するリアルな挑戦
coconala_engineer
0
260
AIプロダクトのプロンプト実践テクニック / Practical Techniques for AI Product Prompts
saka2jp
0
110
【SORACOM UG Explorer 2025】さらなる10年へ ~ SORACOM MVC 発表
soracom
PRO
0
150
オブザーバビリティと育てた ID管理・認証認可基盤の歩み / The Journey of an ID Management, Authentication, and Authorization Platform Nurtured with Observability
kaminashi
1
730
20251027_findyさん_音声エージェントLT
almondo_event
2
440
AI駆動で進める依存ライブラリ更新 ─ Vue プロジェクトの品質向上と開発スピード改善の実践録
sayn0
1
320
あなたの知らない Linuxカーネル脆弱性の世界
recruitengineers
PRO
3
160
ViteとTypeScriptのProject Referencesで 大規模モノレポのUIカタログのリリースサイクルを高速化する
shuta13
3
210
Featured
See All Featured
GraphQLの誤解/rethinking-graphql
sonatard
73
11k
Gamification - CAS2011
davidbonilla
81
5.5k
Building a Scalable Design System with Sketch
lauravandoore
463
33k
Save Time (by Creating Custom Rails Generators)
garrettdimon
PRO
32
1.7k
Documentation Writing (for coders)
carmenintech
75
5.1k
The Invisible Side of Design
smashingmag
302
51k
Navigating Team Friction
lara
190
15k
Reflections from 52 weeks, 52 projects
jeffersonlam
353
21k
Keith and Marios Guide to Fast Websites
keithpitt
411
23k
Connecting the Dots Between Site Speed, User Experience & Your Business [WebExpo 2025]
tammyeverts
10
620
"I'm Feeling Lucky" - Building Great Search Experiences for Today's Users (#IAC19)
danielanewman
230
22k
Creating an realtime collaboration tool: Agile Flush - .NET Oxford
marcduiker
34
2.3k
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)