Swim

Swim: the SWIM failure-detection probe loop over a Membership CRDT (P1 L3).

This is the pure protocol state machine: each transition takes the current state + the clock + any injected randomness (the member to probe, the helper set) and returns the next state plus the I/O Actions the runtime layer must perform (send a ping, ask for an indirect ping, gossip a status change). The socket/timer glue that picks random members, sends frames, and fires timers lives in the runtime layer (same split as NetKernel/ClusterConn) — keeping the detection logic deterministic and unit-testable.

One protocol period probes one target:

begin_period(target) -> SendPing(target) (direct ping)
no ack by ack_timeout_ms -> SendPingReq(h, target)… (k-way indirect)
no ack by period end -> mark Suspect + Gossip, arm suspect timer
suspect timer expires -> mark Dead + Gossip

A node refutes a false suspicion by bumping its own incarnation and re-announcing Alive (incarnation-ordered CRDT merge in Membership).

Types

typeConfigConfig = { ack_timeout_ms : Int, suspect_timeout_ms : Int, indirect_k : Int }#

typeProbeProbe = { target : String, sent_at : Int, indirect_sent : Bool, acked : Bool }#

typeStateState = {#

typeActionAction =#

Functions

fnbegin_periodbegin_period(s : State, now : Int, target : String) : (State, Action)#

fnconfigconfig(ack_timeout_ms : Int, suspect_timeout_ms : Int, indirect_k : Int) : Config#

fnend_periodend_period(s : State, now : Int) : (State, List(Action))#

fnescalate_indirectescalate_indirect(s : State, now : Int, helpers : List(String)) : (State, List(Action))#

fnexpire_suspectsexpire_suspects(s : State, now : Int) : (State, List(Action))#

fnmakemake(me : String, incarnation : Int, members : Members, config : Config) : State#

fnon_ackon_ack(s : State, from : String) : State#

fnon_gossipon_gossip(s : State, member : Member) : State#

fnrefuterefute(s : State) : (State, Option(Action))#