引言

我們在過去十年中，關於如何建構電腦系統的知識進展令人沮喪地少。但我們確實學到了一些如何更精確地完成這項工作的方法，透過撰寫更精確的規格，以及更精確地證明實作符合其規格。用於執行此類工作的方法同時具有學術和實務價值。我將解釋最有用的一種方法，並透過兩個範例來說明：

連線建立：透過不可靠的網路傳送可靠訊息。 交易：將一系列小型動作組合成一個大型原子性動作。

電腦系統設計原則

10 年前：電腦系統設計提示 從那以後學到的不多——令人失望 我們不是站在彼此的肩膀上，而是站在彼此的腳趾上。(Hamming) 一個新發現：如何更精確地建構系統 如果你認為系統昂貴，那就試試混亂吧。

合作夥伴

  • Bob Taylor
  • Chuck Thacker
    • 工作站：Alto, Dorado, Firefly
    • 網路：AN1, AN2
  • Charles Simonyi
    • Bravo WYSIWYG 編輯器
  • Nancy Lynch
    • 可靠訊息
  • Howard Sturgis
    • 交易
  • Martin Abadi
    • 安全性
  • Mike Burrows
  • Morrie Gasser
  • Andy Goldstein
  • Charlie Kaufman
  • Ted Wobber
  • Bob Sproull
    • Alto 作業系統
    • Dover：雷射印表機
    • Interpress：頁面描述語言
  • Mel Pirtle
    • 940 專案，Berkeley Computer Corp.
  • Peter Deutsch
    • 940 作業系統
    • QSPL：系統程式語言
  • Chuck Geschke
  • Jim Mitchell
  • Ed Satterthwaite
    • Mesa：系統程式語言
  • Jim Horning
    • Euclid：可驗證程式語言
  • Ron Rider
  • Gary Starkweather
  • Severo Ornstein
    • Ears：雷射印表機
  • Roy Levin
    • Wildflower：Star 工作站原型
    • Vesta：軟體組態
  • Andrew Birrell, Roger Needham, Mike Schroeder
    • 全局命名服務與認證
  • Eric Schmidt
    • System models：軟體組態
  • Rod Burstall
    • Pebble：多型別語言

從介面到規格

讓模組化變得精確 分而治之 (羅馬箴言)

  • 設計
  • 正確性
  • 文件

遞歸地執行 任何想法遞歸化後都會更好 (Randell)

精化：一個人的實作是另一個人的規格。(改編自 Perlis) 組合：在一個規格中使用另一個規格中的動作。

定義具狀態的系統規格

安全性屬性：永遠不會發生壞事 由狀態機定義：

  • 狀態：一組值，通常分為具名的變數
  • 動作：具名的狀態變更

活潑性屬性：某件好事最終會發生 這些定義了行為：所有可能的動作序列 具狀態系統的範例：

  • 資料抽象
  • 並行系統
  • 分散式系統

你無法從外部觀察系統的實際狀態。 你只能看到動作的結果。

可編輯格式化文字範例

狀態

  • text: sequence of (Char, Property)

動作

  • get(2) returns (‘e’, (Times-Roman, ...))
  • replace(3, 5, 2, 3, H e l p) - 替換位置 3 到 5 的內容（'p', 'p', 'l'）為 'H', 'e', 'l', 'p'
    • a p p l e -> a H e l p l e (假設長度變化)
    • 原文範例似乎是在說明透過replace/look進行的文字操作，其結果如下：
      • 初始文字: a p p l e
      • 某操作後: H e l l o
      • 再操作後: H e l l o
      • 再操作後: H e l l o
  • look(0, 5, italic := true) - 將位置 0 到 5 的文字設定為斜體

這個介面用於 Bravo 編輯器。 其實作大約有 20k 行程式碼。

如何撰寫規格

弄清楚狀態是什麼 選擇能使規格清晰的狀態，而不是匹配程式碼的狀態。 描述動作

  • 它們對狀態做了什麼
  • 它們回傳什麼

實用提示

  • 符號表示很重要；它能幫助你思考正在發生的事情。
  • 創造適合的詞彙。
  • 動作越少越好。Less is more.
  • 非確定性越多越好；它允許更多實作。

很抱歉寫了這麼長的信；我沒時間寫封短的。(Pascal)

可靠訊息

(圖示描述了寄件者與收件者之間透過不可靠網路交換訊息 (B, C, D) 和確認 (A)。狀態包括 OK, lost, ?。操作包括 crash, lose, recover, put(m), getAck(a), get(m)。顯示了佇列 q 在不同狀態下的內容及狀態變化範例。)

可靠訊息規格

