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
今からでも間に合う! 生成AI「RAG」再入門 / Re-introduction to RAG in Generative AI
hideakiaoyagi
1
190
"SaaS is Dead" は本当か!? 生成AI時代の医療 Vertical SaaS のリアル
kakehashi
PRO
3
230
開発効率と信頼性を両立する Ubieのプラットフォームエンジニアリング
teru0x1
0
150
比起獨自升級 我更喜歡 DevOps 文化 <3
line_developers_tw
PRO
0
240
Autonomous Database サービス・アップデート (FY25)
oracle4engineer
PRO
2
780
Javalinの紹介
notoh
0
110
CIでのgolangci-lintの実行を約90%削減した話
kazukihayase
0
310
AWS アーキテクチャ作図入門/aws-architecture-diagram-101
ma2shita
24
8.8k
OAuth/OpenID Connectで実現するMCPのセキュアなアクセス管理
kuralab
2
280
IIWレポートからみるID業界で話題のMCP
fujie
0
510
AI技術トレンド勉強会 #1MCPの基礎と実務での応用
nisei_k
1
220
上長や社内ステークホルダーに対する解像度を上げて、より良い補完関係を築く方法 / How-to-increase-resolution-and-build-better-complementary-relationships-with-your-bosses-and-internal-stakeholders
madoxten
13
7.8k
Featured
See All Featured
The Cult of Friendly URLs
andyhume
79
6.4k
Building a Scalable Design System with Sketch
lauravandoore
462
33k
Six Lessons from altMBA
skipperchong
28
3.8k
Writing Fast Ruby
sferik
628
61k
A Modern Web Designer's Workflow
chriscoyier
693
190k
Speed Design
sergeychernyshev
31
990
A better future with KSS
kneath
239
17k
GraphQLの誤解/rethinking-graphql
sonatard
71
11k
Facilitating Awesome Meetings
lara
54
6.4k
Reflections from 52 weeks, 52 projects
jeffersonlam
351
20k
No one is an island. Learnings from fostering a developers community.
thoeni
21
3.3k
YesSQL, Process and Tooling at Scale
rocio
172
14k
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/