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
問 1:以下のコンパイラを証明せよ(予告編) #kernelvm / Kernel VM St...
Search
y_taka_23
May 11, 2025
Technology
3
750
問 1:以下のコンパイラを証明せよ(予告編) #kernelvm / Kernel VM Study Kansai 11th
Kernel/VM探検隊 @ 関西 11 回目で使用したスライドです。
y_taka_23
May 11, 2025
Tweet
Share
More Decks by y_taka_23
See All by y_taka_23
AWS と定理証明 〜ポリシー言語 Cedar 開発の舞台裏〜 #fp_matsuri / FP Matsuri 2025
ytaka23
9
2.5k
AWS のポリシー言語 Cedar を活用した高速かつスケーラブルな認可技術の探求 #phperkaigi / PHPerKaigi 2025
ytaka23
9
2.3k
NilAway による静的解析で「10 億ドル」を節約する #kyotogo / Kyoto Go 56th
ytaka23
4
660
形式手法の 10 メートル手前 #kernelvm / Kernel VM Study Hokuriku Part 7
ytaka23
7
1.3k
普通の Web エンジニアのための様相論理入門 #yapcjapan / YAPC Hakodate 2024
ytaka23
10
3k
kcp: Kubernetes APIs Are All You Need #techfeed_live / TechFeed Experts Night 28th
ytaka23
1
460
サーバーレスアーキテクチャの数理的理解と分析 #devsumi / Developers Summit 2023 Summer
ytaka23
9
5.3k
形式手法による分散システムの検証 〜S3 の一貫性モデルを例として〜 #ourdevday2023 / Our DevDay 2023
ytaka23
2
1.4k
Amazon S3 の一貫性モデル超入門 #ハードル激低LT大会 / Low-hurdle LT Meetup 2nd
ytaka23
3
2.2k
Other Decks in Technology
See All in Technology
比起獨自升級 我更喜歡 DevOps 文化 <3
line_developers_tw
PRO
0
210
DB 醬,嗨!哪泥嘎斯基?
line_developers_tw
PRO
0
210
VCpp Link and Library - C++ breaktime 2025 Summer
harukasao
0
180
Copilot Agentを普段使いしてわかった、バックエンド開発で使えるTips
ykagano
1
1.2k
Securing your Lambda 101
chillzprezi
0
280
Perk アプリの技術選定とリリースから1年弱経ってのふりかえり
stomk
0
100
In Praise of "Normal" Engineers (LDX3)
charity
2
950
Claude Code どこまでも/ Claude Code Everywhere
nwiizo
47
27k
Devin(Deep) Wiki/Searchの活用で変わる開発の世界観/devin-wiki-search-impact
tomoki10
0
330
マルチテナント+マルチプロダクト SaaS への AI Agent の組み込み方
kworkdev
PRO
2
350
AIエージェントの継続的改善のためオブザーバビリティ
pharma_x_tech
6
1.2k
Bill One 開発エンジニア 紹介資料
sansan33
PRO
4
12k
Featured
See All Featured
GitHub's CSS Performance
jonrohan
1031
460k
Dealing with People You Can't Stand - Big Design 2015
cassininazir
367
26k
The Success of Rails: Ensuring Growth for the Next 100 Years
eileencodes
45
7.3k
Making the Leap to Tech Lead
cromwellryan
134
9.3k
The Cult of Friendly URLs
andyhume
79
6.4k
Optimising Largest Contentful Paint
csswizardry
37
3.3k
Documentation Writing (for coders)
carmenintech
71
4.9k
個人開発の失敗を避けるイケてる考え方 / tips for indie hackers
panda_program
107
19k
jQuery: Nuts, Bolts and Bling
dougneiner
63
7.8k
Facilitating Awesome Meetings
lara
54
6.4k
How to train your dragon (web standard)
notwaldorf
92
6.1k
The Illustrated Children's Guide to Kubernetes
chrisshort
48
50k
Transcript
#kernelvm 問1:以下のコンパイラを 証明せよ(予告編) チェシャ猫 (@y_taka_23) Kernel/VM 探検隊@関西 #11 (11th May.
2025)
#kernelvm ゴールデンウィークといえば コンパイラ
#kernelvm 簡単なコンパイラを正しく作ってみる
#kernelvm コンパイルターゲット:CHIP-8 • 1970 年代のレトロコンピュータ ◦ 35 個の固定 2 バイト長
CPU 命令 ◦ V0 ~ VF の 16 個の汎用レジスタ ◦ 4096 バイトの RAM ◦ 64 x 32 ドットの 2 値ディスプレイ ◦ 16 キー入力 / 単音ビープ / タイマー https://github.com/y-taka-23/rust-chip8
#kernelvm CHIP-8 ROM ソースコード ディスプレイ コンパイル 出力 (x1, x2) に
x0 を Hex 出力
#kernelvm CHIP-8 ROM ソースコード ディスプレイ コンパイル 出力 (x1, x2) に
x0 を Hex 出力
#kernelvm CHIP-8 ROM ソースコード ディスプレイ コンパイル 出力 0x0D 0x18 (x1,
x2) に x0 を Hex 出力
#kernelvm スモールスタートのための単純化 • パーサ / キー入力 / 音 / タイマーは最初は不要
• レジスタ退避が発生しないようにする ◦ 変数は x0 ~ v15 のみとし V0 ~ VF レジスタに割り当て ◦ 全てグローバル変数で、関数呼び出しもなし ◦ 代入は三番地コード形式で、演算も足し算のみ ◦ while の条件部分も「変数 != 即値」に決めうち
#kernelvm CHIP-8 ROM ソースコード コンパイル
#kernelvm CHIP-8 ROM ソースコード 抽象構文木 (パース)
#kernelvm CHIP-8 ROM ソースコード 抽象構文木 CHIP-8 命令列 コンパイル (パース) アセンブル
#kernelvm CHIP-8 ROM ソースコード 抽象構文木 CHIP-8 命令列 ディスプレイ 表示命令列 CHIP-8
VM 実行 コンパイル 出力 (パース) 逆アセンブル
#kernelvm while (x1 != 0x2A) { print(x1, x2, x0); x0
= x0 + 0x01; x1 = x1 + 0x06; } ... SNE V1 0x2A JP (addr + 0x14) LD I V0 DRW V1 V2 0x5 LD V0 V0 ADD V0 0x01 LD V1 V1 ADD V1 0x06 addr addr + 0x02 addr + 0x04 addr + 0x08 addr + 0x0A addr + 0x0C addr + 0x0E addr + 0x10 addr + 0x12 JP addr addr + 0x14 ... ソースコードの一部 コンパイルされた CHIP-8 命令列
#kernelvm while (x1 != 0x2A) { print(x1, x2, x0); x0
= x0 + 0x01; x1 = x1 + 0x06; } ... SNE V1 0x2A JP (addr + 0x14) LD I V0 DRW V1 V2 0x5 LD V0 V0 ADD V0 0x01 LD V1 V1 ADD V1 0x06 addr addr + 0x02 addr + 0x04 addr + 0x08 addr + 0x0A addr + 0x0C addr + 0x0E addr + 0x10 addr + 0x12 JP addr addr + 0x14 ... ソースコードの一部 コンパイルされた CHIP-8 命令列
#kernelvm while (x1 != 0x2A) { print(x1, x2, x0); x0
= x0 + 0x01; x1 = x1 + 0x06; } ... SNE V1 0x2A JP (addr + 0x14) LD I V0 DRW V1 V2 0x5 LD V0 V0 ADD V0 0x01 LD V1 V1 ADD V1 0x06 addr addr + 0x02 addr + 0x04 addr + 0x08 addr + 0x0A addr + 0x0C addr + 0x0E addr + 0x10 addr + 0x12 JP addr addr + 0x14 ... ソースコードの一部 コンパイルされた CHIP-8 命令列 != x1 != 0x2A の場合は JP 命令を避けてループ内に入る
#kernelvm while (x1 != 0x2A) { print(x1, x2, x0); x0
= x0 + 0x01; x1 = x1 + 0x06; } ... SNE V1 0x2A JP (addr + 0x14) LD I V0 DRW V1 V2 0x5 LD V0 V0 ADD V0 0x01 LD V1 V1 ADD V1 0x06 addr addr + 0x02 addr + 0x04 addr + 0x08 addr + 0x0A addr + 0x0C addr + 0x0E addr + 0x10 addr + 0x12 JP addr addr + 0x14 ... ソースコードの一部 コンパイルされた CHIP-8 命令列 == x1 == 0x2A の場合は JP 命令でループ後まで飛ぶ
#kernelvm 簡単なコンパイラを正しく作ってみる
#kernelvm コンパイル結果の「正しさ」とは? • 実行すると時間に伴って変化するディスプレイ ◦ その出力がどうであれば「正しい」と言えるのか • 一般には実行は停止せず、無限ループになる ◦ つまり「最終的な実行結果」が定義できない
• 必ずしも毎ステップ出力がある訳でもない ◦ 単に 1 ステップごとの「結果」を検証することが難しい
#kernelvm インタプリタ実装による意味論 • CHIP-8 VM とは別にインタプリタを実装 ◦ ソース言語の構文木を機械語に変換せず、直接実行する ◦ 副作用としてディスプレイへの表示命令列を出力
◦ この表示命令列を「見本」としてコンパイル版と照合 • ソース言語に操作的意味論を与えることに等しい ◦ インタプリタのステップ実行が意味論の簡約規則に対応
#kernelvm while (x1 != 0x2A) { print(x1, x2, x0); x0
= x0 + 0x01; x1 = x1 + 0x06; } ... x0: 0x0A x1: 0x18 x2: 0x0D ある時点のインタプリタ 環境:変数の値 継続:残りのコード
#kernelvm while (x1 != 0x2A) { print(x1, x2, x0); x0
= x0 + 0x01; x1 = x1 + 0x06; } ... x0: 0x0A x1: 0x2A x2: 0x0D ... x0: 0x0A x1: 0x2A x2: 0x0D 1 ステップ実行 ある時点のインタプリタ 1 ステップ後のインタプリタ x1 == 0x2A x1 == 0x2A の場合はループ全体を捨てる
#kernelvm while (x1 != 0x2A) { print(x1, x2, x0); x0
= x0 + 0x01; x1 = x1 + 0x06; } ... x0: 0x0A x1: 0x18 x2: 0x0D print(x1, x2, x0); x0 = x0 + 0x01; x1 = x1 + 0x06; while (x1 != 0x2A) { print(x1, x2, x0); x0 = x0 + 0x01; x1 = x1 + 0x06; } ... x0: 0x0A x1: 0x18 x2: 0x0D 1 ステップ実行 ある時点のインタプリタ 1 ステップ後のインタプリタ x1 != 0x2A x1 != 0x2A の場合はループを 1 回分展開
#kernelvm CHIP-8 ROM ソースコード 抽象構文木 CHIP-8 命令列 ディスプレイ 表示命令列 CHIP-8
VM 実行 コンパイル 出力 (パース) アセンブル 逆アセンブル
#kernelvm CHIP-8 ROM ソースコード 抽象構文木 CHIP-8 命令列 ディスプレイ 表示命令列 表示命令列
インタプリタ実行 CHIP-8 VM 実行 コンパイル 出力 出力 (パース) アセンブル 逆アセンブル
#kernelvm CHIP-8 ROM ソースコード 初期化 コンパイル ソース言語インタプリタのステップ実行列 CHIP-8 VM のステップ実行列
初期化 出力命令 print(0x18, 0x0D, 0x0A) を比較
#kernelvm 無限に続く状態遷移系の「等しさ」 • A:“外部選択型” 自販機 ◦ コイン投入でコーヒー / 紅茶の両方のボタンが点灯 ◦
人間がボタンを押すと、選んだ商品が出て最初に戻る • B:“内部選択型” 自販機 ◦ コイン投入でコーヒー / 紅茶のどちらかのボタンが点灯 ◦ 人間が点灯した方のボタンを押すと、商品が出て最初に戻る https://staff.aist.go.jp/y-isobe/topse/vic/slides/csp-isobe-2010-07.pdf
#kernelvm A:“外部選択型” 自販機の状態遷移 B:“内部選択型” 自販機の状態遷移 coin tea coffee coin coin
coffee tea 出力列(トレース)は両者とも (coin (coffee | tea))*
#kernelvm この差を区別できる「等しさ」が欲しい
#kernelvm 双模倣による等価性 • 無限に続く状態遷移系同士の比較 • 弱双模倣等価(Weak-Bisimulation Equivalence) ◦ 両者の状態間に何らかの対応関係が定義されている ◦
対応した状態から、両者 1 ステップ進んでもやはり対応 ◦ “弱” とは、何も出力しないステップ(τ遷移)を無視 ◦ 出力列集合の一致(トレース等価)より条件が厳しい
#kernelvm ∀ ∀ ∀ ソース言語インタプリタのステップ実行 print(0x18, 0x0D, 0x0A) 状態間の対応関係
#kernelvm ∀ ∃ ∀ ∀ ソース言語インタプリタのステップ実行 CHIP-8 VM のステップ実行例 print(0x18,
0x0D, 0x0A) ∃ ∃ print(0x18, 0x0D, 0x0A) τ* τ* 状態間の対応関係 遷移先も再び対応関係
#kernelvm まとめ • CHIP-8 をターゲットとするコンパイラ自作 ◦ 機能を制限すれば簡単に作れてそれなりに動く • コンパイラの「正しさ」を意味論の保存として定義 ◦
インタプリタ実装により操作的意味論を与える • (弱)双模倣による動作の比較 ◦ 無限に動き続ける状態遷移系の等価性が定義できる
#kernelvm Let’s Craft Correct Compilers! Presented by チェシャ猫 (@y_taka_23)
#kernelvm タイトルの「証明」要素は?
#kernelvm 次回、To Be Proven! Presented by チェシャ猫 (@y_taka_23) https://lean-lang.org/