Skip to content

Commit c4c14bd

Browse files
committed
feat(cnf): causal stamp + causal election (thread 019f100f-eefe, part A)
Thread every coordination write with :observed — the global seq the writer had SEEN when it decided (reuse OCC's discarded :base, dropped after the single-valued reject). One int per tx, recovered through replay/dump-log! exactly like :seq/:agent. Clamped to the pre-commit head: a writer cannot claim to have observed the future (a backdated stamp only LOSES elections). This turns happens-before into a recorded fact and adds elect-causal — the read-time election ordered by [observed, cid, agent] instead of [cid, agent]. Rival drivers/roles now resolve by "who had the earlier causal VIEW" rather than "who happened to commit first": a later committer that decided earlier wins. Pure fn of recorded claims, so every reader elects identically with zero coordination. Strict refinement of elect (legacy claims with no stamp fall back to seq-of) — never a regression. cnf_causality_test (d) observed survives replay + is clamped; (a) rivals coexist and causal election differs from cid election. cnf_coord / schema / coexist-elect / views / lease / snapshot / occ-verbs all stay green.
1 parent 8be306c commit c4c14bd

2 files changed

Lines changed: 128 additions & 4 deletions

File tree

cnf_coord.clj

Lines changed: 48 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,8 @@
5050
{:k :entity :id id})
5151
(for [[cid mm] (:claims m) :when (>= cid since)]
5252
{:k :claim :cid cid :l (:l mm) :p (:p mm) :r (:r mm) :tx (get (:tx-of m) cid)})
53-
[{:k :tx :tx txid :seq (get-in m [:txs txid :seq]) :agent (get-in m [:txs txid :agent])}
53+
[{:k :tx :tx txid :seq (get-in m [:txs txid :seq]) :agent (get-in m [:txs txid :agent])
54+
:observed (get-in m [:txs txid :observed])} ; causality (thread H): the global seq the writer had SEEN when it decided
5455
{:k :commit :tx txid}])))
5556

5657
;; --- reads over the reified store -------------------------------------------
@@ -83,6 +84,27 @@
8384
(defn agent-of [co cid]
8485
(let [m @(store co)] (get-in m [:txs (get (:tx-of m) cid) :agent])))
8586

87+
;; --- causality / as-of (thread H, Part A): the causal stamp ------------------
88+
;; Every coordination write already reports :base = "the version I had observed when
89+
;; I decided" (the daemon/CLI path passes the GLOBAL :version it round-tripped; commit!/
90+
;; retract! used it ONLY for the single-valued staleness reject, then dropped it). We now
91+
;; THREAD that base into the tx record as :observed — one int per tx, recovered through
92+
;; replay exactly like :seq/:agent. This turns happens-before into a recorded fact:
93+
;; "did peer B's claim exist in the view A read before A acted?" == (<= seq(B) observed(A)).
94+
;; observed-of reads it; nil for legacy/non-causal writes -> callers fall back to seq-of
95+
;; (commit order), so the causal election degrades to cid-order, never throws.
96+
;; RISK GUARD: the writer cannot claim to have observed the FUTURE — observed is clamped
97+
;; to the pre-commit current-seq at the write site (a backdated stamp only LOSES elections).
98+
(defn observed-of [co cid]
99+
(let [m @(store co)] (get-in m [:txs (get (:tx-of m) cid) :observed])))
100+
;; the causal key of a live claim: [observed-or-seq, cid, agent]. observed orders by
101+
;; DECISION time (who saw the empty group first), cid/agent keep it a total order. A LATER
102+
;; commit (higher cid) that DECIDED earlier (lower observed) wins — this is the whole point:
103+
;; election by causal view, not by commit order. Pure fn of recorded claims -> every reader
104+
;; computes it identically with zero coordination.
105+
(defn causal-key [co cid]
106+
[(or (observed-of co cid) (seq-of co cid)) cid (str (agent-of co cid))])
107+
86108
;; --- views-as-claims (thread E): per-branch isolation over the same log ------
87109
;; A VIEW is a first-class subject; (view selects @cid) claims are its OVERLAY —
88110
;; the cids it treats as facts. The object IS a claim id: cids live in the same
@@ -119,6 +141,24 @@
119141
pool (if (seq in-view) in-view cids)]
120142
(first (sort-by (fn [cid] [cid (str (agent-of co cid))]) pool))))))
121143

