← Archive
lm-005259 · 2026-11

SMPDC Paper 04|推測運算與確定性提交:非同步計算進度、版本一致性、權威仲裁與安全恢復

下載 MD 檔 ⬇
title
SMPDC Paper 04|推測運算與確定性提交:非同步計算進度、版本一致性、權威仲裁與安全恢復
english_title
Speculative Execution and Deterministic Commit: Asynchronous Computational Progress, Versioned Consistency, Authoritative Arbitration, and Safe Recovery
series
SMPDC — Stellar Multi-Primary Persistent Diffusive Computing
paper
04 / 11
version
0.1
status
Full Research Manuscript — Proposed Commit Contract and Conditional Propositions; Implementation and Empirical Validation Pending
date
2026-10-16
language
zh-TW
primary_concept_originator
Neo.K
research_collaboration
Aletheia / GPT-6
institution
EveMissLab / 一言諾科技有限公司
canonical_source
UTF-8 Markdown; inline math $...$ ; display math $$...$$
predecessors
SMPDC Paper 00 v0.1 (2026-10-16) · SMPDC Paper 01 v0.1 (2026-10-16) · SMPDC Paper 02 v0.1 (2026-10-16) · SMPDC Paper 03 v0.1 (2026-10-16)
artifact_scope
Speculative-state semantics; authoritative commit protocol; version guards; side-effect isolation; conditional safety propositions; failure and falsification specifications

SMPDC Paper 04|推測運算與確定性提交

——非同步計算進度、版本一致性、權威仲裁與安全恢復

英文題名: Speculative Execution and Deterministic Commit: Asynchronous Computational Progress, Versioned Consistency, Authoritative Arbitration, and Safe Recovery
系列: 群星多主節點持續擴散計算論(SMPDC)
主構想提出: Neo.K
研究協作: Aletheia / GPT-6
機構: EveMissLab/一言諾科技有限公司
日期/版本: 2026-10-16/v0.1
研究成熟度: L0–L1:形式契約、條件性安全命題、反例與實驗設計;尚未建立或測試正式系統。
直接承接: Paper 00–03 [I0–I3]。

作者: Neo.K
日期: 2026-10-16
版本: 0.1


摘要

群星多主節點持續擴散計算論(SMPDC)將多個 CPU 核心承載的持續性主要工作流視為可協作的邏輯節點,由相位呼叫、有界訊息擴散及具型別冗餘資訊協議組織中觀計算。Paper 01 提出主工作流身分與承載映射的分離,Paper 02 定義有界相位擴散及 epoch 靜止偵測,Paper 03 將局部冗餘整合分成 R0 單路、R1 競速、R2 異源佐證及 R3 編碼恢復。然而,資料已到達、候選已驗證、局部工作流完成及擴散世代已靜止,均不足以保證多個持續主節點對共享狀態做出正確、唯一且可恢復的正式修改。

本文提出 SpeculativeCommit Contract v0.1,將計算進度、局部驗證進度、正式提交決策、持久性、狀態可見性與外部效果交付分離。在此模型中,工作流可依具版本的快照產生可撤銷的推測性計算結果;其他節點可在受限規則下消費尚未正式提交的暫態結果,但必須保留依賴血緣與撤銷機制。正式修改須由具權限的提交域驗證輸入版本、讀寫衝突、跨鍵不變量、來源世代及 fencing token,經過原子仲裁,再根據宣告的持久性和可見性契約建立不可混淆的提交紀錄。GPU 僅能提供計算完成或資料可用的證據,不能單靠 kernel 結束事件取得 CPU 世界狀態的提交權。

本文定義多層狀態機、具唯一識別鍵的提交提案、可持久化的仲裁登錄、包含謂詞依賴的版本驗證、具有預寫日誌與重播規則的單域實作策略,以及對外副作用的 Outbox/冪等接收者/補償式交易邊界。本文提出數項條件性安全命題,明示需要原子唯一性、權威 fencing、完整衝突偵測及可恢復日誌等前提;並給出 snapshot isolation 下的 write skew、舊 owner 回寫、GPU 遲到、重送雙重效果和事故後提交結果未知等反例。本文不聲稱發明資料庫交易、線性化、MVCC、共識協議或 CPU 推測執行,而是檢驗其正確性條件如何在「多主 CPU 工作流+相位擴散+局部冗餘聚合+異質執行」中形成一個可編譯、可觀測、可反證的提交層。

在效能層面,本篇不預設推測運算會加速所有任務。系統必須比較可撤銷工作所省下的關鍵路徑等待,與錯誤推測、狀態複製、版本驗證、提交序列化、GPU 同步、日誌、回滾及重試所付出的完整成本。最後提供可在普通 CPU、現有 RTX 3070 及確定性模擬器上展開的 V0–V1 計畫,為 Paper 05 的擴散指令集與 Paper 06 的程式語言效果型別系統提供可檢查的提交原語。

關鍵詞: 推測性計算、持續主工作流、權威提交、原子仲裁、版本驗證、MVCC、snapshot isolation、serializability、linearizability、fencing、預寫日誌、Outbox、回滾、補償交易、GPU 同步、可證偽系統設計。


1. 本篇真正要解決的問題

1.1 快速計算與可發布結果是兩件事

在傳統序列程式中,計算與狀態寫入往往在同一執行緒內依程式順序發生。SMPDC 的多主工作流模型則可能同時出現:

  1. PWN-A 持續處理某個 AI 訓練 step 的局部輸入;
  2. PWN-B 根據 A 的暫態輸出啟動下一段工作;
  3. PWN-C 用 R2 產生不同算法的佐證;
  4. PWN-D 將某些批量運算交由 GPU;
  5. 先完成的候選經 Paper 03 聚合器驗證;
  6. 原始快照卻已被另一項正式操作改變。

第六項使前五項不能直接視為可正式寫入。局部計算結果可能完全符合舊輸入,卻不再符合現在的世界狀態。這是本篇的出發點,不是對 GPU、CPU 或 AI 正確性的否定。

1.2 核心研究問句

RQ04-1|進度: 哪種工作可以先行、哪種輸出只能留在暫態域,何時才可越過正式可見性邊界?

RQ04-2|權威: 多個「主要」工作流如何保持本地自治,同時避免對相同受控狀態出現多個互相矛盾的最終決策?

RQ04-3|一致性: 如何判定版本過期、讀寫衝突與跨鍵不變量破壞?snapshot 相同是否足以保證安全?

RQ04-4|恢復: 若在提交判斷、日誌持久化、公開可見或向外部服務送出效果之間崩潰,系統能否恢復並避免重複生效?

RQ04-5|效能: 在何種 AI/非 AI 工作負載及故障率下,推測提前量大於仲裁、重播及資料搬運成本?

1.3 本篇新增六項契約

  • SpeculativeBranch Contract v0.1:限定推測分支如何建立、引用、失效與安全撤銷。
  • CommitProposal Envelope v0.1:將局部聚合輸出轉成可受權威層審查的型別化提案。
  • CommitAuthority & Fencing Contract v0.1:定義提交域、原子仲裁、世代及寫入租約。
  • Consistency & Isolation Contract v0.1:指定讀寫集合、謂詞、衝突和可見性等級。
  • Effects & Recovery Contract v0.1:持久化、外部效果、回滾、重播及不確定結果處理。
  • V0/V1 Falsification Protocol v0.1:可建立反例的有限模型、故障注入及效能 A/B 規格。

1.4 本篇不處理、也不宣稱的事

  • 不重寫 Paper 02 的 credit 擴散系統或 Paper 03 的候選血緣;沿用其鍵和證據。
  • 不把「確定性提交」解讀為任意分散節點都能在沒有協調、儲存或同步成本下完成原子提交。
  • 不把 CPU 微架構的分支預測、投機管線、Intel TSX 等同於本篇的 Runtime 級推測分支。
  • 不從多主工作流的存在推出「所有資料均可無鎖寫入」。
  • 不宣稱每個核心都可成為同一份全域狀態的無條件寫入權威。
  • 不聲稱「兩次執行、一次提交」自然等於任意外部系統的端到端 exactly-once。
  • 不把抽象的協議安全條件冒充已完成 TLA+ 模型檢查的結果。

2. 與 SMPDC Paper 00–03 的正式銜接

2.1 不更換九元中觀系統

承接 Paper 00 的系統:

St=⟨Vt,Et,Xt,Φt,ρt,Mt,Qt,Rt,Lt⟩.\mathfrak{S}_t=\langle V_t,E_t,X_t,\Phi_t,\rho_t,\mathcal{M}_t,\mathcal{Q}_t,\mathcal{R}_t,\mathcal{L}_t\rangle.

本篇不更動任何已有符號的先驗語義,而是在 XtX_t 中區分暫態狀態與正式可見狀態,在 Qt\mathcal{Q}_t 中擴充驗證/提交契約,在 Lt\mathcal{L}_t 記錄可重演的提交決策與責任,並在 Rt\mathcal{R}_t 加入提交成本、持久化資源與外部效果預算。 VtV_t 的成員仍是邏輯主工作流,不直接等於實體 CPU 核。

2.2 接受 Paper 01 的主節點契約

每個 Primary Workflow Node(PWN)保有 flow_id、generation、fencing_token、局部狀態、持續責任及合法承載位置。工作流可提出結果或執行本地可授權的修改;是否能對某個受控提交域發出最終決策,必須另有 commit_capability。

基本不等式:

Primary⁡(f)⇏CommitAuthority⁡(f,d).\operatorname{Primary}(f)\not\Rightarrow\operatorname{CommitAuthority}(f,d).

多主意味有多個自治執行源,不意味多個無協調的同域最終仲裁者。

2.3 不跨越 Paper 02 的擴散責任帳本

Paper 02 的 event_epoch、topology_generation、send_credit_id、背壓、期限、依賴守衛與控制消息保留額度依然成立。推測分支所產生的後續擴散消息,必須按原協議重新計入義務;不能因為已在本地暫態域運行,就把網路或核心間開銷視為免費。

此外:

EpochQuiescent⁡(e)⇏Committed⁡(e).\operatorname{EpochQuiescent}(e)\not\Rightarrow\operatorname{Committed}(e).

「消息已清償」不等於「有合法提交決策」。

2.4 Paper 03 的輸入形狀

本篇接受下列既有輸出,不自行修改 Paper 03 的欄位定義:

LocalReconciliationOutcomeV0_1 {
    result_key, event_epoch, input_snapshot_id
    plan_id, plan_version, round_id
    owner_flow_id, owner_generation, owner_fencing_token
    mode, terminal_state
    selected_candidate_ids, valid_shard_ids
    comparison_evidence_ref, provenance_ref
    verification_policy_id, local_verification_status
    audit_trace_ref, outstanding_obligation_summary
}

local_verification_status 只描述聚合器在當地證據政策下的判定;selected_candidate_ids 只說明可供提案者選擇的候選血緣。它們既不是提交序號,也不會自動成為授權 token。

2.5 重要的三條不可推論鏈

Received⁡⇏VerifiedLocal⁡,\operatorname{Received}\not\Rightarrow\operatorname{VerifiedLocal}, VerifiedLocal⁡⇏AuthorizedToCommit⁡,\operatorname{VerifiedLocal}\not\Rightarrow\operatorname{AuthorizedToCommit}, DecisionCommitted⁡⇏EffectDelivered⁡.\operatorname{DecisionCommitted}\not\Rightarrow\operatorname{EffectDelivered}.

這三個反蘊含是本篇形式規範、程式語言效果型別和 V0 模型檢查的共同起點。


3. 推測運算的多層進度與六種完成意義

3.1 計算進度(Compute Progress)

計算進度表示一個工作流完成了多少尚未要求公開生效的計算步驟。它可以包含本地推導、GPU kernel 完成、候選比較、暫態資料生成或預計算。執行完畢不代表此計算的輸入版本依然有效,也不能排除其他工作流對狀態的合法更新。

3.2 局部證據進度(Local Verification Progress)

