100 lines
3.1 KiB
TOML
100 lines
3.1 KiB
TOML
|
# Goal 6 — dissemination reaches everyone. A star: the hub is linked to every
|
||
|
|
# leaf, but the leaves are NOT linked to each other. A leaf is therefore a
|
||
|
|
# *direct* probe partner of only the hub; leaf↔leaf liveness is sustained only
|
||
|
|
# by indirect probing through the hub, and leaf↔leaf agreement on membership is
|
||
|
|
# carried only by piggyback gossip relayed through the hub — i.e. past direct
|
||
|
|
# probe partners.
|
||
|
|
#
|
||
|
|
# One leaf ("c") is killed mid-run. The other leaves can never directly observe
|
||
|
|
# c; they converge on its death only via multi-hop relay/infection through the
|
||
|
|
# hub. `convergence_after` over ALL N asserts that agreement is nonetheless
|
||
|
|
# reached — the property that can only hold if dissemination reaches everyone.
|
||
|
|
# Expected verdict: pass-now.
|
||
|
|
|
||
|
|
name = "infection_star"
|
||
|
|
seed = 13
|
||
|
|
duration_ns = 50_000_000_000 # 50 s
|
||
|
|
|
||
|
|
[default_tick]
|
||
|
|
period_ns = 200_000_000
|
||
|
|
|
||
|
|
[default_link]
|
||
|
|
latency_ns = 5_000_000
|
||
|
|
jitter_stddev_ns = 1_000_000
|
||
|
|
loss_prob_ppm = 0
|
||
|
|
reorder_prob_ppm = 0
|
||
|
|
bandwidth_bps = 100_000_000
|
||
|
|
cold_dial_penalty_ns = 50_000_000
|
||
|
|
cache_warm_after_ns = 100_000_000
|
||
|
|
cache_invalidate_after_idle_ns = 30_000_000_000
|
||
|
|
|
||
|
|
# indirect_ping_fanout = 3 guarantees the hub is always among a leaf's relays
|
||
|
|
# (the relay pool for a leaf→leaf probe is {hub, other_leaf}), so leaf↔leaf
|
||
|
|
# probing succeeds through the hub and there are no false suspicions pre-kill.
|
||
|
|
[[peers]]
|
||
|
|
id = "hub"
|
||
|
|
kind = "swim"
|
||
|
|
initial_state = "alive"
|
||
|
|
kind_config = { probe_interval_ns = 1_000_000_000, probe_timeout_ns = 1_000_000_000, suspicion_timeout_ns = 5_000_000_000, indirect_ping_fanout = 3 }
|
||
|
|
[[peers]]
|
||
|
|
id = "a"
|
||
|
|
kind = "swim"
|
||
|
|
initial_state = "alive"
|
||
|
|
kind_config = { probe_interval_ns = 1_000_000_000, probe_timeout_ns = 1_000_000_000, suspicion_timeout_ns = 5_000_000_000, indirect_ping_fanout = 3 }
|
||
|
|
[[peers]]
|
||
|
|
id = "b"
|
||
|
|
kind = "swim"
|
||
|
|
initial_state = "alive"
|
||
|
|
kind_config = { probe_interval_ns = 1_000_000_000, probe_timeout_ns = 1_000_000_000, suspicion_timeout_ns = 5_000_000_000, indirect_ping_fanout = 3 }
|
||
|
|
[[peers]]
|
||
|
|
id = "c"
|
||
|
|
kind = "swim"
|
||
|
|
initial_state = "alive"
|
||
|
|
kind_config = { probe_interval_ns = 1_000_000_000, probe_timeout_ns = 1_000_000_000, suspicion_timeout_ns = 5_000_000_000, indirect_ping_fanout = 3 }
|
||
|
|
|
||
|
|
# Star links only: hub ↔ each leaf. Leaves are NOT linked to one another.
|
||
|
|
[[links]]
|
||
|
|
from = "hub"
|
||
|
|
to = "a"
|
||
|
|
[[links]]
|
||
|
|
from = "a"
|
||
|
|
to = "hub"
|
||
|
|
[[links]]
|
||
|
|
from = "hub"
|
||
|
|
to = "b"
|
||
|
|
[[links]]
|
||
|
|
from = "b"
|
||
|
|
to = "hub"
|
||
|
|
[[links]]
|
||
|
|
from = "hub"
|
||
|
|
to = "c"
|
||
|
|
[[links]]
|
||
|
|
from = "c"
|
||
|
|
to = "hub"
|
||
|
|
|
||
|
|
# Kill leaf "c": the other leaves are not its direct probe partners, so they can
|
||
|
|
# only learn of its death past the hub.
|
||
|
|
[[mutations]]
|
||
|
|
kind = "peer_kill"
|
||
|
|
at_ns = 15_000_000_000
|
||
|
|
peer = "c"
|
||
|
|
|
||
|
|
# A pre-kill snapshot (so the killed leaf has a baseline view for the
|
||
|
|
# all-observers convergence check) plus post-detection snapshots.
|
||
|
|
[[snapshots]]
|
||
|
|
at_ns = 10_000_000_000
|
||
|
|
[[snapshots]]
|
||
|
|
at_ns = 30_000_000_000
|
||
|
|
[[snapshots]]
|
||
|
|
at_ns = 36_000_000_000
|
||
|
|
[[snapshots]]
|
||
|
|
at_ns = 42_000_000_000
|
||
|
|
|
||
|
|
# Goal 6: every node converges on the shared view (hub/a/b Alive, c Dead) —
|
||
|
|
# agreement the leaves can reach only by infection relayed through the hub.
|
||
|
|
[[assertions]]
|
||
|
|
kind = "convergence_after"
|
||
|
|
after_ns = 25_000_000_000
|
||
|
|
within_ns = 20_000_000_000
|
||
|
|
peers = ["hub", "a", "b", "c"]
|