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
780
問 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.8k
AWS のポリシー言語 Cedar を活用した高速かつスケーラブルな認可技術の探求 #phperkaigi / PHPerKaigi 2025
ytaka23
9
2.4k
NilAway による静的解析で「10 億ドル」を節約する #kyotogo / Kyoto Go 56th
ytaka23
4
680
形式手法の 10 メートル手前 #kernelvm / Kernel VM Study Hokuriku Part 7
ytaka23
7
1.3k
普通の Web エンジニアのための様相論理入門 #yapcjapan / YAPC Hakodate 2024
ytaka23
10
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
スタートアップに選択肢を 〜生成AIを活用したセカンダリー事業への挑戦〜
nstock
0
270
モニタリング統一への道のり - 分散モニタリングツール統合のためのオブザーバビリティプロジェクト
niftycorp
PRO
1
230
freeeのアクセシビリティの現在地 / freee's Current Position on Accessibility
ymrl
2
260
マーケットプレイス版Oracle WebCenter Content For OCI
oracle4engineer
PRO
3
980
オフィスビルを監視しよう:フィジカル×デジタルにまたがるSLI/SLO設計と運用の難しさ / Monitoring Office Buildings: The Challenge of Physical-Digital SLI/SLO Design & Operation
bitkey
1
290
第64回コンピュータビジョン勉強会「The PanAf-FGBG Dataset: Understanding the Impact of Backgrounds in Wildlife Behaviour Recognition」
x_ttyszk
0
140
助けて! XからWaylandに移行しないと新しいGNOMEが使えなくなっちゃう 2025-07-12
nobutomurata
2
130
CDK Toolkit Libraryにおけるテストの考え方
smt7174
1
380
Claude Code に プロジェクト管理やらせたみた
unson
7
4.9k
敢えて生成AIを使わないマネジメント業務
kzkmaeda
2
500
Operating Operator
shhnjk
1
640
Delegating the chores of authenticating users to Keycloak
ahus1
0
170
Featured
See All Featured
4 Signs Your Business is Dying
shpigford
184
22k
Measuring & Analyzing Core Web Vitals
bluesmoon
7
510
Six Lessons from altMBA
skipperchong
28
3.9k
Java REST API Framework Comparison - PWX 2021
mraible
31
8.7k
The Invisible Side of Design
smashingmag
301
51k
GraphQLの誤解/rethinking-graphql
sonatard
71
11k
The Success of Rails: Ensuring Growth for the Next 100 Years
eileencodes
45
7.5k
Sharpening the Axe: The Primacy of Toolmaking
bcantrill
44
2.4k
The World Runs on Bad Software
bkeepers
PRO
69
11k
Save Time (by Creating Custom Rails Generators)
garrettdimon
PRO
31
1.3k
VelocityConf: Rendering Performance Case Studies
addyosmani
332
24k
Helping Users Find Their Own Way: Creating Modern Search Experiences
danielanewman
29
2.7k
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/