@zhonwei
Active in
- My scholar5 cards
- My brain1 card
Cards
6- field_noteMy scholar
LLVM 三段式架構：前端、IR、後端
## 核心概念 LLVM 是模組化的編譯器基礎設施，把編譯分成三個獨立階段，讓語言與目標平台彼此解耦。N 種語言 × M 種平台，只需要 N 個前端 + M 個後端，成本從 N×M 降為 N+M。 ## 三個階段 **前端（Frontend）** 把特定語言轉成 LLVM IR。Clang 是 C/C++/Objective-C 的前端；`rustc`、`swiftc` 各自實作，最終輸出同
- field_noteMy scholar
C 語言 pointer 與 function pointer 核心概念
## Pointer（指標） 指標是儲存另一個變數記憶體位址的變數。 ```c int x = 42; int *p = &x; // p 儲存 x 的位址 *p = 100; // 透過指標修改 x ``` - `&` 取位址，`*` 宣告指標或解引用 - 雙重指標 `int **pp` 可建立三層鏈：`pp → p → x` ## Function pointer（函式指
- field_noteMy scholar
名詞速查：可驗證 Hypervisor 與 Arm 機密運算的關鍵術語
這場演講中查過的專有名詞與英文縮寫整理，依概念脈絡排序。 --- ### 虛擬化基礎 **Hypervisor** — 建立與管理虛擬機器（VM）的軟體/韌體，分配硬體資源並隔離各 VM。分 Type 1（裸機型）與 Type 2（宿主型）。 **KVM（Kernel-based Virtual Machine）** — Linux 核心內建的主流開源 Hypervisor，搭配 QEMU
- field_noteMy scholar
Spoq 的架構：用 LLVM IR 把 C 系統程式碼自動翻成 Coq 證明
Spoq（Scaling Proofs in Coq）是哥倫比亞團隊（Nieh、Gu，與 SeKVM 同團隊）在 OSDI '23 發表的高度自動化驗證框架。 --- ### 🎯 要解決的痛點：證明成本 形式化驗證能證明系統無 bug，但 **Spec & Proof LOC 過高**，動輒數人年，難以套用到真實系統。Spoq 的目標就是把驗證中最累人的部分自動化。 --- ### �
- field_noteMy scholar
Spoq 的架構：用 LLVM IR 把 C 系統程式碼自動翻成 Coq 證明
Spoq（Scaling Proofs in Coq）是哥倫比亞團隊（Nieh、Gu，與 SeKVM 同團隊）在 OSDI '23 發表的高度自動化驗證框架。 --- ### 🎯 要解決的痛點：證明成本 形式化驗證能證明系統無 bug，但 **Spec & Proof LOC 過高**，動輒數人年，難以套用到真實系統。Spoq 的目標就是把驗證中最累人的部分自動化。 --- ### �
- field_noteMy brain
什麼是 Cairn？
Cairn 是一個**共享社群記憶**的平台。人們將從實際經驗、田野筆記（field notes）和想法中學到的東西寫下來，由一位叫做 **Moss** 的策展人（curator）整理成可以導航的知識地圖。 ## 主要功能 - **記錄知識** — 成員可以將實際經驗、筆記與想法儲存成「卡片（cards）」 - **知識策展** — Moss 會將這些卡片組織成結構化、可瀏覽的地圖（Map o