diff options
| author | A. Jesse Jiryu Davis <jesse@mongodb.com> | 2020-01-30 11:22:22 -0500 |
|---|---|---|
| committer | Evergreen Agent <no-reply@evergreen.mongodb.com> | 2020-01-30 18:38:40 +0000 |
| commit | 348880238de3229826053491b1163c88dc3a0575 (patch) | |
| tree | 0ee80a302363e70c411f215bd45dc4bf0b4b58da /src/mongo/db/repl/tla_plus | |
| parent | d422e688b9e4b7a933dcafdd779f8f957dc357ab (diff) | |
| download | mongo-348880238de3229826053491b1163c88dc3a0575.tar.gz | |
SERVER-45853 Enable RaftMongo.tla invariants
Also speed up model-checking for all Replication models, and remove an
obsolete comment in RaftMongo.tla.
Diffstat (limited to 'src/mongo/db/repl/tla_plus')
| -rw-r--r-- | src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg | 10 | ||||
| -rw-r--r-- | src/mongo/db/repl/tla_plus/RaftMongo/RaftMongo.tla | 8 | ||||
| -rwxr-xr-x | src/mongo/db/repl/tla_plus/model-check.sh | 3 |
3 files changed, 12 insertions, 9 deletions
diff --git a/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg b/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg index c94a84e89d9..3724efb7f0b 100644 --- a/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg +++ b/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg @@ -14,9 +14,17 @@ 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 +\* 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. +INVARIANT NeverRollbackCommitted +INVARIANT NeverRollbackBeforeCommitPoint + +PROPERTY CommitPointEventuallyPropagates + \* Not configurable. CONSTRAINT StateConstraint SPECIFICATION Spec diff --git a/src/mongo/db/repl/tla_plus/RaftMongo/RaftMongo.tla b/src/mongo/db/repl/tla_plus/RaftMongo/RaftMongo.tla index dbe71dbf738..06bc84baeea 100644 --- a/src/mongo/db/repl/tla_plus/RaftMongo/RaftMongo.tla +++ b/src/mongo/db/repl/tla_plus/RaftMongo/RaftMongo.tla @@ -30,7 +30,7 @@ VARIABLE committedEntries \* The server's term number. VARIABLE currentTerm -\* The server's state ("Follower", "Candidate", or "Leader"). +\* The server's state ("Follower" or "Leader"). VARIABLE state \* The commit point learned by each server. @@ -300,12 +300,6 @@ 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) diff --git a/src/mongo/db/repl/tla_plus/model-check.sh b/src/mongo/db/repl/tla_plus/model-check.sh index f89b5b9f4e1..718254c961a 100755 --- a/src/mongo/db/repl/tla_plus/model-check.sh +++ b/src/mongo/db/repl/tla_plus/model-check.sh @@ -22,4 +22,5 @@ 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" +# Note, cpuinfo is only available on Linux. +java -XX:+UseParallelGC -cp ../tla2tools.jar tlc2.TLC -workers $(grep -c processor /proc/cpuinfo) "$TLA_FILE" |