← Archive
lm-005260 · 2026-11

SMPDC Paper 05|持續擴散指令集:多主工作流、相位、冗餘、推測及權威提交的可執行語義

下載 MD 檔 ⬇
title
SMPDC Paper 05|持續擴散指令集:多主工作流、相位、冗餘、推測及權威提交的可執行語義
english_title
Persistent Diffusive Instruction Set: Executable Semantics for Multi-Primary Workflows, Phase Coupling, Typed Redundancy, Speculation, and Authoritative Commit
series
SMPDC — Stellar Multi-Primary Persistent Diffusive Computing
paper
05 / 11
version
0.1
status
Full Research Manuscript — Candidate Virtual Instruction Set, Formal Contracts, 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) · SMPDC Paper 04 v0.1 (2026-10-16)
artifact_scope
Typed abstract instruction set, operational semantics, virtual machine, verifier, lowering, safety obligations, falsification-first validation, and formal handoff to Paper 06

SMPDC Paper 05|持續擴散指令集

——多主工作流、相位、冗餘、推測及權威提交的可執行語義

英文題名: Persistent Diffusive Instruction Set: Executable Semantics for Multi-Primary Workflows, Phase Coupling, Typed Redundancy, Speculation, and Authoritative Commit
系列: 群星多主節點持續擴散計算論(SMPDC)
主構想提出: Neo.K
研究協作: Aletheia / GPT-6
機構: EveMissLab/一言諾科技有限公司
日期/版本: 2026-10-16/v0.1
研究成熟度: L0–L1;正式提出的候選抽象指令與驗證契約,尚無宣稱已實現的原生 CPU opcode、編譯器或實機加速成果。
直接承接: SMPDC Paper 00–04 [I0–I4]。

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


摘要

SMPDC 前五份原稿(Paper 00–04)依序確立多主節點持續工作流、相位耦合及有界擴散、具型別冗餘資訊流,以及推測運算與權威提交的分層協議。然而,若這些協議只能以論文術語存在,開發者仍須在一般程式語言中手工拼接排程、佇列、傳播預算、版本驗證、GPU 事件與故障恢復,便無法判定實作究竟遵守哪些不可變條件,亦無法將架構優點和手工最佳化混為一談。本篇提出一套持續擴散抽象指令集(Persistent Diffusive Abstract Instruction Set, PDAIS)作為 SMPDC Paper 05 的可執行語義候選。

PDAIS 的目的不是立刻增加 x86、ARM 或 RISC-V 的物理機器碼,而是把多主工作流的生命週期、相位呼叫、耦合資格、有限傳播權、R0–R3 型別冗餘、局部聚合、具血緣的推測分支、正式提交與外部效果分離,定義為一級、具型別、可驗證、具資源計量的效果操作。其最小執行機器維持邏輯工作流、epoch、相位、耦合邊、訊息與 credit 帳本、候選證據、推測分支、提交權威及可觀察事件追蹤等狀態。每一項指令均具有參數與結果型別、必要前置條件、效果集合、進度或失敗型別、重播規則、權限守衛與可選實體映射。

本篇明確區分四種經常被誤稱為「指令」的對象:(1) 源碼語言構造;(2) 抽象執行指令/語義操作;(3) 編譯器中介表示(IR)操作;(4) 具體處理器 opcode。只有第二與第三種屬本篇可直接規範的研究對象。本文給出完整的指令家族、消耗性權限及效果型別、可觀察的小步執行模型、靜態驗證器的最低規則、後端 lowering 的證明義務,並在明確前提下提出六項條件性安全命題。配合反例、差異測試、模型檢查及現有 CPU/GPU 的消融基線,本篇使「持續性擴散」從容易被任意解讀的設計理念,收斂為可被編譯器拒絕、Runtime 監測、測試工具反駁的程序語義契約。

本文不宣稱已發明非同步執行、資料流、actor、效果系統、GPU graph、交易提交或自訂指令擴充。與 LLVM/MLIR/CUDA 等既有機制的對照,被用來說明適當的工程承載與可能的冗餘成本。SMPDC 所需驗證的增量是:這套多主—相位—有界擴散—證據—提交聯合語義,是否比將相同機制分散實作於一般函式庫更易維護、更能保留正確性,或在某些工作負載具有扣除完整成本後的效益。

關鍵詞: 持續擴散指令集、抽象 ISA、虛擬機器、型別效果系統、線性資源、相位耦合、多主工作流、信用式傳播、有界擴散、異源佐證、編碼冗餘、推測執行、權威提交、GPU 異質執行、MLIR、Compiler Lowering、形式化驗證、可證偽實驗。


1. 本篇的研究位置:不再只描述系統,而是定義「合法動作」

1.1 前篇交出的問題

Paper 01 的 PrimaryFlowNode Contract v0.1 讓工作流具有穩定身分與局部受控狀態,並把邏輯工作流與 OS worker、邏輯 CPU、實體 CPU 核心分離。Paper 02 的 PhaseDiffusion Contract v0.1 讓相位只在具互動效果時成為有效執行座標,對訊息傳播引入 event epoch、耦合資格、有限 credit、TTL、背壓與靜止偵測。Paper 03 的 RedundantFlowReconciliation Contract v0.1 區分 R0 單路、R1 精確複製/競速、R2 異源佐證與 R3 編碼恢復,拒絕將副本當作獨立證據。Paper 04 的 SpeculativeCommit Contract v0.1 則將局部計算與正式提交分開,使推測值、設備完成事件、局部證據和權威決策不再可以被無條件互換 [I1–I4]。

上述前提尚未指定程序執行器看見一個操作時,究竟能改變哪些受控狀態。如果 DIFFUSE_SEND 可以無聲增加 credit,或 RECONCILE_SEAL 意外回寫全域狀態,則理論在工程上並不封閉;同理,若 COMMIT_DECIDE 只是普通 bool 函式,任何模組都可以偽造 true,亦不可能保留前篇的安全性。

本篇因此建立語義標準,而不是先發明漂亮語法。

1.2 三項研究問題

RQ05-1|指令資格: 何種行為應被提升成可供編譯器理解的抽象指令?有多少指令只是現有 coroutine、atomic、queue、transaction、GPU kernel 的別名?

RQ05-2|合法性: 如何使「不得複製 credit」「不得越權提交」「局部有效值不等於正式結果」「GPU 完成不等於 HostVisible」成為檢查器能拒絕或 Runtime 能阻止的規則?

RQ05-3|可降階性: 這些操作能否在既有通用 CPU、OS 與 RTX 3070 等一般 GPU 上經過語義保留地執行,再根據實際證據決定是否研究硬體 ISA 擴充?

1.3 本篇的研究交付

  1. PDAIS Abstract ISA Specification v0.1:指令家族、字面識別與規範級別。
  2. PDAIS Type-and-Effect Contract v0.1:型別、效果、授權、消耗性 token。
  3. PDAIS Small-Step Machine v0.1:可觀察轉移及失敗/等待/未知狀態。
  4. PDAIS Verification Obligations v0.1:靜態驗證、Runtime guard、後端轉換。
  5. PDAIS Trace & Conformance v0.1:差異測試、故障注入及可回放證據。
  6. Paper 06 Handoff v0.1:供新程式語言、編譯器前端及型別推導使用的最小介面。

1.4 四個不可混淆的指令層級

層級 本篇名稱 例子 何時可宣稱已實現
L-A Source construct diffuse value to peers 真正有 parser、typed AST 與語言語義
L-B Abstract instruction DIFFUSE_SEND 存在可執行參考解釋器及 conformance tests
L-C Typed IR operation smpdc.diffuse.send 存在 IR verifier、passes 與 lowering
L-D Physical ISA opcode 新的定製 CPU 編碼 ISA 配置、RTL/微碼或硬體載體已實作並驗證

本文規範 L-B、提出 L-C 的候選,僅為 L-A 和 L-D 建立必要條件。高階 instruction set 是可執行語義的名稱,不等於已取得實體 CPU 指令編碼。

1.5 規範詞與研究成熟度

本文中的**必須(MUST)**表示候選規格要求;**應(SHOULD)**表示有理由的預設策略;**可以(MAY)**表示允許但不保證的擴充。這些規範詞不是宣稱已通過實機測試。所有安全結論皆為有限模型或指定故障假設下的候選條件命題;形式證明與硬體實作成熟度應分開標註。


2. SMPDC 與既有指令、資料流和硬體架構的界線

2.1 傳統指令的本地性與跨節點指令的差別

傳統通用 ISA 通常將算術、記憶體、控制流、原子性與特殊設備交互映射為 CPU 可執行操作。PDAIS 處理的則是跨越持續工作流的狀態轉移協議。COUPLE_ADMIT 可以涉及共享狀態、授權與兩個工作流的相位,這通常不是一顆 CPU 核心單步就能原子完成的事情;在現有硬體上,它可能需要一組函式、原子操作、佇列動作和受權威控制的狀態轉換。

如果命名成「一條指令」,並不讓多步協議突然變成單週期、無限頻寬或零延遲的硬體行為。這是 PDAIS 必須嚴格維持的誠實性邊界。

2.2 成熟機制已經存在

以下能力並非本篇首創:資料流觸發、Kahn 程序網絡、擴散計算終止偵測、背壓、actor 訊息、線性型別、原子記憶體操作、快照隔離、交易日誌、可編譯 GPU 圖、MLIR dialect 與 LLVM 的記憶體模型 [E1–E7]。

特別是 MLIR 本身已允許定義新的 operations、types、attributes 與 dialect-specific verification;async 與 gpu dialect 已有非同步 token 和 GPU 依賴模型 [E1–E3]。因此若 PDAIS 只是把 async.await 改名為 PHASE_WAIT,就沒有獨立研究價值。其增量必須是跨協議的可檢查責任,例如:帶有 credit 的擴散不能突破總量、尚未提交的推測值不得被提升為正式可見結果、R1 副本不得偽裝成 R2 獨立證據。

2.3 何時值得研究物理 ISA?

只有在下列證據累積後,才可以將部分 PDAIS 操作列為硬體 opcode 候選:

  1. Reference Runtime 與已優化的傳統 C++/Rust/MLIR 基線在相同工作負載上比較完成;
  2. 明確指出瓶頸位於可由新指令改善的原子性、隊列提交或細粒度狀態更新,而非外部記憶體頻寬不足;
  3. 新指令可提供具體可驗證的記憶體順序、例外、存取控制及中斷/上下文切換語義;
  4. 假設 RTL、FPGA 或模擬硬體的面積、功耗、時序、驗證成本與軟體收益均可計量;
  5. 不能僅用「神經形態」「群星拓撲」或「類似大腦」作為替代工程證據。

RISC-V 提供模組化 ISA 擴充研究的正式文獻環境,但是否採用 RISC-V、如何分配 custom encoding、是否存在必要的指令語義與相容性成本,都應在 Paper 09 或後續硬體專篇再決定 [E6]。


3. 最小抽象執行機器與可觀察語義

3.1 機器狀態

延續 Paper 00 的九元中觀狀態,但不新增第十項本體軸,本篇定義候選抽象機的可檢查投影:

M=⟨F,X,P,K,M,B,R,C,A,T⟩.\mathbb M = \langle F, X, P, K, M, B, R, C, A, T \rangle.

其中:

  • FF:持續工作流身分、生命週期與承載租約登錄;
  • XX:版本化局部狀態與可被保護的共享狀態讀取視圖;
  • PP:具型別 phase 狀態及其因果/版本依賴;
  • KK:合法的耦合邊、拓撲世代及撤銷狀態;
  • MM:邏輯訊息、物理傳送嘗試與佇列義務;
  • BB:有限 credit、容量、位元組數、TTL 及控制通道預算;
  • RR:R0–R3 候選、證據、比較器與局部聚合登錄;
  • CC:可撤銷分支、版本依賴、正式提交及外部效果記錄;
  • AA:權限、受控域、世代 fencing 及可委派能力;
  • TT:事件追蹤與可解釋的可觀察結果。

這是解釋器狀態的分解,不是宣稱每一項需存在獨立的硬體記憶體區。對應舊有九元形式,所有元件可視為工作流、關係、訊息、資源或契約狀態的進一步具體化。

3.2 指令與標籤化狀態轉移

指令集合記為 I\mathcal I,一個合法執行步記為:

M→i,ℓM′,i∈I.\mathbb M \xrightarrow{i,\ell} \mathbb M', \qquad i \in \mathcal I.

ℓ\ell 是具型別事件標籤,記錄 operation_id、flow_id、event_epoch、authority_scope、合法的資源消耗、狀態結果以及因果前驅。對於被拒絕的呼叫,可存在有記錄的拒絕轉移,例如將 InvalidCredit 記入 TT,但不得偷偷改動原應受到保護的 BB 、 CC 或 AA 狀態。

定義成功、等待與失敗的結果代數型別:

StepResult<T> =
    Applied(T, observable_event_ref)
  | Pending(wait_condition, cancel_handle)
  | Rejected(error_code, evidence_ref)
  | Failed(error_code, recovery_hint)
  | Unknown(query_handle, scope)

Pending 不等於 Failed;Unknown 不得當作 Rejected 自動重試,因為某個提交決策可能已完成但回應在途中遺失。

3.3 內部步與外部可觀察結果

容許解釋器擁有對使用者不可見的內部步 τ\tau,例如本地資料結構移動或合法批次整合。但下列效果預設不得直接當成 τ\tau 刪除:

  1. 權威變更及租約世代遞增;
  2. credit 保留、消耗或正式清償;
  3. 具身分訊息的合法送出及失敗;
  4. 候選證據的來源與驗證等級變更;
  5. 提交決策、可見性發布及不可逆外部效果;
  6. 被其他工作流依賴的 phase/耦合資格改變;
  7. 能影響故障恢復、重播及取消的事件。

對可能產生觀察差異的優化,編譯器不能以「最後數值相同」作為唯一等價標準。

3.4 Trace 語義、部分順序與決定性

對完整執行 π\pi,定義可觀察投影 Obs⁡(π)\operatorname{Obs}(\pi),至少包含授權效果、外部可見結果、版本和對應錯誤分類。對兩個實作 AA 與 BB,是否語義等價,必須先指定相同的輸入、環境、故障模型及可允許的事件重排:

A⊑OB⟺Traces⁡O(A)⊆Traces⁡O(B).A \sqsubseteq_{\mathcal O} B \quad \Longleftrightarrow \quad \operatorname{Traces}_{\mathcal O}(A) \subseteq \operatorname{Traces}_{\mathcal O}(B).

這是本篇採用的候選trace refinement 條件。若某程序要求位元級重現,允許重排集合便應縮小;若只要求最終合法提交集與因果偏序一致,則可容許無觀測影響的獨立訊息重排。不得在未聲明一致性等級時籠統宣稱「結果是確定性的」。