此層由 Paper 03 的驗證政策主導。通過版本化 schema、來源、內容、算法或獨立佐證檢查之後,可產生 LocalVerified,但不得省略全域提交域的狀態驗證。

3.3 提交準備度(Commit Preparedness)

某個候選已具備完整 read-set、write-set、預期副作用、權限與隔離規則,稱為 PreparedCandidate。準備好接受仲裁不代表仲裁已勝出。

3.4 正式提交決策(Commit Decision)

對某個提交鍵 kk,權威系統在原子仲裁中決定 Commit 或 Abort,並使決策符合宣告的一致性等級;此層需區分:

  • DecisionRecorded:決策已進入權威日誌;
  • DecisionDurable:若配置為持久提交,所需存儲與複本條件均已完成;
  • StateVisible:符合隔離規則的觀察者可看見該決策對狀態的影響。

不同實作可以藉原子提交點將部分階段合併,但不能因使用相同名稱就省略必需的同步與失敗語義。

3.5 外部效果進度(Effect Progress)

發郵件、呼叫第三方 API、付款、改寫遠端資料庫、輸出不可撤回的對外訊息等,均是正式世界的效果。即使本地交易已提交,外部效果仍可處於 Pending、Delivering、Acknowledged 或 Unknown,不能因本地提交就宣稱已發送成功。

3.6 讀者可見進度(Observer Progress)

可視化進度條、log、AI streaming token 或暫態介面更新可能先於最終提交,但它們必須清楚標記 provisional。如果暫態訊息已被外部消費並觸發無法回復的行動,就不能假裝它仍可撤銷。

本篇將六層進度寫成:

P(c,t)=⟨pc,pv,pp,pd,pe,po⟩.\mathcal{P}(c,t)=\langle p_c,p_v,p_p,p_d,p_e,p_o\rangle.

每一軸可獨立演進,不能將六元進度簡化為一個 0–100% 的「成功率」。


4. 暫態空間、分支身分與生命週期

4.1 SpeculativeBranch 最小定義

對候選計算 cc,一個推測分支由七個元素組成:

Bc=⟨Kc,Sc,Dc,Rc,Wc,Fc,Qc⟩.B_c=\langle K_c,S_c,D_c,R_c,W_c,F_c,Q_c\rangle.
  • KcK_c:與 Paper 03 相容的結果/候選/分支身分及世代;
  • ScS_c:不可變輸入快照參照,並包含有效期限/版本證書;
  • DcD_c:因果依賴與 upstream tentative dependencies;
  • RcR_c:讀取集合(含可觀察謂詞或範圍);
  • WcW_c:待寫入之變更集合或純結果;
  • FcF_c:副作用提案與效果政策,絕不直接表示已發送;
  • QcQ_c:資源信用、風險界限、質量契約與撤銷規則。

此七元組並不另立一套全域計算本體,只在 \mathfrak{S}_t 之上描述一次尚未完成權威決策的分支。

4.2 生命週期狀態

CREATED
  -> ADMITTED
  -> EXECUTING
  -> RESULT_READY
  -> LOCAL_VERIFIED
  -> PREPARED
  -> COMMIT_REQUESTED
  -> DECISION_PENDING
  -> COMMITTED  -> PUBLISHED
                   -> EFFECTS_PENDING -> EFFECTS_SETTLED

任一尚未 COMMITTED 的許可轉移:
  -> INVALIDATED -> DISCARDED
  -> ABORTED     -> RETRY_ELIGIBLE / CLOSED
  -> CANCELLED   -> CLOSED
  -> UNKNOWN     -> RECONCILE_WITH_AUTHORITY

圖中的 COMMITTED 僅指已完成宣告的權威決策與耐久性契約;效果結算可以較晚。各狀態的落點由實作決定,但名字不能取代原子條件。

4.3 推測性讀取的三種來源

穩定已提交快照: 讀取明確版本、合法一致性層級的正式狀態。

另一推測分支: 允許以受限 provisional token 讀取,但需攜帶祖先依賴和 invalidation hook。

未完成的 GPU 結果: 只有設備執行完成與必要資料可見性規則都滿足,才算有效輸入;仍不表示 GPU 結果能正式提交。

4.4 暫態輸出必須不可被誤認為正式資料

建議把 Tentative<T,branch_id,snapshot> 與 Committed<T,domain,commit_index> 作為語言/IR 可辨的不同型別。即使記憶體位置相同,能力與對外可見性也不同。若實作透過原地更新加回滾日誌模擬暫態狀態,必須證明隔離和恢復等價,不能因省略拷貝就自然假定安全。

4.5 暫態資料何時可以安全釋放

至少要求:該分支及其合法後代都不再持有參照、相關設備使用已完成或明確取消、撤銷回呼已收斂、審計/除錯保存政策已滿足、以及沒有仍可能回到同一版本的合法重試。所需內存回收機制可以是 epoch-based reclamation、引用計數或其他方法,不能由 ABORT 一詞自動推定回收安全。


5. 因果依賴、相位觸發與推測視窗

5.1 相位呼叫不等於提交權限

承接 Paper 02,ready、causal、sync、recur、semantic 與 verify 相位可以影響互動資格、資料路由和計算準備度。只有當某個相位屬於提交契約明確驗證的 guard,才會成為合法提交條件;phase=ready 本身不能授權寫入。

5.2 依賴圖與撤銷傳播

設推測分支集合為 Bt\mathcal B_t,有向邊 (bi,bj)(b_i,b_j) 表示後者消費前者的暫態資料。若 bib_i 失效,則所有依賴其不可安全重建的後代都必須失效或重新驗證。

Invalid⁡(bi)∧(bi⇝bj)⇒ValidateAgain⁡(bj)∨Abort⁡(bj).\operatorname{Invalid}(b_i)\land(b_i\leadsto b_j) \Rightarrow\operatorname{ValidateAgain}(b_j)\lor\operatorname{Abort}(b_j).

此為語義約束;其正確實作尚需解決並行撤銷與後代提交競速。若允許合法的依賴切割或已提交等價值替代,必須有明確證書,不能任意刪除因果邊。

5.3 有界推測視窗

至少限制:

  • 每工作流最大未提交分支數 bib_i ;
  • 每提交域的未決提案數 qdq_d ;
  • 推測深度 hspech_{spec} ;
  • 暫態總位元組容量 mspecm_{spec} ;
  • 最大等待/重試次數與最小強制收斂策略;
  • 依賴父節點跨版本變動的容許規則;
  • 設備核發的未完成 kernel/event 數量;
  • 不可撤銷效果的絕對禁止邊界。

即使每個分支都有限,若外部持續產生新根事件,整套系統仍可能長期不靜止;因此仍需入流控制和背壓。

5.4 推測準確率不能偷換成提交率

令 NsN_s 為啟動的推測分支數, NvN_v 為局部驗證通過數, NcN_c 為正式提交決策數。可量測比例為:

ηlocal=Nvmax⁡(1,Ns),ηcommit=Ncmax⁡(1,Ns).\eta_{local}=\frac{N_v}{\max(1,N_s)},\qquad \eta_{commit}=\frac{N_c}{\max(1,N_s)}.

兩者不必相等。即使 ηlocal=1\eta_{local}=1,如果輸入狀態常常過期,正式提交率仍可能很低。

5.5 何時不應推測

只要分支具有不可隔離效果、回滾代價遠高於可節省的等待時間、讀寫衝突密度高、工作極短、GPU 排隊長或其他候選難以驗證,系統應允許直接退回普通序列/非推測執行。沒有推測的有效基線是本理論的一部分,不是實作失敗。


6. 權威提交域與授權分工

6.1 提交域的最小概念

一個 CommitDomain 是在指定權限、可見性和故障模型內,對某些狀態與其不變量做出最終決策的邏輯邊界。它可映射到一個受鎖保護的記憶體物件、一個本機 transactional store、資料庫分區或具有共識機制的複製狀態機;不能僅憑名稱推定它必然跨機容錯。

6.2 多主執行和單次決策的相容性

工作流 f1,…,fnf_1,\ldots,f_n 可並行提案:

{P1,P2,…,Pn}⟶Ad,\{P_1,P_2,\ldots,P_n\}\longrightarrow A_d,

其中 AdA_d 是提交域 dd 的仲裁介面。它可以由可擴展的多副本系統提供,但對同一提交鍵必須具有明確、可測試的原子一致性語義。一個邏輯權威不必等於一顆永久中央 CPU。

6.3 四種權限必須分離

權限/能力 可以做什麼 不能自動做什麼
compute_capability 使用授權算力執行分支 修改正式狀態
reconcile_capability 在指定結果域比對與聚合候選 取得新提交權
proposal_capability 送出具型別提交請求 保證請求會被接受
commit_capability 在授權域內啟動原子仲裁 越過安全檢查或改寫其他域

再將 effect_delivery_capability 獨立出來,避免有提交能力的程序在缺乏對外效果政策時直接發送外部訊息。

6.4 提交鍵(Commit Key)

對一個正式修改目的,定義:

k=(d,e,o,σ,ν),k=(d,e,o,\sigma,\nu),
  • dd:提交域;
  • ee:事件/授權世代;
  • oo:穩定的邏輯操作身分;
  • σ\sigma:業務/計算語義版本;
  • ν\nu:目標提交命名空間(例如訓練 run 與 step)。

提交鍵與 Paper 03 的 result_key 相關但不相同。一次邏輯操作可能有多個候選結果;它們可以競逐同一提交鍵。computation_attempt_id、路徑 attempt、重發序號及 PWN 目前綁在哪顆核心,都不能擅自改變提交鍵,否則重送可能被當成新交易。

6.5 同鍵異載荷應拒絕而不是覆寫

提交域可記錄 candidate_digest、提案版本與決策結果。若同一 kk 後續帶來不同 payload,回傳 ConflictSameKey 或既有決策的安全讀回,不得覆寫已決定的內容。為防止 hash collision/schema 混淆,必要時應保存完整比較所需指紋與版本規則。

6.6 提交順序是邏輯順序,不必是全系統單一時鐘

同一提交域可以定義全序提交索引 ℓd\ell_d ;跨不同域則未必有單一總序,也不必如此設計。若跨域不變量要求一致,必須引入額外協調協議、共同仲裁域或明確限制可獨立提交的操作類型。


7. CommitProposalEnvelopeV0_1:局部候選如何變成正式提案

7.1 必須承接而非取代既有證據

Paper 03 的 LocalReconciliationOutcomeV0_1 仍是上游 canonical 局部結果。Paper 04 的封套以不可變參照及版本化 metadata 指向它;不能只複製一個 LocalVerified=true 字串就跳過候選、來源及比較證據。

CommitProposalEnvelopeV0_1 {
    schema_id: "smpdc.commit-proposal"
    schema_version: 1

    commit_domain_id: DomainId
    commit_key: StableCommitKey
    logical_operation_id: StableOperationId
    event_epoch: EventEpoch
    topology_generation: TopologyGeneration

    proposer_flow_id: StableFlowId
    proposer_generation: MonotonicGeneration
    proposer_fencing_token: AuthenticatedFencingToken
    commit_capability_ref: ScopedCommitCapability

    reconciliation_outcome_ref: ImmutableOutcomeReference
    result_key: LogicalResultKey
    selected_candidate_ids: NonemptyCandidateSet
    verification_policy_id: RegisteredPolicyId
    local_evidence_ref: ImmutableEvidenceReference

    input_snapshot_id: SnapshotId
    read_set_ref: CanonicalVersionedReadSet
    predicate_dependencies_ref: OptionalPredicateReadSet
    write_set_ref: CanonicalVersionedWriteSet
    tentative_parent_commit_keys: BoundedDependencySet
    expected_domain_version: OptionalVersion
    consistency_contract_id: RegisteredIsolationContract

    effect_plan_ref: TypedEffectPlan
    rollback_policy_id: RegisteredRollbackPolicy
    semantic_schema_version: SchemaVersion
    numerical_contract_ref: OptionalNumericalContract

    proposal_digest: VersionedDigest
    request_nonce: DeliveryAttemptNonce
    expiry_rule: ExplicitExpiryPredicate
    trace_id: StableTraceId
}

