SERVER-44458 Model-checking files for RaftMongo.tla

6 files changed, 97 insertions, 20 deletions

diff --git a/src/mongo/db/repl/tla_plus/.gitignore b/src/mongo/db/repl/tla_plus/.gitignore
index 4542aa29c69..a9dcc645fd5 100644
--- a/src/mongo/db/repl/tla_plus/.gitignore
+++ b/src/mongo/db/repl/tla_plus/.gitignore
@@ -1 +1,3 @@
-*.toolbox
+**/*.toolbox
+**/states/
+tla2tools.jar
diff --git a/src/mongo/db/repl/tla_plus/README.md b/src/mongo/db/repl/tla_plus/README.md
new file mode 100644
index 00000000000..04b22f406d3
--- /dev/null
+++ b/src/mongo/db/repl/tla_plus/README.md
@@ -0,0 +1,23 @@
+Replication TLA+ Specifications
+===============================
+
+These are formal specifications for exploring possible replication protocols.
+Some are experiments, some reflect MongoDB's actual implementation. See the
+comments in each spec for details.
+
+Some specs are intended for model-checking. They are in subdirectories like:
+
+```
+SpecName/
+    SpecName.tla     specification
+    MCSpecName.tla   additional operators for model-checking
+    MCSpecName.cfg   configuration for model-checking
+```
+
+Run the model-checker on a spec thus:
+
+```
+./model-check.sh SpecName
+```
+
+There may be additional instructions in the spec or config file.
diff --git a/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg b/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg
new file mode 100644
index 00000000000..c94a84e89d9
--- /dev/null
+++ b/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg
@@ -0,0 +1,22 @@
+\* Config file to run the TLC model-checker on RaftMongo.tla.
+\* See RaftMongo.tla for instructions.
+
+\* The maximum number of oplog entries that can be created on the primary in one
+\* action. For model-checking, this can be 1 or a small number.
+CONSTANT MaxClientWriteSize = 2
+
+\* The number of election terms to simulate during model-checking.
+CONSTANT MaxTerm = 3
+
+\* The longest oplog any server can reach during model-checking.
+CONSTANT MaxLogLen = 3
+
+\* The set of server IDs. Adjust to test different replica set sizes.
+CONSTANT Server = {1, 2, 3}
+
+\* Add invariants if desired.
+INVARIANT NoTwoPrimariesInSameTerm
+
+\* Not configurable.
+CONSTRAINT StateConstraint
+SPECIFICATION Spec
diff --git a/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.tla b/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.tla
new file mode 100644
index 00000000000..057e3dd7a91
--- /dev/null
+++ b/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.tla
@@ -0,0 +1,13 @@
+---- MODULE MCRaftMongo ----
+\* This module defines RaftMongo.tla constants/constraints for model-checking.
+\* See RaftMongo.tla for instructions.
+
+EXTENDS RaftMongo
+
+CONSTANT MaxTerm
+CONSTANT MaxLogLen
+
+StateConstraint ==
+    /\ GlobalCurrentTerm <= MaxTerm
+    /\ \forall i \in Server: Len(log[i]) <= MaxLogLen
+=============================================================================
diff --git a/src/mongo/db/repl/tla_plus/RaftMongo.tla b/src/mongo/db/repl/tla_plus/RaftMongo/RaftMongo.tla
index 2eb32102990..dbe71dbf738 100644
--- a/src/mongo/db/repl/tla_plus/RaftMongo.tla
+++ b/src/mongo/db/repl/tla_plus/RaftMongo/RaftMongo.tla
@@ -6,24 +6,12 @@
 
 --------------------------------- MODULE RaftMongo ---------------------------------
 \* This is the formal specification for the Raft consensus algorithm in MongoDB.
+\*
+\* To run the model-checker, first edit the constants in MCRaftMongo.cfg if desired, then:
+\*     cd src/mongo/db/repl/tla_plus
+\*     ./model-check.sh RaftMongo
 
-\* INSTRUCTIONS FOR MODEL-CHECKING IN THE TLA+ TOOLBOX
-\* "What is the behavior spec?"
-\*     Temporal formula: Spec
-\* "What is the model?"
-\*     "Specify the value of declared constants"
-\*         MaxClientWriteSize = small number like 2 to limit state space
-\*         Servers = a set of your desired replica set size, e.g. {1, 2, 3}
-\* "What to check?"
-\*     Deadlock: checked
-\*     Invariants: NeverRollbackCommitted and NoTwoPrimariesInSameTerm
-\* "Additional Spec Options"
-\*     "State Constraint"
-\*         Add a state constraint to limit the state space like:
-\*             /\ GlobalCurrentTerm <= 3
-\*             /\ \forall i \in Server: Len(log[i]) <= 5
-
-EXTENDS Integers, FiniteSets, Sequences, TLC
+EXTENDS Integers, FiniteSets, Sequences
 
 \* The set of server IDs.
 CONSTANT Server
@@ -312,6 +300,12 @@ TwoPrimariesInSameTerm ==
 
 NoTwoPrimariesInSameTerm == ~TwoPrimariesInSameTerm
 
+\* NeverRollbackCommitted and NeverRollbackBeforeCommitPoint can be violated,
+\* although it's not ultimately a safety issue: SERVER-39626. The issue
+\* requires at least 5 servers, 3 terms, and oplogs of length 4+, which are
+\* larger limits than we can easily model-check. The properties
+\* are here if you want to experiment with them.
+
 RollbackCommitted(i) ==
     /\ [term |-> LastTerm(log[i]), index |-> Len(log[i])] \in committedEntries
     /\ \E j \in Server: CanRollbackOplog(i, j)
@@ -326,8 +320,6 @@ RollbackBeforeCommitPoint(i) ==
        \/ /\ LastTerm(log[i]) = commitPoint[i].term
           /\ Len(log[i]) <= commitPoint[i].index
 
-\* This is violated, although it's not ultimately a safety issue: SERVER-39626
-\* The property is here if you want to experiment with it.
 NeverRollbackBeforeCommitPoint == \A i \in Server: ~RollbackBeforeCommitPoint(i)
 
 \* Liveness check
diff --git a/src/mongo/db/repl/tla_plus/model-check.sh b/src/mongo/db/repl/tla_plus/model-check.sh
new file mode 100755
index 00000000000..f89b5b9f4e1
--- /dev/null
+++ b/src/mongo/db/repl/tla_plus/model-check.sh
@@ -0,0 +1,25 @@
+#!/bin/sh
+
+if [ "$#" -ne 1 ]; then
+  echo "Usage: $0 SPEC_DIRECTORY" >&2
+  exit 1
+fi
+if ! [ -e "$1" ]; then
+  echo "Directory $1 not found" >&2
+  exit 1
+fi
+if ! [ -d "$1" ]; then
+  echo "$1 not a directory" >&2
+  exit 1
+fi
+
+TLA_FILE="MC$1.tla"
+if ! [ -f "$1/$TLA_FILE" ]; then
+  echo "$1/$TLA_FILE does not exist" >&2
+  exit 1
+fi
+
+echo "Downloading tla2tools.jar"
+curl -LO tla.msr-inria.inria.fr/tlatoolbox/dist/tla2tools.jar
+cd "$1"
+java -cp ../tla2tools.jar tlc2.TLC "$TLA_FILE"