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
形式手法の 10 メートル手前 #kernelvm / Kernel VM Study Hok...
Search
y_taka_23
November 09, 2024
Technology
6
1.2k
形式手法の 10 メートル手前 #kernelvm / Kernel VM Study Hokuriku Part 7
Kernel / VM 探検隊 @ 北陸 Part 7 で使用したスライドです。
y_taka_23
November 09, 2024
Tweet
Share
More Decks by y_taka_23
See All by y_taka_23
AWS のポリシー言語 Cedar を活用した高速かつスケーラブルな認可技術の探求 #phperkaigi / PHPerKaigi 2025
ytaka23
7
1.5k
NilAway による静的解析で「10 億ドル」を節約する #kyotogo / Kyoto Go 56th
ytaka23
4
610
普通の Web エンジニアのための様相論理入門 #yapcjapan / YAPC Hakodate 2024
ytaka23
9
2.6k
kcp: Kubernetes APIs Are All You Need #techfeed_live / TechFeed Experts Night 28th
ytaka23
1
400
サーバーレスアーキテクチャの数理的理解と分析 #devsumi / Developers Summit 2023 Summer
ytaka23
9
5.2k
形式手法による分散システムの検証 〜S3 の一貫性モデルを例として〜 #ourdevday2023 / Our DevDay 2023
ytaka23
2
1.4k
Amazon S3 の一貫性モデル超入門 #ハードル激低LT大会 / Low-hurdle LT Meetup 2nd
ytaka23
3
2.2k
謎は全て解けた!安楽椅子探偵に捧げる AWS ネットワーク分析入門 #CNDT2022 / CloudNative Days Tokyo 2022
ytaka23
2
4k
サーバーレスは操作的意味論の夢を見るか? #AWSDevDay / AWS Dev Day 2022 Japan
ytaka23
4
6.9k
Other Decks in Technology
See All in Technology
ペアプログラミングにQAが加わった!職能を超えたモブプログラミングの事例と学び
tonionagauzzi
1
150
Amazon GuardDuty Malware Protection for Amazon S3を使おう
ryder472
2
110
Proxmox VE超入門 〜 無料で作れるご自宅仮想化プラットフォームブックマークする
devops_vtj
0
160
AIエージェント完全に理解した
segavvy
4
270
Javaの新しめの機能を知ったかぶれるようになる話 #kanjava
irof
3
4.9k
非エンジニアにも伝えるメールセキュリティ / Email security for non-engineers
ykanoh
13
4k
3/26 クラウド食堂LT #2 GenU案件を通して学んだ教訓 登壇資料
ymae
1
210
20250328_RubyKaigiで出会い鯛_____RubyKaigiから始まったはじめてのOSSコントリビュート.pdf
mterada1228
0
130
Compose MultiplatformにおけるiOSネイティブ実装のベストプラクティス
enomotok
1
210
SaaSプロダクト開発におけるバグの早期検出のためのAcceptance testの取り組み
kworkdev
PRO
0
460
Explainable Software Engineering in the Public Sector
avandeursen
0
370
AI・LLM事業部のSREとタスクの自動運転
shinyorke
PRO
0
300
Featured
See All Featured
Optimizing for Happiness
mojombo
377
70k
Mobile First: as difficult as doing things right
swwweet
223
9.5k
Build your cross-platform service in a week with App Engine
jlugia
229
18k
How STYLIGHT went responsive
nonsquared
99
5.4k
Cheating the UX When There Is Nothing More to Optimize - PixelPioneers
stephaniewalter
280
13k
GraphQLの誤解/rethinking-graphql
sonatard
70
10k
Designing for Performance
lara
606
69k
Raft: Consensus for Rubyists
vanstee
137
6.8k
What's in a price? How to price your products and services
michaelherold
245
12k
Gamification - CAS2011
davidbonilla
81
5.2k
Being A Developer After 40
akosma
90
590k
Building a Scalable Design System with Sketch
lauravandoore
462
33k
Transcript
形式手法の 10 メートル手前 チェシャ猫 (@y_taka_23) Kernel / VM 探検隊 @
北陸 Part 7 9th Nov. 2024
前回(8 月)の Kernel / VM 探検隊
r1ru さん (@ri5255) Rust で自作モデル検査器 https://speakerdeck.com/riru/symbolic-model-checker-from-scratch-in-rust
かなり 本格的な 解説
偶然居合わせたチェシャ猫 「参考文献の著者です」 https://speakerdeck.com/riru/symbolic-model-checker-from-scratch-in-rust?slide=46
参考文献の その「先」へ
しかし得てして 難しめ
「先」だけでなく 「手前」についても
勢いと割り切りで
手前側 10 メートルを キーワード 10 個で 雰囲気解説
仕様を自動的に検証 https://speakerdeck.com/riru/symbolic-model-checker-from-scratch-in-rust?slide=3
【残り 10 m】 単体テスト
0 を入れると 42 が返る getAnswerOfEverything(0) == 42
人間は 「入力と出力の対応」 を記述
バグをピンポイントに 引き当てる必要性
【残り 9 m】 プロパティベーステスト
テストケースは ランダム生成
人間は 「関数の性質」 を記述
エンコードしてから デコードすると元に戻る decode(encode(x)) == x
最適化の前後で 結果が変わらない naiveImpl(x) == optimizedImpl(x)
これで確実に テスト可能?
近頃はそうでもない
【残り 8 m】 非決定性
マルチスレッドの タイミング系バグ
分散システムの サーバ故障
ネットワーク 通信の遅延
コントロール不能
再現性のあるテスト が書けない
ならば何を テストする?
【残り 7 m】 グラフ構造
二つのスレッド A と B A: 0, B: 0
A が 1 step 動いた世界線 A: 0, B: 0 A:
1, B: 0
B が 1 step 動いた世界線 A: 0, B: 0 A:
0, B: 1
全パターン網羅すると グラフ構造が現れる A: 0, B: 0 A: 1, B: 0
A: 0, B: 1 A: 2, B: 0 A: 1, B: 1 A: 0, B: 2 A: 3, B: 0 A: 2, B: 1 A: 1, B: 2 A: 0, B: 3
【残り 6 m】 時相論理
グラフを見ると 「時間経過」 が表現できる
どう辿っても 「ずっと」成立
どう辿っても 「いずれ必ず」成立
【残り 5 m】 安全性と活性
悪いことが 「ずっと起こらない」 安全性
良いことが 「いずれ起こる」 活性
両方合わせて仕様
なぜ両方?
何もしないシステムは 安全だが無意味
グラフに対する テストフレームワーク が欲しい
【残り 4 m】 モデル検査
仕様を グラフの性質 として表現
グラフアルゴリズムで 自動的に検査可能
アルゴリズムの詳細は r1ru さんのスライド参照 https://speakerdeck.com/riru/symbolic-model-checker-from-scratch-in-rust
【残り 3 m】 形式手法
数学チックな 検査手法の総称(雑)
モデル検査以外にも 定理証明など
そうそう
「型」も形式手法です
【残り 2 m】 モデル検査ツール
TLA+ https://lamport.azurewebsites.net/tla/tla.html
Alloy https://alloytools.org/
SPIN https://spinroot.com/spin/whatispin.html
【残り 1 m】 採用事例
TLA+ 大人気
AWS で使ってる https://www.amazon.science/publications/how-amazon-web-services-uses-formal-methods
MS Azure でも使ってる https://github.com/Azure/azure-cosmos-tla
難しそう?
たかが 10 メートル
冬休みの自由研究に
自分へのクリスマス プレゼントに
お歳暮に
モデル検査
形式手法
おすすめです
【残り 0 m】 Presented by チェシャ猫 (@y_taka_23)