request_nonce 用於辨認提交請求配送嘗試,不可成為新的提交鍵。可按傳輸技術使用不可變資料參照而不是傳送完整候選;但 side table 的權限、版本、生命週期及不可變性仍須可驗證。

7.2 提案接收的必要檢查順序

  1. 驗證封套版本、大小、欄位互斥性與內容界限。
  2. 驗證提交域、操作身分、event_epoch 及 namespace 契約。
  3. 驗證工作流身分、來源 generation 和 fencing token。
  4. 驗證 proposal/commit/effect 能力是否在相同作用域內有效。
  5. 讀回 Paper 03 局部結果,確認所引用候選及證據沒有被替換。
  6. 驗證快照、讀寫集合、謂詞依賴及數值/語義版本。
  7. 檢查前置的暫態祖先是否已正式提交,或本次是否為受支援的共同原子提交。
  8. 進入對該域宣告的原子衝突與不變量仲裁。
  9. 依持久性政策登錄 COMMIT/ABORT 決策。
  10. 對正式狀態發布可見性,再使外部效果進入可交付狀態。

不同層可以在內部實作中合併,但檢查的邏輯依賴順序不得被破壞。第 8 至第 10 步之間若可能發生競爭,需要交易化或可證明等價的同步機制。

7.3 拒絕的原因不能被折成一個布林值

CommitDecisionStatus =
    Committed(commit_index, durability_class)
  | Aborted(reason, retry_class)
  | AlreadyDecided(existing_decision_reference)
  | InvalidScope(reason)
  | StaleOwner(current_generation)
  | StaleSnapshot(conflict_witness)
  | IsolationConflict(conflict_class)
  | InvalidEvidence(proof_or_schema_error)
  | MissingDependencies(missing_commit_keys)
  | ResourceDenied(resource_kind)
  | UnknownDecision(query_handle)

UnknownDecision 不等於 Aborted;網路中斷或進程崩潰後,發送者通常不能僅依 timeout 猜測交易是否已提交。實作應按穩定提交鍵查詢,且若需要重試,使用同鍵冪等提案規則。

7.4 提案不是許可證書

LocalVerified、Proposed、Prepared、Committed 是不同型別,應當禁止未經守衛的自動轉型:

LocalOutcome  -> CommitProposal        // requires proposer capability
CommitProposal -> PreparedCandidate    // requires validation
PreparedCandidate -> CommitDecision    // requires authority arbitration
CommitDecision -> CommittedValue       // requires visibility/durability contract
CommittedValue -> ExternalEffect       // requires effect delivery policy

Paper 05/06 將把這種效果分離發展為指令效果與靜態/動態型別守衛;本篇只定義最低協議。


8. 版本化狀態、讀寫集合與提交一致性

8.1 版本狀態表示

令正式狀態由版本化物件集合構成:

Xd={(x,value⁡(x),ver⁡(x))∣x∈Dd}.\mathcal X_d=\{(x,\operatorname{value}(x),\operatorname{ver}(x))\mid x\in D_d\}.

每一個推測分支記錄取得其輸入的快照資訊 SbS_b,以及可供提交驗證的讀集 RbR_b 、寫集 WbW_b 和謂詞依賴 PbP_b。

讀集應含每個讀取版本及其語義;寫集應包含期望舊版、候選新版與更新意圖。對範圍/集合查詢,只記錄已返回的元素可能不足以偵測 phantom 或 write skew。

8.2 單物件 CAS 不是完整交易隔離

對一個單獨的原子資料格,可以使用比較並交換來避免某些重疊寫入。但當操作需要維護 x+y≥1x+y\ge 1 等跨物件不變量時,即使所有單鍵寫入都是原子的,整體仍可能違反約束。故原子性、隔離、持久性與正確性分別有不同證明義務。

8.3 樂觀驗證的最小守衛

對 OptimisticValidate(b),必要但一般不足的條件可寫成:

∀x∈Rb:ver⁡now(x)=ver⁡snap(x).\forall x\in R_b:\operatorname{ver}_{now}(x)=\operatorname{ver}_{snap}(x).

此形式只適用於完整讀集被追蹤,且對相關變更可觀察的限定模型。涉及 range query、索引謂詞或變動的外部資源時,還必須有對應的 predicate/version range guard。

8.4 最小一致性等級表

宣告等級 可接受模型示例 應防範的錯誤 備註
LocalAtomic 單受控物件的線性化操作 兩個核心同時改同物件 不等於跨鍵 serializability
PerKeySerializable 對每鍵的原子順序 相同鍵衝突 跨鍵約束仍可能失效
SnapshotConsistent 版本化一致快照 dirty/inconsistent read 單純 snapshot isolation 仍可有 write skew
Serializable 與某個合法序列交易次序等價 write skew、幻讀等致命異常 需要合適的並行控制與重試
LinearizableOperation 符合實時先後次序的單操作語義 回應前後的違序可見性 與交易 serializability 不是同義詞
CrossDomainCoordinated 明確的跨域原子或補償協議 雙重提交與部分可見 需具體指明共識/協調/補償成本

這些名稱是 SMPDC 建議的 API 需求等級,不是宣稱任何關聯式資料庫會原生使用完全相同的 enum。正式實作須映射到該儲存系統真正提供的隔離語義。[E1–E4]

8.5 write skew 反例:兩個分支都通過局部快照

設共同約束為 至少有一名值班者:

已提交狀態: Alice=ON, Bob=ON

T1 在快照 v10 讀取 (Alice=ON, Bob=ON)
T2 在快照 v10 讀取 (Alice=ON, Bob=ON)

T1 驗證局部條件後只寫入 Alice=OFF
T2 驗證局部條件後只寫入 Bob=OFF

寫集不重疊;若只檢查 write-write conflict,兩者可能均提交。
最終狀態: Alice=OFF, Bob=OFF
業務不變量遭破壞。

這是隔離層次的反例,不是 CPU 多核心的硬體 bug。解法可以是可序列化驗證、明確鎖定共同謂詞、單一仲裁物件或改寫資料模型,使共享約束在提交點被原子檢查。不能僅靠消息重複驗證、加大 CPU 或更多 GPU kernel 消除。

8.6 read-only 分支也需要快照契約

讀取操作沒有寫集,不意味一定可隨時被正式輸出。例如讀取途中跨多個資料物件取得混合版本,可能生成從未存在於任何合法狀態的輸出。若應用只需要 best-effort analytics,允許較弱快照;若結果會成為後續正式提交的 guard,必須有與之相符的版本證明。

8.7 計算決定性與交易決定性

相同輸入在固定數值規則下給出相同候選,不表示提交順序固定。多個候選在不同時刻通過仲裁,可能產生不同但仍合法的提交歷史。因此:

DeterministicCompute⁡⇏DeterministicHistory⁡.\operatorname{DeterministicCompute}\not\Rightarrow\operatorname{DeterministicHistory}.

若要「相同輸入與相同事件序列產生完全相同正式結果」,需固定被允許的仲裁順序、數值規約與所有外部輸入;這是比局部可重現運算更強的模型。


9. 世代、權威租約與 fencing

9.1 為何只檢查 lease 時間不足

舊 PWN 可能在租約到期前進入暫停,直到新 owner 已經取得權限之後才恢復。如果舊 PWN 只根據自己記憶中的「租約有效」或已保存的 API token 進行寫入,就可能破壞新的正式狀態。作業系統時間、CPU clock 或簡單 timeout 無法自行解決此問題。

9.2 受保護資源必須驗證 fencing token

設提交域 dd 持有單調增加的世代 gdg_d。合法寫入者應攜帶同域受信 token fdf_d ;權威存儲在原子仲裁時驗證:

Permit⁡(b,d)⇒(gb=gd)∧(fb=fd)∧ScopedCap⁡(b,d).\operatorname{Permit}(b,d)\Rightarrow (g_b=g_d)\land(f_b=f_d)\land\operatorname{ScopedCap}(b,d).

上述規則是參考契約的一種實作形式。若系統採比單調數字更強的 capability revocation/epoch fencing,也需證明舊寫入者無法在新世代正式生效。

9.3 遷移與提交競速

初始: Owner A, generation=12, fence=901

A 準備提交 proposal P
A 停頓
權威域完成交接: Owner B, generation=13, fence=902
B 成功提交同鍵的 proposal Q
A 恢復並重送 P

期望: A 的舊 fence 必須在權威點被拒絕。

如果 A 的請求已在交接前通過原子提交點,則 B 應讀到它已決定;若 A 尚未跨過提交點,則交接後 A 不得宣稱自己仍有寫入權。沒有原子仲裁位置的實作無法僅靠設計圖排除兩者競速。

9.4 提交權與計算權可以轉移不同步

A 失去 commit_capability 之後,可能仍在計算或保有暫態記憶體;其結果可依版本契約作為普通 candidate 移交給 B,但不得繼續使用 A 的舊權威世代。PermitCompute、PermitEmitMessage 和 PermitCommit 為不同權限。

9.5 防止 ABA 版本混淆

單純比較目前 value 與先前 value 可能無法辨別資料經歷 A→B→A 的變更。若同值仍可能代表不同因果史,須使用單調版本號、不可重用物件 incarnation 或其他能排除 ABA 的標記。快照哈希也不應獨自取代必要的因果版本及 schema 身分。


10. 正式提交狀態機與兩個原子邊界

10.1 CommitRecord 的不可混淆欄位

CommitRecordV0_1 {
    commit_key: StableCommitKey
    domain_id: CommitDomainId
    decision: Commit | Abort
    decision_index: MonotonicDomainIndex
    authority_generation: MonotonicGeneration
    authority_fence: VerifiedFencingToken
    accepted_proposal_digest: VersionedDigest
    read_snapshot_ref: SnapshotReference
    validation_witness_ref: EvidenceReference
    resulting_write_set_digest: Digest
    resulting_state_version: OptionalNewVersion
    durability_class: Volatile | ProcessRecoverable | CrashDurable | ReplicatedDurable
    publication_state: Unpublished | Visible
    effect_intent_ref: OptionalOutboxRef
    created_by_authority: AuthenticatedAuthorityId
    trace_id: TraceId
}

durability_class 是契約聲明,不表示每一種底層存儲都可達成。ProcessRecoverable、CrashDurable 和 ReplicatedDurable 的故障模型也不同;例如本機 WAL 不能保證主機或儲存媒體完全毀損後仍可恢復。

10.2 原子邊界 A:狀態驗證與決策記錄

對一致性要求為 Serializable 的提交域,版本/謂詞驗證、唯一鍵決策、所需不變量與被保護的狀態更新必須具有一個可證明的交易化臨界區,或在可重演的狀態機中產生等價的可序列化結果。

禁止: 將「先在鎖外檢查版本」「後來在鎖外寫入」當作一個原子操作。

10.3 原子邊界 B:權威決策與正式可見性

當系統宣稱 CrashDurable,對外回報成功前應確保承諾所需的持久化完成,並保證恢復時可重建已承諾的決策。可採 log-before-data/redo、copy-on-write + root swap、合適的交易儲存等方式。

不要求所有正式狀態頁面都必須在 ack 前落盤;WAL 類方案可透過先持久化必要日誌再恢復性套用狀態頁面達到安全。但不能因稱作「WAL」就省略同步、刷盤與重演正確性檢查。[E5]

10.4 參考單域決策程序(概念偽程式碼)

