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
670
問 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 を活用した高速かつスケーラブルな認可技術の探求 #phperkaigi / PHPerKaigi 2025
ytaka23
8
1.8k
NilAway による静的解析で「10 億ドル」を節約する #kyotogo / Kyoto Go 56th
ytaka23
4
650
形式手法の 10 メートル手前 #kernelvm / Kernel VM Study Hokuriku Part 7
ytaka23
7
1.3k
普通の Web エンジニアのための様相論理入門 #yapcjapan / YAPC Hakodate 2024
ytaka23
10
2.9k
kcp: Kubernetes APIs Are All You Need #techfeed_live / TechFeed Experts Night 28th
ytaka23
1
440
サーバーレスアーキテクチャの数理的理解と分析 #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
謎は全て解けた!安楽椅子探偵に捧げる AWS ネットワーク分析入門 #CNDT2022 / CloudNative Days Tokyo 2022
ytaka23
2
4.1k
Other Decks in Technology
See All in Technology
AWS パートナー企業のテクニカルサポートが日々思っていること 〜そして、4/15 の現場から〜
kazzpapa3
2
390
名刺メーカーDevグループ 紹介資料
sansan33
PRO
0
730
AIのための オンボーディングドキュメントを整備する - hirotea
hirotea
9
1.9k
SmartHRの複数のチームにおけるMCPサーバーの活用事例と課題
yukisnow1823
2
860
マップを速く表示するために
tsuboyan5
0
170
ゼロコードで実現! - OpenTelemetryとOCI APM Agentによる簡単アプリケーション監視 - / Zero-Code Observability with OpenTelemetry and OCI APM
oracle4engineer
PRO
1
180
GigaViewerにおけるMackerel APM導入の裏側
7474
0
150
[JAWS-UG 栃木 #2]AWS FISはドSなのか?システムに試練を与えて強くする!
sh_fk2
1
260
他チームへ越境したら、生データ提供ソリューションのクエリ費用95%削減へ繋がった話 / Cross-Team Impact: 95% Off Raw Data Query Costs
yamamotoyuta
0
160
ソフトウェアは捨てやすく作ろう/Let's make software easy to discard
sanogemaru
3
830
Project Referencesを活用した実行環境ごとのtsconfig最適化
itatchi3
1
230
令和トラベルQAのAI活用
seigaitakahiro
0
390
Featured
See All Featured
Being A Developer After 40
akosma
91
590k
Reflections from 52 weeks, 52 projects
jeffersonlam
349
20k
Responsive Adventures: Dirty Tricks From The Dark Corners of Front-End
smashingmag
251
21k
Art, The Web, and Tiny UX
lynnandtonic
298
21k
Optimising Largest Contentful Paint
csswizardry
37
3.2k
Let's Do A Bunch of Simple Stuff to Make Websites Faster
chriscoyier
507
140k
Designing for humans not robots
tammielis
253
25k
The World Runs on Bad Software
bkeepers
PRO
68
11k
XXLCSS - How to scale CSS and keep your sanity
sugarenia
248
1.3M
The Myth of the Modular Monolith - Day 2 Keynote - Rails World 2024
eileencodes
25
2.8k
Visualization
eitanlees
146
16k
Designing Experiences People Love
moore
142
24k
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/