celld durability gate

✓ Passing This code compiles and runs correctly.

Code

input.k

Actual

node-a claims the cell
  held msg-1 at pos 1 — response gated
  ack  msg-1 — durable through 1
  held msg-2 at pos 2 — response gated
  fail msg-2 — durability unproven
  release node-a

Expected output

node-a claims the cell
  held msg-1 at pos 1 — response gated
  ack  msg-1 — durable through 1
  held msg-2 at pos 2 — response gated
  fail msg-2 — durability unproven
  release node-a

Flows

flow ~new click a branch to expand · @labels scroll to their anchor
new (expr: own, capacity: 1, source: epoch: 0[i64], etag: 0[i64])
flow ~new click a branch to expand · @labels scroll to their anchor
new (expr: st, capacity: 1, source: pos: 0[i64], synced: 0[i64])
subflow ~cas.claim click a branch to expand · @labels scroll to their anchor
if (guard == own.etag)
subflow ~cas.release click a branch to expand · @labels scroll to their anchor
print.ln (expr: " release {{ lease:s }}")
subflow ~cell.write click a branch to expand · @labels scroll to their anchor
if (own.epoch > 0)
subflow ~replica.sync click a branch to expand · @labels scroll to their anchor
if (upto <= st.pos)
subflow ~gate.ack click a branch to expand · @labels scroll to their anchor
print.ln (expr: " ack {{ r:s }} — durable through {{ proof:d }}")
subflow ~gate.fail click a branch to expand · @labels scroll to their anchor
print.ln (expr: " fail {{ r:s }} — {{ why:s }}")
subflow ~handle click a branch to expand · @labels scroll to their anchor
cell.write (lease, data)
flow ~print.ln click a branch to expand · @labels scroll to their anchor
print.ln (expr: "node-a claims the cell")
flow ~cas.claim click a branch to expand · @labels scroll to their anchor
cas.claim (node: "node-a", guard: 0)

Test Configuration

MUST_RUN