11. Invariants

Goal

Say what must never happen, then make it happen.

New in this chapter

always (…) form always spec/05 §5.7
always (…) context check spec/05 §5.4

Steps

The animation shows what the system does, but you also want to say what it must never do. A rule written once and checked after every step of the run is an invariant, and Synod writes it with always.

always takes a condition and is checked after each step of the simulation. When the condition turns false, the trace records sim.Broken with the rule's source line, once, and the run goes on. A rule is usually a phrase that gives a bool, so it can be long and still read in one line: always Agree.

Agree looks at the whole system. It goes through sim.NodesRunning rumor, the list of running nodes of the package, and collects the different rumors that they know. The result is true when at most one differs. Reading another node's Known is fine here: this code runs in a new context, check, which may read the state of any node but can write nothing except its own locals. Step 1 adds the rule, and the run keeps it:

Step 1

# package rumor
use std/disk
use std/lists
use std/net
use std/random
use std/sim

Rumor has
  set Text to ""

Ack has
  set Text to ""

Join has
  set Peers to {}

Node has
  set Peers to {}
  set Known to ""
  set Acked to {}
  set GaveUp to 0

# Every node in the list is told about all the others
define Connect [ns: list of Node]
  each n in ns
    deliver (message Join with Peers (lists.Without n from ns)) to n

# The peers that have not confirmed the rumor yet
define [n: Node] Pending
  set rest to {}
  each p in n.Peers
    if (p is not in n.Acked)
      set rest to (lists.Append p to rest)
  result rest

# Run b now. If p has not confirmed 300ms later, run it again, up to k times in all, then run c
define [n: Node] Retry [k: number] times for [p: node] [b: block] otherwise [c: block]
  b
  after 300ms
    if (p is not in n.Acked)
      if (k more than 1)
        n.Retry (k minus 1) times for p
          b
        otherwise
          c
      else
        c

# Tell one random peer that has not confirmed, and again until all have
define [n: Node] Tell
  set open to n.Pending
  if ((lists.Size open) more than 0)
    set peer to (random.Pick open)
    n.Retry 3 times for peer
      net.Send (message Rumor with Text n.Known) from n to peer
    otherwise
      set n.GaveUp to (n.GaveUp plus 1)
    after (random.TimeBetween 200ms and 600ms)
      n.Tell

# Believe a rumor the first time it is heard, keep it on disk, and start telling it
define [n: Node] Learn [t: text]
  if (n.Known is "")
    set n.Known to t
    disk.Write t at "known" on n
    n.Tell

# After a restart the fields are fresh, but the disk remembers
define [n: Node] start
  set n.Peers to (disk.Read "peers" on n or {})
  set n.Known to (disk.Read "known" on n or "")
  if (n.Known is not "")
    n.Tell

# Peers are kept on disk too
when [n: Node] (sim.Delivered Join)
  set n.Peers to Join.Peers
  disk.Write n.Peers at "peers" on n

when [n: Node] (sim.Delivered Rumor)
  n.Learn Rumor.Text

# Confirm every telling, even of a rumor already known
when [n: Node] (net.Received Rumor from sender)
  n.Learn Rumor.Text
  net.Send (message Ack with Text Rumor.Text) from n to sender

when [n: Node] (net.Received Ack from sender)
  if (sender is not in n.Acked)
    set n.Acked to (lists.Append sender to n.Acked)

# True while the running nodes know at most one rumor between them
define Agree
  set texts to {}
  each n in (sim.NodesRunning rumor)
    if ((n.Known is not "") and (n.Known is not in texts))
      set texts to (lists.Append n.Known to texts)
  result ((lists.Size texts) at most 1)

# Must hold after every step of the run
always Agree

To break it, two rumors must start while the network is split. Step 2 asks the viewer to predict, then delivers a second rumor to the far side. The two halves end up knowing different rumors, and the trace shows sim.Broken:

Step 2

# package main
use example.com/tutorial/rumor
use std/lesson
use std/net
use std/sim

define main
  sim.Seed 4
  set nodes to (sim.Cluster of 6 running rumor)
  set left to {(item 0 of nodes), (item 1 of nodes), (item 2 of nodes)}
  set right to {(item 3 of nodes), (item 4 of nodes), (item 5 of nodes)}
  rumor.Connect nodes
  deliver (message rumor.Rumor with Text "The leader is n1") to (item 0 of nodes)
  net.DropNext "Rumor" from (item 0 of nodes) to (item 1 of nodes)
  after 300ms
    net.Partition left from right
  after 1s
    lesson.Ask "The network is split. A second rumor starts on the far side. Will the nodes still agree?" choosing {"Yes: they check with each other first", "No: each side believes its own rumor"}
    deliver (message rumor.Rumor with Text "The leader is n6") to (item 5 of nodes)
  after 3s
    net.Heal

Another rule counts nodes that are down. sim.Nodes is the list of all nodes, up or not, and sim.IsUp n says whether one is running; the rule says fewer than three may be down at any moment. Step 3 crashes three nodes at once and the rule breaks, but the others still spread the rumor:

Step 3

# package main
use example.com/tutorial/rumor
use std/lesson
use std/net
use std/sim

