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
740
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
形式手法特論:位相空間としての並行プログラミング #kernelvm / Kernel VM Study Tokyo 18th
ytaka23
3
1.8k
AWS と定理証明 〜ポリシー言語 Cedar 開発の舞台裏〜 #fp_matsuri / FP Matsuri 2025
ytaka23
10
4.3k
問 1:以下のコンパイラを証明せよ(予告編) #kernelvm / Kernel VM Study Kansai 11th
ytaka23
3
860
AWS のポリシー言語 Cedar を活用した高速かつスケーラブルな認可技術の探求 #phperkaigi / PHPerKaigi 2025
ytaka23
11
2.9k
形式手法の 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
「何となくテストする」を卒業するためにプロダクトが動く仕組みを理解しよう
kawabeaver
0
410
dbt開発 with Claude Codeのためのガードレール設計
10xinc
2
1.2k
roppongirb_20250911
igaiga
1
240
Generative AI Japan 第一回生成AI実践研究会「AI駆動開発の現在地──ブレイクスルーの鍵を握るのはデータ領域」
shisyu_gaku
0
270
Evolución del razonamiento matemático de GPT-4.1 a GPT-5 - Data Aventura Summit 2025 & VSCode DevDays
lauchacarro
0
190
Rustから学ぶ 非同期処理の仕組み
skanehira
1
140
ZOZOマッチのアーキテクチャと技術構成
zozotech
PRO
4
1.6k
新アイテムをどう使っていくか?みんなであーだこーだ言ってみよう / 20250911-rpi-jam-tokyo
akkiesoft
0
270
Snowflake Intelligenceにはこうやって立ち向かう!クラシルが考えるAI Readyなデータ基盤と活用のためのDataOps
gappy50
0
240
BPaaSにおける人と協働する前提のAIエージェント-AWS登壇資料
kentarofujii
0
140
Webブラウザ向け動画配信プレイヤーの 大規模リプレイスから得た知見と学び
yud0uhu
0
230
AWSを利用する上で知っておきたい名前解決のはなし(10分版)
nagisa53
10
3.1k
Featured
See All Featured
Thoughts on Productivity
jonyablonski
70
4.8k
Helping Users Find Their Own Way: Creating Modern Search Experiences
danielanewman
29
2.9k
Reflections from 52 weeks, 52 projects
jeffersonlam
352
21k
Save Time (by Creating Custom Rails Generators)
garrettdimon
PRO
32
1.6k
個人開発の失敗を避けるイケてる考え方 / tips for indie hackers
panda_program
112
20k
Intergalactic Javascript Robots from Outer Space
tanoku
272
27k
Practical Orchestrator
shlominoach
190
11k
Statistics for Hackers
jakevdp
799
220k
What’s in a name? Adding method to the madness
productmarketing
PRO
23
3.7k
The Cult of Friendly URLs
andyhume
79
6.6k
Chrome DevTools: State of the Union 2024 - Debugging React & Beyond
addyosmani
7
840
Easily Structure & Communicate Ideas using Wireframe
afnizarnur
194
16k
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)