function commit_single_domain(proposal):
    assert_schema_and_bounds(proposal)
    assert_authenticated_scope(proposal)

    authority.atomic_scope(proposal.commit_domain_id):
        old = ledger.find(proposal.commit_key)
        if old exists:
            return stable_replay(old)  // reject if different payload policy

        if not valid_owner_generation_and_fence(proposal):
            return StaleOwner

        if not local_evidence_matches(proposal):
            return InvalidEvidence

        if not dependencies_committed(proposal):
            return MissingDependencies

        if not isolation_validation_passes(proposal):
            return IsolationConflict

        if not invariant_guards_pass(proposal):
            return Aborted(InvariantViolation)

        record = build_commit_record(proposal, next_domain_index())
        append_to_transactional_log(record, proposal.write_set, proposal.outbox)
        ensure_required_durability(record)
        publish_or_schedule_replay(record)
        return Committed(record.commit_key, record.decision_index)

上列 authority.atomic_scope 是需要工程實作證明的規格級抽象。它可以映射到合適的交易型 KV Store、資料庫、可序列化操作或複製狀態機;若其底層先持久化才發布可見性,應以正式恢復規格定義崩潰窗口。此偽程式碼不可直接當作已具原子/耐久保證的生產程式。

10.5 已存在決策時的重放策略

同鍵新請求若與既有已決定記錄相容,返回既有結果(AlreadyDecided);若新 payload 衝突,返回 ConflictSameKey。已持久化的 COMMIT 不可因另一副本稍後抵達就被改寫為 ABORT;若業務必須修正已提交狀態,應提交新操作,清楚保留修正血緣。

10.6 為何不以全球大鎖當作最終設計

全域互斥可以做最小正確性基線,但有吞吐瓶頸,且與「多主」的效率目標衝突。SMPDC 不預設永遠只有一個仲裁鎖;獨立提交域、可交換更新及可證明的分區策略應允許並行。但若跨域存在共享不變量,則不可為了性能直接刪除所需協調。


11. 決策持久化、WAL、重播及結果未知

11.1 崩潰窗口分類

崩潰時機 是否可能正式提交 恢復程序
A. 產生暫態分支前 否 可重新執行原操作
B. 暫態計算中 否 丟棄/重建分支,清償義務
C. LocalVerified 後、仲裁前 否 重新驗證版本及權限
D. 仲裁中、決策尚未可信持久化 未知 先查權威恢復後日誌,勿推測結果
E. durable COMMIT 已寫、狀態頁未更新 是,依契約 redo 或發佈已提交 root
F. 狀態可見、效果仍未送出 是,本地 處理 outbox,不重提狀態交易
G. 效果可能送達、ACK 遺失 本地已是 用穩定 effect key 查詢/冪等重試

在第 D 類,使用者或提交者不應因為 timeout 就說「確定失敗」。先處理 UnknownDecision,讓權威在恢復後提供可檢驗的結果。

11.2 WAL 的基本正確性條件

對 CrashDurable,至少要求:

  1. 需要重演的資料及 commit 決策先於成功回覆達到所宣告的穩定存儲條件;
  2. 日誌 record 的順序、checksum/校驗和 schema 有明確規範;
  3. 恢復算法對已提交操作只套用一次邏輯效果,或具冪等 redo;
  4. 未提交的暫態寫入不會被當作正式狀態;
  5. 錯誤的 checkpoint/log truncation 不能刪除尚需回復的證據;
  6. 任何跨記錄的不變量受同一適用的交易/恢復協議保護。

這些屬成熟交易技術的使用條件,不是 SMPDC 原創的 WAL 定理。[E5]

11.3 durable record 與 memory visible 的排序

建議宣告兩個明確點:

  • durable_decision_point:已無法在所承諾的故障模型內遺失決策;
  • visibility_point:其他正式讀者可按指定隔離契約觀察到其結果。

如需保證「已回覆成功的操作必須對後續合法讀者可見」,不得在尚未滿足可見性契約時提前回覆;否則只能承諾較弱的異步可見性。請勿用「寫入完成」同時代表日誌 append、fsync、redo 與讀者可見。

11.4 分支重播與結果可重現

重播必須分兩種:

重播提交日誌: 恢復權威已決定的正式狀態;應禁止外部效果重複執行。

重跑推測計算: 可以重新生成候選與證據;若程序含時間、隨機數、非決定性 GPU reduce、外部讀取或浮點順序差異,則必須固定其來源、比較契約或允許合法的非逐位一致結果。

「同一提交歷史可恢復」不代表「每次重跑訓練都會逐 bit 相同」。兩者是不同的研究目標。

11.5 防止無限重試與紀錄膨脹

對 retry 應有上限、指數退避或調度 fairness 策略;某些永久版本衝突應重新規劃而非單純重送同一舊快照。日誌、tombstone 和 dedup 保留期限必須長於相關合法重試窗口或由其他不可重用世代規則取代;若提早刪除,重送可能再次生效。


12. 外部副作用:不能靠本地回滾魔法消除

12.1 效果型別分類

效果類型 實例 推測期允許? 提交後安排
Pure 在私有資料上算術、解析、比較 可以 不需要效果交付
SnapshotRead 讀取具版本快照 可以(記錄版本) 提交前仍需檢查
LocalReversible 暫態 arena 或 shadow copy 可以(有回收契約) 發布或丟棄
BufferedObservable 暫存訊息、進度事件 僅作 provisional 確認或撤回標示
OutboxMediated 交易消息、可冪等 API 呼叫 先記錄 intent 由合法 delivery worker 執行
Irreversible 不可撤回金流、物理控制、外部公開行動 不可先行發出 明確授權、提交及效果政策

部分外部操作可能具有補償行動,但「可補償」不等於已發生的歷史可以被刪除。退款不等於原付款從未存在,撤稿也不等於讀者從未看過資訊。

12.2 交易式 Outbox 的位置

若正式狀態變更與對外發送意圖落在同一支援原子交易的存儲邊界,可把狀態與 outbox intent 一起提交,再由 delivery worker 讀取 outbox 並向外部投遞。這避免本地「先寫狀態、後發事件」的常見 dual-write 崩潰窗口,但交付者仍可能因 ACK 遺失重複投遞;消費端需要穩定的效果鍵和冪等處理/查詢機制。[E6]

12.3 EffectIntentV0_1

EffectIntentV0_1 {
    effect_key: StableEffectKey
    parent_commit_key: StableCommitKey
    parent_commit_index: MonotonicDomainIndex
    effect_kind: RegisteredEffectKind
    target_authority: AuthorizedTargetRef
    payload_ref: ImmutableVersionedPayload
    receiver_idempotency_key: OptionalStableKey
    delivery_policy: AtLeastOnce | QueryBeforeRetry | ManualResolution
    compensation_policy_ref: OptionalCompensationPolicy
    authorization_scope: ScopedEffectCapability
    status: Pending | Delivering | Acknowledged | Unknown | Failed
}

AtLeastOnce 在缺少消費端去重時,可能重複產生業務效果; QueryBeforeRetry 的安全性取決於目的端是否提供可靠查詢和一致鍵; ManualResolution 用於無法判定是否已生效且不能安全重試的情況。

12.4 exactly-once 的三個分界

  1. At-most-once commit record: 同一提交鍵至多有一個成功的權威決策,可在指定模型中成立。
  2. Exactly-once logical state effect: 若內部重演具冪等且交易記錄完整,可以在特定受控資料域內實作。
  3. Exactly-once arbitrary external action: 對不受控第三方、不可查詢效果或不支援冪等鍵的服務,無法由本地提交日誌單方面保證。

本篇只提出第 1 和有條件的第 2;不無條件聲稱第 3。

12.5 補償交易不是 rollback

Saga/補償式流程允許已正式發生的操作由後續反向交易修正,但不能抹去歷史;外部觀察、費用、延遲及信任後果可能保留。因此 Compensated 應是新狀態或新操作,而不是把舊 Committed 改成 NeverHappened。[E7]

12.6 不能撤銷的生成內容

AI 系統若已將推測性 token 串流直接顯示給使用者,該 token 在資訊層面已經可被觀察與轉傳。介面可以標示 provisional 或撤回,但不能保證收回已被看見的內容。對需要嚴格正確性或隱私的輸出,應在發布前驗證,或明確允許帶有風險的增量發布。


13. 安全回滾、依賴失效與恢復

13.1 回滾的三個不同意思

Discard: 未發布暫態狀態直接丟棄。

Undo: 把曾寫入受控暫態區域的變更逆轉到事先記錄的合法狀態。

Compensation: 對已提交且可能外部可見的行動提交一個新修正動作。

這三者的可行性、證明和成本不同。SMPDC 應優先讓推測分支寫入私有 shadow state,降低必要時的 undo 複雜度;但若資料量過大或 GPU 傳輸成本高,也可以實驗受控的 copy-on-write、undo log 等替代方案。

13.2 安全 rollback 的必要守衛

  • 推測分支未越過其正式提交點;
  • 全部尚未正式提交的後代已失效或接受重新驗證;
  • 沒有被遺漏的本地/設備 DMA 讀寫仍指向將回收的緩衝;
  • 所有尚未清償的擴散與請求義務遵守 Paper 02 規則;
  • 沒有已發出的不可逆外部效果需要假裝被撤銷;
  • 過期 PWN owner 不再能發出有效的提交或消息;
  • 恢復紀錄允許在事故後分辨新舊世代及重試責任。

13.3 依賴分支的撤銷路徑

parent P0: tentative result r0
   ├── child P1: tentative transform(r0)
   └── child P2: tentative verify(r0)
           └── child P3: tentative next-step

發現 P0 版本不合法:
1. mark P0 INVALIDATED
2. freeze submission of descendants P1,P2,P3
3. propagate invalidation metadata by bounded control path
4. revoke any uncommitted proposals rooted in P0
5. wait/track device completion and memory ownership
6. discard or recompute descendants on legal new snapshot
7. retain trace / lineage for audit

其中步驟 3 不能假定控制消息必然無延遲;真正避免後代「已在路上」的提交通過,還需要在提交仲裁時驗證 ancestor commit certificates 或版本證書,而不只依賴取消通知。

13.4 局部取消與真正取消

GPU kernel、I/O、遠端任務可能無法即刻中止。CANCEL_REQUESTED 不代表物理工作已停止,更不代表緩衝可立即回收;取消後遲到的完成事件須通過 epoch、owner generation、snapshot 與分支身分檢查才能被接納,否則只能當作隔離的過期結果。

13.5 記錄不可更動已提交歷史

一旦 durable COMMIT 已完成,回滾不能在同一提交序號上直接宣稱未提交。若錯誤來自商業規則或外部情報,可透過新一筆更正提交、補償操作或版本遷移修復;必須保留原操作的歷史因果鏈。


14. CPU/GPU 異質推測運算:可並行不等於可立即提交

14.1 GPU 執行事件只是一種完成證據

在 CUDA 等非同步 GPU 執行系統中,host 發出 kernel launch 後,呼叫返回不代表 kernel 已經完成。必須透過適用的 stream 或 event 同步,確認相關裝置計算、必要資料複製與可見性條件均成立,才能將 GPU 結果作為 RESULT_READY 候選。[E8]

GPUResultReady 與 CommitAuthorized 仍是不同的契約:

GPUComplete⁡(b)⇏CommitAllowed⁡(b).\operatorname{GPUComplete}(b)\not\Rightarrow\operatorname{CommitAllowed}(b).

如果底層 GPU 工作本身把結果直接寫到正式對外狀態,就破壞了本篇隔離邊界;首輪原型應限制 GPU 只能寫到有明確生命週期的暫態緩衝。

14.2 GPU 批次的真正可能收益

適合的操作包括:多候選純比較、向量化依賴狀態運算、固定 schema 的批次校驗、部分大規模資料更新的候選計算。對少量、頻繁且相互依賴的提交請求,GPU 排隊與 H2D/D2H 成本可能高於 CPU 直接處理。不能因為 GPU 有更多平行單元,就先驗認定適合執行權威仲裁。

14.3 延遲到達的 GPU 結果案例

Epoch 40:PWN-A 在 snapshot V5 啟動 GPU 候選 K
Epoch 40:PWN-A 因外部事件被遷移/撤銷
Epoch 41:PWN-B 在授權下提交 V6
Epoch 41:舊 GPU kernel 完成並將 K 傳回主記憶體