3.5 安全、進度與公平性分開

  • 安全性: 不應出現未授權成功送出、不可解釋的 credit 擴張、未經審核的提交、非法效果或失效世代回寫。
  • 活性: 某些有資格繼續的操作是否最終獲得執行機會,取決於排程公平、資源可用、網路及故障假設。
  • 停止性: 單次已封閉 event epoch 能否靜止,需考察在途義務及新消息封閉,而不由工作流物件是否仍存活來判定。
  • 效能: 安全與活性條件既不單獨推出低延遲,也不推出能源效率。

4. 指令操作所依賴的身分、世代與型別

4.1 跨層生命週期識別、世代與正式鍵

以下識別不得共用單一可碰撞計數器來取代語義:

身分/世代 作用 不可推導的事項
FlowId 長期主要工作流身分 不等於某顆 OS CPU ID
FlowGeneration 工作流管理版本 不等於事件世代
EventEpoch 一批相位擴散義務 不等於權威世代
TopologyGeneration 耦合圖有效版本 不等於提交序列號
AuthorityGeneration 作用域權威 fencing 不等於租約到期時間
StateVersion 局部或共享狀態視圖版本 不等於 wall-clock 時間
CommitKey 正式決策的冪等識別鍵 不等於 message hash
EffectKey 外部效果與重試身分 不等於外部服務已完成證據

一個事件可能包含多個上述欄位;哪一些必須實際傳輸,取決於 receiver 是否能以不可變或受保護的本地資料恢復完整語義。

4.2 值型別、封套型別與權限型別

以下為 Paper 05 的抽象型別,不是已能被 Rust/C++ 編譯器直接接受的原生型別:

FlowHandle<F>                 FlowState<F, S, V>
Lease<F, G, Scope>            PhaseState<F, E, Kind>
PhaseEvidence<E, Kind>        CouplingProposal<Edge, E>
AdmittedEdge<Edge, TopGen>    EpochHandle<E, State>
SendCredit<E, Id>             ReservedCredit<E, Id>
DeliveryPermit<E, MsgId>      Message<MsgId, Payload>
DeliveryAttempt<MsgId, A>     Candidate<ResultId, Origin>
IndependentWitness<Origin>    EncodedShard<Group, Index>
LocalOutcome<ResultId>        SealedLocalOutcome<ResultId>
Snapshot<T, Version>          Tentative<T, Branch>
SpecBranch<Branch, State>     CommitProposal<Domain, K>
ValidatedProposal<Domain, K>  CommitDecision<Domain, K>
Committed<T, K>               EffectRecord<EffectKey>
GPUEvent<Device, Work>        BufferLease<Device, Buffer>
HostVisible<T, Buffer>        TraceEvidence<EventId>

IndependentWitness 必須帶有已審核的來源與獨立性條件;它不能僅由程式員執行 cast,或由 R1 的第二次傳送得到。HostVisible 也不是一個可由 GPUEvent 任意轉型的證書。

4.3 效果型別

候選效果集合定義為:

Effect =
  PhaseObserve | PhasePropose | CouplePropose | CoupleAdmit
  | SendReserve | SendNonAuthoritative | SendAcknowledge
  | ReconcileLocal | VerifyLocal | WriteOwnedState
  | SpeculateLocal | GPUEnqueue | GPUWait
  | CommitPropose | CommitValidate | CommitArbitrate
  | PublishCommitted | EffectEnqueue | EffectDeliver
  | LeaseRebind | TraceAudit | EpochLifecycle

每個操作都對一個效應集合 ε(i)\varepsilon(i) 作出聲明。只持有 PhaseObserve 的工作流,不能透過呼叫 PHASE_SIGNAL 取得 WriteOwnedState;同理持有 VerifyLocal 也不構成 CommitArbitrate。

4.4 消耗性權限:線性與仿射

對有限發送 credit、單次提交能力及有獨占責任的 buffer lease,可採**線性(必須明確移交或清償)或仿射(最多使用一次,可依規範棄置)**的型別規則。其基本資源約束為:

Γ;Δ⊢i:T  !  ε,\Gamma;\Delta \vdash i : T\;!\;\varepsilon,

其中 Γ\Gamma 存一般可複用資料, Δ\Delta 存需控制使用次數的能力 token。消耗性操作要使原 token 離開可使用上下文;不得因 SSA 名稱仍可讀取,就讓它被第二次使用。

此類型限制只是預防一般程式錯誤的第一道防線。跨程序共享、惡意呼叫、crash-restart 及外部串接仍必須在 Runtime 與真正仲裁權威再次檢查。不能宣稱型別檢查可以替代實體授權或耐久日誌。

4.5 時間、快取與設備型別不代表能力

LogicalCPU、PhysicalCore、CacheDomain、CCD、NUMARegion、GPUDevice 是承載描述子而非寫入權威。編譯器可用來估計 latency、data locality 及 kernel placement,但不可把「預期某核心比較快」推導成「該核心有更強的提交權限」。P-core/E-core 的能力差異、多 CCD 快取拓撲及 SMT 資源共享,均須由實際平台發現與量測提供。


5. 操作分類與版本相容規則

5.1 三級操作等級

本篇將操作分為三種規格等級:

  • Core(C): V0 參考解釋器必須支援,失敗必須可觀察。
  • Extension(X): 由 capability discovery 宣告後才能使用;缺少實作時應拒絕而非虛構成功。
  • Alias(A): 為方便閱讀或承接舊稿保留的語法糖,須明確展開為 C/X 操作。

例如 Paper 00 的 DIFFUSE 是 Alias,不得與具 credit、message envelope 及 epoch check 的 DIFFUSE_SEND 視為同一種無條件 primitive。

5.2 核心家族索引

家族 命名空間 工作 對接前篇
Flow FLOW_* 穩定工作流、生命週期、租約 Paper 01
Phase PHASE_* 相位訊號、就緒及監測 Paper 02
Coupling COUPLE_* 動態邊與拓撲世代 Paper 02
Diffusion DIFFUSE_*, EPOCH_* 傳輸、配額、背壓、靜止 Paper 02
Redundancy REDUNDANCY_*, MESSAGE_*, RECONCILE_* R0–R3 與局部證據 Paper 03
Speculation SPEC_* 可撤銷分支與血緣 Paper 04
Commit COMMIT_* 正式提交域與版本驗證 Paper 04
Effects EFFECT_* 外部副作用隔離及投遞 Paper 04
Device GPU_* 異質批量協作與可見性 Paper 08,承接 Paper 04

5.3 每條指令都必須公開的七件事

一個 conformant operation 必須公開:signature(輸入/輸出型別)、guard(前置條件)、effect(受控狀態變動)、cost(可用資源與計量)、failure(拒絕/異常)、replay(重播規則)、trace(最低證據欄位)。缺少任何一項,就不能被視為可對外宣稱符合 PDAIS v0.1 的完整操作。

5.4 版本協商與未知指令

ABI/協議封套最低需提供:

PDAISModuleHeaderV0_1 {
    pdais_major: 0
    pdais_minor: 1
    required_features: Set[FeatureId]
    optional_features: Set[FeatureId]
    schema_registry_digest: Digest
    effect_policy_digest: Digest
    lowering_target: Virtual | HostCPU | HostGPU | Hybrid
}

任何未知且帶權威或資料副作用的 required operation,必須 UnsupportedRequiredOperation 結束,不能默默跳過。讀取不到 feature 的 optional operation 可以採在規格中登記過、具有相同可觀察契約的 fallback;無 fallback 時回傳顯式錯誤。此限制適用於向前相容,也適用於惡意或不可信 IR 輸入。


6. Flow、Phase 與 Coupling 家族

6.1 Flow 家族

指令 等級 最小簽名與結果 規範效果/限制
FLOW_OPEN C (spec, cap) -> FlowHandle 登記穩定 flow_id,不能憑命名取得共享寫入權
FLOW_PERSIST C (flow, state, persistence_policy) -> SnapshotRef 保留版本與工作流責任,不強制實體 CPU 一直忙碌
FLOW_WAKE C (flow, event) -> StepResult<Ready> 只在合法租約及足夠資源下喚醒
FLOW_YIELD C (flow, reason) -> StepResult<Suspended> 明確暫停/歸還可用執行資源
FLOW_REBIND X (flow, target, new_fence) -> Lease 必須先按 Paper 01 撤銷或 fence 舊 lease
FLOW_CLOSE C (flow, closure_policy) -> Closed 確認未清責任、發送和提交處理方式

FLOW_PERSIST 的「持續」不能解讀為一個 OS thread 永遠佔用同一顆 physical core。只要邏輯身份、狀態及責任受契約維持,休眠後再喚醒仍然是同一個工作流。

6.2 Phase 家族

指令 等級 最小簽名與結果 規範效果/限制
PHASE_READ C (flow, phase_kind) -> PhaseObservation 可觀察且可注明版本,無權修改相位
PHASE_SIGNAL C (flow, epoch, kind, payload, permit) -> PhaseEvidence 發布具型別、可驗證依賴及來源的相位事件
PHASE_WAIT C `(flow, predicate, deadline) -> Pending Ready`
PHASE_VALIDATE C (phase_evidence, relevant_task) -> EvidenceStatus 判斷相位是否對任務具有實際互動效果

PHASE_SIGNAL 的參數 kind 不會因填入文字 semantic 就自動獲得語義正確性。可採用 readiness、causal、sync、verification 等已定義類型,但 predicate 及合法 transitions 必須由 scope-specific schema 定義。不能以 phase=ready 取代依賴完成的證據。

6.3 Coupling 家族

指令 等級 最小簽名與結果 規範效果/限制
COUPLE_PROPOSE C (from, to, guard, quota) -> Proposal 提出候選連結,沒有啟用效果
COUPLE_ADMIT C (proposal, authority, top_gen) -> AdmittedEdge 檢查同意、權限、相位條件與拓撲世代
COUPLE_REVOKE C (edge, reason, authority) -> RevokedEdge 拒絕之後新工作;已在途義務仍需清償
COUPLE_QUIESCE C (edge, epoch) -> StepResult<Quiescent> 只能在該邊受控義務清償後成功

對已失效的 topology_generation,接收者不可因對方握有先前 AdmittedEdge 的快照就重新啟用資料擴散;需重新驗證,或依明確的 in-flight grandfathering policy 對既有義務有限處理。

6.4 局部自治與必要仲裁的界線

以上指令不意味所有網絡呼叫都由一個中央 scheduler 決定。某些合法 AdmittedEdge 可以在預授權的容量與 epoch 範圍內由各 PWN 自行使用;但預授權本身、撤銷語義、credit 身分及正式權威提交不可因此消失。多主自治是可授權的局部決策空間,不是每個節點擁有對所有狀態的主權。


7. Diffusion/Epoch 家族:把「持續擴散」寫成有限權利

7.1 指令索引

指令 等級 最小簽名與結果 關鍵守衛
EPOCH_OPEN C (root, admission_permit, budget) -> EpochHandle 外部種子入場有界;新世代不得繞過系統總額度
DIFFUSE_RESERVE C (edge, credit, bytes, epoch) -> DeliveryPermit 原子保留唯一 credit 和必要容量
DIFFUSE_SEND C (permit, message) -> DeliveryStatus 一次性消耗 permit;檢查 epoch、lease、schema、TTL
DIFFUSE_ACK C (message_key, attempt_key, outcome) -> Acknowledged ACK 不得自動增加已花費 data credit
DIFFUSE_THROTTLE C (scope, throttle_policy) -> AppliedPolicy 限制入場、佇列或並行度;不得跳過必要清償通道
DIFFUSE_CANCEL C (message_or_epoch, cause) -> CancelStatus 對已送與未送區分取消;不能偽裝召回外部副作用
EPOCH_SEAL C (epoch, authority) -> Sealing 停止新外部種子;內部未清義務照常處理
EPOCH_QUIESCE C `(epoch, obligations) -> Quiescent Pending`

DIFFUSE、THROTTLE、QUIESCE 可作為語言簡稱,但不能成為沒有 epoch 與 authority_scope 的黑盒捷徑。

7.2 發送權的資源方程

沿用 Paper 02 的不可複製 credit 模型。對已封閉的世代 ee,設定初始資料發送 credit B0(e)B_0(e) 、尚未消耗且唯一歸屬的 token 數 Ue(t)U_e(t) 、已完成保留且等待最終消耗的 token 數 Qe(t)Q_e(t),與累計已消耗 token 數 Se(t)S_e(t)。在不擴增額度、不複製、不退款、轉移保守且仲裁可線性化的候選模型下:

Ue(t)+Qe(t)+Se(t)=B0(e).U_e(t)+Q_e(t)+S_e(t)=B_0(e).

此等式只計算data credit 的邏輯許可權,不是資料位元組總數,也不是所有重試封包數。對實體嘗試的 byte budget、control traffic 和不同 epoch 的 admission budget,另行配置並監測。某發送若宣稱一次 credit 多路重送,必須明確說明:是否只是 transport 層同一邏輯發送的重試?那些重試是否另受 attempt_budget 限制?不可用此名目製造無限流量。

7.3 reserve 與 send 的原子邊界

DIFFUSE_RESERVE 最低需滿足:

  1. 唯一的 credit_id 被驗證目前可花費;
  2. edge 與 event epoch 均有效;
  3. reservation record 原子地由 Available 變為 Reserved;
  4. bytes_cap、message_cap、deadline、TTL 和必要佇列槽位被檢查;
  5. 成功後回傳唯一的 DeliveryPermit,不得把同一 credit 同時授給另一 flow。

DIFFUSE_SEND 可以在檢查後將 Reserved 變為 Spent,再建立具 message_id 的受控發送義務。真正的「送出是否發生」與「接收者是否收到」在故障窗口可能未知,因此不得在 crash 後無條件重新花費新 credit。恢復流程應先查詢 durable dispatch record 與允許的重試政策。

7.4 示意性規範轉移

對合法保留,記 uu 為可用資源, qq 為預留資源,成功轉移為:

(u,q)→reserve(c)(u−1,q+1).(u,q)\xrightarrow{\mathrm{reserve}(c)}(u-1,q+1).

對可獲准的送出,預留變為已花費:

(q,s)→send(c,m)(q−1,s+1).(q,s)\xrightarrow{\mathrm{send}(c,m)}(q-1,s+1).

這裡的 11 代表一個唯一邏輯發送許可。它不描述位元數,也不隱含多跳訊息只花一個 credit。每次新獲准的資料傳播應按 policy 消耗相應許可;R1 多路、R2 佐證和 R3 shard 傳輸同樣必須計入。

7.5 失敗、取消與歸還

若 DIFFUSE_RESERVE 因容量不足被 Rejected,原 credit 不得被隱形扣掉。若 reservation 已成功但還未 send,取消可以釋放佇列槽位及位元組預留;至於 credit token 是否可返回,v0.1 為了維持 Paper 02 的「不退款」簡化安全命題,預設不能回到可重新使用的 data credit 池,而是轉入 Burned/Retired 帳本。若未來設計可退款版本,必須新立原子 token 回收契約,並重新證明傳播數量上界。

