[OS_4] 數學視角 | 多狀態 | 模型檢查器

程序 = 狀態機

gdb 單步執行 = 狀態遷移

- 狀態里有什么？gdb 可以打印
- 有一些特殊的狀態遷移

硬件 = 狀態機

指令執行 = 狀態遷移

- 從 CPU Reset 開始執行 Firmware
- Firmware 加載操作系統 (程序)

操作系統 = 狀態機 (毫無疑問)

程序是一種真正意義上的 “數學嚴格” 的對象

Everything is a state machine

- 程序 = 初始狀態 + 遷移函數
- 在這個視角下，程序和數學對象已經無限接近了：

Quick Quiz

怎樣給出 f 的定義? (《離散數學》課程內容)

用數學嚴格的語言描述計算機世界中的對象

- 《計算機科學的數學基礎》

- - Proof Assistant (妄想)

為什么會有程序？

是因為程序必須在無情執行指令的機器上執行
只有程序才配得上它

程序天生是 “人類” 的，也是 “反人類” 的

人類的一面：程序連接了人類世界需求

- 大語言模型有非常驚艷的編程能力

反人類的一面：程序會在機器上執行

- 大語言模型還是經常有幻覺

- - (對程序的行為的 100% 掌控就是非常困難的)

“Maintainability”: 代碼字面意義和實際行為直接關聯
軟件：物理世界實際的事在計算機世界的需求投影

所以我們要盡量寫出寫絕對正確的代碼

我們能證明程序的正確性嗎？

int popcount(int x) {int count = 0;while (x) {x -= (x & -x);count++;}return count;
}

我們還需要 “什么叫對”
Specification: 不 crash; 沒有 UB; assert satisfy, ...

