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
NilAway による静的解析で「10 億ドル」を節約する #kyotogo / Kyoto ...
Search
y_taka_23
December 14, 2024
Technology
4
680
NilAway による静的解析で「10 億ドル」を節約する #kyotogo / Kyoto Go 56th
Kyoto.go #56 オフライン忘年 LT 会で使用したスライドです。
y_taka_23
December 14, 2024
Tweet
Share
More Decks by y_taka_23
See All by y_taka_23
AWS と定理証明 〜ポリシー言語 Cedar 開発の舞台裏〜 #fp_matsuri / FP Matsuri 2025
ytaka23
10
2.9k
問 1:以下のコンパイラを証明せよ(予告編) #kernelvm / Kernel VM Study Kansai 11th
ytaka23
3
790
AWS のポリシー言語 Cedar を活用した高速かつスケーラブルな認可技術の探求 #phperkaigi / PHPerKaigi 2025
ytaka23
10
2.5k
形式手法の 10 メートル手前 #kernelvm / Kernel VM Study Hokuriku Part 7
ytaka23
7
1.3k
普通の Web エンジニアのための様相論理入門 #yapcjapan / YAPC Hakodate 2024
ytaka23
11
3.1k
kcp: Kubernetes APIs Are All You Need #techfeed_live / TechFeed Experts Night 28th
ytaka23
1
490
サーバーレスアーキテクチャの数理的理解と分析 #devsumi / Developers Summit 2023 Summer
ytaka23
9
5.4k
形式手法による分散システムの検証 〜S3 の一貫性モデルを例として〜 #ourdevday2023 / Our DevDay 2023
ytaka23
2
1.4k
Amazon S3 の一貫性モデル超入門 #ハードル激低LT大会 / Low-hurdle LT Meetup 2nd
ytaka23
3
2.3k
Other Decks in Technology
See All in Technology
2025-07-25 NOT A HOTEL TECH TALK ━ スマートホーム開発の最前線 ━ SOFTWARE
wakinchan
0
120
「AI駆動開発」のボトルネック『言語化』を効率化するには
taniiicom
1
100
Building GoReleaser - from shell script to paid product
caarlos0
0
270
ML Pipelineの開発と運用を OpenTelemetryで繋ぐ @ OpenTelemetry Meetup 2025-07
getty708
0
240
Snowflake のアーキテクチャは本当に筋がよかったのか / Data Engineering Study #30
indigo13love
0
250
メモ整理が苦手な者による頑張らないObsidian活用術
optim
0
120
Semantic Machine Intelligence for Vision, Language, and Actions
keio_smilab
PRO
2
390
低レイヤソフトウェア技術者が YouTuberとして食っていこうとした話
sat
PRO
7
5.8k
Ktor + Google Cloud Tasks/PubSub におけるOTel Messaging計装の実践
sansantech
PRO
1
270
株式会社島津製作所_研究開発(集団協業と知的生産)の現場を支える、OSS知識基盤システムの導入
akahane92
1
1.2k
少人数でも回る! DevinとPlaybookで支える運用改善
ishikawa_pro
1
220
DatabricksのOLTPデータベース『Lakebase』に詳しくなろう!
inoutk
0
110
Featured
See All Featured
[Rails World 2023 - Day 1 Closing Keynote] - The Magic of Rails
eileencodes
35
2.5k
CoffeeScript is Beautiful & I Never Want to Write Plain JavaScript Again
sstephenson
161
15k
Java REST API Framework Comparison - PWX 2021
mraible
31
8.7k
Embracing the Ebb and Flow
colly
86
4.8k
It's Worth the Effort
3n
185
28k
10 Git Anti Patterns You Should be Aware of
lemiorhan
PRO
656
60k
Design and Strategy: How to Deal with People Who Don’t "Get" Design
morganepeng
130
19k
XXLCSS - How to scale CSS and keep your sanity
sugarenia
248
1.3M
Responsive Adventures: Dirty Tricks From The Dark Corners of Front-End
smashingmag
251
21k
Navigating Team Friction
lara
187
15k
Improving Core Web Vitals using Speculation Rules API
sergeychernyshev
18
1k
Art, The Web, and Tiny UX
lynnandtonic
301
21k
Transcript
#kyotogo NilAway による静的解析で 「10 億ドル」を節約する チェシャ猫 (@y_taka_23) Kyoto.go #56 オフライン忘年
LT 大会 (15th Dec. 2024)
#kyotogo 第 1 問(初級)
#kyotogo 何が起こる? 1. 改行のみ出力して正常終了 2. 何も出力せず正常終了 3. panic になる
#kyotogo 何が起こる? 1. 改行のみ出力して正常終了 2. 何も出力せず正常終了 3. panic になる【正解】
#kyotogo 第 2 問(中級)
#kyotogo 何が起こる? 1. 改行のみ出力して正常終了 2. 何も出力せず正常終了 3. panic になる
#kyotogo 何が起こる? 1. 改行のみ出力して正常終了 2. 何も出力せず正常終了 3. panic になる【正解】
#kyotogo 第 3 問(上級)
#kyotogo あなたは nil 判定をどうやって解いた?
#kyotogo 無効な参照によるエラー • 10 億ドルの過ち(The Billion Dollar Mistake) ◦ null
を「発明」した Hoare による 2009 年の後悔の言 ◦ Dijkstra 「独身者が全員一人の null と重婚した状態」 • nil 参照は実行時エラーとしてはかなり厄介 ◦ あらゆる型に対し nil チェックが必要になってしまう ◦ 原因と結果がコード的にも時間的にも遠く離れがち 参考:https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare/
#kyotogo 実行前に静的に nil 参照を検出したい
#kyotogo NilAway by Uber https://github.com/uber-go/nilaway
#kyotogo NilAway の特徴 • ソースコードから静的に nil エラーを発見 ◦ 関数やパッケージを跨いだエラーが検知可能 ◦
nil になり得る具体的な原因をメッセージとして表示 • go/analysis パッケージを使用 ◦ 内部は複数の Analyzer でモジュール化され並列動作 ◦ golangci-lint や bazel+nogo などのツールから呼び出し可能 参考:静的解析のモジュール化(https://zenn.dev/tenntenn/books/d168faebb1a739/viewer/9d590e)
#kyotogo NilAway による検査結果 • ソースコードの nil flow を解析 ◦ foo()
が nil リテラルを返却(10 行目) ◦ foo() を参照(6 行目)
#kyotogo nil flow による因果推論 • nil の発生と参照の因果関係を辺としたグラフを構築 ◦ 発生:nil リテラル、var
宣言、関数の引数など ◦ 参照:デリファレンス、フィールドアクセスなど • 各ノードに対して「nil であり得るか」をマーク ◦ 発生側を true、参照側を false として伝播・確定させていく ◦ true かつ false の矛盾したノードが現れたら nil エラー
#kyotogo *foo(x, bar()) bar() foo の x foo の y
foo(x, y) main の x bar の nil リテラル var 宣言 引数 return 引数 デリファレンス return if x == nil
#kyotogo *foo(x, bar()) bar() foo の x foo の y
foo(x, y) main の x bar の nil リテラル var 宣言 引数 return 引数 デリファレンス return if x == nil 赤は nil 確定 緑は nil 不可能 黒は矛盾
#kyotogo *foo(x, bar()) bar() foo の x foo の y
foo(x, y) main の x bar の nil リテラル var 宣言 引数 return 引数 デリファレンス return if x == nil 赤は nil 確定 緑は nil 不可能 黒は両方(矛盾)
#kyotogo というかそれは自明では?
#kyotogo 冒頭の第 3 問への回答 • ちゃんとした形式化の複雑さ ◦ 人間も基本的には因果関係を辿って nil を発見
◦ 意外なトリックがあるという感じではない ◦ しかしアルゴリズムに落とし込むとなると割と複雑 • 計算機科学の裏付けによるスケール可能性 ◦ 因果グラフ推論は 2-SAT 問題とみなせ、線形時間で判定可能
#kyotogo まとめ • nil 参照は厄介なタイプの実行時エラー ◦ 考案者 Hoare 自身も後に「10 億ドルの過ち」と認める
• NilAway により静的に解析が可能 ◦ nil の可能性を制約としてグラフ上で伝播させ矛盾を検出 • 人間が頭の中で行う「普通にわかる」の形式化 ◦ 意外と複雑な処理だが、厳密に記述できればスケール可能
#kyotogo Save the Billion Dollars by NilAway! Presented by チェシャ猫
(@y_taka_23)