144+
;; elect-causal — the CAUSAL election policy (thread H, Part C): same view-relative
145+
;; pool as `elect`, but ordered by the CAUSAL key [observed, cid, agent] instead of
146+
;; [cid, agent]. So of a contended live (l,p) group, the winner is the member whose
147+
;; writer DECIDED earliest (saw the empty/oldest group), tie-broken by commit order
148+
;; then agent. This is what lets rival drivers/roles COEXIST and resolve by "who had
149+
;; the earlier causal view" rather than "who happened to commit first" — both readers
150+
;; agree, nothing blocks. Degrades to `elect` when no :observed stamps exist (legacy
151+
;; claims fall back to seq-of via causal-key), so it is a strict refinement, never a
152+
;; regression. nil on an empty group.
153+
(defn elect-causal
154+
([co cids] (elect-causal co nil cids))
155+
([co view cids]
156+
(when (seq cids)
157+
(let [sel (when view (view-selects co view))
158+
in-view (when (seq sel) (filterv sel cids))
159+
pool (if (seq in-view) in-view cids)]
160+
(first (sort-by (fn [cid] (causal-key co cid)) pool))))))
161+
122162
(defn- ent! [co tx nm]
123163
(or (s/resolve-name (store co) nm)
124164
(let [e (c/entity! (store co))] (s/name! (store co) e nm tx) e)))
@@ -210,8 +250,10 @@
210250
{:ok (current-seq co) :idempotent true}
211251

