
@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