$30 off During Our Annual Pro Sale. View Details »
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
950
形式手法の 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
普通の Web エンジニアのための様相論理入門 #yapcjapan / YAPC Hakodate 2024
ytaka23
7
2.1k
kcp: Kubernetes APIs Are All You Need #techfeed_live / TechFeed Experts Night 28th
ytaka23
1
300
サーバーレスアーキテクチャの数理的理解と分析 #devsumi / Developers Summit 2023 Summer
ytaka23
9
4.9k
形式手法による分散システムの検証 〜S3 の一貫性モデルを例として〜 #ourdevday2023 / Our DevDay 2023
ytaka23
2
1.3k
Amazon S3 の一貫性モデル超入門 #ハードル激低LT大会 / Low-hurdle LT Meetup 2nd
ytaka23
3
2.1k
謎は全て解けた!安楽椅子探偵に捧げる AWS ネットワーク分析入門 #CNDT2022 / CloudNative Days Tokyo 2022
ytaka23
2
3.6k
サーバーレスは操作的意味論の夢を見るか? #AWSDevDay / AWS Dev Day 2022 Japan
ytaka23
4
6.5k
賢く「振り分ける」ための Topology Aware Hints #k8sjp / Kubernetes Meetup Tokyo 52nd
ytaka23
4
3.3k
ネットワークはなぜつながらないのか 〜インフラの意味論的検査を目指して〜 #AWSDevDay / AWS Dev Day Online Japan 2021
ytaka23
4
8k
Other Decks in Technology
See All in Technology
Kaggleふりかえり会〜LLM 20 Questions & ISIC 2024
recruitengineers
PRO
2
110
【CNDW2024】SIerで200人クラウドネイティブのファンを増やした話
yuta1979
1
310
乗っ取れKubernetes!!~リスクから学ぶKubernetesセキュリティの考え方~/k8s-risk-and-security
mochizuki875
3
450
Empowering Customer Decisions with Elasticsearch: From Search to Answer Generation
hinatades
PRO
0
210
ARRが3年で10倍になったプロダクト開発とAI活用の軌跡
akiroom
0
210
ミスが許されない領域にAIを溶け込ませる プロダクトマネジメントの裏側
t01062sy
0
650
Reliability Engineering at Studist
katsuhisa91
PRO
0
100
GeminiとUnityで実現するインタラクティブアート
hokkey621
0
410
データカタログを自作したけど 運用しなかった話@Findy Lunch LT「データカタログ 事例から学ぶメタデータ管理の実態」
ryo_suzuki
2
610
[GDG DevFest Bangkok 2024] - The Future of Retail E-commerce with Gemini AI
punsiriboo
0
240
お悩みハンドブック紹介資料
grafferhandbook
0
360
【Oracle Cloud ウェビナー】【入門&再入門】はじめてのOracle Cloud Infrastructure [+最新情報]
oracle4engineer
PRO
2
250
Featured
See All Featured
Become a Pro
speakerdeck
PRO
25
5k
Statistics for Hackers
jakevdp
796
220k
Evolution of real-time – Irina Nazarova, EuRuKo, 2024
irinanazarova
4
410
What's new in Ruby 2.0
geeforr
343
31k
Templates, Plugins, & Blocks: Oh My! Creating the theme that thinks of everything
marktimemedia
27
2.1k
RailsConf 2023
tenderlove
29
920
Practical Tips for Bootstrapping Information Extraction Pipelines
honnibal
PRO
10
770
Agile that works and the tools we love
rasmusluckow
327
21k
Site-Speed That Sticks
csswizardry
0
120
Code Reviewing Like a Champion
maltzj
520
39k
Fight the Zombie Pattern Library - RWD Summit 2016
marcelosomers
232
17k
Raft: Consensus for Rubyists
vanstee
136
6.7k
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)