必要判斷:
- 裝置工作是否確實完成且資料可見?
- K 所屬事件 epoch、owner generation 是否過期?
- K 所依賴的 V5 對當前提交政策是否仍有效?
- 可否重作為普通候選,還是必須丟棄?
- 不可讓 K 直接覆寫 V6。

14.4 Buffer 所有權與同步

先把 CPU/GPU 共用 buffer 明確分成 TentativeWritable、DevicePending、HostReadable、SubmittedForCommit、Retired。只有符合裝置與 host 存取規則的狀態才能安全切換;若使用 pinned memory、Unified Memory、GPU graph 或共享頁,仍必須依實際硬體/API 的可見性保證處理,而非只依變數名稱。

14.5 效果不可跨設備偷渡

GPU 語言或 kernel 可讀到某個 output pointer,不代表它擁有對外部金流、磁碟交易或跨主機服務的提交權。SMPDC 提倡的是計算與正式效果的授權分離,不是「在 GPU 跑了就跳過 OS 控制」。


15. AI 訓練與推論:最值得嘗試、也最容易踩雷的適用域

15.1 AI 訓練的 step-level 提交

對訓練 step ss,提出以下正式鍵與狀態:

ks=(run⁡,step⁡,σ),Rs={modelver⁡,optimizerver⁡,batchver⁡}.k_s=(\operatorname{run},\operatorname{step},\sigma),\qquad R_s=\{\operatorname{modelver},\operatorname{optimizerver},\operatorname{batchver}\}.

在此 ksk_s 保留穩定的訓練操作身分; RsR_s 是提交驗證的版本化讀取依賴(實際實作應攜帶具體版本值與鍵,不只是欄位名稱)。重試不能僅因模型、最佳化器或候選 attempt 改變而偷偷變成新提交鍵,否則會跳過同一步驟只准提交一次的守衛。

一個可接受的訓練步驟需同步界定:

  • 模型參數版本與需要的權重快照;
  • 最佳化器狀態(例如 momentum/Adam moments)版本;
  • 梯度累積與 sample/microbatch 集合識別;
  • 混合精度/loss scaling 更新規則;
  • 隨機數種子、資料採樣位置與去重策略;
  • 語義上是否容許非同步/陳舊梯度更新。

最重要的是,兩條 R1 競速梯度路徑不能因都完成而把同一個訓練步驟更新兩次。另一種合法算法可以允許異步 stale gradient,但必須作為不同的訓練算法與收斂假說單獨驗證,不能宣稱它與同步 SGD 天然等價。

15.2 模型版本與最佳化器版本不能混為一談

即使模型權重版本相同,若兩個候選使用不同的 optimizer state,對同一梯度的更新結果也可能不同。僅驗證 model_version 仍不足以保證訓練 step 的一致性。需要將相應讀集完整納入 ConsistencyContract。

15.3 推測式解碼的候選提交

推測式推論可先生成候選 token 序列,再以與目標模型及採樣契約相符的驗證規則接受一段前綴;若驗證失敗,後段候選應被丟棄或重新生成。此時「接受 token」是一種受限模型輸出語義,不應直接等同 database WAL,也不等於已向外部使用者發表的文字可以撤銷。

15.4 MoE 與稀疏模型

MoE 動態路由可能有大量獨立或稀疏的計算支路,值得測試 PWN 持續工作流、相位擴散及 GPU 批次是否能減少排程等待。但其 expert assignment、all-to-all 通訊、KV/weight cache、GPU 記憶體容量與模型精度可能才是主要瓶頸。若未量測端到端 token/s、延遲和品質,就不能因 PWN 隊列較短宣稱 AI 推論變快。

15.5 Agent 與長期持續狀態

多 Agent 工作流通常存在非同步外部讀取、工具呼叫及可回溯的局部策略。這些工作負載很適合在模型上區分計算進度與外部效果,但也最容易錯把「AI 已決定」當「外部工具已成功」。若要讓 Agent 自動執行退款、發布、刪檔、設定變更等行為,仍須遵守個別系統的實際權限與提交政策。

15.6 AI 不是提交仲裁者的神諭

AI 可建議:需要多少推測深度、哪些候選先算、何時使用 R1/R2、如何分配 CPU/GPU 資源、是否轉回非推測基線。它不能直接繞過提交域的有效權限、數值正確性、版本衝突和持久性條件。最小 Runtime 必須在沒有 AI 模型的情況下可運作,並可提供確定性基線。


16. 條件性安全命題及證明概要

下列命題只對明示的參考模型成立,並非聲稱已經完成形式驗證、實作與實機測試。本篇區分安全性(不應發生之事不會發生)與活性(合宜事件終將發生),不把兩者混淆。

16.1 命題 A:同鍵至多一次正式提交決策

前提 A1: 提交域對同一 commit_key 實施線性化的原子唯一性檢查與決策寫入。
前提 A2: 已提交的同鍵記錄不能被以不同 payload 覆寫。
前提 A3: 發生故障時,提交紀錄的恢復契約可以保留所有已對外宣稱成功的決策。
前提 A4: 合法重試保持同一穩定提交鍵,且作用域/語義版本不被惡意重解釋。

則對任何提交鍵 kk:

#{r∈Ld∣r.commit_key⁡=k∧r.decision⁡=Commit}≤1.\#\{r\in\mathcal L_d\mid r.\operatorname{commit\_key}=k\land r.\operatorname{decision}=\mathrm{Commit}\}\le 1.

證明概要: A1 使兩個競爭提案只有其中一個能成功建立首個原子決策;A2 排除已決定鍵被修改;A3 避免崩潰後失去「已決定」的證據;A4 排除以變造鍵繞開唯一性。此處的「一次」指一個邏輯提交鍵的正式決策,不是網路封包只能發一次、GPU 只能算一次,也不保證任意外部效果 exactly-once。

16.2 命題 B:世代 fencing 排除舊 owner 的有效提交

前提 B1: 權威提交域保存不可回退的有效世代/fence。
前提 B2: fencing 檢查與正式決策在同一原子仲裁界內。
前提 B3: 舊 owner 無法取得新世代可寫 token,且沒有旁路修改正式資料的能力。

若新世代 gnewg_{new} 已生效且 gold<gnewg_{old}<g_{new},則:

CommitAllowed⁡(gold,d)=false.\operatorname{CommitAllowed}(g_{old},d)=\mathrm{false}.

證明概要: 由 B1 與 B2,所有真正生效的提交都必須在新世代下比較;舊 token 必不通過;B3 排除旁路寫入。此命題不阻止舊 owner 繼續消耗 CPU 時間或產生被隔離的遲到結果。

16.3 命題 C:隔離足夠時,尚未提交的分支不可產生正式效果

前提 C1: SpeculativeBranch 只對不可見暫態空間寫入。
前提 C2: 對外讀者沒有讀取暫態區的正式權限。
前提 C3: 所有正式效果通道皆經由已授權提交或受控 outbox。
前提 C4: 無未納入模型的 DMA、I/O、外部工具或旁路 publication。

則對任何最終 ABORT 的分支 bb,它不會直接造成該模型中的已提交狀態變更:

Abort⁡(b)⇒¬FormalStateEffectFrom⁡(b).\operatorname{Abort}(b)\Rightarrow \neg\operatorname{FormalStateEffectFrom}(b).

限制: 分支仍可能消耗時間、電力、快取、日誌或留下觀測痕跡;若威脅模型包含微架構側通道,需額外安全分析。此處沒有聲稱完整資訊流不干涉(noninterference)。

16.4 命題 D:完整依賴守衛防止已失效祖先的後代獨立提交

前提 D1: 每個引用暫態祖先的分支保有不可偽造的依賴證書。
前提 D2: 後代提交時原子驗證所有必要祖先的合法提交或等價證書。
前提 D3: 已失效祖先不能被錯誤地認證為合法,且驗證後到提交之間不存在未受保護的競速。

若祖先 pp 最終無效,且後代 cc 未取得合法替代證書,則 cc 不可藉本協議正式提交。這是受限 DAG 提交規則下的結論,不表示任意分散應用已自然支援跨域原子交易。

16.5 命題 E:快照一致性不足以保證跨鍵不變量

考慮 §8.5 的 write skew 反例。兩個交易讀到相同 snapshot,並修改不同鍵;各自的局部運算與單鍵寫入皆可正確,但組合結果仍破壞共享約束。

推論: 若提交層只有一致快照加 write-write conflict 檢查,不能無條件聲稱串行化或跨鍵不變量保持。這是已知資料庫隔離研究的經典負面結果 [E3–E4],不是 SMPDC 原創的不可能定理。

16.6 命題 F:有完整耐久日誌的限定模型可恢復已承諾狀態

前提 F1: 所有已對外確認的提交決策及重建所需資料皆按宣告故障模型持久化。
前提 F2: replay interpreter、schema、順序及版本解析規則確定,且恢復算法具邏輯冪等性。
前提 F3: 未提交寫入不會混入正式恢復狀態。
前提 F4: 外部不可重演效果經獨立的 outbox/effect ledger 管理。

則於所宣告故障範圍內,重啟後可重建一份與已承諾日誌相符的正式狀態。此結論不保證所有遺失的暫態分支可逐位重生,也不保證所有第三方外部效果已發生一次且只發生一次。

16.7 活性命題的限制

即使 A–F 成立,系統仍可能在永遠產生新衝突、資源永久不可用或權威日誌失效時不前進。若要提出條件性活性命題,至少須增加:公平調度、有限衝突或衝突後有進展策略、有效授權最終可取得、必要通訊可送達、提交域可用及某些可計算工作的終止前提。

在缺少這些前提時,返回 Unknown 或 Unavailable 可能是安全的結果,不能偽造成功以維持表面吞吐。


17. 二十四項提交安全不變量

下列列為 SpeculativeCommit Invariant Set v0.1;未來 TLA+/Rust Runtime 必須逐項標註 enforced / checked / unsupported / violated,不能只在文件中宣稱通過。

ID 不變量 最小違規案例
SC-01 邏輯結果鍵與正式提交鍵具清楚映射 傳送 attempt 被當新交易
SC-02 同一提交鍵不能建立兩個矛盾正式決策 複本先到與後到各寫一次
SC-03 同鍵不同載荷不允許悄悄覆蓋 版本不同卻直接更新
SC-04 本地驗證不自動產生提交能力 LocalVerified 直接修改全域
SC-05 主工作流身分不等於提交主權 每顆 CPU 都有全域寫權
SC-06 提交域權限必須在原子決策點驗證 先授權後撤銷仍可提交
SC-07 舊世代 fencing 在提交點失效 停頓舊 owner 恢復寫入
SC-08 event_epoch 不可單獨當資料版本 同 epoch 內快照已改
SC-09 讀寫集合的語義必須匹配隔離要求 僅看 write conflict
SC-10 共享謂詞約束須防止 write skew 雙人同時下班反例
SC-11 暫態祖先關係不得無證據消去 已取消 parent 的 child 提交
SC-12 正式輸出不得讀到非法部分提交 一半權重已更新一半未更新
SC-13 提交決策與持久性契約不得混淆 日誌未 durable 就 ack
SC-14 UnknownDecision 不得被默認 Abort timeout 後新鍵重做交易
SC-15 回滾只針對仍可撤銷的狀態 已匯款卻以本地刪 log 當退款
SC-16 外部效果不得從未提交暫態域直通 speculative branch 直接發信
SC-17 outbox 意圖與正式狀態需符合其原子契約 寫入狀態後 outbox 漏寫
SC-18 效果交付須有穩定 idempotency 身分 ACK 遺失造成重複扣款
SC-19 CPU/GPU buffer 撤銷須等待合法生命週期 GPU 尚在寫已釋放記憶體
SC-20 GPU event 不授予正式提交權 kernel complete 直接修改權威庫
SC-21 冗餘支路不能複製發送 credit 多送幾次就多了授權
SC-22 無 AI 時硬性正確性守衛仍然運作 AI 模型離線即跳過驗證
SC-23 已提交結果的可追溯記錄不得被重試覆寫 舊 commit index 被另一版本污染
SC-24 效能比較只在同等品質與一致性條件下有效 以 weaker isolation 的速度冒充加速