從而對取消引入終態 De(t)D_e(t) (已作廢且不可再花費的預留),資源方程修正為:

Ue(t)+Qe(t)+Se(t)+De(t)=B0(e).U_e(t)+Q_e(t)+S_e(t)+D_e(t)=B_0(e).

這一修正與上一節的簡化式不是矛盾:上一節不含取消作廢時 De(t)=0D_e(t)=0 ;實際執行器應採含 DeD_e 的完整方程。Spent 的送出許可也不會在 ACK 後重生。

7.6 control credit 與活性

DIFFUSE_ACK、取消、租約撤銷與 epoch 清償都需要資源。如果控制訊息使用同一個已耗盡的資料 credit 池,可能形成永久等待。故參考機器必須將 data_credit、control_budget 與 external_epoch_admission_budget 明確分離,並要求 EPOCH_QUIESCE 能追查未完成的 control obligations。這不是保證在任意網路故障下必然終止,而是避免由資源設計本身構成可預見的無法進展情況。


8. 冗餘資訊流與聚合指令:R0–R3 不能被合併成一種 REPLICATE

8.1 紅線:傳送身分不等於證據身分

延續 Paper 03,必須維持四層不同的識別鍵:

ResultId
  └─ CandidateId
      └─ MessageId
          └─ DeliveryAttemptId

此階層是可能的關聯樹示意,不是所有情況都一對一。某結果有多個獨立候選;一個候選可能由多條訊息承載;相同訊息可以有多次 physical delivery attempts。兩次 R1 傳輸若指向同一 CandidateId,不能自動算作兩份獨立佐證。

8.2 Redundancy 家族

