Add TLA+ specification for unified WAL replication/bottomless

Author: penberg

Diff for: tlaplus/wal_replication.tla

@@ -0,0 +1,88 @@
+---------------------------- MODULE wal_replication ---------------------------
+\* A formal specification of write-ahead log (WAL) replication algorithm.
+\*
+\* The algorithm assumes the presence of a write-ahead log (WAL), like the one
+\* used in SQLite, where transactions append modified pages to a WAL. Each
+\* modified page within the WAL is referred to as a frame and is assigned a
+\* monotonically increasing frame index.
+\*
+\* A write is not guaranateed durability until it is backed up. Therefore,
+\* when recovering, primary and replicas revert back to the latest durable
+\* index.
+
+EXTENDS Integers
+
+VARIABLE
+    \* Index to the latest ephemeral frame.
+    latestIndex,
+    \* Index to the latest durable frame.
+    durableIndex,
+    \* Durable frames.
+    durableFrames,
+    \* The primary WAL.
+    primaryWAL,
+    \* The replica WAL.
+    replicaWAL
+
+Maximum(s) ==
+    IF s = {} THEN
+        0
+    ELSE
+        CHOOSE x \in s : \A y \in s : x >= y
+
+\* Recovery reverts to the durable index and all ephemeral writes are lost. 
+Recover ==
+    /\ latestIndex' = durableIndex
+    /\ primaryWAL' = {}
+    /\ replicaWAL' = {}
+    /\ UNCHANGED(<<durableFrames, durableIndex>>)
+
+\* Checkpoint the primary database and store frames to durable storage.
+Checkpoint ==
+    /\ durableFrames' = durableFrames \union primaryWAL
+    /\ durableIndex' = Maximum(durableFrames')
+    /\ primaryWAL' = {}
+    /\ UNCHANGED(<<latestIndex, replicaWAL>>)
+
+\* Replication pulls frames from the primary WAL. All durable frames
+\* are also visible to the replica.
+Replicate ==
+    /\ replicaWAL' = primaryWAL
+    /\ UNCHANGED(<<latestIndex, durableIndex, durableFrames>>)
+
+\* Append a frame to the primary WAL.
+AppendToPrimaryWAL(index) ==
+    /\ primaryWAL' = primaryWAL \union {index}
+
+\* Update the primary WAL.
+Update ==
+    /\ AppendToPrimaryWAL(latestIndex + 1)
+    /\ latestIndex' = latestIndex + 1
+    /\ UNCHANGED(<<durableIndex, durableFrames, replicaWAL>>)
+
+Next ==
+    \/ Update
+    \/ Checkpoint
+    \/ Replicate
+    \/ Recover
+
+Init ==
+    /\ latestIndex = 0
+    /\ durableIndex = 0
+    /\ durableFrames = {}
+    /\ primaryWAL = {}
+    /\ replicaWAL = {}
+
+\* Invariants
+
+\* INVARIANT: No durable frames are lost.
+NoDurableFramesLost ==
+    \A i \in 1..durableIndex : i \in durableFrames
+
+\* INVARIANT: Replica is not ahead of primary.
+ReplicaIsNotAhead ==
+    Maximum(replicaWAL) <= latestIndex
+
+\* TODO INVARIANT: Read your writes on replica
+
+====