SC-02、SC-07、SC-10、SC-13、SC-16 是 V0 首輪的高優先級安全門檻;任一失敗均不得進入「已驗證系統」的對外宣稱。


18. 三十種必須主動製造的反例與故障

  1. 重送替代新鍵: 同一操作用隨機 nonce 產生新 commit key,導致雙重提交。
  2. 同鍵不同載荷: 舊提案與新提案具有相同 commit_key,但 payload 衝突。
  3. 舊 owner 復活: 交接後舊世代遲到寫入。
  4. 時間戳假權威: 系統依本地 clock 先後決定誰擁有寫入權。
  5. 世代 ABA: generation/slot 重複使用,舊 token 重新有效。
  6. 快照過期: 局部驗證通過時輸入仍是舊版本。
  7. write skew: 兩個不相交寫集聯合破壞共享不變量。
  8. phantom read: 範圍查詢只記實際讀出列,忽略新插入符合謂詞的資料。
  9. partial update: 多鍵更新中途對讀者公開一半。
  10. 準備態當已提交: 某個 Prepared 被無意發布為最終狀態。
  11. WAL 未刷盤即 ack: 斷電後丟失已宣稱成功的交易。
  12. 恢復重演雙算: redo 同一提交多次造成計數器翻倍。
  13. 效果先於提交: speculative branch 在正式仲裁前呼叫不可逆外部 API。
  14. 外部 ACK 消失: 目的端已處理,發送者以新鍵重送。
  15. 狀態和 outbox 雙寫: 其中一方成功一方失敗。
  16. 取消不等於停止: GPU kernel 取消請求後依然寫入其 buffer。
  17. 提早釋放: CPU 以為 GPU 工作已結束而 free 暫態緩衝。
  18. 事件跨 stream 誤用: CPU 等錯 event,讀到不完整 GPU 結果。
  19. 錯誤父分支: 子候選引用已失效的 speculative ancestor。
  20. 控制消息延遲: invalidate 遲到,後代已送進提交仲裁。
  21. 無窮重試: 每次版本衝突都立即重送,導致 livelock。
  22. 過量日誌: 複製與回滾造成 WAL 放大及磁碟頻寬瓶頸。
  23. 快取競爭: 多主工作流因共同提交鎖產生 cache-line ping-pong。
  24. NUMA/CCD 跨域: 版本表遠端讀取成本吞噬提前計算收益。
  25. AI 改寫 policy: 調度建議誤成縮小驗證範圍的權威。
  26. R2 錯誤佐證: 兩候選來源實為同一模型,卻被當獨立真理證據。
  27. GPU 數值重排: 不同 reduce 次序造成 bytes 不同,被誤判為語義衝突。
  28. 不安全 UI 串流: 暫態輸出已被外部觀察,後續還宣稱完全回滾。
  29. 跨域雙決策: 兩個不相容提交域各自發生局部 COMMIT,沒有協調。
  30. 權威域永久不可用: Runtime 為維持速度偽造最後的提交結果。

每個故障應記錄預期狀態、實際狀態、是否違反安全性、是否只是活性失敗,以及完整開銷。對於尚不支援的故障模型,回傳明確 UnsupportedFailureModel,不可以暗中跳過測試。


19. V0:有限狀態模型與模型檢查

19.1 為什麼要先做 V0

推測運算最難的失敗通常出現在少數事件的特定交錯,而非長時間平均跑分。例如「A 通過版本檢查、B 寫入新版本、A 再提交」在單線程測試下可能永遠不出現。V0 用可枚舉轉移系統尋找極小反例,再把相同 schedule 投射到 Rust/C++ 原型。

19.2 建議有限模型的邊界

flows: 3
commit_domains: 1
state_keys: [x, y]
epochs: [e0, e1]
owner_generations: [g0, g1]
candidates_per_result: up to 2
redundancy_modes: [R0, R1, R2]
proposal_status: [new, verified, prepared, pending, committed, aborted]
commit_decisions: [none, commit, abort]
log_states: [not_appended, buffered, durable]
effect_states: [none, pending, delivered, unknown]
crash_points: before_log, after_log, before_publish, after_publish, before_ack

R3 的碼理論可維持在 Paper 03 模型;本篇只測試 R3 重建完成後的 LocalVerified 是否仍受提交守衛約束。GPU 在 V0 可先作為帶非同步 DEVICE_DONE 事件的模擬 executor。

19.3 建議的狀態轉移字母表

CREATE_BRANCH
ADMIT_BRANCH
READ_SNAPSHOT
SPECULATE_STEP
DEVICE_LAUNCH
DEVICE_COMPLETE
LOCAL_VERIFY
BUILD_PROPOSAL
AUTH_CHECK
VALIDATE_SNAPSHOT
VALIDATE_PREDICATES
ARBITRATE
APPEND_LOG
DURABLE_FLUSH
PUBLISH_STATE
ENQUEUE_OUTBOX
DELIVER_EFFECT
EFFECT_ACK
AUTHORITY_HANDOFF
CANCEL_BRANCH
INVALIDATE_ANCESTOR
CRASH
RESTART
RECOVER_LEDGER
REPLAY_STATE
RETRY_SAME_KEY
QUERY_UNKNOWN_DECISION

19.4 模型至少檢查的性質

安全性: SC-02、SC-04、SC-07、SC-10、SC-11、SC-13、SC-16、SC-18 以及 Committed 不被 Abort 覆寫。

一致性: 對指定 serializable 模型,每個可觀察歷史存在合法序列化次序;此性質不能只從所有單鍵 CAS 成功推導。

恢復性: 在限定 crash 模型下,所有已 ack 的 committed decisions 於重啟後仍可查詢並重建。

活性: 在公平及故障終止假設下,是否有合法可提交請求永遠卡在 Prepared?需要分開標註假設。

19.5 三個必備 counterexample trace

CE-A (write skew)
T1 read (x=1,y=1)
T2 read (x=1,y=1)
T1 write x=0
T2 write y=0
commit both -> invariant violation
CE-B (stale owner)
A acquire gen1
A paused
B acquire gen2
B commits
A resumes and attempts commit gen1
accept A -> fencing violation
CE-C (uncertain commit)
Client proposes key K
Authority writes durable COMMIT K
Authority crashes before ACK
Client times out and retries with key K2
commit K2 -> duplicate logical effect

V0 的正確設計應能排除這些違規後續,或把弱一致性造成的反例明確標記為非承諾之模型。

19.6 模型檢查產出的證據格式

每次 V0 應輸出:完整參數、模型版本、狀態數、探索策略、是否全域覆蓋有限空間、違反的不變量、最短或代表性 trace、重放種子、執行環境與結果 hash。若 bounded model checking 僅覆蓋深度 kk,不能宣稱對所有事件交錯都已證明安全。[E9]


20. V1:消費級 CPU/GPU 上的參考 Runtime

20.1 第一輪不依賴新硬體採購

可先以一般 AMD/Intel 消費級 CPU 測試邏輯多主工作流、隔離、提交日誌及 CPU core affinity。使用者現有舊款 AMD CPU、32GB RAM 與 RTX 3070 可作為功能原型和部分 GPU 參考測試;不把曾討論但尚未購買的新型 CPU 當成已備設備。

第一輪實驗不能從這台既有 CPU 推論「Intel P/E core 異質性」或「AMD 3D V-Cache 雙 CCD」的實測效果;那些需要相對應的實體平台另行量測。

20.2 最小實作元件

SMPDC-V1
  FlowRegistry
  PWNExecutorPool
  PhaseTracker / BoundedDiffusionAdapter
  ReconciliationAdapter (Paper 03)
  SnapshotManager
  SpeculativeArena
  VersionedReadWriteTracker
  CommitDomainRegistry
  AuthorityFencingValidator
  AtomicCommitLedger
  CommitLog / DurableStoreAdapter
  OutboxAdapter
  EffectDeliveryWorker
  CrashRecoveryHarness
  CPU/GPU DeviceCompletionAdapter
  TraceRecorder
  BenchmarkHarness

其中 CommitLedger 應能以強一致性單域參考實作先通過 V0;再研究分片、多域、低鎖結構。不要為了追求高並行,一開始就把正確性核心拆成多個無協調權威。

20.3 B0–B7 A/B/消融比較組

組別 配置 目的
B0 單工作流、序列執行、等價提交品質 正確性與低開銷下界基線
B1 傳統 thread pool/task scheduler+等價提交 現有主流併行基線
B2 PWN 持續工作流、無推測、正式提交 分離多主工作流效果
B3 PWN+有界相位擴散、無冗餘、無推測 分離 phase/diffusion 成本
B4 B3+R1 或 R2(分開測)、無推測 分離 Paper 03 冗餘成本
B5 B3+有界推測+同等隔離提交 測試推測本身是否有用
B6 B5+R1/R2(分開測)+CPU-only 測試冗餘與推測的交互作用
B7 B6+GPU 可選批量運算 測試加速器對端到端收益的增量

另外應加入一組成熟 transactional runtime(例如具 serializable 隔離的資料庫/KV Store)作為比較;不能只和自行寫出的弱基線相比。若各組使用不同耐久或隔離等級,必須重調到相同品質,否則相關跑分無法支援性能結論。

20.4 工作負載矩陣

  1. 純 CPU、無外部效果的版本化計算 DAG。
  2. 高讀、低寫、局部性佳的工作流,測試推測能否覆蓋等待。
  3. 高寫入衝突與 shared counter,故意尋找最差情況。
  4. 跨鍵業務不變量的 write skew 測試。
  5. 長尾服務候選與 R1 冗餘競速。
  6. 多模型來源佐證與 R2 衝突隔離。
  7. 帶有持續記憶的 Agent mock-workload,不發真正外部效果。
  8. 小型訓練/推論 step 模型,包含 optimizer state 版本驗證。
  9. GPU 大批次純關係計算,量測 H2D/D2H/stream/event 同步。
  10. 非 AI 的事件處理負面控制,防止只挑對 SMPDC 有利的案例。

20.5 失效注入策略

關閉與重開 worker、在 append/before flush/after flush/before ack 注入故障、延遲或重排消息、重送提交提案、偽造過期 fence、觸發 GPU delayed completion、製造快取競爭與高比例 abort;每個錯誤都應保留最小 trace,供 V0–V1 交叉重演。

20.6 平台因素應固定或報告

CPU core topology、SMT、CPU frequency/thermal、RAM 容量與頻寬、GPU driver/CUDA 版本、PCIe 連接、NUMA/CCD、作業系統版本、編譯器旗標、timer 精度、log flush 政策、batch size、相位與冗餘策略。CPU 使用率不能作為主要成果指標;它只能協助解釋資源使用。


21. 延遲、吞吐、能源與錯誤推測的完整成本模型

21.1 不能簡單把所有階段時間相加

某些 CPU、GPU、傳輸與日誌工作可以重疊;某些是依賴必經的關鍵路徑。故應透過帶資源占用的事件 DAG 測量端到端 makespan,而不是把各 microbenchmark 的總時間直接當完成時間。

對一個完成操作的實測路徑 π\pi,可寫成:

Tend(π)=Tobserve_success(π)−Tadmit(π).T_{end}(\pi)=T_{observe\_success}(\pi)-T_{admit}(\pi).

再記錄各階段成本及重疊比例:

C04=⟨Ccompute,Cdiffuse,Cverify,Carb,Clog,Cmem,Cgpu,Cretry,Ceffect⟩.\mathcal C_{04}=\langle C_{compute},C_{diffuse},C_{verify},C_{arb},C_{log},C_{mem},C_{gpu},C_{retry},C_{effect}\rangle.