212252
:else
213-
(let [since (:next-id @(store co))
253+
(let [since (:next-id @(store co))
254+
observed (let [pre (current-seq co)] (min (or base pre) pre)) ; causal stamp, clamped to head (no future)
214255
tx (c/begin-tx! (store co) agent)
256+
_ (swap! (store co) assoc-in [:txs tx :observed] observed)
215257
te (ent! co tx te-name)]
216258
(case kind
217259
:link (s/link! (store co) te pred (ent! co tx r-spec) tx)
@@ -282,7 +324,9 @@
282324
(if (empty? victims)
283325
{:ok (current-seq co)}
284326
(let [since (:next-id @(store co))
327+
observed (let [pre (current-seq co)] (min (or base pre) pre)) ; causal stamp on the retract tx
285328
tx (c/begin-tx! (store co) agent)
329+
_ (swap! (store co) assoc-in [:txs tx :observed] observed)
286330
sup (c/value! (store co) "cnf-supersedes")]
287331
(doseq [old victims] (c/claim! (store co) old sup old tx))
288332
(append-tx! co (delta-records co since tx))
@@ -392,7 +436,7 @@
392436
ents (vec (for [r recs :when (= (:k r) :entity)] (:id r)))
393437
claims (vec (for [r recs :when (= (:k r) :claim)] [(:cid r) {:l (:l r) :p (:p r) :r (:r r)}]))
394438
tx-of (vec (for [r recs :when (= (:k r) :claim)] [(:cid r) (:tx r)]))
395-
txs (vec (for [r recs :when (= (:k r) :tx)] [(:tx r) {:seq (:seq r) :agent (:agent r)}]))
439+
txs (vec (for [r recs :when (= (:k r) :tx)] [(:tx r) {:seq (:seq r) :agent (:agent r) :observed (:observed r)}])) ; recover the causal stamp through replay (acceptance d)
396440
sup (some (fn [[id v]] (when (= v "cnf-supersedes") id)) vals)
397441
superd (vec (for [[_ m] claims :when (= (:p m) sup)] (:r m)))
398442
all-id (concat (map first vals) ents (map first claims) (map first txs))
@@ -425,7 +469,7 @@
425469
(emit {:k :entity :id id}))
426470
(doseq [[cid cl] (:claims m)]
427471
(emit {:k :claim :cid cid :l (:l cl) :p (:p cl) :r (:r cl) :tx (get (:tx-of m) cid)}))
428-
(doseq [[tx t] (:txs m)] (emit {:k :tx :tx tx :seq (:seq t) :agent (:agent t)}))
472+
(doseq [[tx t] (:txs m)] (emit {:k :tx :tx tx :seq (:seq t) :agent (:agent t) :observed (:observed t)}))
429473
(emit {:k :commit :tx :migration}))
430474
(.force (.getChannel os) true))))
431475

tests/cnf_causality_test.clj

Lines changed: 80 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
;; cnf_causality_test.clj — thread 019f100f-eefe: causality/as-of + first-class
2+
;; retraction + (the death of) the internal lease. The acceptance gate for thread H.
3+
;;
4+
;; Sections map to the thread's ACCEPTANCE criteria:
5+
;; (d) the causal STAMP (:observed) survives a log replay round-trip + is clamped
6+
;; to the pre-commit head (a writer cannot claim to have observed the future).
7+
;; (a) causal ELECTION: two agents assert rival multi-valued claims, BOTH land (no
8+
;; reject, no block), and select-causal-1 elects an IDENTICAL winner across all
9+
;; readers purely from recorded observed/cid — and it picks by DECISION order
10+
;; (observed), which can DIFFER from commit order (cid).
11+
;; (c) first-class RETRACTION: a withdrawn multi-valued member drops under remove-wins
12+
;; and RESURRECTS under an add-wins view — the policy is view-relative, not kernel.
13+
;; (b) :as-of {:seq S} reconstructs the pre-collision view AND re-sees a later-
14+
;; withdrawn claim (retraction-as-append is what makes as-of EXACT).
15+
;;
16+
;; bb -cp out tests/cnf_causality_test.clj
17+
(require '[fram.cnf :as c] '[fram.schema :as s])
18+
(load-file "cnf_coord.clj")
19+
20+
(def checks (atom []))
21+
(defn chk [nm ok] (swap! checks conj [nm (boolean ok)]))
22+
(defn live-of [co te-name pred]
23+
(vec (live-cids-lp co (s/resolve-name (store co) te-name) (c/value-id (store co) pred))))
24+
25+
;; ============================================================================
26+
;; (d) the causal stamp survives replay + is clamped to the head
27+
;; ============================================================================
28+
(let [log "/tmp/cnf-causality-d.log"
29+
co (new-coord log)
30+
_ (commit! co "w" "T0" "note" :assert "x" nil) ; advance the global seq
31+
_ (commit! co "w" "T0" "note2" :assert "y" nil)
32+
;; agentA reports it had observed an EARLY seq (1) when it decided
33+
_ (commit! co "agentA" "T1" "zzz" :assert "alice" 1)
34+
cidA (first (live-of co "T1" "zzz"))
35+
;; a writer that claims to have observed the FUTURE is clamped to the head AT ITS COMMIT
36+
headB (current-seq co)
37+
_ (commit! co "agentB" "T2" "zzz" :assert "bob" 999999)
38+
cidB (first (live-of co "T2" "zzz"))
39+
;; round-trip through the v2 log
40+
st2 (replay log)
41+
obs (fn [st cid] (get-in @st [:txs (get (:tx-of @st) cid) :observed]))]
42+
(chk "(d) observed recorded = the base the writer reported (1)" (= 1 (observed-of co cidA)))
43+
(chk "(d) observed CLAMPED to the pre-commit head (no future stamp)"
44+
(= headB (observed-of co cidB)))
45+
(chk "(d) observed survives a cold log REPLAY round-trip" (= 1 (obs st2 cidA)))
46+
(chk "(d) clamped observed survives replay too" (= headB (obs st2 cidB))))
47+
48+
;; ============================================================================
49+
;; (a) causal election — rivals coexist; the EARLIEST-DECIDER wins (observed),
50+
;; which can differ from earliest-COMMITTER (cid).
51+
;; ============================================================================
52+
(let [log "/tmp/cnf-causality-a.log"
53+
co (new-coord log)
54+
;; advance the global head so the two rivals can carry distinct observed stamps
55+
_ (dotimes [i 50] (commit! co "w" "Tseq" "n" :assert (str i) nil))
56+
;; "drv" is undeclared -> MULTI -> rivals coexist (no supersede, no reject).
57+
;; agentA COMMITS FIRST (smaller cid) but DECIDED LATE (observed 40).
58+
rA (commit! co "agentA" "TH" "drv" :assert "A" 40)
59+
;; agentB COMMITS SECOND (larger cid) but DECIDED EARLY (observed 5).
60+
rB (commit! co "agentB" "TH" "drv" :assert "B" 5)
61+
live (live-of co "TH" "drv")
62+
[cA cB] (sort live) ; cA = agentA's (earlier cid), cB = agentB's
63+
cid-win (elect co live) ; [cid, agent] -> earliest COMMIT
64+
causal-win (elect-causal co live)] ; [observed, cid, agent] -> earliest DECISION
65+
(chk "(a) both rival multi writes COMMITTED — no block, no reject" (and (:ok rA) (:ok rB)))
66+
(chk "(a) BOTH coexist live (no supersede)" (= 2 (count live)))
67+
(chk "(a) cid-election picks the earliest COMMITTER (agentA)" (= cid-win cA))
68+
(chk "(a) causal-election picks the earliest DECIDER (agentB, observed 5)" (= causal-win cB))
69+
(chk "(a) causal election DIFFERS from cid election here (the whole point)" (not= cid-win causal-win))
70+
(chk "(a) causal election is input-order-INDEPENDENT" (= causal-win (elect-causal co (vec (reverse live)))))
71+
(chk "(a) causal election is STABLE across reads" (= causal-win (elect-causal co live) (elect-causal co live)))
72+
(chk "(a) the elected member's value is the earliest decider's (B)"
73+
(= "B" (c/literal (store co) (:r (c/claim-of (store co) causal-win))))))
74+
75+
;; ---- summary ---------------------------------------------------------------
76+
(let [cs @checks fails (remove second cs)]
77+
(doseq [[nm ok] cs] (println (if ok " [PASS] " " [FAIL] ") nm))
78+
(if (empty? fails)
79+
(println "\ncnf-causality:" (count cs) "/" (count cs) "PASS")
80+
(do (println "\ncnf-causality:" (count fails) "FAILED of" (count cs)) (System/exit 1))))

0 commit comments

Comments
 (0)