Name Guard Effect
put(m) append m to q, status := ?
*get(m) m first on q remove head of q, if q = <>, then status = OK
*getAck(a) status = a status := lost
lose recs or recr delete some element from q; if it’s the last then status := lost, or status := lost

「實作」的含義

將動作分為外部動作和內部動作。 如果 Y 實作 X：

  • Y 的每個外部行為都是 X 的外部行為，並且
  • Y 的活潑性屬性蘊含 X 的活潑性屬性。

這表達了 Y 實作 X 的想法是： 你僅透過觀察外部動作無法區分 Y 與 X。

證明 Y 實作 X

定義一個從 Y 的狀態到 X 的狀態的抽象函數 f。 證明 Y 模擬 X：

  1. f 將 Y 的初始狀態映射到 X 的初始狀態。
  2. 對於每個 Y 動作和每個狀態 y 存在一系列 X 動作，其外部表現相同， 且圖表交換。
    f(y) ---(X-actions)---> f(y')
     ^                          ^
     | f                        | f
     |                          |
     y -----(Y-action)----> y'

這總能奏效！

延遲決策規格範例

(圖示類似於可靠訊息圖示，但訊息 (B, D) 有標記 (#)，狀態 ?# 表示部分遺失。描述了狀態變化範例如 drop(B), drop(D), mark(B), mark(D) 等。)

實作者希望規格盡可能非確定性， 這能給他更大的自由度，並更容易證明正確性。

泛型協定 G (1-4)

(圖示描述了寄件者 (Sender) 和收件者 (Receiver) 的狀態機、動作、以及透過不可靠通道 (unreliable channels) 傳輸的訊息 (msg) 和狀態資訊 (sr, rs)。變數包括 lasts, lastr, gs, gr, recs, recr, newr。動作包括 put(m), get(m), getAck(a), growr(i), grows(i), choose(i)。)

泛型協定 G 的運作範例

(圖示展示了協定 G 在一系列動作 (put(C), crashs, crashr, recover, get(C), shrinkr(3), cleanLog...) 及其引發的狀態變數 (gs, lasts, msg, sr, rs, gr, lastr, mark) 和抽象狀態 (q, status) 變化的具體範例。)

協定 G 的抽象函數

  • cur-q = if msg ≠ nil and (lasts = nil or lasts ∈ gr) otherwise < >
  • old-q = the messages in sr with i’s that are good and not = lasts
  • q = old-q + cur-q
  • status = ? if cur-q ≠ < > OK if lasts = lastr ≠ nil lost if lasts ∉ (gr ∪ {lastr}) or lasts = nil
  • recs/r = recs/r

交握協定 H (1-6)

(圖示描述了交握協定 H 的狀態機、動作和變數 (j-new, js, ir, rs, sr, needI, jr, lasts, lastr, done)。動作包括 put(m), assignI(j, i), choose(i), get(m), getAck(a), cleanup, newr。這是一種實作可靠訊息協定的方式。)

協定 H 的抽象函數

  • G -> H

  • ggss -> the i’s with (js, i) in rs

  • ggrr -> {ir} – {nil}

  • ssrr and rrss -> the (I, M) and (I, A) messages in sr and rs

  • news/r, lasts/r, and msg are the same in G and H

  • growr(i) -> receiver sets ir to an identifier from newr

  • grows(i) -> receiver sends (js, i)

  • shrinks(i) -> channel rs loses the last copy of (js, i)

  • shrinkr(i) -> receiver gets (ir, done)

一個高效的程式是一場邏輯的邊緣冒險。(Dijkstra)

可靠訊息：總結

想法

  • 訊息上的識別碼
  • 好的識別碼集合，寄件者的 ⊆ 收件者的
  • 清理

規格很簡單。 實作因故障而變得微妙。 抽象函數揭示了它們的秘密。 微妙性可以透過精確的方式一步步引入。

原子性動作

狀態：S

Name Guard Effect
do(a):Val (S, val) := a(S)

一個分散式系統是指我無法完成工作，因為某台我從未聽說過的電腦故障了。(Lamport)

  • X Y -> 執行 do(x := x–1) -> 4 5 -> 執行 do(y := y+1) -> 4 6

交易：一次一個動作

狀態：S, s

Name Guard Effect
do(a):Val (s, val) := a(s)
commit S := s
crash s := S
  • X Y | x y
  • 5 5 | 5 5 -> 執行 do(x := x–1); do(y := y+1)
  • 5 5 | 4 6 -> 在 commit 前 crash
  • 5 5 | 5 5
  • 5 5 | 4 6 -> commit
  • 4 6 | 4 6

伺服器故障

狀態：S, s φ : {nil, run} := nil

Name Guard Effect
begin φ = nil φ := run
do(a):Val φ = run (s, val) := a(s)
commit φ = run S := s, φ := nil
crash s := S, φ := nil

請注意，我們清除了輔助狀態 φ。

  • X Y | x y | φ
  • 5 5 | 5 5 | nil -> 執行 do(x := x–1); do(y := y+1)
  • 5 5 | 4 6 | run -> 在 commit 前 crash
  • 5 5 | 5 5 | nil
  • 5 5 | 4 6 | run -> commit
  • 4 6 | 4 6 | nil

增量狀態變更：日誌 (1)

狀態：S, s SS = S + L L, l : SEQ Action := < > ss, φφ = s, φ φ : {nil, run} := nil

Name Guard Effect
begin φ = nil φ := run
do(a):Val φ = run (s, val) := a(s), l +:= a
commit φ = run L := l, φ := nil
. . .
crash l := L, s := S+L, φ:=nil
  • X Y | x y | φ | Logs
  • 5 5 | 5 5 | nil | -> begin; do(x:=x–1); do(y:=y+1)
  • 5 5 | 4 6 | run | x := 4*, y := 6*
  • 5 5 | 4 6 | run | x := 4*, y := 6* -> commit
  • 5 5 | 4 6 | nil | x := 4*, y := 6*
  • 5 5 | 4 6 | run | x := 4*, y := 6* -> 在 commit 前 crash
  • 5 5 | 5 5 | nil | x := 4*, y := 6*

增量狀態變更：日誌 (2)

狀態：S, s SS = S + L L, l : SEQ Action ss, φφ = s, φ φ : {nil, run}

Name Guard Effect
begin, do, and commit as before
apply(a) a = head(l) S := S + a, l := tail(l)
cleanLog L in S L := < >
crash l := L, s := S+L, φ:=nil
  • X Y | x y | φ | Logs
  • 5 5 | 4 6 | nil | x := 4*, y := 6* -> apply(x := 4)
  • 4 5 | " | nil | y := 6* -> apply(y := 6)
  • 4 6 | " | nil | -> cleanLog
  • 4 6 | " | nil |
  • 4 5 | " | nil | y := 6* -> 在 apply(x:=4) 後 crash
  • 4 5 | " | nil | x := 4*, y := 6*

增量日誌變更

狀態：S, s LL = L if φ = com else < > L, l : SEQ Action φφ = φ if φ ≠ com else nil Φ, φ : {nil, run*, commit}

Name Guard Effect
begin and do as before
flush φ = run copy some of l to L
commit φ = run, L = l Φ := φ := commit
apply(a) φ = commit, a = head(L) S := S + a, L := tail(L)
cleanLog head(L) in S or φ = nil L := tail(L)
cleanup L = < > Φ := φ := nil
crash l := < > if Φ = nil else L; s := S + l, φ := Φ
  • X Y | x y | Φ φ | Logs
  • 5 5 | 4 6 | nil run | x := 4*, y := 6* -> flush; commit
  • 5 5 | " | com com | x := 4*, y := 6* -> apply(x := 4); apply(y := 6)
  • 4 6 | " | com com | -> cleanLog; cleanup
  • 4 6 | " | nil nil |
  • 4 5 | " | nil nil | x := 4*, y := 6* -> 在 flush 後 crash
  • 4 5 | " | nil nil | x := 4*, y := 6*

分散式狀態與日誌

狀態：Si, si φφ = run if all φi = run Li, li : SEQ Action com if any φi = com and any Li ≠ < > Φi, φi : {nil, run*, commit} nil otherwise S, L, Φ are the products of the Si, Li, Φi

Name Guard Effect
begin and do as before
flushi φi = run copy some of li to Li
preparei φi = run, Li=li Φi := run
commit φ = run, L = l some Φi :=φi :=commit
cleanLog and cleanup as before
crashi li := < >if Φi = nil else Li; si := Si + li, φi := Φi

高可用性

Φ = commit 是可能的單點故障 (single point of failure)。 在使用傳統的兩階段提交 (2PC) 時，這確實是可用性的限制。 如果資料有複本，未複本的提交是一個弱點。 透過使用高可用的共識演算法來處理 Φ。 Lamport 的 Paxos 演算法是目前已知最好的。

交易：總結

想法

  • 日誌
  • 提交記錄
  • 關鍵點上的穩定寫入：prepare 和 commit
  • 延遲清理

規格很簡單。 實作因故障而變得微妙。 抽象函數揭示了它們的秘密。 微妙性可以一步步加入。

如何撰寫規格

弄清楚狀態是什麼 選擇能使規格清晰的狀態，而不是匹配程式碼的狀態。 描述動作

  • 它們對狀態做了什麼
  • 它們回傳什麼

實用提示

  • 符號表示很重要；它能幫助你思考正在發生的事情。
  • 創造適合的詞彙。
  • 動作越少越好。Less is more.
  • 非確定性越多越好；它允許更多實作。

很抱歉寫了這麼長的信；我沒時間寫封短的。(Pascal)

安全性

存取控制模型

守衛控制對寶貴資源的存取。 (圖示描述了 Principal 透過 Guard 向 Object 發出 Request 來 Do operation，Guard 則依據 Rules 控制 Principal 對 Object 的存取。核心元件包括 Principal, Object, Operation, Guard, Reference monitor, Rules, Source, Resource。)

規則控制每個 Principal 和 Object 允許的操作。 Principal 可以 do Operation on Object

範例：

  • Taylor Read File “Raises”
  • Jones Pay invoice 4325 Account Q34
  • Schwarzkopf Fire three rounds Bow gun

分散式系統範例

(圖示展示了 Workstation 和 Server，各自運行 Operating system。Workstation 運行 Excel application，Server 運行 NFS Server。它們透過 NFS network channel 互動，Workstation 向 Server 發出 request。)

主體

認證：

  • 誰傳送了訊息？

授權：

  • 誰是可信任的？

Principal — "誰" 的抽象：

  • People：Lampson, Taylor
  • Machines：VaxSN12648, Jumbo
  • Services：SRC-NFS, X-server
  • Groups：SRC, DEC-Employees
  • Channels：Key #7438

主體理論

Principal says statement P says s

  • Lampson says “read /SRC/Lampson/foo”
  • SRC-CA says “Lampson’s key is #7438”

Principal A speaks for B A => B 如果 A 說了什麼，B 也說了。所以 A 比 B 強。

一個安全通道： 直接說話 C says s 如果 P 是 C 上唯一的寄件者 C => P

範例

  • Lampson => SRC
  • Key #7438 => Lampson

權限移交

移交規則： 如果 A says B => A 則 B => A 如果 A 有能力且可存取，這是合理的。

範例：

  • SRC says Lampson => SRC
  • Node key says Channel key => Node key

電腦科學中的任何問題都可以透過增加一層間接來解決。(Wheeler)

伺服器認證

(圖示展示了 Workstation 和 Server 之間的認證流程。Logged in user 運行 Excel，透過 NFS network channel 連接到 Server 上的 NFS Server。涉及的 principals 包括 bwl (使用者), WS14 (工作站), Excel (應用程式), SRC-node (伺服器節點), SRC (群組), 以及 keys (Kl, Kws, Kbwl, Kca)。流程顯示了如何從使用者身份和應用程式透過工作站和通道建立一個代表 (SRC-node as Excel) and bwl 的 principal，用於檔案 (file foo) 的存取控制 (may read)。證明鏈涉及 Kca says Kws => WS14, Kca says Kbwl => bwl, SRC says WS14 => SRC-node。)

存取控制

檢查存取： 給定

  • 一個請求：Q says read O
  • 一個 ACL：P may read O

檢查 Q speaks for P (Q => P)

審計 每個步驟都透過以下方式證明其正當性：

  • 一個簽署的陳述，或
  • 一個規則

通道認證

認證 — 誰可以在通道上傳送。 C => P；C 是通道，P 是寄件者。 要獲得新的 C => P 事實，必須信任某個 Principal，即一個憑證授權中心 (Certification Authority)，來告知你。 最簡單的：信任 Kca 認證任何名稱： Kca => Anybody 然後 CA 可以認證通道：

  • Kca says Kws => WS
  • Kca says Kbwl => bwl

群組認證

定義群組：群組是一個 Principal；其成員 speaks for 它。

  • Lampson => SRC
  • Taylor => SRC
  • ...

證明群組成員身份：使用憑證。

  • Ksrc says Lampson => SRC
  • Kca says Ksrc => SRC

(圖示與伺服器認證圖示相同，但強調了群組 SRC 和群組成員身份證明在認證流程中的作用。)

安全性：總結

想法

  • 主體 (Principals)
  • 通道作為主體
  • 「Speaks for」關係
  • 權限移交

價值

  • 給出精確的規則。
  • 將其應用於涵蓋許多情況。

參考資料

提示

  • Lampson, Hints for Computer System Design. IEEE Software, Jan. 1984.

規格

  • Lamport, A simple approach to specifying concurrent systems. Communications of the ACM, Jan. 1989.
  • 可靠訊息在 Mullender, ed., Distributed Systems, Addison-Wesley, 1993 (summer) 中

交易

  • Gray and Reuter, Transaction Processing: Concepts and Techniques. Morgan Kaufman, 1993.

安全性

  • Lampson, Abadi, Burrows, and Wobber, Authentication in distributed systems: Theory and practice. ACM Transactions on Computer Systems, Nov. 1992.