C_effect 不能在測試外部效果工作負載時被隱藏;若只量 durable COMMIT 而未等待效果完成,必須將結果清楚標為 local-commit latency。

21.2 推測收益的正確分母

若基線完成時間為 TBT_B 、方案完成時間為 TST_S,在相同一致性、持久性與輸出品質下,速度比:

Speedup⁡=TBTS.\operatorname{Speedup}=\frac{T_B}{T_S}.

若 TS>TBT_S>T_B,就代表該工作負載變慢。不能以縮短 candidate completion 時間的局部結果掩蓋正式提交或效果交付變慢。

21.3 錯誤推測的資源浪費

定義已實際消耗計算資源、但其結果未被任何合法提交或必要驗證使用的推測工作成本:

Wwaste=∑b∈BResourceCost⁡(b)⋅1[Unused⁡(b)].W_{waste}=\sum_{b\in\mathcal B}\operatorname{ResourceCost}(b)\cdot\mathbf 1[\operatorname{Unused}(b)].

這裡 Unused 的判定需要區分「提供了 R2 負面證據」與「純粹白算」。若一支候選因揭露錯誤而被拒絕,它可能仍具有驗證價值,不應全部以錯誤推測解釋。

21.4 提交瓶頸的可擴展性

在多主工作流都寫同一受控狀態時,權威提交域可能成為 throughput 上界。若平均每個決策需要 τarb\tau_{arb} 的序列化處理,則在不能並行的單域極端下可提出理想化上界:

Throughput⁡domain≤1τarb.\operatorname{Throughput}_{domain}\le\frac{1}{\tau_{arb}}.

此處只針對無法並行的仲裁臨界段,並非對所有可能設計的 CPU 系統提出單一普適上界。分區、group commit、批次驗證或可交換操作可能改變該值;但其安全性仍須另證。

21.5 能源與記憶體

至少量測 wall-clock、CPU package energy、GPU energy(若工具支援)、DRAM/VRAM footprint、WAL bytes、傳輸 bytes、相位消息、abort/retry 次數、cache miss 與 outbox backlog。若能源計量精度不足,必須標示估算與儀器限制,不可只因跑得快就假定更省電。

21.6 提早完成但沒有早提交的情況

若計算提前完成,卻必須等權威域排隊、驗證版本與 fsync,收益可能趨近於零。這不是反例被忽略,而是可以直接用實驗檢驗的核心問題。SMPDC 的性能主張只在端到端進度改善時成立。


22. 與既有學術與工業技術的邊界

22.1 Herlihy–Wing 的 Linearizability

線性化是成熟的並發物件正確性條件,說明每一操作可抽象為在呼叫與回覆之間的某個原子瞬間生效。本篇採其思維來定義單一 CommitDomain 的原子仲裁,但線性化單物件本身不足以保證跨物件交易的 serializability。[E1]

22.2 Lamport 因果順序

事件因果偏序早有經典研究;SMPDC 的 event_epoch、世代、相位及消息血緣應保留與 causal ordering 可比對的關係,但不能把不同時間戳直接當作全域真理順序。[E2]

22.3 MVCC/Snapshot Isolation/Serializable

多版本並發控制是成熟資料庫基礎。SMPDC 不是重新發明 MVCC;本篇新增的是如何對「分散在多個 PWN、GPU candidate、Paper 03 聚合結果」建立版本化輸入與正式提交守衛。SI 的 write skew 反例也使本篇不會對弱隔離做強一致性宣稱。[E3–E4]

22.4 WAL 與交易式 Outbox

預寫日誌與交易式 outbox 是成熟可靠性方法。SMPDC 不把它們作為原創性賣點,而是把 commit/effect 邊界變成新型擴散語言可能需要的一級語義。[E5–E6]

22.5 Sagas/補償

長期操作可能無法用單一原子交易覆蓋,Saga 允許以補償處理部分完成的流程。但補償仍保留歷史與成本,不能寫成推測分支的完全撤銷。[E7]

22.6 CUDA 非同步工作

CUDA streams、events、同步與 graph 執行已有成熟支援。SMPDC 研究的是讓這些完成事件與多主版本化提交安全銜接,不宣稱是首次讓 CPU/GPU 並行、也不宣稱 GPU 能取代實體 CPU 互連。[E8]

22.7 TLA+ 與具體模型檢查

本文提出的有限轉移系統可以用 TLA+/TLC 或其他適用工具檢查,但書面命題與模型檢查結果是兩種不同證據。若尚未產生模型、工具輸出和覆蓋範圍,就只能把命題標記為待檢查。[E9]

22.8 分散式交易的共識與提交

當提交域橫跨故障獨立的多台機器,單機鎖和普通檔案 WAL 不足以提供高可用、容錯一致決策。兩階段提交可能在協調者故障時阻塞;共識式交易提交及 replicated log 方案已有成熟文獻。本篇只要求對所宣告故障模型實作對應權威機制,不宣稱本地 Runtime 自帶容錯共識。[E10–E11]

22.9 CPU 硬體投機不等於 SMPDC Runtime 投機

CPU 微架構的 branch speculation/transactional memory 會涉及不同的快取、指令與 rollback 邊界;即使硬體支援部分記憶體事務撤銷,也不能回復任意外部 I/O。SMPDC 的推測分支是執行語義及授權協議,不是微碼的別名。[E12]

22.10 內部 GCCFT/GCCWT/GCM 的分工

GCCFT 描述廣義耦合計算場、相位、動態計算域與可證偽基線;GCCWT 處理更大尺度的異質世界、資源與跨域規劃;GCM 既有規劃與執行授權分離。SMPDC Paper 04 將這些抽象收斂到每核/每工作流與相鄰記憶體層級的正式提交契約。它並不重新宣稱發明全域計算,也不把現有 GCM 工程封閉狀態等同本篇 Runtime 已完成。


23. 對後續論文的契約交接

23.1 Paper 05|持續擴散抽象指令集

Paper 05 至少應定義下列抽象操作的前置條件、效果型別、資源計量、可撤銷性與失敗狀態。此清單不是立即新增 x86/ARM opcode 的要求。

SPEC_BEGIN(scope, snapshot, rollback_policy)
SPEC_READ(branch, object, version_guard)
SPEC_DERIVE(branch, operation, dependencies)
SPEC_FORK(branch, candidate_plan, bounded_credit)
SPEC_ATTACH_GPU(branch, event_or_stream, buffer_contract)
SPEC_INVALIDATE(branch, reason)
SPEC_ABORT(branch, reason)

COMMIT_PROPOSE(branch, local_outcome, isolation_contract)
COMMIT_VALIDATE(proposal, versions, predicates, authority_fence)
COMMIT_DECIDE(commit_key, proposal_digest, authority)
COMMIT_QUERY(commit_key, authority)
COMMIT_PUBLISH(committed_record, visibility_contract)

EFFECT_ENQUEUE(commit_record, stable_effect_key, payload)
EFFECT_DELIVER(effect_key, receiver_policy)
EFFECT_QUERY(effect_key, target_authority)
EFFECT_COMPENSATE(effect_key, new_operation)

核心禁止轉換:

TentativeValue      -X-> CommittedValue
LocalVerified       -X-> CommitAuthorized
DeviceComplete      -X-> CommitDecision
MessageAck          -X-> ExternalEffectSettled
SameValueDifferentKey -X-> SameCommit

其中 -X-> 表示沒有明確證書/權限守衛時禁止直接轉換,不是說兩端之間永遠不存在合法的受審操作。

23.2 Paper 06|語言與型別系統

語言至少應辨識:

  • FlowId、EventEpoch、AuthorityGeneration;
  • Snapshot<T,V>、Tentative<T,B> 與 Committed<T,K>;
  • LocalOutcome<K>、CommitProposal<K>、CommitDecision<K>;
  • ReadSet<V>、PredicateSet<V>、WriteSet<V>;
  • CommitCapability<D>、EffectCapability<E>;
  • Rollbackable<E> 與 NonRollbackable<E>;
  • GPUEvent<BufferLease> 與 HostVisible<T>;
  • UnknownCommit<K> 和 QueryHandle<K>。

一個候選語言可用 linear/affine 類型減少 credit 重複使用及權威 token 複製,但仍須有 runtime guard 防止跨程序、故障及不可信資料造成的破壞。不能只靠靜態型別宣稱物理硬體或外部服務都已安全。

23.3 Paper 07|OS、Runtime 與 AI 控制平面

OS/Runtime 應提供明確 API:註冊工作流、建立隔離暫態區、設定 core affinity、查詢實體拓撲、取得提交能力、完成帶 generation 的 owner handoff、回復未知提交與守護 outbox。AI 可以輸出調度建議但不得編輯硬性安全 guard;任何 AI 推薦都需要對照確定性策略。

23.4 Paper 08|CPU–GPU 協作

應量測 GPU kernel 提交與完成事件、裝置/主機同步、資料複製、buffer lease 與版本 guard 如何影響有效提交時間。若 GPU 加速只降低候選計算時間而提高 end-to-end p99,必須如實記錄失敗。

23.5 Paper 09|記憶體、快取與微觀映射

應比較 CAS、鎖、MVCC、append-only log、cache-line 負載、NUMA、CCD、SMT 及 P/E 核的實際成本;不可由概念上「多顆星」推導晶片物理布局。若研究 FPGA/NoC,需把此篇提交權威守衛映射到可信的硬體仲裁點。

23.6 Paper 10|AI 訓練與推論

固定模型、資料集、訓練品質/生成品質、device budget、batching 與一致性等級,先測是否在某些 AI 工作負載取得真正收益,再觀察效能最佳點對各參數的敏感度。不要把多次不一致更新的高吞吐錯認為等價訓練成果。

23.7 Paper 11|總體可證偽結案

除了成功案例,最終報告必須包含未達成性能優勢的工作負載、推測無效區間、過高的 logging/fencing/GPU 成本、性能與品質權衡、已知不變量違反及未覆蓋的故障模型。若完整成本比較顯示沒有可觀的適用域,該結論也可正式成立,不得以「理論尚未被理解」取代數據。


24. 結論:讓運算先行,但讓權威有明確位置

SMPDC 的多主工作流概念不是要求每個 CPU 核心都獨占某一份全域真理,也不是把 GPU 的並行計算速度等同原子提交速度。它希望在中觀—宏觀執行層容許多個計算中心同時前進,並經有界相位擴散、冗餘資訊聚合和正式權威判定共同形成可用結果。

在此前提下,本篇提出五項結論:

  1. 計算可先於正式提交,但不合法的外部副作用不可先於提交。 推測性資料必須具身分、版本、依賴、隔離及失效規則。
  2. 多主執行不排除有明確的提交權威。 執行主節點與正式仲裁者是兩種角色;權威可以按作用域分散,但同一受控域須有可證明的安全決策邊界。
  3. 局部驗證不保證當前狀態可用。 必須檢查完整讀寫與謂詞約束;單靠 snapshot isolation 和不同鍵的原子寫入仍可能出現 write skew。
  4. 正式提交、持久化與外部效果交付不是同一事件。 本地提交紀錄至多一次可於指定模型內保證;任意外部行動是否只生效一次,取決於對端、協議及故障模型。
  5. 能否更快是一個獨立且可反駁的實驗問題。 有界推測省下的關鍵路徑等待,必須超過版本驗證、資料搬移、衝突、回滾、日誌和仲裁的總成本。

本文所提出的原創研究目標,不是把 MVCC、WAL、linearizability 或 CUDA 重新取名,而是問:能否把這些成熟的安全邊界,重新組成一個支援多個持續主工作流、可選冗餘擴散和異質候選運算的通用執行協議,使其可編譯、可重演、可證偽,並對特定 AI 工作負載獲得正確性不降級的端到端收益?

截至 v0.1,此問題仍未由模擬器、原始碼或實機性能資料獲得肯定回答。Paper 04 建立的是進入實作階段所需的明確安全契約,而不是已完成的系統或加速結果。


