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.8k
形式手法特論:位相空間としての並行プログラミング #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.5k
問 1:以下のコンパイラを証明せよ(予告編) #kernelvm / Kernel VM Study Kansai 11th
ytaka23
3
890
AWS のポリシー言語 Cedar を活用した高速かつスケーラブルな認可技術の探求 #phperkaigi / PHPerKaigi 2025
ytaka23
12
3k
NilAway による静的解析で「10 億ドル」を節約する #kyotogo / Kyoto Go 56th
ytaka23
7
840
形式手法の 10 メートル手前 #kernelvm / Kernel VM Study Hokuriku Part 7
ytaka23
7
1.4k
普通の Web エンジニアのための様相論理入門 #yapcjapan / YAPC Hakodate 2024
ytaka23
12
3.4k
kcp: Kubernetes APIs Are All You Need #techfeed_live / TechFeed Experts Night 28th
ytaka23
1
570
サーバーレスアーキテクチャの数理的理解と分析 #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
動画データのポテンシャルを引き出す! Databricks と AI活用への奮闘記(現在進行形)
databricksjapan
0
150
M5製品で作るポン置きセルラー対応カメラ
sayacom
0
160
E2Eテスト設計_自動化のリアル___Playwrightでの実践とMCPの試み__AIによるテスト観点作成_.pdf
findy_eventslides
1
420
社内報はAIにやらせよう / Let AI handle the company newsletter
saka2jp
3
290
How to achieve interoperable digital identity across Asian countries
fujie
0
120
Goに育てられ開発者向けセキュリティ事業を立ち上げた僕が今向き合う、AI × セキュリティの最前線 / Go Conference 2025
flatt_security
0
350
生成AIを活用したZennの取り組み事例
ryosukeigarashi
0
210
AIAgentの限界を超え、 現場を動かすWorkflowAgentの設計と実践
miyatakoji
0
140
Green Tea Garbage Collector の今
zchee
PRO
2
390
AWSにおけるTrend Vision Oneの効果について
shimak
0
130
OCI Network Firewall 概要
oracle4engineer
PRO
1
7.8k
業務自動化プラットフォーム Google Agentspace に入門してみる #devio2025
maroon1st
0
190
Featured
See All Featured
Designing for Performance
lara
610
69k
Navigating Team Friction
lara
189
15k
CSS Pre-Processors: Stylus, Less & Sass
bermonpainter
358
30k
Writing Fast Ruby
sferik
629
62k
Testing 201, or: Great Expectations
jmmastey
45
7.7k
Building Better People: How to give real-time feedback that sticks.
wjessup
368
20k
Facilitating Awesome Meetings
lara
56
6.6k
Build your cross-platform service in a week with App Engine
jlugia
232
18k
Site-Speed That Sticks
csswizardry
11
880
A Modern Web Designer's Workflow
chriscoyier
697
190k
Fashionably flexible responsive web design (full day workshop)
malarkey
407
66k
Making the Leap to Tech Lead
cromwellryan
135
9.5k
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)