Reaching consensus with gossip and pruning semi-lattice

This article was originally planned to be a retelling of sync9 and antimatter. It quickly got out of hand.

REL:

• https://braid.org/sync9
• https://braid.org/drafts/time-machines
• https://braid.org/antimatter

Semi-lattice

If you have a “up” and partial ordering for a type (α below), the type is semi-lattice.

Collaborative text editing is showcased in the sync9 demo. α is a list of edits like Insert('a'@0), Delete(0:1). Two lists of edits can merge (the “up”).

Pruning Semi-lattice

It’s like morphing semi-lattice, yet not morphism. Partial morphism? The definition:

import Mathlib.Order.Basic
import Mathlib.Order.Lattice

def larger [PartialOrder α] (a : α) (s : Set α) := ∃ b ∈ s, a ≥ b

class PrunableSemilatticeSup (α : Type u) extends SemilatticeSup α where
  PrunedType : Set α -> Type u
  -- PrunedType can be pruned further
  preserve_prune : (s : Set α) -> PrunableSemilatticeSup (PrunedType s)
  prune : (s : Set α) -> α -> Option (PrunedType s)
  -- nothing important is pruned away
  correct : (s : Set α) -> ∀ a: α, larger a s → (prune s a).isSome = true
  -- preserve local morphology
  preserve_morphology : ∀ a b: α, (l : larger a s ∧ larger b s) → prune s (a ⊔ b) = (prune s a).get (correct s a l.left) ⊔ (prune s b).get (correct s b l.right)

(The above code doesn’t compile. mentioned later.)

I was a bit surprised to find out that the underlying data type changes at runtime. This doesn’t happen much in practice. The role of a type system is to make invalid states unrepresentable. Here, what is considered invalid changes at runtime, so the type changes at runtime as well. In this case, even Zig can’t help me.

Consensus Algorithm

Can we use raft here? Why sync9?

Raft:

• the total number of nodes is fixed
• has one leader
• uses log. allows arbitrary data type

sync9:

• the total number of nodes is unknown
• the author of every point is responsible collecting global :ack and sending global :commit for that point
• every node keeps track of points with global :commit

I have trouble understanding the ack and commit mechanism after reading the reference implementation over and over. So, I made up my own.

The algorithm is as follows:

First, every participant keeps track of a list of current peers and the last state received from them.

structure Frontier [PrunableSemilatticeSup α] (α : Type u) where
  current_peers: Set PeerId
  current_acks: PeerId -> α

Pruning can happen based on current_acks. preserve_morphology ensures that prune don’t discard necessary information to use the pruned semilattice type later.

Communication happens over unreliable packet exchange network like UDP/IP.

Every one second (or some other duration), every participant broadcast its copy of Frontier (each inside one packet) to its neighbours. This is the heartbeat that ensures liveliness.

netjoin is handled similarly to “welcome” in antimatter. Basically, a new participant Z asks an existing participant A for a copy of the state. A add Z to current_peers and set its ack to be the ack of any existing peer. Then, A replies with the modified copy to Z. (potential impl footgun: this operation should be atomic and not happen interleaved with heatbeat read.)

netsplit is handled automatically due to how UDP works.

Forgetting about peers unseen after a certain duration

If timeout is implemented (ttl: PeerId -> Timestamp), then there are edge cases where some participants forget early or late due to clock skew.

The netjoin process should be modified to deal with this case. I don’t know how to solve this case, especially when unreliable transmission and timeout are involved.

Maybe the three-wave-ack can be used here?

Forgetting saves memory. Will you remember friends you have lost contact with forever? This was a problem in Scuttlebutt, where disk space grows unbounded. PZP claims to have solved this issue.

When reconnecting after being forgotten, here are some choices:

1. Forget about edits since the split.
2. Use conventional merge methods on the presentation type. e.g. git merge-file -p current /dev/null other for text. (not relying on the properties of semi-lattice)

There is no rebase since history is pruned away.

Proof and PoC

None yet. I think I broke Lean. Here’s the WIP source code, if you are interested.

Musings

Curious, I looked up “morphism” on Wikipedia and discovered that this is partial morphism. I didn’t expect morphism to appear here.

Now you’re thinking with semi-lattices.

Appendix – Proper Replace in Sync9

locations are like version numbers. There can be 3.0 and 3.1.

If you type “abcd”, then select and delete “bc”, the cursor is between “a” and “d” but at the location 1.1.

If you type “ad” and put the cursor in the middle, the cursor is at the location 1.0.

Then, when you insert some text,

If your conflict-free data type loses information when merging, you should be concerned.