define main
  sim.Seed 4
  set nodes to (sim.Cluster of 6 running rumor)
  set left to {(item 0 of nodes), (item 1 of nodes), (item 2 of nodes)}
  set right to {(item 3 of nodes), (item 4 of nodes), (item 5 of nodes)}
  rumor.Connect nodes
  deliver (message rumor.Rumor with Text "The leader is n1") to (item 0 of nodes)
  net.DropNext "Rumor" from (item 0 of nodes) to (item 1 of nodes)
  after 300ms
    net.Partition left from right
  after 1s
    lesson.Ask "Three of the six nodes crash. Does the rumor still reach the others?" choosing {"Yes: gossip does not need everyone", "No: it needs every node"}
    sim.Crash (item 3 of nodes)
    sim.Crash (item 4 of nodes)
    sim.Crash (item 5 of nodes)
  after 3s
    net.Heal
  sim.StopAt 10s

# package rumor
use std/disk
use std/lists
use std/net
use std/random
use std/sim

Rumor has
  set Text to ""

Ack has
  set Text to ""

Join has
  set Peers to {}

Node has
  set Peers to {}
  set Known to ""
  set Acked to {}
  set GaveUp to 0

# Every node in the list is told about all the others
define Connect [ns: list of Node]
  each n in ns
    deliver (message Join with Peers (lists.Without n from ns)) to n

# The peers that have not confirmed the rumor yet
define [n: Node] Pending
  set rest to {}
  each p in n.Peers
    if (p is not in n.Acked)
      set rest to (lists.Append p to rest)
  result rest

# Run b now. If p has not confirmed 300ms later, run it again, up to k times in all, then run c
define [n: Node] Retry [k: number] times for [p: node] [b: block] otherwise [c: block]
  b
  after 300ms
    if (p is not in n.Acked)
      if (k more than 1)
        n.Retry (k minus 1) times for p
          b
        otherwise
          c
      else
        c

# Tell one random peer that has not confirmed, and again until all have
define [n: Node] Tell
  set open to n.Pending
  if ((lists.Size open) more than 0)
    set peer to (random.Pick open)
    n.Retry 3 times for peer
      net.Send (message Rumor with Text n.Known) from n to peer
    otherwise
      set n.GaveUp to (n.GaveUp plus 1)
    after (random.TimeBetween 200ms and 600ms)
      n.Tell

# Believe a rumor the first time it is heard, keep it on disk, and start telling it
define [n: Node] Learn [t: text]
  if (n.Known is "")
    set n.Known to t
    disk.Write t at "known" on n
    n.Tell

# After a restart the fields are fresh, but the disk remembers
define [n: Node] start
  set n.Peers to (disk.Read "peers" on n or {})
  set n.Known to (disk.Read "known" on n or "")
  if (n.Known is not "")
    n.Tell

# Peers are kept on disk too
when [n: Node] (sim.Delivered Join)
  set n.Peers to Join.Peers
  disk.Write n.Peers at "peers" on n

when [n: Node] (sim.Delivered Rumor)
  n.Learn Rumor.Text

# Confirm every telling, even of a rumor already known
when [n: Node] (net.Received Rumor from sender)
  n.Learn Rumor.Text
  net.Send (message Ack with Text Rumor.Text) from n to sender

when [n: Node] (net.Received Ack from sender)
  if (sender is not in n.Acked)
    set n.Acked to (lists.Append sender to n.Acked)

# True while the running nodes know at most one rumor between them
define Agree
  set texts to {}
  each n in (sim.NodesRunning rumor)
    if ((n.Known is not "") and (n.Known is not in texts))
      set texts to (lists.Append n.Known to texts)
  result ((lists.Size texts) at most 1)

# Must hold after every step of the run
always Agree

# How many nodes are down
define Down
  set count to 0
  each n in sim.Nodes
    if (not (sim.IsUp n))
      set count to (count plus 1)
  result count

# Fewer than three nodes down, always
always (Down less than 3)

You have now met all four contexts, and each is where it is for a reason:

Context	Starts at	Reads	Writes
main	`define main`	any node's state	any node's state, and faults
node	`start`, `when [n: Node]`, receiver phrases	its own node	its own node
check	`always`	any node's state	only locals
look	`when` on trace events	exported state of any node	only shapes

Look comes next chapter.

What to watch

In step 2 the run goes on after the break: nothing stops, nothing is repaired. On the stage the border of the scene flashes red at the moment of sim.Broken. In step 3 the rule breaks as soon as the third node goes down, and only then.

Why it looks like this

A rule is checked after every step, in any order, so it must have no effects. Calling a node phrase from always would send messages from the checker:

rumor/rumor.synod:95:5: error[context]: "n.Tell" is node code; it cannot run in check context
    |
 95 |     n.Tell
    |     ^^^^^^
...
109 | always Careless
    |        -------- called from check context here
    |
    = note: "Careless" runs in check context

Error context

synod check says error[context] and the hint names the rule that calls it.

Exercises

In step 2 deliver the second rumor to item 0 of nodes instead of item 5. Is the rule broken?

Expected

No. The first node already knows the first rumor, and a node believes only the first rumor it hears, so nothing differs.

Change Down less than 3 to Down less than 4. What does step 3 show?

Expected

Three crashed nodes are allowed; sim.Broken does not appear.

Write a rule that at least four nodes are running.

Expected

always ((lists.Size (sim.NodesRunning rumor)) at least 4), with use std/lists. Crash three nodes and it breaks.