指令 等級 輸入/輸出概要 規範效果
REDUNDANCY_PLAN C (result_id, R0–R3, cost, policy) -> Plan 驗證模式、證據與預算;不立即發送
BRANCH_ADMIT C (candidate, target, guard, credit) -> AdmittedBranch 請求對某合法擴散路徑入場
MESSAGE_REGISTER C `(logical_key, digest, epoch) -> Registered Existing
RECONCILE_COMPARE C (candidate_set, comparator, evidence) -> Comparison 比較內容、來源、版本;不能默默消除衝突
RECONCILE_SELECT C `(result_id, quality_contract) -> Selection Hold`
CODED_RECOVER X `(scheme, indexed_shards, erasure_model) -> Recovered Insufficient`
CONFLICT_HOLD C (result_id, conflicts, reason) -> OnHold 保留不可任意合併的證據和來源
RECONCILE_SEAL C (result_id, round_id) -> SealedLocalOutcome 關閉一輪局部選擇;不是正式提交
RECONCILE_EXPORT C (sealed, evidence_ref) -> LocalOutcome 向 Paper 04 提供可審查的候選輸出

RECONCILE、REPLICATE、VERIFY 在 Paper 00 是便利名稱;本篇把其實際合法性分解到上述原語,避免一個泛用函式同時宣稱完成去重、糾錯、來源認證與權威提交。

8.3 R0/R1/R2/R3 的型別義務

類型 允許的建構 本地結論上限 必須禁止的推論
R0 單路結果與必要校驗 單候選結果 傳送成功不等於答案正確
R1 相同結果的多路、hedging、重送 更早可用的同源候選 兩路相符 ⇒ 獨立驗證
R2 真正異源、異算法、異失效域的候選 有條件佐證或衝突揭露 兩票多數 ⇒ 真理
R3 已宣告編碼、索引與錯誤模型的 shard 通過解碼與驗證的恢復 payload 任意兩份相似資料 ⇒ 可恢復

所有 R 類型均受 quality policy、來源檢查與正式提交邊界約束。

8.4 R1:競速是延遲策略,不是雙重證據

令兩次傳送的耗時為 T1,T2T_1,T_2,驗證時間為 VV,競速策略在某些獨立路徑且資源競爭可接受的情況下,可使可用候選時間近似為:

TR1=min⁡(T1,T2)+V+H,T_{R1}=\min(T_1,T_2)+V+H,

其中 HH 是建立、排程、複製、取消與競爭開銷,且在真實系統中可能依兩條路徑共同變動。因此, TR1T_{R1} 不一定小於 T1+VT_1+V ;兩份傳送內容一致亦不增加 IndependentWitness 的數量。可用對照包含 Hedged Requests 與先到先處理模型 [E8]。

8.5 R2:來源獨立性不得用型別名稱偽造

對候選 cic_i 及 cjc_j,定義待檢查的條件集合:source_lineage、model_or_algorithm_id、shared_training_data、seed、shared_failure_domain、quality_policy。只有通過該任務所需的獨立性門檻,才可發給 IndependentWitness<Origin>。發給此類型別不表示結果自動真實,而是表示某種已聲明的依賴分離條件通過。

若兩候選互相矛盾,RECONCILE_COMPARE 必須產生 Conflict 或 NeedsFurtherEvidence,不能只因其中一個路徑較快而視其正確。

8.6 R3:編碼復原須列明錯誤模型

對一個 (n,k)(n,k) 擦除碼模型,若有 kk 個滿足指定解碼條件的有效份額,才可能重建原資料:

Recover⁡n,k(S)=xrequires∣Svalid∣≥k.\operatorname{Recover}_{n,k}(S) = x \quad\text{requires}\quad |S_{valid}|\ge k.

此公式只描述在合適編碼與擦除模型下的最低門檻。當存在惡意錯誤份額、索引重複、共用錯誤來源或未通過完整性檢查時,必須另外引入正確的錯誤/拜占庭模型,不可直接沿用擦除保證。CODED_RECOVER 失敗須保留可審計原因,不能輸出未驗證的完整 payload。

8.7 Aggregator 不得被迫合併不可交換操作

若 RECONCILE_SELECT 要合併多個 state delta,必須明確提供結合性、交換性、冪等性或合法順序的證據。對一般的覆寫、檔案寫入、付款、模型權重變更、資料庫跨鍵約束,不能因「去重成功」就認為 merge 合法。CRDT 可作特定資料型別的有用對照,卻不能替代交易授權與所有副作用的安全界線。


9. 推測執行指令:計算可以先行,效果不得偷渡

9.1 Speculation 家族

指令 等級 輸入/輸出概要 關鍵約束
SPEC_BEGIN C (scope, snapshot, rollback_policy) -> Branch 快照版本、隔離及撤銷能力完整
SPEC_READ C (branch, object, version_guard) -> TentativeRead 記錄讀集合和相關版本或謂詞
SPEC_DERIVE C (branch, pure_or_isolated_op, deps) -> Tentative 不得觸發不可撤銷外部效果
SPEC_FORK C (branch, candidate_plan, bounded_credit) -> ChildBranch 血緣有界且 lineage 不得遺失
SPEC_ATTACH_GPU X (branch, gpu_event, buffer_contract) -> TentativeDeviceDependency 必須保留 device/host 資料可見性契約
SPEC_INVALIDATE C (branch, reason) -> Invalidated 將所有依賴後代列為需重新驗證或撤銷
SPEC_ABORT C `(branch, reason) -> Aborted PendingCleanup`

SPEC_DERIVE 允許本地計算、對受控暫態區寫入或帶完整依賴的異步啟動;它不允許直接回寫 canonical state,也不可以透過外部 API 暗中提交帳務或發送不可撤銷通知。

9.2 推測結果的型別不是正式結果

定義:

Tentative<T, BranchId, SnapshotVersion>

它可在受信任的分支隔離域中被另個 SPEC_DERIVE 消費,卻不能隱式轉為 Committed<T,K> 或一般不可回滾的外部值。若語言內建 unwrap_tentative() 而不要求上下文攜帶分支血緣,便破壞 Paper 04 的先前承諾。

9.3 推測可視性與依賴撤銷

當 A 產生暫態結果 aa,B 依其繼續計算 b=f(a)b=f(a),則 B 必須保留對 A 的證據性依賴。若 A 因輸入版本過期被宣告失效,B 不得默默丟棄依賴後提交。候選依賴關係形成有向圖 GBG_B,對失效分支 bib_i 的撤銷閉包為:

InvalidateClosure⁡(bi)={bi}∪Descendants⁡GB(bi).\operatorname{InvalidateClosure}(b_i) = \{b_i\}\cup\operatorname{Descendants}_{G_B}(b_i).

若使用 cache 共用或跨工作流值重用,Compiler 需要證明該值與被撤銷祖先無關,才能將它從閉包中排除。

9.4 何時不得建立推測分支

  • 完全不可隔離的外部效果是分支核心操作;
  • Snapshot 或資料來源缺少版本驗證能力;
  • 狀態依賴帶有不可接受的隱藏讀取;
  • Runtime 無法控制回滾資源上界;
  • GPU 任務已占據大量 VRAM、難以撤銷且預測收益很小;
  • 同一 commit domain 缺少能安全仲裁其結果的權威。

此時應回退到有明確同步的傳統執行,不應為維持理論形象強迫使用 speculation。


10. 權威提交指令:提交不能等於寫入布林值

10.1 Commit 家族

指令 等級 輸入/輸出概要 最低實際語義
COMMIT_PROPOSE C (branch, sealed_outcome, isolation) -> Proposal 必須有提交提議權,帶 read/write/predicate sets
COMMIT_VALIDATE C `(proposal, versions, predicates, fence) -> Validated Rejected`
COMMIT_DECIDE C `(commit_key, digest, authority) -> Decision Unknown`
COMMIT_QUERY C `(commit_key, authority) -> KnownDecision Unknown`
COMMIT_PUBLISH C `(decision, visibility_contract) -> Published Pending`

COMMIT_VALIDATE 只是必要的一道 guard,不能單靠 Validated=true 就完成正式提交。COMMIT_DECIDE 必須由合法的 authority domain 處理;API 呼叫者自行傳入 authority="admin" 字串不是授權證明。

10.2 五段進度與不可混淆的事件

參照 Paper 04:

ComputedTentative
  -> LocalVerified
  -> PreparedCandidate
  -> AuthoritativelyDecided
  -> PublishedCommitted

其中可見性和持久性還需要自己的 contract。下面是禁止直接轉型的路徑:

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

任何合法的中介轉換均必須有明確的能力與證據。這個禁止關係是對無守衛隱式轉型的否定,不是說操作永遠不可經合法程序轉換。

10.3 COMMIT_DECIDE 的線性化需求

對單一 commit domain dd 與同一穩定提交鍵 kk,需由權威登錄維持:

∀k,∣AuthoritativeDecision⁡(d,k)∣≤1.\forall k,\quad |\operatorname{AuthoritativeDecision}(d,k)|\le 1.

此約束須透過被所有相關寫入路徑共同尊重的原子唯一仲裁來維持,而不是透過兩個互不連通的 thread-local map 假裝全域唯一。若多個互不協調的權威都對相同 domain 自稱合法,則上述命題沒有前提基礎;真正跨 fault domain 的共識與持久性成本不得隱去。

10.4 Unknown 的非冪等風險

若 COMMIT_DECIDE 在持久化決策後崩潰,呼叫者可能只看到逾時。這時候不能立即生成新 commit_key 再提交一次。合法流程應先 COMMIT_QUERY(k,d),依決策記錄回覆重試或顯式保留 Unknown。對一組相同鍵但不同 payload digest 的提案,仲裁必須回 ConflictingProposal,不能把第二個覆蓋第一個。

10.5 Snapshot isolation 不是所有任務的足夠契約

如 Paper 04 所示,兩個基於同一快照的交易可能各自寫入不同鍵,但一起破壞跨鍵不變量。因此 COMMIT_VALIDATE 不能只檢查每個寫入鍵的舊版值。若 workload 要求 serializable 或跨鍵約束,須包括謂詞依賴與必要的衝突檢查/鎖定或可證明的序列化策略;否則指令必須拒絕虛假的隔離保證。


11. 外部效果指令:正式狀態與不可逆世界之間的牆

11.1 Effects 家族

指令 等級 最小輸入/輸出 最低要求
EFFECT_ENQUEUE C (commit_record, effect_key, payload) -> OutboxRef 效果必須與有效提交記錄有明確關聯
EFFECT_DELIVER C (outbox, receiver_policy) -> DeliveryOutcome 接收者冪等能力或明確重試風險
EFFECT_QUERY C `(effect_key, target) -> Known Unknown`
EFFECT_COMPENSATE X (effect_key, new_operation) -> CompensationRecord 以新操作補償,不能宣稱原效果從未發生

某效果可以先記入耐久 outbox,再由工作者對外投遞。但若接收端沒有可靠的去重或事務協議,端到端 exactly-once 通常無法只靠本地 outbox 保證。對付款、郵件、外部 API 及檔案系統副作用,本篇要求清楚聲明使用者可見的真正保證,而不是把 at-least-once 嘗試包裝成 exactly-once。

11.2 攔截不可逆副作用的型別規則

候選規則:

SpecBranch<Open> + NonRollbackableEffect
  => TypeError(EffectOutsideCommitDomain)

CommittedRecord<K> + EffectCapability<E>
  => MayEnqueueEffect<K,E>

只在受控 Runtime 中可攔截的效果能靜態保證不越權;透過未受控的 native FFI 或惡意 plugin 仍可能繞過語言監督。若允許此類能力,模組應被標示為 unsafe_external_effect,並以額外 sandbox 與審計約束限制範圍。

11.3 補償不是回滾

EFFECT_COMPENSATE 必須有新的識別鍵與明確、可見的補償紀錄。例如已寄出的通知不能回滾成「從未寄出」;已退款操作不能等同原扣款根本沒發生。任何使用此操作的論文效能或可靠性評估都必須把補償成本納入。


12. GPU 家族:異質運算必須有真實的記憶體與事件語義

12.1 指令索引

指令 等級 最小輸入/輸出 規範效果
GPU_BATCH X (device, operation, input_leases, policy) -> GPUEvent 提交適合並行的運算工作及依賴
GPU_WAIT X `(event, timeout) -> DeviceComplete Pending`
GPU_MAKE_HOST_VISIBLE X (event, buffer, visibility_policy) -> HostVisible 經合法同步、轉移與 memory ordering 才可使用
GPU_RELEASE_BUFFER X `(buffer_lease, outstanding_use) -> Released Pending`

SPEC_ATTACH_GPU 與 GPU_BATCH 層次不同:前者將某個已存在的設備依賴掛在推測分支上;後者真正啟動工作或提交一個 GPU 計算圖的執行。

12.2 CPU/GPU 並不共享一個抽象的零延遲資訊海

在一般帶離散顯示卡的桌機上,CPU 與 GPU 之間仍存在傳輸、記憶體管理、driver、排程和同步成本。具有 shared memory 的某些平台也不保證所有資料對任意執行者即時一致。使用 GPU 以 batch 或 graph 形式處理一大批耦合權重、圖遍歷、比較器、稀疏路由或編碼恢復可能有價值,但 GPU_BATCH 的結果只能是經明確合法映射後的設備執行證據,而不是新的 CPU 核心互連。

12.3 參照 MLIR 與 CUDA 的既有非同步語義

MLIR gpu dialect 支援可作為依賴的 GPU async token,async dialect 亦有明確的 await 機制 [E2–E3]。NVIDIA CUDA Graphs 已經將圖定義、實例化與多次啟動分開,並討論 GPU ordered allocation 的生命週期、graph update 和 device-side graph launch [E4]。因此 PDAIS 不應將「GPU 圖重用」「GPU 異步任務」「token 同步」包裝為本篇首創;它需要增加的是這些設備事件和 SMPDC 的 epoch、版本、推測分支、提交責任之間的可驗證接口。

12.4 必須明確的記憶體順序

合法的 host-side queue 寫入、讀取及跨執行緒傳輸,須根據 target 的記憶體模型建立正確的 happens-before 關係。CPU atomics 的 release/acquire 或 seq_cst 等並非裝飾字詞,LLVM 也已具體規範其意義 [E5]。但 CPU 對 host memory 的可見性不會自動推出 GPU device buffer 已同步完畢;GPU_MAKE_HOST_VISIBLE 必須依設備 API 支援的事件、轉移、同步與緩衝生命週期實作。

12.5 可選 GPU 無損回退

若 GPU_BATCH 只是參考 CPU operator 的可並行實作,且其語義允許使用同樣精度、順序與失敗處理的 CPU 路徑,可以降階回 CPU。若 GPU operator 使用不同的浮點精度、非確定性 reduction、特殊位元級演算法或缺少可替代的 driver 支援,編譯器不得宣稱無損回退。可採精度契約或審核後的近似模式,但必須在模型品質及可重現性報告中公開。


13. 狀態碼、失敗代數與恢復規則

13.1 共用的最小狀態分類

任何具有傳播、版本、權威或外部副作用的指令,必須回傳下列分類之一,或返回可明確映射的更具體型別:

類別 最低狀態 不可以當作
Accepted Applied, Prepared, Scheduled 對所有後續階段保證成功
Wait PendingCredit, PendingPhase, PendingGPU, PendingAuthority 永久故障
Soft refusal Backpressure, BudgetExceeded, EpochSealed 執行器損壞
Guard failure StaleEpoch, StaleLease, InvalidCredit, InvalidTopology 自動重送的授權
Evidence failure BadSchema, InsufficientEvidence, CorrelatedWitness, InvalidShard 原值已被修正
Commit failure StaleSnapshot, PredicateConflict, MissingDependency, ConflictingProposal 未曾嘗試寫入
External uncertainty UnknownCommit, UnknownEffect, ExternalReceiverUnavailable DefinitelyNotApplied
Fatal InvariantViolation, CorruptLog, UnsupportedRequiredOperation 可靜默忽略

當存在 Pending,執行器需要 cancellation handle、deadline、查詢路徑或可證明的等待條件。對 Unknown,查詢必須優先於新提交鍵及重複外部效果。

13.2 錯誤分配與狀態原子性

若指令 i 在其主要 guard 之前失敗,受控狀態應維持可檢查的無成功效果狀態;若 i 是跨多階段的協議(如 send 或 commit),錯誤模型必須區分尚未嘗試、已保留未提交、決策可能已完成但回應遺失。錯誤碼不能簡化為單個 false。

13.3 回滾不是時間倒流

SPEC_ABORT 可以撤銷合法暫態資料,但不能恢復已被其他流程觀察或在不受控設備上產生的副作用。COMMIT_PUBLISH 若已使正式結果在約定的範圍可見,後續改變必須經新的正式狀態變更或相應補償。對外部效果只能討論可證明的冪等/補償/風險報告,而不可宣稱所有結果都能完整「回到原點」。

13.4 記錄拒絕不應製造新的權限

為了審計,被拒絕指令可以寫入 trace。但 trace sink 的生命週期、隱私與資源成本受獨立政策約束。絕對不能因 TraceAudit 能儲存某個 event,便把它當成 WriteOwnedState 或 CommitArbitrate。


14. 可執行小步規則:從型別合法到實際允許

14.1 靜態規則與動態規則的不同

靜態 verifier 可拒絕未定義型別、重複消耗 SSA 線性 token、資料依賴缺失或非法效果轉換;但 epoch 是否真正尚在接受發送、lease 是否已被別的 worker fence、buffer 是否還有效,可能只能在實際執行時檢查。因此本篇要求:

Admissible⁡(i)=StaticWellTyped⁡(i)∧RuntimeGuard⁡(i,M).\operatorname{Admissible}(i) = \operatorname{StaticWellTyped}(i) \land \operatorname{RuntimeGuard}(i,\mathbb M).

此處 Admissible 不保證會完成或取得性能優勢,只說明符合目前安全進入條件。

14.2 PHASE_SIGNAL 的語義草案

step_phase_signal(machine, flow, epoch, kind, payload, capability):
    if not authorized(capability, PhasePropose, flow.scope):
        return Rejected(UnauthorizedPhaseProposal)
    if not epoch.accepts_phase_events:
        return Rejected(EpochSealed)
    if not validate_phase_schema(kind, payload):
        return Rejected(BadSchema)
    if not validate_current_fence(flow, machine):
        return Rejected(StaleLease)
    evidence = append_typed_phase_event(flow, epoch, kind, payload)
    return Applied(evidence, audit_event_ref)

此處的 append_typed_phase_event 只寫入相位事件或相位登錄的合法域,沒有隱含的共享結果提交副作用。接收端仍必須檢查自己任務的 phase-relevance predicate。

14.3 DIFFUSE_SEND 的語義草案

step_diffuse_send(machine, permit, message):
    assert_static_type(permit, DeliveryPermit)
    if not current_epoch_and_edge(permit):
        return Rejected(StaleEpochOrEdge)
    if not source_lease_valid(permit.source_flow):
        return Rejected(StaleLease)
    if not matches_reserved_identity(permit, message):
        return Rejected(EnvelopeMismatch)
    if message.hop_count >= message.max_hops:
        return Rejected(HopBudgetExceeded)
    result = durable_consume_once_and_register_dispatch(permit, message)
    if result == ALREADY_CONSUMED:
        return Rejected(CreditAlreadySpent)
    if result == INDETERMINATE:
        return Unknown(query_handle_for_dispatch(message))
    enqueue_transport_with_bounded_attempts(message)
    return Applied(DispatchRegistered(message.message_id), trace_ref)

durable_consume_once_and_register_dispatch 指參考語義要求的原子化/可恢復抽象;它並非代表單一 CPU 指令可對網路通道做到 exactly-once。具體實作應將「許可已耗」「發送記錄已落地」「外部傳輸可能發生」的 crash window 明確拆出。

14.4 RECONCILE_SEAL 的語義草案

step_reconcile_seal(machine, result_id, round_id, capability):
    if not authorized(capability, ReconcileLocal, result_id.scope):
        return Rejected(UnauthorizedLocalReconciliation)
    if unresolved_required_evidence(result_id, round_id):
        return Pending(RequiredEvidenceOutstanding)
    outcome = freeze_local_round(result_id, round_id)
    return Applied(SealedLocalOutcome(outcome), trace_ref)

該函式不觸碰 CommitLedger。若候選必須等待 R2 異源證據或 R3 shard 才能滿足契約,不能因某副本早到便強行封存為 LocalVerified。

14.5 COMMIT_DECIDE 的語義草案

step_commit_decide(authority, proposal):
    require authorized_commit_scope(authority, proposal.domain)
    require validated_and_fresh(proposal)
    existing = authority.atomic_lookup_or_decide(
        commit_key=proposal.commit_key,
        digest=proposal.proposal_digest,
        generation=proposal.authority_generation,
        decision_record=proposal.decision_intent,
    )
    if existing.digest != proposal.proposal_digest:
        return Rejected(ConflictingProposal)
    if existing.state == INDETERMINATE:
        return Unknown(query_handle_for_commit(proposal.commit_key))
    return Applied(existing.authoritative_decision, trace_ref)

validated_and_fresh 在取得驗證結果與正式決策之間必須避免 TOCTOU:可以透過同一交易、鎖、版本化 compare-and-swap、或另一種可證明的並行控制協議,使被驗證的前提在仲裁線性化點仍有效。若是「先讀完 validation,十分鐘後不再重檢就 commit」,則不是合規實作。

14.6 處理 Pending/Unknown 的正確模式

對任何跨 fault domain 的操作:

match invoke(op):
    Applied(value, event) -> continue_with(value)
    Pending(wait, handle) -> wait_or_cancel_with_deadline(handle)
    Rejected(error, evidence) -> branch_on_defined_policy(error)
    Failed(error, recovery) -> enter_recovery(recovery)
    Unknown(query, scope) -> query_same_stable_identity(query, scope)

不應把 Unknown 寫成 continue_with(default_success) 或 retry_with_new_key()。這是本篇最重要的可操作錯誤語義之一。


15. PDAIS-IR:使協議不變量可以被編譯器看見

15.1 為何需要新的 IR 層而不是再造一個 VM 語法糖

如果源碼把 DIFFUSE_SEND 寫成普通 call @send,而呼叫只接受一段無型別 byte buffer,編譯器看不到發送 credit、epoch、權威與資料血緣;任意 pass 便可能把它提前、複製或消除。由此,本篇建議一個具體可實作的 smpdc IR dialect/自有 typed intermediate representation(簡稱 PDAIS-IR),目的在保留效果與權限資訊,並使後端的合法轉換可以被驗證。

MLIR 是優先研究的工程載體之一,因其原生提供 dialect、operation、type、attribute、trait、interface 與 verifier 機制 [E1]。但本文以下表示採MLIR 風格概念語法,不是已由真實 MLIR parser 驗證可解析的程式;正式 implementation 必須由實際 TableGen/C++ verifier 定義每一種 op。

15.2 最小 PDAIS-IR 操作描述

PDAISOperationV0_1 {
    op_name: NamespacedOperationId
    signature: InputOutputTypeSignature
    effect_set: EffectSet
    authority_requirements: CapabilityRequirements
    consumes: List[AffineOrLinearTokenType]
    produces: List[TypedResult]
    phase_guard: OptionalTypedPredicate
    event_epoch_binding: OptionalEventEpoch
    resource_estimate: ResourceUpperBound
    failure_variants: ClosedTaggedUnion
    replay_class: Pure | Idempotent | QueryFirst | NonReplayable
    trace_contract: RequiredTraceFields
    lowering_contract: TargetSpecificProofObligation
}

任何 op_name 自行宣告 NoMemoryEffect,卻實際會修改在途義務、權威登錄或 outbox,均屬 IR 規格違反。若編譯器因為該錯誤聲明重排指令,責任不能推給 CPU 記憶體模型。

15.3 建議的基本型別

!smpdc.flow<f>
!smpdc.epoch<e, open|sealing|closed>
!smpdc.phase<kind, scope>
!smpdc.edge<source,target,topology_generation>
!smpdc.credit<epoch,credit_id>
!smpdc.permit<epoch,message_id>
!smpdc.message<logical_message_id,payload_type>
!smpdc.candidate<result_id,origin>
!smpdc.evidence<source_lineage,policy>
!smpdc.local_outcome<result_id>
!smpdc.snapshot<type,version>
!smpdc.tentative<type,branch_id>
!smpdc.commit_proposal<domain,key>
!smpdc.commit_decision<domain,key>
!smpdc.committed<type,key>
!smpdc.gpu_event<device>
!smpdc.host_visible<type,buffer_id>
!smpdc.authority_cap<scope,generation,effect>

尖括號內的欄位不要求全部能在編譯期固定;編譯期未知的 epoch、version 或 binding lease,應保留成運行時必檢的動態型別攜帶資訊,不可把未知一律視為合法。

15.4 一個具體的 SSA 概念例子

// Illustrative PDAIS-IR; NOT executable MLIR.
%flow = smpdc.flow.open %spec, %flow_cap
    : (!smpdc.flow_spec, !smpdc.cap<flow_create>) -> !smpdc.flow<f0>

%phase = smpdc.phase.signal %flow, %epoch, %ready_payload, %phase_cap
    {kind = "readiness"} : (...) -> !smpdc.phase<readiness,scope0>

%proposal = smpdc.couple.propose %flow, %peer, %phase
    : (...) -> !smpdc.edge_proposal

%edge = smpdc.couple.admit %proposal, %edge_cap
    : (...) -> !smpdc.edge<f0,f1,topgen3>

%permit = smpdc.diffuse.reserve %edge, %credit, %message_desc
    : (...) -> !smpdc.permit<epoch7,msg9>

%receipt = smpdc.diffuse.send %permit, %message
    : (...) -> !smpdc.dispatch_receipt

%sealed = smpdc.reconcile.seal %candidate_group, %round
    : (...) -> !smpdc.local_outcome<res12>

%proposal2 = smpdc.commit.propose %sealed, %branch, %proposal_cap
    : (...) -> !smpdc.commit_proposal<domain2,k31>

%decision = smpdc.commit.decide %proposal2, %authority_cap
    : (...) -> !smpdc.commit_decision<domain2,k31>

上例最後一個 commit.decide 只是概念性短寫;實際 PDAIS-IR 需要顯示 commit.validate 的證書/版本、原子檢查及 Unknown 錯誤處理分支。若將例子逐字當作可執行版本,verifier 應拒絕缺少完整驗證及結果分支的版本。這種故意可被拒絕的示例,是本篇測試編譯器守衛的材料。

15.5 更完整的合法路徑

flow.open
  -> phase.signal / phase.validate
  -> couple.propose / couple.admit
  -> diffuse.reserve / diffuse.send / diffuse.ack
  -> message.register / reconcile.compare / reconcile.select
  -> reconcile.seal / reconcile.export
  -> spec.begin / spec.read / spec.derive
  -> commit.propose / commit.validate
  -> commit.decide / commit.query-if-unknown
  -> commit.publish
  -> effect.enqueue / effect.deliver / effect.query-if-unknown

這不是所有工作流都必須走過的固定線性控制流。有些工作已在允許的非推測路徑上產生具版本候選;有些任務沒有外部效果;有些不需要 R2、R3 或 GPU。必要的是型別與前提,而不是強迫所有案例都啟動全部階段。

15.6 具型別 dependency edge 而非單靠文字順序

若效果 e2e_2 依賴 e1e_1 所承諾的可見結果,IR 應明確保留依賴:

e1≺e2.e_1\prec e_2.

這個偏序不要求所有無關事件全域同步。對獨立、可交換且無外部效果的純計算片段,可以平行或重排;對 credit 分配、authority generation、commit key 等狀態轉移,必須提供額外合法性證明。


16. 靜態驗證器、Runtime guard 與 lowering 的三層責任

16.1 三層防線

第一層:靜態檢查(Compile-time)。 檢查 op 名稱、型別、效果宣告、必需的依賴、權限參數、線性資源一次使用及不可兼容的轉換。

第二層:執行時守衛(Runtime)。 檢查實際 lease、fence、epoch、topology generation、信用餘額、版本、GPU event 完成、提交域合法性,以及可執行資源是否滿足預算。

第三層:外部權威(Authority / Receiver)。 對不可由本地可信度完整代表的權限、提交原子性和外部效果施行自身授權與冪等檢查。即使 Compiler 與 Runtime 都回報成功,外部 authority 仍可能拒絕請求。

16.2 最低 verifier 規則集

規則 ID 必須拒絕的 IR 情況 可觀察拒絕碼
V05-01 使用未宣告 required op 或未知型別 UnsupportedRequiredOperation
V05-02 同一 SendCredit 在兩路 reserve 重複消耗 LinearCreditReuse
V05-03 同一 DeliveryPermit 供兩個獨立 message send PermitAliasing
V05-04 DeliveryAttempt 被 cast 為 IndependentWitness EvidenceKindMismatch
V05-05 EncodedShard 直接當作完整 payload UnprovenRecovery
V05-06 Tentative<T> 隱式轉 Committed<T> IllegalAuthorityPromotion
V05-07 由 GPUEvent 直接創造 HostVisible MissingDeviceVisibilityProof
V05-08 COMMIT_DECIDE 不帶權威 capability MissingCommitAuthority
V05-09 EFFECT_DELIVER 在未合法提交情況下直接執行 EffectBeforeCommit
V05-10 對不可撤銷效果進行推測性重排 UnsafeSpeculativeEffect
V05-11 op effect declaration 與實作規格不符 EffectDeclarationMismatch
V05-12 未處理 UnknownCommit 卻建立新 stable commit key 重送 UnsafeUnknownCommitRetry
V05-13 沒有 epoch admission,卻藉迴圈產生無界 event epoch UnboundedEpochAdmission
V05-14 編譯器移除必要背壓而沒有等價證明 InvalidBackpressureElision
V05-15 兩個互斥的權威 generation 同時寫入同一域 ConflictingAuthorityGeneration
V05-16 缺失 trace 需求而仍標記為 auditable MissingTraceObligation
V05-17 宣告 Pure 卻有可觀察狀態副作用 InvalidPurityClaim
V05-18 將錯誤代數簡化成 success boolean LossyErrorLowering
V05-19 將未驗證候選標記成 SealedLocalOutcome MissingLocalVerification
V05-20 承載變更後仍使用失效 lease 發送具權威效果 StaleLeaseEffect

上述規則中有些只能部分靜態判定。對編譯期未知但有合法 Runtime guard 的欄位,可以產生 guard_required 標記;但不能把無法證明的權威提升當作「動態行為無法理解」而放行。

16.3 Lowering pipeline 候選

Source Language (Paper 06)
  -> Lexer / Parser / Typed AST
  -> PDAIS-IR construction
  -> Type & Effect Verification
  -> Dependency / Phase / Credit Analysis
  -> Static Budget and Alias Analysis
  -> Protocol Refinement Passes
  -> HostCPU/GPU Partitioning
  -> ABI & Runtime Lowering
  -> LLVM IR / Native Object + Runtime Library
  -> OS & Device Execution
  -> Event Trace / Validation / Commit Layer

若第一階段採用純 VM 解釋器,可在 PDAIS-IR construction 後直接交由參考執行器,不必完成 LLVM 後端。這使 V0 的形式語義能與 V1 的硬體效能工程分離。

16.4 何時可以把多個操作合併

例如同一 flow 針對同一相位 schema 的兩次 PHASE_READ,若中間沒有可能改變相位的事件,且兩次讀取沒有不可消除的審計效果,可以重用結果。若中間存在 PHASE_SIGNAL、topology rebinding、版本更新或接收對端訊息,兩次觀察可能不同,不能無條件消去。

類似地,將兩次小型 GPU_BATCH 合成一個更大批次,有可能降低 launch overhead,但必須保留各自的依賴、buffer lease、精度、取消與 deadline,不能因 GPU throughput 更高就犧牲 p99 SLA 或改變 deterministic training contract。

16.5 CPU target:從虛擬操作到現有 hardware

第一版最務實的 lowering 是:

  • FLOW_OPEN / FLOW_WAKE:OS 執行緒/協程、work queue、PWN registry、wakeups;
  • COUPLE_*:共享內存狀態、受控 registry 和 epoch 世代更新;
  • DIFFUSE_*:SPSC/MPSC 或其他正確的佇列、原子 token 帳本、release-acquire;
  • RECONCILE_*:CPU scalar/SIMD 或批次比較、checksum、必要時 GPU kernel;
  • SPEC_*:versioned snapshots、branch DAG、sandboxed work units;
  • COMMIT_*:CAS/鎖/交易/持久登錄及明確 authority;
  • EFFECT_*:outbox、receiver-specific retries 與可審計效果紀錄;
  • GPU_*:設備 command queue、CUDA stream/graph、事件與資料可見性檢查。

此映射保留既有硬體資源限制。若某 PDAIS 操作在 x86/ARM 上沒有單一對應 opcode,它依然可以透過正確的 Runtime protocol 完成,而不是標示成 CPU 不支援多主計算。


17. 六項條件性安全命題與證明責任

本節不是宣稱已在 Lean、Coq、TLA+ 或硬體模型上完成形式證明。以下是具明確前提的可檢查命題、證明概要及反例條件,供 V0 實作和之後正式驗證。

17.1 命題 A:有限 data credit 下,已封閉 epoch 的准許擴散次數有上界

前提: (A1) 每個 epoch 的初始 credit 數為有限 B0B_0 ;(A2) 每一次新增受控 data emission 均消耗唯一許可;(A3) token 不可複製、退款或超額發放;(A4) 轉移與消耗由共同遵守的原子仲裁實作;(A5) 論證不包括未計費的控制封包或新開 epoch;(A6) 重試不在此模型之外偷偷重創許可。

結論: 對該 epoch,已受准許的新增資料擴散量 Se(t)S_e(t) 滿足:

0≤Se(t)≤B0(e).0\le S_e(t)\le B_0(e).

證明概要: 由不變量 U+Q+S+D=B0U+Q+S+D=B_0,且四項非負,得 S≤B0S\le B_0。若允許 credit refund 以重用同一 ID、或不計成本無限開新 epoch,本結論不能直接延伸到累積 physical bytes。此命題僅對已聲明的 credit 制度成立。

17.2 命題 B:在有權限檢查的路徑中,低權限型別不能單步升格為權威決策

前提: (B1) 可產生 CommitDecision 的受控路徑都經過 COMMIT_DECIDE;(B2) 該操作必須持有有效權威 capability;(B3) Runtime 對 capability 進行 scope 與 generation 檢查;(B4) 不存在未管制 FFI 或繞過仲裁的寫入通道。

結論: 僅持有 LocalOutcome、GPUEvent、MessageAck 或 Tentative 的執行者,不能在受控機器中直接製造合法 CommitDecision。

證明概要: 對轉移關係作歸納:只有規範的權威操作能引入該型別,所有其他操作對 CommitLedger 的效果集合為空或無權寫入。若存在 bypass 通道,假設 B4 不成立,命題不能外推。

17.3 命題 C:R1 精確副本不會自動增生獨立來源證據

前提: (C1) CandidateId 與 OriginId 是按血緣解析的穩定識別;(C2) DeliveryAttempt 不能 cast 為 IndependentWitness;(C3) RECONCILE_COMPARE 依正式獨立性 policy 計數來源。

結論: 複製或重送一個候選的傳輸份數,不能單靠份數提高 IndependentWitness 的有效基數。

證明概要: 所有衍生傳輸都引用同一來源血緣,且型別驗證禁止以 delivery ID 改寫 source ID,因此對獨立來源集合的投影不變。若來源被惡意偽造,必須靠 provenance authentication 和信任模型補足。

17.4 命題 D:尚未獲權威批准的推測分支不能合法發布受控正式結果

前提: (D1) 所有正式發布須透過 COMMIT_PUBLISH;(D2) 其輸入須是有效 CommitDecision;(D3) commit authority 的唯一性與隔離檢查成立;(D4) 推測性外部效果完全被隔離。

結論: 單靠 SPEC_DERIVE、RECONCILE_SEAL 或 GPU_WAIT,不能達成受控的正式可見發布。

證明概要: 各操作的可觀察效果不含 PublishCommitted;若沒有 CommitDecision,COMMIT_PUBLISH 的 guard 必須失敗。命題不涵蓋未受控第三方系統已經偷跑的 I/O。

17.5 命題 E:舊世代無法在受保護的仲裁點重獲有效寫入權

前提: (E1) 對受控 state domain 存在可比較、單調有效的 authority generation;(E2) 每項受控寫入必須在仲裁點驗證最新 generation;(E3) 轉移期間禁止雙重有效 owner;(E4) 世代記錄不會因 crash 丟失或回退。

結論: 持有過期 fencing_token 的 worker 無法完成該 domain 的合法受控寫入,即使舊 worker 後來醒來並重新送出先前計算。

證明概要: 仲裁點只接受目前 generation 的令牌;舊令牌在時間上晚抵達並不使它重新有效。若使用只靠本地 wall clock 的 lease 而沒有共同可比較 fencing,E1–E3 不能保證。

17.6 命題 F:在合法 lowering 下,可觀察安全事件必須受參考語義約束

前提: (F1) 有一個已驗證的 PDAIS 參考解釋器;(F2) 所有會產生受控可觀察效果的原語在 lowering 中具備相同或更嚴格的 guard;(F3) target memory/device model 得到正確處理;(F4) 不新增未受保護的外部通路;(F5) 可觀察投影和失敗模型已固定。

預期結論(需正式證明): Lowered implementation 的受控 trace 應是參考規格所允許的 trace 或其合法精煉:

Traces⁡O(Lowered)⊆Traces⁡O(Reference).\operatorname{Traces}_{\mathcal O}(\mathrm{Lowered}) \subseteq \operatorname{Traces}_{\mathcal O}(\mathrm{Reference}).

證明義務: 需要逐 op 建立模擬關係,證明每個下層動作在上層可視為合法步或不改變觀測結果的內部步,並核對 fault、atomicity、ordering 與 liveness 例外。這是一項候選 refinement theorem,不是本文已取得的完整形式證明。

17.7 活性與速度不能從上述命題自動推出

A–F 主要處理 safety。若排程器永遠不執行某個 eligible flow、control queue 塞住、authority 永遠無法回應、GPU kernel 無法結束,則仍可能合法地停止進展。即使所有 guard 皆正確,多階段版本查核與耐久日誌也可能使整體系統明顯慢於傳統實作。因此本系列不能以命題 A–F 宣稱已證明加速或必然終止。


18. 編譯最佳化的合法性:快,不可以靠偷偷刪除安全契約

18.1 一個 pass 必須交付的證明材料

編譯器最佳化 PP 作用於模組 mm,若宣稱語義保留,至少需宣告:所保留的觀測集合、效果分類、記憶體模型、錯誤語義、版本讀取、權威域及 resource budget。候選合法性要求為:

Obs⁡(P(m))⊆AllowedObs⁡(m),\operatorname{Obs}(P(m))\subseteq\operatorname{AllowedObs}(m),

且其成本報告須獨立測量。只有完全限定的純計算片段才能依一般語言常見的代數法則自由重排;帶有外部效果或安全 token 的指令通常不能進行任意 common subexpression elimination、dead code elimination、loop fusion 或 speculation。

18.2 典型最佳化表

Pass 候選 何時可能合法 何時必須拒絕
FusePhaseReads 中間無相位變更或不可消除審計事件 版本或因果世代不同
CoalesceMessages 同樣 source、same epoch,且 aggregation 已證可交換 非交換消息,來源不同或證據被折疊
MovePhaseGuardEarlier Guard 對資料與授權在移動區間保持有效 時序更新可撤銷 guard
CreditSplit 唯一原 token 被消耗,新 token 總權利有界 複製 credit、提高總入場
CreditBatchReserve 原子性、所有權及對外可觀察結果得到保留 原因不同的失敗被合成成功
LocalQueueFusion 受影響訊息具有等價順序與 backpressure 更動因果序或刪掉必要 ACK
GPUOffload 精度、資料有效期、依賴與完成事件有保證 不可觀察的 host-device 差異
GPUFusion Kernel 依賴與 buffer lifetime 保留 非法跨 stream 重排/buffer 提早釋放
SpecHoist 純、可撤銷、前提恆成立 不可逆外部效果或版本需重驗
DedupKnownMessages 相同 message identity + replay contract 不同 candidate/來源被混為一談
PreCommitReorder 無衝突且 isolation policy 允許 serializability/predicate 依賴被破壞
HoistCommitQuery 未越過任何可能使查詢結果改變的仲裁 UnknownCommit 被誤判成未決定
OutboxBatch 可重試政策與 effect key 全保留 多個外部副作用被誤合為單次

18.3 不允許的「假提升」

案例 1: 編譯器把兩次不同 ResultId 的 DIFFUSE_SEND 合併,只因 payload hash 相同。結果可能讓其中一個結果再也無法完成其因果或提交責任,非法。

案例 2: 以「局部 RECONCILE_SELECT 已驗證」為由,提前執行 EFFECT_DELIVER。這是跳過正式權威提交,而不是執行最佳化。

案例 3: 把每個主要工作流常駐 busy-spin,導致 CPU 使用率上升卻吞吐下降。忙碌率不是有效工作量。

案例 4: 在 R1 負載下,複製更多傳輸得到較短單筆平均延遲,卻造成 p99 惡化、佇列飽和與整體吞吐下降。不能只展示較好看的 median。

案例 5: 以更低精度 GPU reduction 比較同精度 CPU 結果,然後把數值差異稱為「硬體加速但結果相同」。沒有合法的品質契約便不可比較。

18.4 降階合法性必須能 fail closed

當 IR dialect conversion 不能合法化所有必要操作時,編譯器應明確失敗,而不是產出「大致能執行」的可執行檔。MLIR 的 dialect conversion 已提供 full、partial 等不同模式與 legality model [E9]。SMPDC 預設對安全關鍵模組使用全部 required operations 必須可合法化的原則,除非有顯式且經過審核的 fallback;這是對已有 compiler 技術的特定治理要求,而非發明 dialect conversion。


19. 最小虛擬機器、Runtime ABI 與序列化協議

19.1 Reference VM 的可執行責任

PDAIS Reference Virtual Machine(PDAIS-VM) 建議包含:

  1. ModuleLoader:檢查版本、required features、schema digest 與效果政策;
  2. PWNRegistry:管理穩定 flow_id、局部狀態與權威租約;
  3. PhaseRegistry:維持具型別 phase evidence;
  4. CouplingRegistry:管理 admitted edges 和 topology generation;
  5. CreditLedger:管理唯一 token、耗用/作廢與限額;
  6. MessageTransport:區分邏輯訊息和 physical delivery attempt;
  7. ReconciliationEngine:處理 R0–R3 與證據來源;
  8. SpecBranchStore:保存推測依賴及撤銷閉包;
  9. CommitAuthorityAdapter:權威仲裁與可恢復決策;
  10. EffectOutbox:正式效果、接收策略與未知結果查詢;
  11. DeviceAdapter:GPU 批次、event 及 buffer lease;
  12. TraceRecorder:審計/效能/模型回放事件。

可依效能需求合併實作模組,但不可因此省去上述可觀察責任。當某組件被完全移除,IR 必須能辨識相應指令不可使用。

19.2 最小訊息 envelope

下面的 schema 將 Paper 02–04 關鍵欄位分成 required 與按特性存在的 extension,保證同一資訊流的多路傳送不會遺失版本及來源語義。

PDAISMessageEnvelopeV0_1 {
  protocol_version: Version
  message_id: StableMessageId
  result_id: StableResultId
  candidate_id: StableCandidateId
  root_event_id: StableEventId
  lineage_id: LineageId
  event_epoch: EventEpochId
  source_flow_id: StableFlowId
  source_generation: FlowGeneration
  target_flow_id: StableFlowId
  topology_generation: TopologyGeneration
  source_state_version: StateVersion
  source_fencing_token: FencingToken
  authority_scope: AuthorityScope
  phase_evidence_ref: PhaseEvidenceRef
  causal_parents: BoundedCausalParentSet
  payload_schema_id: SchemaId
  payload_digest: Digest
  payload_ref: PayloadReference
  redundancy_mode: R0 | R1 | R2 | R3
  send_credit_id: UniqueCreditId
  delivery_attempt_id: DeliveryAttemptId
  hop_count: NonNegativeInt
  max_hops: NonNegativeInt
  expiry_policy: ExpiryPolicy
  trace_id: TraceId
  extension_fields: VersionedTypedMap
}

為了降低封包大小,可以將固定欄位以 session registry 或本地引用方式編碼;但 receiver 必須在其授權可見域內恢復相同的語義資訊。將 source_fencing_token 從封包移除而沒有可信的 session binding,不能叫做壓縮最佳化。

19.3 序列化、記憶體壓力與零複製的代價

使用 payload_ref 不代表真正沒有資料複製。若指向共享 buffer,必須解決生命週期、寫入時機、cache coherence、版本和接收者授權;若使用 reference-counted buffer,計數器及 cache-line contention 會成為開銷。Zero-copy 的實效取決於平台和 workload,不可由 API 名稱推論。對大 payload 可使用 scatter-gather、batch、shard 或經驗證的 shared memory,但應把額外 pinning、映射與 GC 成本計入。

19.4 外部權限和 ABI 安全

CommitCapability、SendCredit、AdmittedEdge 都不能只靠容易偽造的 user-supplied 字串獲得合法性。進程內的可信 Runtime 可使用不可偽造 handle、代數 token 或受保護的 capability table;跨進程、跨機器則可能需要 OS handle、MAC/簽章、隔離 sandbox 或外部 authority。具體方式由信任模型與威脅模型決定。

19.5 V0 排程器的最小公平性策略

初步 Reference VM 可以採用確定性 round-robin、有限工作配額及可注入的虛擬時間,便於重播。對 live V1 Runtime,則可研究局部隊列、work stealing 與 core affinity。是否需要 AI 幫忙排程,是 Paper 07 的可選優化,不能變成協議正確性的必要條件。

19.6 Trace schema

PDAISTraceEventV0_1 {
    trace_id: TraceId
    event_id: EventId
    op_name: InstructionName
    op_version: Version
    result_variant: Applied | Pending | Rejected | Failed | Unknown
    flow_id: FlowId
    flow_generation: FlowGeneration
    worker_id: OptionalWorkerId
    observed_logical_cpu: OptionalOSCPUId
    event_epoch: OptionalEventEpoch
    topology_generation: OptionalTopologyGeneration
    authority_generation: OptionalAuthorityGeneration
    message_id: OptionalMessageId
    credit_id: OptionalCreditId
    branch_id: OptionalBranchId
    candidate_id: OptionalCandidateId
    commit_key: OptionalCommitKey
    effect_key: OptionalEffectKey
    causal_parents: List[EventId]
    timestamp_monotonic: LocalMonotonicTime
    cost_cpu_ns: OptionalDuration
    cost_gpu_ns: OptionalDuration
    cost_bytes: OptionalByteCount
    state_digest: OptionalDigest
    evidence_ref: OptionalEvidenceRef
}

跨執行緒或 CPU/GPU 的事件不能只依 wall-clock timestamp 形成全域總序;因果邊和各層自己的可用序列號才是能重建合法偏序的核心證據。對高頻路徑可壓縮 trace,但抽樣不能成為驗證安全不變量的唯一資料來源。


20. 成本與效能:指令少,不代表整個 AI 任務更快

20.1 終端到終端延遲

對工作流 ww,真實完成時間應從外部輸入可處理時刻 tint_{in} 到契約指定的有效結果可見時刻 toutt_{out} 計量:

L(w)=tout(w)−tin(w).L(w)=t_{out}(w)-t_{in}(w).

並行工作階段的時間不能簡單把每一段 CPU、GPU 時間相加當作 wall-clock latency,但每一段消耗的資源、能源與資料搬運仍然必須計入。

20.2 一個結構性的成本拆分

令 WW 為有效完成的受認可工作量,對某組工作負載與等價品質標準:

Ctotal=Ccompute+Cschedule+Cqueue+Cmemory+Ctransport+Cverify+Ccommit+Crecovery.C_{total}=C_{compute}+C_{schedule}+C_{queue}+C_{memory} +C_{transport}+C_{verify}+C_{commit}+C_{recovery}.

上述項目可以在時間上重疊,所以不能把此式當成無條件延遲相加方程。它是資源成本帳目,用來避免把 CPU/GPU kernel 本身的加速錯認為系統整體加速。

20.3 有效吞吐而非忙碌率

定義:

Θvalid=Nvalid_commitsΔt,Eunit=EconsumedNvalid_commits.\Theta_{valid}=\frac{N_{valid\_commits}}{\Delta t}, \qquad E_{unit}=\frac{E_{consumed}}{N_{valid\_commits}}.

其中 valid_commit 只能按預先宣告的 correctness/quality/durability 等級計數。對 AI 訓練,若比較的是訓練吞吐,則必須另定義等價品質或等價收斂目標;不能讓模型品質下降的一方僅因每秒更新步數高就被認作勝出。

20.4 相位與擴散的開銷組成

最需單獨量測的是:phase_guard_ns、edge_admission_ns、credit_reservation_ns、data_send_attempts、dedup_lookup_ns、lineage_verify_ns、reconcile_ns、branch_checkpoint_bytes、commit_fence_ns、gpu_queue_wait_ns、gpu_launch_ns、host_device_transfer_ns、replay_overhead_ns、trace_write_bytes。

如果觀察到 SMPDC 對某任務優於 baseline,應透過消融展示增益來自哪些部件;若增益只來自將 queue 換成更好的資料結構,則應承認那是 queue 的工程改善,而不自動當成擴散新範式的證據。

20.5 候選 GPU offload 收益條件

令純 CPU 執行同一 operator 的有效時間為 TcpuT_{cpu},GPU 路徑的資源成本包含準備 TpT_p 、搬移 TmT_m 、排隊 TqT_q 、計算 TgT_g 、同步 TsT_s 、回收驗證 TvT_v。只對沒有可利用重疊的簡化串行路徑而言,GPU 具有加速機會的必要比較是:

Tg+Tp+Tm+Tq+Ts+Tv<Tcpu.T_g+T_p+T_m+T_q+T_s+T_v<T_{cpu}.

當 pipeline 可重疊時,必須改以完整 schedule critical path 和 throughput 量測,不能直接用上式決定勝負。對小而頻繁的 PHASE_SIGNAL/DIFFUSE_ACK,GPU 往往不是自然的優先實作;對批次圖更新、編碼修復、稀疏運算或 AI 張量操作才可能值得研究。

20.6 主工作流常駐的適用條件

若以 FLOW_PERSIST 減少反覆建立 executor/重載上下文成本,可能改善中高頻、具局部狀態重用的 workload。但工作流長期佔有資源亦可能導致 cache pollution、SMT sibling contention、熱節流、頻繁跨 CCD 同步或電力上升。虛擬工作流持續存在,不代表每個物理核心永不休眠。


21. 三種實驗層級與成熟度分離

21.1 V0:參考語義驗證

V0 不追求性能,只檢驗:

  • 同一 SendCredit 是否可能被兩次合法消耗;
  • 被撤銷 edge 是否能在新拓撲世代再次合法發送;
  • R1 傳輸是否被錯當 R2 獨立證據;
  • 已失效分支的後代是否能偷渡正式提交;
  • UnknownCommit 是否被誤判成未提交;
  • GPU device event 是否能繞過 host-visible guard;
  • 未知 required op 是否被錯誤忽略;
  • EPOCH_QUIESCE 是否能在仍有在途責任時回報成功。

V0 的成果應是:可執行最小 interpreter、有限狀態模型、反例 trace、差異測試套件及失敗分類,不是宣稱「新 CPU 已發明」。

21.2 V1:既有 CPU 的第一輪測試

使用已有桌機 CPU 進行 V1,保留 OS affinity、實際 P/E 或 CCD 分組(只有硬體確實存在時才分類)、快取域、記憶體頻寬、佇列配置與功耗報告。若設備只有同類型核心,仍可測多主工作流、相位與擴散語義;不能因沒有異質 P/E 核就宣稱 V1 不可實作。

V1 建議不以幾十萬元 CPU 為先決條件。與一般 thread pool、actor-like Runtime、work stealing、共享隊列以及明確編碼的 state machine 進行公平對照,驗證 PDAIS 增量到底在安全性與效能上有多少實際價值。

21.3 V1-G:可選的 GPU 延伸

對現有 RTX 3070,可先測簡單的批次比較器、R3 編碼運算與有限圖更新的 CPU-only/GPU-offload A/B;固定相同結果品質、批次大小、暖機條件和資料位置。若 GPU 調用時間和拷貝成本壓倒收益,允許提出明確的不適用區間,不能為了報告好看而移除負例。

21.4 V2:真正硬體擴充之前的閘門

只有在 V0 的安全路徑基本通過、V1 重現某些受控收益,且 profiling 明確顯示 CPU 現有 ISA/cache-coherent queue 的缺口時,才考慮研究 FPGA、RISC-V 模擬器、專用 mailbox、credit allocator 或 NoC。Hardware V2 若改變了先前定義的可觀察語義,需明確分叉版本,而不能宣稱完全相容。


22. 可證偽實驗:比較的不只是新名詞和舊名詞

22.1 預註冊假說

H05-SAFETY: 在相同的受控故障模型下,帶 typed effects、credit 和權威守衛的 PDAIS VM 比刻意弱化守衛的實作更能阻止違法狀態轉移;觀測的是違例可重現、拒絕適當與 coverage,而不以「沒有撞到 bug」宣稱無錯。

H05-EXPRESSIVITY: 對指定 PWN workflow、R1/R2、推測分支與正式提交任務,PDAIS-IR 能在不逃逸至未受管制 FFI 的條件下完整表達合法執行,並使主要不變量可由 compiler/Runtime 明確定位。

H05-PERF: 至少存在可事先定義的 task family 與資源預算,使 PDAIS-IR lowering 的執行在同品質下,其延遲、有效吞吐或能源成本優於經公平調整的傳統實作,且增益可由消融結果解釋。

H05-NEGATIVE: 對低頻、小消息、高衝突或低並行度的負載,完整 PDAIS 有可能沒有收益甚至顯著劣於成熟 baseline;這種反例屬研究應有結論。

上述假說均無預設成功比例;在實驗前應鎖定 workload、主要指標、最小有意義差異及統計方法,避免研究完成後只選最好看的資料集。

22.2 B0–B8 比較組

組別 工作內容 研究用途
B0 單執行緒 direct implementation 檢查最小負載的協議開銷下限
B1 一般 thread pool/work stealing 對照成熟 CPU work scheduling
B2 常駐 per-core/sharded event loop 拆分持續工作流的效果
B3 一般消息隊列+有限背壓 對照資料擴散控制本身
B4 一般 actor-like/dataflow pipeline 對照節點自治與訊息語義
B5 B2 + typed phase guard、無多路冗餘 辨識相位門檻效用
B6 B5 + R1/R2/R3(無正式 speculation) 辨識資訊協議的附加成本
B7 B6 + speculation/commit(以一般 library 手寫) 區分「編譯器可理解」與「功能相同」
B8 完整 PDAIS-IR lowering+Runtime SMPDC Paper 05 候選實驗組

不能在 B8 使用 GPU、B1 只允許 CPU,然後把差異都歸功於 PDAIS。GPU 比較須另設 matching CPU/GPU baseline;若兩組 driver、精度、RAM、thread-count、batching 或 affinity 不同,需將差異固定或在報告中公開。

22.3 主要工作負載矩陣

類別 例子 最關鍵變數 必須保留的品質契約
W-A 連續工作流與低頻事件 idle time、wake latency 相同事件結果與順序約束
W-B 小消息密集圖 fanout、hop、credit 上限 不丟消息、不越權、已封閉 epoch 可驗證
W-C 高延遲尾端消息 延遲分布、R1 hedging rate 相同結果正確性與同一來源血緣
W-D 異源檢查 R2 witness independence 相同證據與衝突報告等級
W-E 資料擦除恢復 R3 (n,k)(n,k) 、erasure rate 完整 payload digest 校驗
W-F 高寫入衝突狀態 read/write sets、fence 變更 serializable 或預定 isolation 等級
W-G 推測型 pipeline branch depth、abort rate 無非法正式效果與相同輸出
W-H 批次稀疏圖更新 kernel size、GPU transfer 精度/順序與數值容差固定
W-I 模擬持續 AI 推論/Agent 模型固定、工具延遲 相同輸出品質與副作用權限
W-J AI 訓練局部 pipeline step、batch、梯度策略 等價訓練品質/收斂條件
W-K 故障與恢復 kill/restart、失聯、重送 不變量與未知狀態正確處理
W-L 小型單步 arithmetic 訊息成本遠高於算術成本 允許得到「傳統直接呼叫更好」

22.4 V0 的有限狀態空間

一個第一輪可模型檢查的縮小系統可以採:3 個 PWN、2 個 event epoch、3 條耦合邊、最多 4 個 credit、2 種冗餘模式、2 個 commit key、2 個 authority generations、最多 2 個推測分支、1 個可回覆/不可回覆的 GPU executor。這只是建議的狀態空間上界,非要求所有建模工具一次涵蓋完整機器。

至少需檢查:

NoCreditDuplication
NoAuthorityEscalation
NoStaleGenerationWrite
NoR1AsIndependentWitness
NoUnvalidatedPublish
NoExternalEffectBeforeCommit
NoFalseEpochQuiescence
QueryUnknownBeforeUnsafeRetry
PreservedDependencyAfterSpecInvalidation
NoUseAfterGPUBufferRelease

若模型在公平性假設下驗證活性,必須將 fairness 選項、故障模型和 timeouts 另外寫入模型,不得把 safety model check 的 PASS 當成全域活性已證明。

22.5 V1 可量測工作

第一輪即可實作:

  1. 載入固定輸入及 seed,使用同一資料集對所有方案測試;
  2. 收集核數/OS logical CPUs、實際 affinity、CPU 時脈、溫度、快取域與記憶體;
  3. 在 warmed-up 與 cold-start 兩種模式分開測試;
  4. 逐組執行多次,報告 median、p95、p99、throughput、錯誤率及能源(可得時);
  5. 對 R1 額外報告 backup traffic、取消成功率與 shared-failure correlation;
  6. 對 Commit 報告 unknown_decision_rate、durability failure、conflict abort;
  7. 對 GPU 額外報告 kernel launch、H2D/D2H、device wait 及 data-lifetime;
  8. 保留失敗 workload,不以更動品質契約補救跑分;
  9. 逐項關閉 phase、R1、R2、speculation、AI planner、GPU offload,建立消融矩陣;
  10. 以 trace 證明所有有效結果都符合先前契約,而非只比較輸出值表面相同。

22.6 顯式的研究否證門檻

若經充分匹配與調校,PDAIS 不能帶來比等價 library 更好的可維護性、規格可檢查性或可重現效能,那麼 Paper 05 應退化為一份嚴謹的高階協議語義規範,而非宣稱開啟不可替代的新硬體紀元。若指令的守衛成本在主要 AI workload 中超過改善收益,應記錄適用域縮小或提出更窄的必要指令子集,不得無限擴張定義來掩飾結果。


23. 三十項必須主動製造的失敗與反例

以下不是已經實測出現的缺陷;它們是 Reference VM 與 V1 Runtime 應刻意注入的反例候選。每一項必須對應可觀察拒絕、故障、告警或正確恢復,而非籠統的 PASS/FAIL。

ID 對抗情境 正確觀察或恢復要求
F05-01 同一 credit 被兩個 PWN 同時 reserve 最多一個合法成功;其餘拒絕
F05-02 crash 後 replay 舊 credit 不得重新增生可用許可
F05-03 cancel 之後把 token 無聲退款 不得突破預設的不退款契約
F05-04 新開無限 epoch 繞過 data credit admission budget 必須生效
F05-05 控制通道與 data credit 一起耗盡 必須留下可觀察的 blocked/failure,不得偽造 quiescent
F05-06 edge 已 revoke,舊送件遲到 依在途政策處理,不能獲得新權限
F05-07 topology version 改變,沿用舊 edge 拒絕或重新審查合法性
F05-08 source worker 已被新 owner fence 拒絕舊 generation 的受控效果
F05-09 將普通 timestamp 當因果充分證據 PHASE_VALIDATE 必須識別不足
F05-10 沒有相位相關性也強制 phase guard 消融可證明無效且增加成本
F05-11 不同 DeliveryAttempt 假裝 R2 兩來源 CorrelatedWitness 或型別拒絕
F05-12 同源兩份 payload 同錯 不得誤稱提高正確率
F05-13 R3 shard 索引重複 不可重建虛假的 payload
F05-14 shard 數低於解碼最低門檻 InsufficientShards
F05-15 R2 候選互相矛盾 必須保留 conflict/擴增驗證
F05-16 遺失 result/candidate 身分,錯誤去重 必須由 schema 或 runtime 守衛拒絕
F05-17 已封存局部證據仍被直接 cast 成 committed 靜態或 runtime 拒絕
F05-18 依賴上游失效,後代先行提交 血緣驗證拒絕;必要時回滾
F05-19 Snapshot isolation 發生 write skew 以所需 serializable 契約拒絕
F05-20 authority 決策完成但回應丟失 UnknownCommit 查詢同鍵,不能改鍵重送
F05-21 同 commit key 但 digest 不同 ConflictingProposal
F05-22 非法新 generation 重複寫入 由共同仲裁拒絕
F05-23 未提交卻先執行外部效果 EffectBeforeCommit
F05-24 outbox delivered 回覆遺失 查詢同 effect key;不偽稱 exactly-once
F05-25 GPU event 完成但 host buffer 尚不可見 GPU_MAKE_HOST_VISIBLE 不得成功
F05-26 GPU buffer lease 早於 kernel 結束被釋放 拒絕並捕捉 use-after-release
F05-27 IR optimizer 複製一次性令牌 verifier 拒絕
F05-28 IR optimizer 將 Unknown 轉為 Applied verifier/差異測試發現非法精煉
F05-29 Runtime 默默忽略新版本的 required op UnsupportedRequiredOperation
F05-30 高頻繁相位通知造成同步與快取風暴 記錄負面性能及適用域,而非捏造收益

23.1 故障注入的完成條件

每個 F05 case 至少應具有 (input, initial_state, event_schedule, fault_injection, expected_trace_constraint, observed_result, reproducibility_seed)。若某故障是由 OS、GPU driver 或外部 Receiver 決定,需另外標明假設與不可控制因素。不可用「整體程式沒有 crash」取代真正的正確性驗證。

23.2 必須留下的負面證據

對失敗或反例,保留失敗版本、配置、機器環境、原始 log、縮小後的 trace、被破壞的不變量和復現步驟。修補後應再次執行同一測例和完整回歸;不能把曾經能觸發的反例從公開基準中刪除。


24. 完整小型執行案例:五個 PWN 的多路擴散、推測與權威提交

24.1 假想設定

假設一個 AI 資料處理 pipeline 有五個邏輯 PWN:

  • F_A:輸入接收及事件階段判斷;
  • F_B:主候選計算;
  • F_C:同源 R1 的 backup transport executor;
  • F_D:異源驗證與局部聚合;
  • F_E:版本化狀態的主工作流與提交提案提出者。

另有獨立 CommitAuthority_D,不把其權力內建到某一顆 physical CPU 的名稱。可選的 GPU0 負責適合批次的 operator,但在此示例不假設其必定加速。初始 event_epoch = 17、topology_generation = 8、source_generation(F_B)=4、state_version=31、data_credit=5。每個新 R1 route transmission 均須按規格持有不同 credit;外部控制訊息具獨立預留通道。

24.2 事件追蹤

T00  Epoch admission opens e17, data credit {c1,c2,c3,c4,c5}
T01  F_A FLOW_WAKE / PHASE_SIGNAL(readiness, e17)
T02  F_A COUPLE_PROPOSE(B,C,D); authority COUPLE_ADMIT for edges
T03  F_A SPEC_BEGIN(snapshot v31, branch b17)
T04  F_B SPEC_DERIVE -> tentative candidate x; origin oB
T05  F_B REDUNDANCY_PLAN(R1, two approved routes)
T06  F_B DIFFUSE_RESERVE(edge B->D, c1, msg m17)
T07  F_B DIFFUSE_SEND(m17, attempt a1); credit c1 Spent
T08  F_C DIFFUSE_RESERVE(edge C->D, c2, msg m17)
T09  F_C DIFFUSE_SEND(m17, attempt a2); credit c2 Spent
T10  F_D MESSAGE_REGISTER(m17, candidate x, origin oB)
T11  F_D receives attempt a2 first; first valid R1 candidate accepted
T12  F_D receives attempt a1 later; dedup by logical identity
T13  F_D PHASE_SIGNAL(verification_ready, e17)
T14  F_D RECONCILE_COMPARE(x, policy v5): valid local candidate
T15  F_D RECONCILE_SEAL(res17, round1)
T16  F_E receives SealedLocalOutcome, proposes commit key k17
T17  COMMIT_VALIDATE checks snapshot v31, predicates, fence
T18  COMMIT_DECIDE(k17, digest17, authority D) -> authoritative decision
T19  COMMIT_PUBLISH(k17) -> committed visible result
T20  EFFECT_ENQUEUE(effect e17, linked to k17)
T21  EFFECT_DELIVER(e17, receiver idempotency policy)
T22  EPOCH_SEAL(e17)
T23  In-flight data/control obligations drain
T24  EPOCH_QUIESCE(e17) -> Quiescent

注意: m17 在兩條 R1 路上是否使用同一 logical message ID,以及物理 attempt ID 如何分配,均按 Paper 03 的 identity contract 處理;c1 和 c2 是兩個獨立 data transmission permits,不是同一 token 被複製。F_E 的本地主要工作流身份不表示它天然是 CommitAuthority_D。此 trace 只是可重演的示意,不構成實測性能資料或形式驗證證書。

24.3 替代 trace A:快照過期

若在 T17 之前,另一已合法提交的工作改變了 v31 所依賴的共享狀態:

T17' COMMIT_VALIDATE -> Rejected(StaleSnapshot)
T18' SPEC_INVALIDATE(b17, StaleSnapshot)
T19' descendants of b17 become Invalidated / NeedRecompute
T20' EFFECT_ENQUEUE forbidden; k17 has no committed decision
T21' Recompute on new lawful snapshot, if policy permits

此路徑仍可以稱局部 R1 競速成功,卻不能稱正式 AI 工作流完成;這正是 Paper 04 分離計算進度與提交進度的必要性。

24.4 替代 trace B:提交回應遺失

T18a COMMIT_DECIDE durable-authority result stored
T18b response to F_E is lost
T18c F_E observes UnknownCommit(k17)
T18d F_E COMMIT_QUERY(k17, same authority domain)
T18e authoritative record found -> resume COMMIT_PUBLISH

若 F_E 直接改用 k18 再提交,無法再主張同一操作在整體世界只生效一次。Unknown 的合法查詢與 stable key 使用是指令語義的必要部分,而非可由底層 OS 速度補救的小細節。

24.5 替代 trace C:GPU 尚未完成

假設 T04 的候選由 GPU0 執行,則:

G00 F_B GPU_BATCH -> event g17, buffer lease l17
G01 GPU_WAIT(g17) -> Pending
G02 No local candidate verification may use device buffer as HostVisible
G03 GPU_WAIT(g17) -> DeviceComplete
G04 GPU_MAKE_HOST_VISIBLE(g17,l17) -> HostVisible<T>
G05 SPEC_ATTACH_GPU(b17,g17,l17)
G06 RECONCILE_COMPARE may read valid host-visible result

G05/G04 的實際次序取決於依賴規格;可以先掛事件依賴,再等待完成。這裡以教學追蹤展示設備完成與 host-visible 的不同。只要 HostVisible<T> 未成立,使用者就不得假定 GPU 的數值輸出已安全進入 CPU 受控驗證域。


25. 與先前 EveMissLab 計算理論的精確繼承關係

25.1 群星模型及早期計算機構想

早期群星模型使用具有不同資源強度、功能與連結的「星點」描繪動態可協作系統,並曾把此概念投射到 CPU、記憶體、主機板和動態傳輸 [I5–I6]。PDAIS 把其中各主要工作流可自治、可耦合的思想進一步形式化,但拒絕把群星/環狀圖像直接當成晶片物理布線圖。新系列的候選貢獻不是「星點」類比本身,而是跨作用域的操作語義、限制與可檢查行為。

25.2 PCMT:相位不只是週期角

既有《相位計算機理論》把相位本體、表示、演化機制及計算承載架構分離 [I7]。PHASE_SIGNAL、PHASE_WAIT 和 PHASE_VALIDATE 沿用此分離,只處理與執行交互有關的相位,不要求物理振盪器、量子機理或特定語義流形成為所有 CPU 的底層實作。

25.3 GCCFT:計算場本體與執行規格不同

GCCFT Paper 06–08 已論及 Coupled Computation Planner、AI 計算場與可證偽 A/B 基線 [I8–I10]。PDAIS 接收其任務相對耦合和相位作用的思想,專注縮到單機或近硬體多主 Runtime 的合法操作。GCCFT 不因此被 PDAIS 取代,PDAIS 也不能宣稱重新建立一個全域計算本體。

25.4 GCCWT 與 GCM:世界級規劃和局部指令不得混成同一層

GCCWT 分離世界級資源身分、計算場、權威與全域規劃;GCM Phase C 計畫把 AI proposal 與真正 allocator execution authority 分開 [I11–I12]。PDAIS 的 CommitCapability 及 EFFECT_* 正好承接這種分離,但對外部世界調度的抽象權限不直接成為 CPU ISA 的特權位元。

25.5 ISQL/NICA/24/72 的可選介面

若未來要讓 ISQL 或其他語義表示、NICA、計算 24 範式與 72 格參與 SMPDC,可由 compiler front-end 的 task metadata、operator classification、representation policy、routing hint 或驗證證書輸入 PDAIS-IR。但PDAIS 安全性不必依賴這些更大理論先行成立。在需要公平 A/B 的基準中,應允許完全沒有這些擴充的純一般數學與一般 CPU workflow。

25.6 原創性與既有文獻的界線

本篇沒有證明一個硬體上全新的計算複雜度類,也沒有宣稱所有計算都能從序列處理轉為擴散計算。若一組 PDAIS 程序能被傳統 actor/dataflow/coroutine+transaction library 完整且不失真地模擬,那是合法且預期存在的情況。研究價值必須由更清晰的效果與資源契約、降低錯誤組合風險、可分析的新型 compiler optimization 以及待實測的適用域建立,而不能用「命名不同」代替學術差異。


26. 對 Paper 06–11 的嚴格交接

26.1 Paper 06|擴散程式語言與編譯器

Paper 06 至少必須完成:

  1. 正式或半正式 grammar:宣告 flow、持續性、相位、局部狀態、訊息及權限;
  2. 語言層 effect 與 capability 的型別檢查,不依賴原生語法的黑箱 cast;
  3. 對 R0/R1/R2/R3 的不同 typed constructors 和 evidence check;
  4. SendCredit 一次性與 DeliveryPermit ownership 的靜態/動態結合;
  5. Tentative<T,B>、LocalOutcome<K>、CommitProposal<K> 與 Committed<T,K> 的不可隱式轉型;
  6. Pending/Rejected/Failed/Unknown 的非丟失式模式比對;
  7. AST → PDAIS-IR 的 type-preserving translation;
  8. PDAIS-IR verifier、降低階段、合法性回報及 debug trace;
  9. 確定性最小 interpreter 和 executable examples;
  10. 原稿、測試、可重現建置及可接受的向後相容規則。

第一輪語言可以採嚴格 DSL、嵌入式語言或 Rust-like 前端,但不能因為討論「新程式語言」就預設必須先寫獨立完整 IDE、生態系或自己的 CPU assembly。語義正確比語法漂亮優先。

26.2 Paper 07|OS 與 AI 控制平面

必須讓不接 AI 的確定性排程器完整運作,定義:flow registration、wakeup、core placement、backpressure、policy admission、stale lease fencing、GPU adapter、承載遷移與回復。AI 只可提出受硬性政策檢查的建議,例如估計 fanout、batching、路由、放置與精度策略;不得直接創造 credit、提交能力或跳過本篇的 hard guards。

26.3 Paper 08|CPU–GPU 並行資訊處理

應用對應 IR 的 typed GPU event、buffer lease、合法資料視圖、batch、kernel/graph 重用及 host-visible guard,並建立端到端 p95/p99、資料搬移、GPU/CPU busy time 與能耗模型。若 GPU 支援不足,也要測 CPU-only 的結果和退化路徑。

26.4 Paper 09|記憶體與微觀硬體映射

可以探討共享記憶體、cache-line 佈局、NUMA/CCD、P/E core、NoC、FPGA 和未來 ISA 自訂指令,但必須將每個候選改進映射到已在 V1 找到的明確瓶頸,並測量安全成本、功耗、資源競爭與硬體驗證投入。

26.5 Paper 10|AI 訓練、推論與可重現比較

固定模型、資料、數值精度、輸入批量、設備資源與品質契約,研究 sparse/MoE、梯度 pipeline、長期 Agent 與混合符號計算的適用性。不要只展示 Token/s 或 step/s 而忽略模型精度、訓練收斂與最終可用結果。

26.6 Paper 11|總體可證偽結案

匯整多輪 V0–V2 證據,列出支持、否證、僅有局部優勢、成本過高及尚未覆蓋的故障模型。若 PDAIS 主要價值是可驗證協議語義,而不是硬體速度,也應正式如實報告。這樣的結論仍屬有用的研究成果。


27. 結論:讓擴散成為語義,而不是口號

SMPDC Paper 05 的核心並不是要求 CPU 一夜間長出神經網絡般的實體線路,也不是把 GPU 的大量並行運算等同於 CPU 核心之間的物理傳輸。它嘗試把「每個可參與核心皆能承載主要工作流」以及「工作流之間依相位發生有界資訊傳播」轉成可供新語言、Compiler、Runtime 與測試器共同理解的抽象機器。

本篇建立五項可交付的理論結果:

  1. 指令層級分離: 抽象 ISA、IR 與物理 opcode 不可混淆;現有硬體仍可承載全部參考語義。
  2. 型別與效果分離: flow、phase、credit、candidate、tentative value、commit decision、GPU event 及 effect record 各有不可越權的轉換。
  3. 有限擴散契約: data credit、外部 epoch admission 與控制通道獨立計量,避免把傳播當作免費無界廣播。
  4. 局部進度/正式提交的隔離: 可以讓計算、接收、合併與驗證先行,但正式狀態由授權的提交域決定。
  5. 可證偽與可降階的語義: 提供精確的失敗型別、trace、verifier、合法 lowering 和公平 baseline,使整體構想可以被真正否證。

後續 Paper 06 的關鍵問題因此不再是「應該為這套架構創造哪些漂亮關鍵字」,而是:何種程式語言與編譯器可以在仍允許局部自治和異質並行最佳化的情況下,完整保持 PDAIS 的可觀察執行、安全權限與資源契約?

本論文至此形成完整的候選抽象指令集研究稿。距離「硬體層級的效能提升已被證明」「物理 ISA 已存在」及「真實 AI 訓練已加速」仍有明確的實驗與工程距離;此區分是正式研究質量的一部分,而不是可省略的註腳。


附錄 A|PDAIS Abstract ISA Specification v0.1 最低規範檢查表

以下各項供 V0 參考解釋器、IR verifier 與協議測試程式使用;它們不是宣稱已通過測試的實驗結果。

Check ID 必須具備的條件 對應章節
PDAIS-C01 四個指令層級明確分離 §1
PDAIS-C02 模組載入檢查 required features §5
PDAIS-C03 所有 op 具 signature/guard/effect §5
PDAIS-C04 FlowId 與 worker/core 身分不同 §4、§6
PDAIS-C05 各 epoch、topology、authority generation 不混同 §4
PDAIS-C06 相位必須具任務相對的互動作用 §6
PDAIS-C07 Coupling proposal 不等於 admitted edge §6
PDAIS-C08 Credit 不能複製、透支或無聲退款 §7
PDAIS-C09 物理重送有自己的 attempt budget §7
PDAIS-C10 Data/control/epoch admission 預算分離 §7
PDAIS-C11 Epoch quiescent 需檢查全部相關義務 §7
PDAIS-C12 R1 重送不能變成 R2 獨立證據 §8
PDAIS-C13 R3 shard 必須通過 schema/碼參數 §8
PDAIS-C14 Conflict 不得默默化為 verified §8
PDAIS-C15 Tentative 不可隱式轉 Committed §9–10
PDAIS-C16 Invalidated branch 的後代安全處理 §9
PDAIS-C17 Snapshot/predicate guards 受權威域檢查 §10
PDAIS-C18 Commit decision 有原子唯一性契約 §10
PDAIS-C19 Unknown commit 必須先查詢同鍵 §10
PDAIS-C20 外部效果不先於合法提交 §11
PDAIS-C21 Outbox 不假冒接收者 exactly-once §11
PDAIS-C22 GPU event 不直接變 HostVisible §12
PDAIS-C23 Buffer lease 生命週期得到保護 §12
PDAIS-C24 Typed failure 不可折成無意義 bool §13–14
PDAIS-C25 PDAIS-IR effect declaration 正確 §15–16
PDAIS-C26 Lowering 未漏掉權威與記憶體守衛 §16–18
PDAIS-C27 V0 反例與 trace 可重現 §21–24
PDAIS-C28 性能報告完整計入傳輸/驗證/提交 §20–22
PDAIS-C29 完全沒有 AI 時仍有可運作的控制層 §19、§26
PDAIS-C30 對不適用工作負載主動報告負面證據 §21–23

附錄 B|跨篇契約相容矩陣與執行權限

B.1 前篇輸入、Paper 05 使用方式與不可偷渡的效果

來源契約 被 PDAIS 接收的核心資料 對應 op 不得偷渡
Paper 01 PrimaryFlowNode flow_id、state_version、lease、fence FLOW_* 工作流自治 ⇒ 全域任意寫入
Paper 02 PhaseDiffusion event_epoch、phase_kind、topology_generation、credit_id PHASE_*、COUPLE_*、DIFFUSE_* 訊息到達 ⇒ 任務完成
Paper 03 Reconciliation candidate_id、message_id、R 模式、lineage_id、local evidence REDUNDANCY_*、RECONCILE_* 多路吻合 ⇒ 新的獨立真理
Paper 04 SpeculativeCommit branch_id、版本集合、commit_key、authority_generation SPEC_*、COMMIT_*、EFFECT_* local verified ⇒ 具權威提交
Paper 04 GPU dependency gpu_event、buffer_lease、version guard SPEC_ATTACH_GPU、GPU_* device complete ⇒ HostVisible/Committed

B.2 最小作用域權限表

FlowCreate      -> FLOW_OPEN
FlowControl     -> FLOW_WAKE, FLOW_YIELD, FLOW_CLOSE
LeaseAuthority  -> FLOW_REBIND (guarded)
PhaseObserve    -> PHASE_READ
PhasePropose    -> PHASE_SIGNAL
CouplePropose   -> COUPLE_PROPOSE
CoupleAdmit     -> COUPLE_ADMIT, COUPLE_REVOKE
SendReserve     -> DIFFUSE_RESERVE
SendPermit      -> DIFFUSE_SEND (consumptive)
ReconcileLocal  -> RECONCILE_COMPARE, RECONCILE_SELECT, RECONCILE_SEAL
SpeculateLocal  -> SPEC_BEGIN, SPEC_DERIVE, SPEC_FORK
CommitPropose   -> COMMIT_PROPOSE
CommitValidate  -> COMMIT_VALIDATE
CommitArbitrate -> COMMIT_DECIDE
PublishCommitted -> COMMIT_PUBLISH
EffectEnqueue   -> EFFECT_ENQUEUE
EffectDeliver   -> EFFECT_DELIVER
DeviceSubmit    -> GPU_BATCH
DeviceObserve   -> GPU_WAIT
DeviceVisibility -> GPU_MAKE_HOST_VISIBLE (guarded)

此表列的是效果能力種類,不是持有該能力便不需檢查物件、作用域、版本與硬體資源。對第三方 plugin 或人為注入的 capability 欄位,仍須驗證其不可偽造性及委派鏈。

B.3 一組禁止「方便但錯誤」的隱式轉型

DeliveryAttempt<Msg,A>    ≠ IndependentWitness<Origin>
EncodedShard<Group,Index> ≠ CompletePayload<Group>
PhaseRead                 ≠ PhaseWriteCapability
AdmittedEdge              ≠ UnlimitedDataSend
Tentative<T,B>            ≠ Committed<T,K>
LocalOutcome<K>           ≠ CommitDecision<K>
GPUEvent<Device>          ≠ HostVisible<T>
CommitDecision<K>         ≠ EffectSettled<E>
OSCPUId                    ≠ FlowId
MessageDigest             ≠ StableCommitKey

附錄 C|參考實作的最小 repo 構想與完成定義

建議先由一個獨立可版控的研究分支或實驗 repo 承擔 v0.1;不假定使用者已建立新的專案或已購買新的 CPU。

pdais-v0/
  spec/
    PDAIS_ABSTRACT_ISA_v0.1.md
    PDAIS_TYPE_EFFECT_v0.1.md
    PDAIS_ERROR_ALGEBRA_v0.1.md
    PDAIS_PROTOCOL_INTEROP_v0.1.md
  schemas/
    module-header.schema.json
    message-envelope.schema.json
    trace-event.schema.json
  interpreter/
    machine_state/
    op_flow/
    op_phase_coupling/
    op_diffusion/
    op_reconciliation/
    op_speculation_commit/
    op_effects/
    op_device_stub/
  verification/
    static_verifier/
    finite_state_model/
    trace_checker/
    replay_checker/
  baselines/
    single_thread/
    thread_pool/
    actor_like/
    sharded_event_loop/
  workloads/
    cpu_message_graph/
    redundancy_r1_r2_r3/
    versioned_commit/
    gpu_optional/
  tests/
    positive_contract/
    negative_contract/
    crash_injection/
    optimizer_legality/
    cross_target_refinement/
  evidence/
    runs/
    failure_traces/
    provenance/
  docs/
    V0_REFERENCE_REPORT.md
    V1_ABLATION_PLAN.md

V0 的最低完成定義:能解析或直接構建 typed op、拒絕 20 條以上代表性非法操作、在有限模型中檢查核心安全不變量、輸出可重演的 trace,並通過獨立 oracle/差異測試。V1 的最低完成定義則需要可執行本地 CPU baseline 與完整成本量測;GPU 與原生硬體擴充不屬 V0 必備項目。


附錄 D|發表、形式證明與 UTF-8 原稿驗證規則

D.1 四種不相同的成熟度

  • L0:構想與研究綱領。 問題和目標已表述,但沒有可執行語義。
  • L1:形式候選規格。 有明確型別、狀態、轉移和可反證條件;目前 Paper 05 屬此級。
  • L2:有可重現的參考實作及 formal/test evidence。 必須提交實際執行紀錄,不以論文中寫有測試方案冒充已測試。
  • L3:實體硬體上經公平 baseline 實測並取得外部可檢查證據。 只對確實測得的適用域提出效能主張。

D.2 正式原稿規則

本文採 UTF-8 Markdown 為 canonical source。數學源碼僅使用 $...$ 與 $$...$$ 分隔符;聊天畫面、PDF 或其他渲染結果不是正式數學原稿。不得經過 Unicode 數學字元 round-trip 改寫 LaTeX,也不得使用 unicode_escape 往返重建 source。任何完成/提交版本都應對 UTF-8、碼框、公式分隔符及引用清單進行真實檔案驗證,然後輸出可下載原始檔。

D.3 禁止事後補造證據

不得以「合理推測」「理論上應該可以」取代具體跑分、形式模型檢查報告或 compiler test log。若尚未進行 L2/L3,必須明記待驗證。不允許在參考文獻中列出不存在的 DOI、虛構 Git commit 或憑空宣稱某個測試已 PASS。


參考文獻與原始研究來源

內部正式系列原稿

  • [I0] Neo.K × Aletheia, SMPDC Paper 00 — Stellar Multi-Primary Persistent Diffusive Computing, v0.1, 2026-10-16;原始檔:SMPDC_Paper00_Stellar_Multi_Primary_Persistent_Diffusive_Computing_v0.1_2026-10-16.md。
  • [I1] Neo.K × Aletheia, SMPDC Paper 01 — Multi-Primary Workflow Nodes, v0.1, 2026-10-16;原始檔:SMPDC_Paper01_Multi_Primary_Workflow_Nodes_v0.1_2026-10-16.md。
  • [I2] Neo.K × Aletheia, SMPDC Paper 02 — Phase Coupling and Bounded Persistent Diffusion, v0.1, 2026-10-16;原始檔:SMPDC_Paper02_Phase_Coupling_and_Bounded_Persistent_Diffusion_v0.1_2026-10-16.md。
  • [I3] Neo.K × Aletheia, SMPDC Paper 03 — Redundant Information Flows and Primary-Node Reconciliation, v0.1, 2026-10-16;原始檔:SMPDC_Paper03_Redundant_Information_Flow_and_Primary_Node_Reconciliation_v0.1_2026-10-16.md。
  • [I4] Neo.K × Aletheia, SMPDC Paper 04 — Speculative Execution and Deterministic Commit, v0.1, 2026-10-16;原始檔:SMPDC_Paper04_Speculative_Execution_and_Deterministic_Commit_v0.1_2026-10-16.md。

雲端既有理論(本篇脈絡,不等同公開同行審查)

  • [I5] Neo.K, 群星模型:基於宇宙星系概念的 AI 模型設計方法論。
  • [I6] Neo.K, 群星架構在計算機系統中的應用與改良計畫。
  • [I7] Neo.K, 相位計算機理論 v0.1;無界智庫公開版:https://unboundedaxiom.org/p/lm-001850/。
  • [I8] Neo.K × Aletheia, GCCFT Paper 06:從 Scheduler 到 Coupled Computation Planner。
  • [I9] Neo.K × Aletheia, GCCFT Paper 07:AI 實例化。
  • [I10] Neo.K × Aletheia, GCCFT Paper 08:可證偽驗證。
  • [I11] Neo.K, GCCWT Paper 04:計算場與資源激發;無界智庫公開版:https://unboundedaxiom.org/p/lm-004846/。
  • [I12] EveMissLab, GCM Phase C — AI-assisted Compute Orchestrator Engineering Blueprint v0.1。

公開研究與正式工程文獻(2026-10-16 查核)

原創性、證據與引用聲明

本文源自 Neo.K 提出的群星式多主工作流、相位呼叫、GPU 連結運算、冗餘聚合與持續擴散指令研究方向。上列既有文獻用來劃清先例、建立公平基線,不構成第三方為 SMPDC 提供正確性、原創性或效能背書。所有模型、命題、IR 與實驗設定均為待實作及待驗證的候選研究成果;正式學術新穎性和效能價值應由後續可重現的程式、測試與相關文獻比對決定。