int popcount(int x) {int count = 0;while (x) {x -= (x & -x);count++;}return count;
}void popcount_spec() {for (uint64_t x = 0; x <= 0xffffffff; x++) {assert( ((x >> 0) & 1) + ((x >> 1) & 1) + ...((x >> 31) & 1) == popcount(x) );}

For all executions of ff, the specification is satisfied.

暴力枚舉

寫一個 driver code，枚舉所有的 xx，運行 f(x)f(x)

- Testing: 選一些有代表性的

寫出證明

直接證明 “For all executions of ff, the specification is satisfied.”

- 就和在《離散數學》課上的證明一樣

“Proof Assistant” (Coq, Lean, ...)

它會拒絕一切偽證

- EMMS Lecture by Terence Tao

計算機輔助證明

這并不是一個新概念：我們不再用自然語言，而是用嚴格的、機器可檢查的邏輯語言書寫證明，核心技術是揭示了數學證明與類型系統之間的深刻聯系的 Curry-Howard Correspondence：

命題即類型：邏輯中的命題 (如 A→B) 對應函數類型 A→B。
證明即程序：命題的構造性證明過程對應該類型的一個具體程序（例如，一個實現 A→B的函數即為 “A 蘊含 B” 的證明）。

邏輯中的蘊含消除規則對應函數調用：若有一個類型為 A→B的函數 (證明)，且輸入類型 AA的值 (前提)，則輸出類型 B 的值 (結論)。而對于一階謂詞，例如 ?x.P(x)，就必須提供一個 x 的實例，這構成了基于構造的 “直覺邏輯” 的基礎。

Proof assistant 是人工智能時代堪稱完美的輔助工具：如果我們要信任 AI 產生的結果，可以讓它們給出一個 proof assistant 認可的證明！延伸閱讀：科普文章: “Formal verification doesn’t result in perfect code; it simply narrows the possibility for errors and vulnerabilities to creep in,” Parno says. “What makes the technique so attractive is that you push the uncertainty or scope of problems down to smaller and smaller windows”

<<正式的軟件驗證措施>>

4.2 數學視角的操作系統

程序 = 狀態機

狀態

- 棧幀中的變量和 PC ; 局部變量

初始狀態

- main(argc, argv)

狀態遷移

- 執行 “當前棧幀 PC” 的語句
- 有一種特殊的語句：syscall

(我們不妨就認可狀態機是可以 “數學定義” 的)

操作系統 = 狀態機的管理者

可以同時容納多個 “程序狀態機”

- 程序內計算：選一個程序執行一步
- 系統調用：創建新狀態機、退出狀態機、打印字符……

有了一個有趣的想法……

能不能我們自己定義 “狀態機”

- 用我們喜歡的語言、喜歡的方式
- 不要受限于 C、匯編……

自己模擬狀態機的執行

- 不就有了一個 “玩具操作系統” 嗎？

Life is short, you need Python!

def StateMachine():b = sys_read()if b == 0:sys_write('I got a zero.')else:sys_write('I got a one.')def main():sys_spawn(StateMachine)

操作系統中的對象

狀態機 (進程)

- Python 代碼
- 初始時，僅有一個狀態機 (main)
- 允許執行計算或 read, write, spawn 系統調用

一個進程間共享的 buffer (“設備”)

系統調用

read(): 返回隨機的 0 或 1
write(s): 向 buffer 輸出字符串 s
spawn(f): 創建一個可運行的狀態機 f

難點是多狀態機的管理

如何在狀態機之前來回切換
實現我們單 CPU 上運行多個程序的效果？

一些途徑

用一個模擬器去解釋執行語句 (2022 年的實現)

- 創建多個模擬器對象單步執行 (J2ME KVM 就是如此)
- “虛擬機” (QEMU TCG)

是否有語言機制能 “暫存” 函數的運行狀態，并且之后回復？

- 有：Generators/Coroutines

30 行代碼講完 UNIX 系統的基本模型

進程
系統調用
上下文切換
調度

你會在 Linux Kernel 中看到 “類似” 的代碼

“procs” → cpu->runqueue
“current” → current = (current_thread_info()->task)

借助 py 來看看

操作系統是最早的實用并發程序

每個進程 (程序) 都是順序狀態機

- 但發生中斷/系統調用以后，操作系統代碼直接執行
- 如果有多個處理器 (或者允許此時切換到另一個程序執行)，就有了并發

4.3 狀態機模型與模型檢查器

Mosaic Model and Checker

狀態

多個 “應用程序” 狀態機

- 當然，可以是模型

初始狀態

僅有一個 “main” 狀態機

- 這個狀態機處于初始狀態

遷移

選擇一個狀態機執行一步

- 就像我們在操作系統模型上看到的那樣

計算機系統中的不確定性 (non-determinism)

程序中的不確定性都是操作系統給的

調度：狀態機的選擇不確定

多處理器的 “選擇” 是無法控制的
操作系統可以主動隨機選擇狀態機執行一步

I/O：系統外的輸入不確定

read 返回的結果也有兩種可能性

這樣程序的執行就不是 “一條線” 了

從初始狀態出發，可能有多個可能的 “下一個狀態”

這就是為什么并發程序難以預測了

Mosaic Model and Checker

看到并發的這個模型圖，《離散數學》忽然更有用了

程序定義了狀態機 G(V,E)

加上一個起點 v0
再加上 F?V是 “壞” (faulty) 的狀態

- 程序正確 ≡ 不存在從 v0到 v∈F 的路徑

也可以通過這個來理解網絡安全的驗證思路

還記得你們怎么在 G 里找路徑嗎

DFS/BFS 啊！
恭喜你！你離圖靈獎進了一步 (邁出了重要的第一步 Bush)

- 要有一個瘋狂的想法：軟件是可以自動證明的
- Turing Award Lecture: Model checking: algorithmic verification and debugging

插曲：如果你想得圖靈獎？

需要找一個 tractable 的問題

F?V+ 暴力枚舉顯然太 trivial 了

- 我們有更好的方式表達規約 (temporal logic)
- G(A→FB)

- - “如果 A 發生，則最終 B 會發生”
  - 哦！你需要構建一個好的邏輯系統

提出一些有趣的檢查算法

在軟件系統里又是 useful 的

要走很多彎路，而且今天 temporal logic（時序邏輯）也沒落了
但 Verification(驗證）沒有死，而且在 AI 時代肯定會走得更遠

Putting Them Together

模型

理論上，我們可以建模任何系統調用
當然，我們選擇建模最重要的那些

- Three Easy Pieces!

檢查器

最簡單的 BFS 就行 (只要能獲得狀態機的狀態)

可視化

我們就是繪制一個頂點是狀態的圖 G(V,E)

于是，我們有了一個更復雜的“玩具”

模塊	系統調用	行為
基礎	choose(xs)	返回一個 xs 中的隨機的選擇
基礎	write(s)	向調試終端輸出字符串 s
基礎	sched()	切換到隨機的線程/進程執行
虛擬化	fork()	創建當前狀態機的完整復制
并發	spawn(fn)	創建從 fn 開始執行的線程
持久化	bread(k)	讀取虛擬設磁盤塊 kk 的數據
持久化	bwrite(k, v)	向虛擬磁盤塊 kk 寫入數據 vv
持久化	sync()	將所有向虛擬磁盤的數據寫入落盤
持久化	crash()	模擬系統崩潰

操作系統模型和檢查器：

我們可以把 “狀態機的管理者” 這個思想在 Python 世界中構造出來：

我們用 Python 的函數來聲明狀態機，并且實現狀態空間的遍歷。
所有的實現都是 “最簡” 的——但它真的能用來澄清 Three Easy Pieces 里的概念：Concurrency, Virtualization, 和 Persistence。

下面是我們繪制一個 “Hello World” 狀態空間的例子。Hello 會調用一個有趣的系統調用 fork，它的行為是復制狀態機的當前狀態：

將會在這個專欄里，同時分析模型和真實操作系統 (Linux) 系統調用的行為，在概念 (抽象) 和具體 (實現) 層面理解操作系統。

4.4 總結

Take-away Messages: 程序就是狀態機；狀態機可以用程序表示。因此：我們可以用更 “簡單” 的方式 (例如 Python) 描述狀態機、建模操作系統 上的應用，并且實現操作系統的可執行模型。而一旦把操作系統、應用程序當做 “數學對象” 處理，那么我們圖論、數理邏輯中的工具就能被應用于處理程序，甚至可以用圖遍歷的方法證明程序的正確性。