sml-vectorclock

Vector clocks for causal ordering in distributed systems, in pure Standard ML. A vector clock maps node identifiers to monotonically increasing integer counters; comparing two clocks recovers Lamport's happens-before relation (and its negation, concurrency), and merging takes the componentwise least upper bound. Complements sml-crdt and sml-raft.

No FFI, no IO, no wall-clock, no randomness, no threads, and no external dependencies — the structure is pure and deterministic, behaving byte-identically under both MLton and Poly/ML.

Status

• 43 assertions, green on MLton and Poly/ML.
• Basis-library only; no vendored dependencies (Layout A, standalone).
• Pure: no FFI, IO, clock, randomness, or threads. toList is node-sorted so every observable output is deterministic.

Install

With smlpkg:

smlpkg add github.com/sjqtentacles/sml-vectorclock
smlpkg sync

Include the MLB from your own:

local
  $(SML_LIB)/basis/basis.mlb
  lib/github.com/sjqtentacles/sml-vectorclock/... (via smlpkg)
in
  ...
end

This brings the opaque structure VectorClock into scope.

Quick start

val a0 = VectorClock.empty
val a1 = VectorClock.tick a0 "alice"        (* {alice:1}            *)
val a2 = VectorClock.tick a1 "alice"        (* {alice:2}            *)

val () = print (Int.toString (VectorClock.get a2 "alice"))   (* 2 *)

(* bob receives alice's clock, then does local work *)
val b1 = VectorClock.tick (VectorClock.merge VectorClock.empty a2) "bob"
val ord = VectorClock.compare a2 b1          (* Before: alice2 -> b1 *)

(* concurrent divergence from a shared prefix *)
val base  = VectorClock.tick VectorClock.empty "alice"
val left  = VectorClock.tick base "bob"      (* {alice:1,bob:1}      *)
val right = VectorClock.tick base "carol"    (* {alice:1,carol:1}    *)
val c = VectorClock.compare left right       (* Concurrent           *)

(* merge reconciles the histories (componentwise max) *)
val m = VectorClock.merge left right         (* {alice:1,bob:1,carol:1} *)
val pairs = VectorClock.toList m             (* sorted by node id    *)

API (signature VECTOR_CLOCK)

type t   (* abstract map from node id (string) to counter; absent nodes read 0 *)

datatype ord = Before | After | Concurrent | Equal

val empty   : t
val tick    : t -> string -> t          (* increment this node's counter      *)
val merge   : t -> t -> t               (* componentwise max (least upper bound) *)
val compare : t -> t -> ord             (* happens-before relation             *)
val get     : t -> string -> int        (* node's counter (0 if absent)        *)
val toList  : t -> (string * int) list  (* non-zero nodes, sorted by node id   *)

Conventions

• empty is the all-zero clock; any absent node reads as 0 via get.

• tick c n increments only node n's counter, by one — the sole way a counter advances.

• merge a b is the componentwise maximum, i.e. the least upper bound in the lattice of clocks. It is After-or-Equal to both inputs under compare, commutative, and idempotent.

• compare a b is the partial happens-before order:

  • Before — a strictly precedes b (a <= b componentwise, a <> b);
  • After — b strictly precedes a;
  • Equal — identical clocks;
  • Concurrent — neither precedes the other.

  Before is transitive (a -> b and b -> c imply a -> c), and Before/After are duals.

• toList returns the (node, counter) pairs with a non-zero counter, sorted ascending by node id, so output is deterministic regardless of tick order.

Build & test

make test        # MLton
make test-poly   # Poly/ML
make all-tests   # both
make example     # build + run examples/demo.sml
make clean

Both compilers run the same strict-TDD suite (43 assertions, written before the implementation). It pins: tick advances exactly one node by exactly one; compare reports Equal for identical clocks, Before/After for causal chains (including transitivity across a -> b -> c), and Concurrent for diverged clocks; and merge is the componentwise least upper bound (>= both inputs under compare, commutative, idempotent). toList is checked for deterministic node-sorted output independent of insertion order.

Example

make example replays a small deterministic distributed scenario — a causal chain, a concurrent divergence, and a reconciling merge — with output that is byte-identical under MLton and Poly/ML:

=== sml-vectorclock demo ======================================

Causal history
  alice after 2 events       = {alice:2}
  bob after recv(alice)+tick = {alice:2,bob:1}
  compare alice2 b1          = Before (happens-before)   (alice2 -> b1)

Concurrent divergence (no message between them)
  left  (alice,bob)          = {alice:1,bob:1}
  right (alice,carol)        = {alice:1,carol:1}
  compare left right         = Concurrent

Merge (componentwise least upper bound)
  merge(left,right)          = {alice:1,bob:1,carol:1}
  compare merged left        = After
  compare merged right       = After
  get alice / bob / carol    = 1 / 1 / 1

===============================================================

Poly/ML note

CI builds Poly/ML 5.9.1 from source rather than using the Ubuntu package (Poly/ML 5.7.1), whose X86 code generator crashes (asGenReg raised while compiling) on some code. See .github/workflows/ci.yml.

License

MIT — see LICENSE.