附錄 A|SpeculativeCommit Contract v0.1 最低合規檢查表

編號 最低必需條件 未滿足的處理
SCC-01 SpeculativeBranch 有穩定身分、快照與依賴 拒絕啟動/保守降級
SCC-02 Paper 03 的 LocalReconciliationOutcome 可追溯 拒絕提交提案
SCC-03 R0/R1/R2/R3 模式不混用候選與送達鍵 InvalidEvidence
SCC-04 每個提案具有穩定 commit_key InvalidCommitKey
SCC-05 提交鍵不隨重送 nonce 改變 InvalidIdentity
SCC-06 同鍵 payload 衝突可查出 ConflictSameKey
SCC-07 commit_capability 有精確作用域 InvalidScope
SCC-08 authority generation/fence 在仲裁時驗證 StaleOwner
SCC-09 read/write/predicate sets 匹配隔離策略 IsolationConflict
SCC-10 跨鍵不變量由有效機制保護 拒絕 Serializable 宣稱
SCC-11 祖先依賴完整可檢查 MissingDependencies
SCC-12 版本驗證與決策具原子競速防護 停止正式提交
SCC-13 已 committed 決策不可被另一候選覆寫 AlreadyDecided / ConflictSameKey
SCC-14 durability class 有確實的儲存語義 降級並明示政策
SCC-15 崩潰後可分辨 durable COMMIT 與未決提案 UnknownDecision 查詢
SCC-16 replay 不重複邏輯效果 RecoverySafetyError
SCC-17 未提交分支不能直接發出不可逆效果 立即拒絕/隔離
SCC-18 outbox 與本地提交具一致原子域 拒絕 exactly-once 類宣稱
SCC-19 效果投遞具穩定 effect key 可能需人工核對
SCC-20 補償被視為新操作 不許竄改提交史
SCC-21 GPU 工作完成且資料可見才可作候選 DevicePending
SCC-22 取消後仍存活的 GPU buffer 不可提早 free 推遲回收
SCC-23 speculative 依賴的撤銷與提交競速已防護 拒絕 unsafe descendant
SCC-24 UnknownDecision 不自動默認失敗 以同鍵查詢或冪等重試
SCC-25 日誌留存、tombstone 保留與重送期限協調 禁止提早清理
SCC-26 無 AI 時硬性驗證可執行 選擇確定性 fallback
SCC-27 每次比較報告相同隔離與品質 不允許發布比較結論
SCC-28 所有反例有最小可重演 trace 標記未驗證

附錄 B|三組可逐事件重演的參考案例

B.1 R1 競速、局部正確但快照過期

情境: PWN-A 提供影像資料分析候選,兩個不同傳輸嘗試將同一候選送到聚合者 PWN-C;PWN-B 稍早正式更新分析設定。

t0  Committed config_version = 3
    logical_operation_id = "analyze/frame-007"

t1  A generates result K(snapshot=config_v3)
t2  R1 attempts u1 and u2 carry the same candidate C
t3  B commits config_version = 4

t4  C receives u2 first; payload valid for config_v3
    local_verification_status = LocalVerified

t5  C builds CommitProposal for "analysis/frame-007"
    read_set includes config_v3

t6  Commit authority sees config_v4
    -> StaleSnapshot
    -> no authoritative state update

t7  optional retry on config_v4 with same stable logical operation
    -> new candidate under appropriate retry version policy

必要判斷: R1 的尾延遲優勢可能成立,但與是否能提交是兩種不同觀察。若政策允許「歷史版本 v3 的分析結果」另存在版本化輸出域,則可在不同明確語義的提交目標中合法保存;不能偷偷把它當成 v4 當下結果。

B.2 舊 owner 提案與新 owner 提案競爭

CommitDomain D: authority_generation=20
Old owner A holds fence=740
A prepares P on commit key K
A is descheduled

D authoritatively changes to generation=21, fence=741
New owner B proposes Q on K
D accepts Q, creates decision_index=94, COMMIT durable

A resumes and proposes P on K using fence=740
D returns AlreadyDecided(Q) or StaleOwner
No second decision can be created

若實作在檢查 K 時先看到既有決策,回應 AlreadyDecided;如果先檢查舊世代,則可能回應 StaleOwner。這些 API 可有不同優先回覆策略,但正式安全性必須一致:不許 P 再度生效。

B.3 GPU 推測、耐久提交與 Outbox 的崩潰窗口

1  PWN-A computes tentative gradient on GPU
2  stream/event and memory visibility checks complete
3  PWN-B validates read-set/model+optimizer versions
4  CommitAuthority records COMMIT K=run42/step8
5  WAL for state delta + outbox intent becomes durable
6  machine crash before ack
7  recovery loads log and reconstructs step8 exactly once logically
8  caller uses K to query -> AlreadyDecided COMMIT
9  delivery worker sends outbox effect E=run42/step8/notify
10 receiver processes E but ACK packet drops
11 worker retries E using stable idempotency key
12 receiver dedups E; effect state becomes Acknowledged

關鍵假設: 第 12 步只有在接收方確實支援該去重協議、保留必要記錄、且效果與去重在它自己的安全範圍內協調時,才能宣稱相同業務效果未重複發生。否則必須保留 Unknown/人工處理可能。


附錄 C|追蹤結構、審計事件與計量欄位

C.1 建議的 SpeculativeCommitTraceV0_1

SpeculativeCommitTraceV0_1 {
    trace_id, monotonic_trace_sequence
    event_name, local_timestamp, clock_domain_id
    event_epoch, topology_generation
    flow_id, worker_id, physical_core_optional
    owner_generation, owner_fencing_token_ref
    result_key, candidate_id, logical_message_id, delivery_attempt_id
    speculative_branch_id, tentative_dependency_ids
    snapshot_id, read_set_digest, predicate_set_digest, write_set_digest
    commit_domain_id, commit_key, proposal_digest
    commit_decision, commit_index, durability_class
    gpu_stream_id_optional, gpu_event_id_optional, buffer_lease_id_optional
    outbox_id_optional, effect_key_optional, effect_status_optional
    cpu_time_ns, wall_time_ns, bytes_moved, log_bytes, rollback_bytes
    rejection_class, fault_injection_id, correctness_witness_ref
}

local_timestamp 只協助單機測量;跨 clock domain 不得直接當作 happens-before 證書。若需要跨主機因果順序,須保留事件依賴和明確同步規則。[E2]

C.2 必須能從 trace 推回的查詢

  • 同一 commit key 發生多少 proposals、physical deliveries 與正式 decisions?
  • LocalVerified 到 durable COMMIT 的等待分布如何?
  • Committed 到 EffectsSettled 相差多少,多少仍是 Unknown?
  • 取消後有多少 GPU 或 CPU work 仍在執行?
  • 多少 speculative branches 因 snapshot/fence/ancestor 被拒絕?
  • abort 是否增加額外 RAM、VRAM、WAL 或 cache traffic?
  • 各基線於同等 isolation 與 durability 下的 p50/p95/p99 和 throughput?
  • 任何一個不變量違反能否被還原為可重演的有限 trace?

C.3 典型效能報告欄位

run_id
implementation_commit_hash
platform_topology
runtime_version
compiler_flags
workload_contract
isolation_level
durability_policy
effect_delivery_policy
seed
N_submitted / N_local_verified / N_committed
N_aborted / N_retry / N_unknown
p50 / p95 / p99(end_to_end_ms)
p50 / p95 / p99(commit_only_ms)
throughput_committed_per_second
CPU_usage / GPU_usage
CPU_energy_joule / GPU_energy_joule (where available)
peak_ram_bytes / peak_vram_bytes
log_bytes / message_bytes / rollback_bytes
fatal_safety_violations
reproducible_trace_bundle_digest

若某指標不可用,應明確填 NOT_MEASURED,不要留空後推定為零。


附錄 D|版本治理、研究完成度與原始檔規則

D.1 四層主張成熟度

  • L0:構想與可反駁假說。 本系列的多主擴散形式設計屬此層起點。
  • L1:形式契約、條件性論證與反例。 本篇 Paper 04 v0.1 的主要完成範圍。
  • L2:可重演模型檢查、實作與單機/異質 A/B 原始數據。 目前尚未完成。
  • L3:跨平台重現、獨立驗證、明確的效能適用域。 目前尚未完成。

不得將 L1 的條件性命題表示成已通過機械證明,也不得把示例 trace 當成實際 CPU/GPU benchmark。

D.2 Canonical Markdown 源檔

  1. 正式內容由此 UTF-8 Markdown 原始檔承載,而非聊天渲染文字。
  2. 數學原始分隔符僅用 $...$ 與 $$...$$。
  3. 原稿不做反斜線轉換、Unicode 數學字元 round-trip 或自動「美化」公式。
  4. 修改須產生新的版本/提交紀錄,保留本篇版本的研究主張和負面結果。
  5. 每次正式 commit 前檢查 YAML metadata、結構、公式分隔符、參考文獻、來源辨認和研究成熟度聲明。
  6. 不因使用者或 AI 的主觀期望修飾正式故障、反例、負面性能結果。

參考文獻與原始研究來源

內部正式原稿及研究前史

  • [I0] Neo.K × Aletheia(2026-10-16)。《SMPDC Paper 00|群星多主節點持續擴散計算論:形式總綱》,v0.1。Canonical source:SMPDC_Paper00_Stellar_Multi_Primary_Persistent_Diffusive_Computing_v0.1_2026-10-16.md。
  • [I1] Neo.K × Aletheia(2026-10-16)。《SMPDC Paper 01|多主工作流節點論》,v0.1。Canonical source:SMPDC_Paper01_Multi_Primary_Workflow_Nodes_v0.1_2026-10-16.md。
  • [I2] Neo.K × Aletheia(2026-10-16)。《SMPDC Paper 02|相位耦合與有界持續擴散動力學》,v0.1。Canonical source:SMPDC_Paper02_Phase_Coupling_and_Bounded_Persistent_Diffusion_v0.1_2026-10-16.md。
  • [I3] Neo.K × Aletheia(2026-10-16)。《SMPDC Paper 03|冗餘資訊流與主節點聚合協議》,v0.1。Canonical source:SMPDC_Paper03_Redundant_Information_Flow_and_Primary_Node_Reconciliation_v0.1_2026-10-16.md。
  • [I4] Neo.K。《群星架構在計算機系統中的應用與改良計畫》。
  • [I5] Neo.K。《相位計算機理論 v0.1》,2026-07-25。無界智庫公開版:https://unboundedaxiom.org/p/lm-001850/。
  • [I6] Neo.K × Aletheia。《GCCFT Paper 06|從 Scheduler 到 Coupled Computation Planner》。
  • [I7] Neo.K × Aletheia。《GCCWT Paper 04|計算場與資源激發》。無界智庫公開版:https://unboundedaxiom.org/p/lm-004846/。
  • [I8] Neo.K。《GCM Phase C — AI-assisted Compute Orchestrator Engineering Blueprint v0.1》。

外部學術與工程文獻(來源核對:2026-10-16)

原創性、引用及證據聲明

本文將成熟的線性化、交易隔離、WAL、outbox、補償流程、設備同步與分散式共識作為已知先例,不聲稱它們由 SMPDC 首次發明。Neo.K 本輪的構想重點在於:多個 CPU 核心可各自承載持續主要工作流,透過相位耦合與有界擴散進行協作,並在冗餘資訊聚合後與 GPU 可選並行運算結合;正式系統須額外建立正確的提交與副作用邊界。 本篇的研究協作工作是將其提交層細化為候選協議、狀態機、條件性命題、反例及實驗規格。

文件中所有時序範例、協議偽程式碼、性能成本模型與測試矩陣都屬研究定義或待驗證方案,不是實測數據。沒有宣稱完成 Runtime 程式碼、TLA+ 模型檢查、CPU/GPU benchmark、獨立重現或經同行審查的正式證明。


SMPDC Paper 04 v0.1 — End of Canonical UTF-8 Research Manuscript