"ran out of memory" checking spec with a large tuple #413
Comments
This comment has been minimized.
This comment has been minimized.
lemmy
added
bug
This comment has been minimized.
This comment has been minimized.
How long does it take TLC to parse the file (I killed it after ~5 minutes)? How many workers do you run the spec with? It is a long shot, but if more than one, please check with a single worker. Generally, the problems indicates that we want a special operator - such as |
|
@ajdavis How do you create To skip parsing - which will be difficult to optimize - the Python program could be rewritten to convert the execution log directly into TLC's IValue instances that can then be efficiently serialized and later read back into TLC during model checking. |
|
Thanks @lemmy. I'm not explicitly passing The I think these are all the data types I'm going to need. I don't think I'll need to nest any more deeply than this. You're correct, One idea is: break Trace.tla into chunks. Perhaps Trace1.tla has states 1-100 inclusive, Trace2.tla has states 100-200 inclusive, and so on. I can run TLC on each TraceN.tla file and check that all the state transitions in that file are allowed by RaftMongo.tla. Since each file's last state is equal to the next file's first state, I'll be confident that the entire sequence of all files is a valid trace according to RaftMongo.tla. |
|
@quaeler The bottleneck WRT parsing is: tlaplus/tlatools/src/pcal/Validator.java Line 88 in fa260e8 Ideas how to make this faster (especially for specs with no PlusCal)? |
|
The second bottleneck - affecting @ajdavis - is semantic processing of the parse tree: markus@avocado:~/src/TLA/models/tlcbugs/Github413$ jstack -l 24290
2020-01-05 22:40:29
Full thread dump OpenJDK 64-Bit Server VM (11.0.5+10-post-Ubuntu-0ubuntu1.118.04 mixed mode, sharing):
Threads class SMR info:
_java_thread_list=0x00007ffa900ad260, length=13, elements={
0x00007ffafc015000, 0x00007ffafc054800, 0x00007ffafc056800, 0x00007ffafc05d800,
0x00007ffafc05f800, 0x00007ffafc061800, 0x00007ffafc063800, 0x00007ffafc0ab000,
0x00007ffafc169800, 0x00007ffafc1ad000, 0x00007ffaa0001800, 0x00007ffafc1b8000,
0x00007ffabc001000
}
"main" #1 prio=5 os_prio=0 cpu=19863,08ms elapsed=406,89s tid=0x00007ffafc015000 nid=0x5ee7 runnable [0x00007ffb0335b000]
java.lang.Thread.State: RUNNABLE
at java.util.HashSet.<init>(java.base@11.0.5/HashSet.java:106)
at tla2sany.semantic.LevelNode.<init>(LevelNode.java:70)
at tla2sany.semantic.ExprOrOpArgNode.<init>(ExprOrOpArgNode.java:22)
at tla2sany.semantic.ExprNode.<init>(ExprNode.java:77)
at tla2sany.semantic.OpApplNode.<init>(OpApplNode.java:171)
at tla2sany.semantic.Generator.processRcdForms(Generator.java:3837)
at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:3194)
at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:3035)
at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:3035)
at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:3035)
at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:3035)
at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
at tla2sany.semantic.Generator.processOperator(Generator.java:2436)
at tla2sany.semantic.Generator.generateModule(Generator.java:2032)
at tla2sany.semantic.Generator.generate(Generator.java:1973)
at tla2sany.drivers.SANY.frontEndSemanticAnalysis(SANY.java:301)
at tla2sany.drivers.SANY.frontEndMain(SANY.java:130)
at tlc2.tool.impl.SpecProcessor.processSpec(SpecProcessor.java:318)
at tlc2.tool.impl.SpecProcessor.<init>(SpecProcessor.java:157)
at tlc2.tool.impl.Spec.<init>(Spec.java:121)
at tlc2.tool.impl.Tool.<init>(Tool.java:126)
at tlc2.tool.impl.Tool.<init>(Tool.java:121)
at tlc2.tool.impl.Tool.<init>(Tool.java:116)
at tlc2.TLC.process(TLC.java:930)
at tlc2.TLC.main(TLC.java:247)
Locked ownable synchronizers:
- None
...markus@avocado:~/src/TLA/models/tlcbugs/Github413$ jstack -l 24290
2020-01-05 22:41:45
Full thread dump OpenJDK 64-Bit Server VM (11.0.5+10-post-Ubuntu-0ubuntu1.118.04 mixed mode, sharing):
Threads class SMR info:
_java_thread_list=0x00007ffa900ad260, length=13, elements={
0x00007ffafc015000, 0x00007ffafc054800, 0x00007ffafc056800, 0x00007ffafc05d800,
0x00007ffafc05f800, 0x00007ffafc061800, 0x00007ffafc063800, 0x00007ffafc0ab000,
0x00007ffafc169800, 0x00007ffafc1ad000, 0x00007ffaa0001800, 0x00007ffafc1b8000,
0x00007ffabc001000
}
"main" #1 prio=5 os_prio=0 cpu=19863,92ms elapsed=483,49s tid=0x00007ffafc015000 nid=0x5ee7 runnable [0x00007ffb0335b000]
java.lang.Thread.State: RUNNABLE
at tla2sany.semantic.LevelNode.<init>(LevelNode.java:85)
at tla2sany.semantic.ExprOrOpArgNode.<init>(ExprOrOpArgNode.java:22)
at tla2sany.semantic.ExprNode.<init>(ExprNode.java:77)
at tla2sany.semantic.NumeralNode.<init>(NumeralNode.java:43)
at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:2838)
at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
at tla2sany.semantic.Generator.processRcdForms(Generator.java:3830)
at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:3194)
at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:3035)
at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:3035)
at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:3035)
at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
at tla2sany.semantic.Generator.generateExpressionOrLAP(Generator.java:3035)
at tla2sany.semantic.Generator.generateExpression(Generator.java:2816)
at tla2sany.semantic.Generator.processOperator(Generator.java:2436)
at tla2sany.semantic.Generator.generateModule(Generator.java:2032)
at tla2sany.semantic.Generator.generate(Generator.java:1973)
at tla2sany.drivers.SANY.frontEndSemanticAnalysis(SANY.java:301)
at tla2sany.drivers.SANY.frontEndMain(SANY.java:130)
at tlc2.tool.impl.SpecProcessor.processSpec(SpecProcessor.java:318)
at tlc2.tool.impl.SpecProcessor.<init>(SpecProcessor.java:157)
at tlc2.tool.impl.Spec.<init>(Spec.java:121)
at tlc2.tool.impl.Tool.<init>(Tool.java:126)
at tlc2.tool.impl.Tool.<init>(Tool.java:121)
at tlc2.tool.impl.Tool.<init>(Tool.java:116)
at tlc2.TLC.process(TLC.java:930)
at tlc2.TLC.main(TLC.java:247)
Locked ownable synchronizers:
- None
|
|
@ajdavis Can you share the original execution log? |
|
Sure, I've added three log files to the Dropbox folder. They were written by three MongoDB server processes acting as a replica set (also known as a "Raft group"): https://www.dropbox.com/sh/nq1guc0nqv940ns/AAC1031rhi5sxCziig4rUSOFa?dl=0 My Python script merges these three server process's logs (sorting by timestamp), reads JSON representations of the states, and writes Trace.tla. Earlier I made a mistake and duplicated one of the logs; now that I've removed the duplicate, Trace.tla is only 97MB, not 130MB. I've updated the Trace.tla in the Dropbox folder. Model-checking now completes in a couple minutes! I haven't investigated why, I'm surprised that fixing my mistake and reducing the size of Trace.tla by a moderate amount has had such a large effect. |
|
I hacked a TLC module override for your trace file that parse the trace into memory relying on the schema outlined above: /*******************************************************************************
* Copyright (c) 2020 Microsoft Research. All rights reserved.
*
* The MIT License (MIT)
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
* in the Software without restriction, including without limitation the rights
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
* of the Software, and to permit persons to whom the Software is furnished to do
* so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
* AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
* WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*
* Contributors:
* Markus Alexander Kuppe - initial API and implementation
******************************************************************************/
package tlc2.overrides;
import java.io.IOException;
import java.nio.file.Files;
import java.nio.file.Paths;
import java.util.ArrayList;
import java.util.List;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
import tlc2.value.IValue;
import tlc2.value.impl.IntValue;
import tlc2.value.impl.RecordValue;
import tlc2.value.impl.StringValue;
import tlc2.value.impl.TupleValue;
import tlc2.value.impl.Value;
import util.UniqueString;
public class IOUtils {
private static List<String> allLines;
static {
try {
allLines = Files.readAllLines(Paths.get("Trace.txt"));
} catch (IOException e) {
e.printStackTrace();
}
}
@TLAPlusOperator(identifier = "Trace", module = "Trace")
public static final IValue readline(final IntValue idx) throws IOException {
String line = allLines.get(idx.val - 1);
// final String bak = new String(line.substring(0, line.length() - 1));
final Value[] values = new Value[6];
// Skip first tuple marker.
line = line.substring(2);
// field 0:
values[0] = IntValue.gen(Integer.parseInt(line.substring(0, 1)));
line = line.substring(3);
// field 1:
int indexOf = line.indexOf('"');
values[1] = new StringValue(line.substring(0, indexOf));
line = line.substring(indexOf + 2);
// field 2: find end of first triple.
indexOf = line.indexOf(">>>>");
String triple = line.substring(2, indexOf + 2);
line = line.substring(indexOf + 5);
Matcher matcher = f2.matcher(triple);
matcher.find();
Value[] triplet = new Value[3];
triplet[0] = tupleToRecordsWrap(matcher.group(1));
triplet[1] = tupleToRecordsWrap(matcher.group(2));
triplet[2] = tupleToRecordsWrap(matcher.group(3));
values[2] = new TupleValue(triplet);
// field 3: <<"Leader","Follower","Follower">>,
indexOf = line.indexOf(">>");
String substring = line.substring(2, indexOf);
line = line.substring(indexOf + 3);
String[] split2 = substring.split(",");
Value[] stngs = new Value[3];
for (int i = 0; i < split2.length; i++) {
stngs[i] = new StringValue(split2[i].replace("\"", ""));
}
values[3] = new TupleValue(stngs);
// field 4:
indexOf = line.indexOf(">>");
values[4] = tupleToRecords(line.substring(0, indexOf + 2));
line = line.substring(indexOf + 3);
// field 5:
indexOf = line.lastIndexOf('"');
values[5] = new StringValue(line.substring(1, indexOf));
TupleValue tupleValue = new TupleValue(values);
// String replaceAll = tupleValue.toString().replaceAll("\\s", "");
// assert replaceAll.equals(bak.replaceAll("\\s", ""));
return tupleValue;
}
private static final Pattern f2 = Pattern.compile("<<(.*?)>>,<<(.*?)>>,<<(.*?)>>");
private static final Pattern pattern = Pattern.compile("(\\[.*?\\])");
private static Value tupleToRecordsWrap(String tuple) {
return tupleToRecords("<<"+tuple+">>");
}
private static Value tupleToRecords(String tuple) {
if ("<<>>".equals(tuple))
return TupleValue.EmptyTuple;
String rcds = tuple.substring(2, tuple.length() - 2);
List<Value> v = new ArrayList<>();
Matcher matcher = pattern.matcher(rcds);
while (matcher.find()) {
String group = matcher.group();
v.add(toRecord(group));
}
return new TupleValue(v.toArray(new Value[v.size()]));
}
private static Value toRecord(String rcd) {
rcd = rcd.substring(1, rcd.length() - 1);
String[] split = rcd.split(",");
UniqueString[] keys = new UniqueString[split.length];
Value[] vals = new Value[split.length];
for (int i = 0; i < split.length; i++) {
String[] kv = split[i].trim().split(" \\|-> ");
keys[i] = UniqueString.uniqueStringOf(kv[0]);
vals[i] = IntValue.gen(Integer.parseInt(kv[1]));
}
return new RecordValue(keys, vals, false);
}
}with --------------------------------- MODULE Trace ---------------------------------
EXTENDS Integers, Sequences
\* Generated by repl-trace-checker.py 2020-01-05 09:49:06.209179 local time.
\* This execution trace was generated from an actual replica set's log files.
\* Each tuple is <<globalCurrentTerm, action, log, state, commitPoint, serverLogLocation>>
TraceLen == 72
Trace(idx) == TRUE
\* Adapted from Pressler 2018, including Pressler's comments.
VARIABLES globalCurrentTerm, log, state, commitPoint
Model == INSTANCE RaftMongo WITH
MaxClientWriteSize <- 11,
Server <- {1, 2, 3}
vars == <<globalCurrentTerm, log, state, commitPoint>>
VARIABLE i \* the trace index
\* "Reading" a record is just vars = Trace(i), but unfortunately TLC isn’t happy
\* with that, so:
Read == LET Rec == Trace(i)
IN
/\ globalCurrentTerm = Rec[1]
/\ log = Rec[3]
/\ state = Rec[4]
/\ commitPoint = Rec[5]
\* Unfortunately, TLC also isn’t happy with just Read' – which is equivalent to:
ReadNext == LET Rec == Trace(i')
IN
/\ globalCurrentTerm' = Rec[1]
/\ log' = Rec[3]
/\ state' = Rec[4]
/\ commitPoint' = Rec[5]
Init == i = 1 /\ Read
Next == \/ i < TraceLen /\ i' = i + 1 /\ ReadNext
\/ UNCHANGED <<i, vars>> \* So that we don’t get a deadlock error in TLC
TraceBehavior == Init /\ [][Next]_<<vars, i>>
\* Because we’re dealing with a finite trace, we only care about safety
\* properties, as liveness concerns only infinite behaviors.
THEOREM TraceBehavior => Model!SpecBehavior
\* To verify, we check the spec TraceBehavior in TLC , with Model!SpecBehavior
\* as a temporal property. As we’re always wary of success, we modify the above
\* trace to ensure that TLC finds an error.
\* Added by A. Jesse Jiryu Davis, for command-line model checking with TLC:
SpecBehavior == Model!SpecBehavior
===============================================================================and <<0,"Init",<<<<>>,<<>>,<<>>>>,<<"Follower","Follower","Follower">>,<<[term |-> 0, index |-> 0],[term |-> 0, index |-> 0],[term |-> 0, index |-> 0]>>,"">>,
<<1,"BecomePrimaryByMagic",<<<<>>,<<>>,<<>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 0, index |-> 0],[term |-> 0, index |-> 0],[term |-> 0, index |-> 0]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:412">>,
<<1,"ClientWrite",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<>>,<<>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 0, index |-> 0],[term |-> 0, index |-> 0],[term |-> 0, index |-> 0]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:426">>,
<<1,"AdvanceCommitPoint",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<>>,<<>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 4],[term |-> 0, index |-> 0],[term |-> 0, index |-> 0]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:459">>,
<<1,"ClientWrite",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<>>,<<>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 4],[term |-> 0, index |-> 0],[term |-> 0, index |-> 0]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:461">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 4],[term |-> 1, index |-> 4],[term |-> 0, index |-> 0]>>,"/home/emptysquare/RollbackFuzzer/mongod.log:455">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 4],[term |-> 1, index |-> 4],[term |-> 1, index |-> 4]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:455">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 4],[term |-> 1, index |-> 4],[term |-> 1, index |-> 4]>>,"/home/emptysquare/RollbackFuzzer/mongod2.log:455">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 4],[term |-> 1, index |-> 4],[term |-> 1, index |-> 4]>>,"/home/emptysquare/RollbackFuzzer/mongod.log:456">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 4],[term |-> 1, index |-> 4],[term |-> 1, index |-> 4]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:456">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 4],[term |-> 1, index |-> 4],[term |-> 1, index |-> 4]>>,"/home/emptysquare/RollbackFuzzer/mongod2.log:456">>,
<<1,"ClientWrite",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 4],[term |-> 1, index |-> 4],[term |-> 1, index |-> 4]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:473">>,
<<1,"AdvanceCommitPoint",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 5],[term |-> 1, index |-> 4],[term |-> 1, index |-> 4]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:475">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 5],[term |-> 1, index |-> 4],[term |-> 1, index |-> 5]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:457">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 5],[term |-> 1, index |-> 5],[term |-> 1, index |-> 5]>>,"/home/emptysquare/RollbackFuzzer/mongod.log:457">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 5],[term |-> 1, index |-> 5],[term |-> 1, index |-> 5]>>,"/home/emptysquare/RollbackFuzzer/mongod2.log:457">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 5],[term |-> 1, index |-> 5],[term |-> 1, index |-> 5]>>,"/home/emptysquare/RollbackFuzzer/mongod.log:458">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 5],[term |-> 1, index |-> 5],[term |-> 1, index |-> 5]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:458">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 5],[term |-> 1, index |-> 5],[term |-> 1, index |-> 5]>>,"/home/emptysquare/RollbackFuzzer/mongod2.log:458">>,
<<1,"AdvanceCommitPoint",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 6],[term |-> 1, index |-> 5],[term |-> 1, index |-> 5]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:476">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 6],[term |-> 1, index |-> 5],[term |-> 1, index |-> 6]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:459">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 6],[term |-> 1, index |-> 6],[term |-> 1, index |-> 6]>>,"/home/emptysquare/RollbackFuzzer/mongod.log:459">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 6],[term |-> 1, index |-> 6],[term |-> 1, index |-> 6]>>,"/home/emptysquare/RollbackFuzzer/mongod2.log:459">>,
<<1,"ClientWrite",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 6],[term |-> 1, index |-> 6],[term |-> 1, index |-> 6]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:537">>,
<<1,"ClientWrite",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 6],[term |-> 1, index |-> 6],[term |-> 1, index |-> 6]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:538">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 6],[term |-> 1, index |-> 6],[term |-> 1, index |-> 6]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:514">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 6],[term |-> 1, index |-> 6],[term |-> 1, index |-> 6]>>,"/home/emptysquare/RollbackFuzzer/mongod.log:514">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 6],[term |-> 1, index |-> 6],[term |-> 1, index |-> 6]>>,"/home/emptysquare/RollbackFuzzer/mongod2.log:514">>,
<<1,"AdvanceCommitPoint",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 7],[term |-> 1, index |-> 6],[term |-> 1, index |-> 6]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:539">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 7],[term |-> 1, index |-> 6],[term |-> 1, index |-> 6]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:516">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 7],[term |-> 1, index |-> 7],[term |-> 1, index |-> 6]>>,"/home/emptysquare/RollbackFuzzer/mongod.log:516">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 7],[term |-> 1, index |-> 7],[term |-> 1, index |-> 6]>>,"/home/emptysquare/RollbackFuzzer/mongod2.log:516">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 7],[term |-> 1, index |-> 7],[term |-> 1, index |-> 7]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:517">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 7],[term |-> 1, index |-> 7],[term |-> 1, index |-> 7]>>,"/home/emptysquare/RollbackFuzzer/mongod.log:517">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 7],[term |-> 1, index |-> 7],[term |-> 1, index |-> 7]>>,"/home/emptysquare/RollbackFuzzer/mongod2.log:517">>,
<<1,"AdvanceCommitPoint",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 8],[term |-> 1, index |-> 7],[term |-> 1, index |-> 7]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:540">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 8],[term |-> 1, index |-> 8],[term |-> 1, index |-> 7]>>,"/home/emptysquare/RollbackFuzzer/mongod.log:518">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 8],[term |-> 1, index |-> 8],[term |-> 1, index |-> 8]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:518">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 8],[term |-> 1, index |-> 8],[term |-> 1, index |-> 8]>>,"/home/emptysquare/RollbackFuzzer/mongod2.log:518">>,
<<1,"ClientWrite",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 8],[term |-> 1, index |-> 8],[term |-> 1, index |-> 8]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:581">>,
<<1,"ClientWrite",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 8],[term |-> 1, index |-> 8],[term |-> 1, index |-> 8]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:582">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 8],[term |-> 1, index |-> 8],[term |-> 1, index |-> 8]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:557">>,
<<1,"AdvanceCommitPoint",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 9],[term |-> 1, index |-> 8],[term |-> 1, index |-> 8]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:584">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 9],[term |-> 1, index |-> 8],[term |-> 1, index |-> 9]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:559">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 9],[term |-> 1, index |-> 8],[term |-> 1, index |-> 9]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:560">>,
<<1,"ClientWrite",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 9],[term |-> 1, index |-> 8],[term |-> 1, index |-> 9]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:586">>,
<<1,"AdvanceCommitPoint",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 10],[term |-> 1, index |-> 8],[term |-> 1, index |-> 9]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:587">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 10],[term |-> 1, index |-> 8],[term |-> 1, index |-> 10]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:561">>,
<<1,"AppendOplog",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 10],[term |-> 1, index |-> 8],[term |-> 1, index |-> 10]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:564">>,
<<1,"AdvanceCommitPoint",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 11],[term |-> 1, index |-> 8],[term |-> 1, index |-> 10]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:592">>,
<<1,"LearnCommitPointFromSyncSourceNeverBeyondLastApplied",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 11],[term |-> 1, index |-> 8],[term |-> 1, index |-> 11]>>,"/home/emptysquare/RollbackFuzzer/mongod1.log:565">>,
<<1,"ClientWrite",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 11],[term |-> 1, index |-> 8],[term |-> 1, index |-> 11]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:596">>,
<<1,"ClientWrite",<<<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>,<<[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1],[term |-> 1]>>>>,<<"Leader","Follower","Follower">>,<<[term |-> 1, index |-> 11],[term |-> 1, index |-> 8],[term |-> 1, index |-> 11]>>,"/home/emptysquare/RollbackFuzzer/mongod0.log:602">>,
...You can download a custom TLC build at https://tla.msr-inria.inria.fr/kuppe/tla2tools-gh413.jar. TLC finds a violation for a state for which I don't have the time to check if it is due to a parsing bug: Generally, this is upside-down. Instead of parsing the output of your Python script, a Java program should parse your exec log into Value instances directly. |
|
That spec violation is expected - fixing that is my next hurdle. Therefore, seeing that spec violation shows that your code is working correctly, thank you! |
|
For the complete log of 6351 lines, TLC takes ~20secs to read Trace.txt and model check it. |
lemmy
added a commit
that referenced
this issue
Jan 6, 2020
Came up in the context of #413 (comment) [Bug][TLC]
|
This is excellent, I really appreciate it. If I wanted to continue development, what would be a less hacky way to proceed? Create a custom module like one of these?: https://github.com/tlaplus/CommunityModules/tree/master/modules/tlc2/overrides Could I use this technique with a standard tla2tools.jar? |
Trace.tla (Note IOUtils module and IODeserialize operator)--------------------------------- MODULE Trace ---------------------------------
EXTENDS Integers, Sequences, IOUtils
\* Generated by repl-trace-checker.py 2020-01-05 09:49:06.209179 local time.
\* This execution trace was generated from an actual replica set's log files.
\* Each tuple is <<globalCurrentTerm, action, log, state, commitPoint, serverLogLocation>>
Trace == IODeserialize("Trace.bin", TRUE)
\* Adapted from Pressler 2018, including Pressler's comments.
VARIABLES globalCurrentTerm, log, state, commitPoint
Model == INSTANCE RaftMongo WITH
MaxClientWriteSize <- 11,
Server <- {1, 2, 3}
vars == <<globalCurrentTerm, log, state, commitPoint>>
VARIABLE i \* the trace index
\* "Reading" a record is just vars = Trace(i), but unfortunately TLC isn’t happy
\* with that, so:
Read == LET Rec == Trace[i]
IN
/\ globalCurrentTerm = Rec[1]
/\ log = Rec[3]
/\ state = Rec[4]
/\ commitPoint = Rec[5]
\* Unfortunately, TLC also isn’t happy with just Read' – which is equivalent to:
ReadNext == LET Rec == Trace[i']
IN
/\ globalCurrentTerm' = Rec[1]
/\ log' = Rec[3]
/\ state' = Rec[4]
/\ commitPoint' = Rec[5]
Init == i = 1 /\ Read
Next == \/ i < Len(Trace) /\ i' = i + 1 /\ ReadNext
\/ UNCHANGED <<i, vars>> \* So that we don’t get a deadlock error in TLC
TraceBehavior == Init /\ [][Next]_<<vars, i>>
\* Because we’re dealing with a finite trace, we only care about safety
\* properties, as liveness concerns only infinite behaviors.
THEOREM TraceBehavior => Model!SpecBehavior
\* To verify, we check the spec TraceBehavior in TLC , with Model!SpecBehavior
\* as a temporal property. As we’re always wary of success, we modify the above
\* trace to ensure that TLC finds an error.
\* Added by A. Jesse Jiryu Davis, for command-line model checking with TLC:
SpecBehavior == Model!SpecBehavior
===============================================================================Trace.txtJars:
Parse Trace.txt into TLA+ values (Trace.bin)markus@avocado:~/src/TLA/models/tlcbugs/Github413$ java -cp tla2tools.jar:mongo2tla.jar tlc2.contrib.MongoToTLA Trace.txt Trace.bin
Parsing 6351 lines in Trace.txt to Trace.bin.
Successfully parsed Trace.txt to Trace.bin.
markus@avocado:~/src/TLA/models/tlcbugs/Github413$ ls -lah Trace.bin
-rw-r--r-- 1 markus markus 1,1M Jan 6 20:47 Trace.binCheck trace with TLCmarkus@avocado:~/src/TLA/models/tlcbugs/Github413$ java -cp CommunityModules-202001070430.jar:tla2tools.jar tlc2.TLC Trace
TLC2 Version 2.15 of Day Month 20?? (rev: e6ec62b)
Warning: Please run the Java VM which executes TLC with a throughput optimized garbage collector by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 64 and seed 7241795494624237021 with 1 worker on 4 cores with 5964MB heap and 64MB offheap memory [pid: 15787] (Linux 4.18.0-16-generic amd64, Private Build 11.0.5 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/markus/src/TLA/_specs/models/tlcbugs/Github413/Trace.tla.plain
Parsing file /tmp/Integers.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/IOUtils.tla
Parsing file /tmp/Naturals.tla
Parsing file /home/markus/src/TLA/_specs/models/tlcbugs/Github413/RaftMongo.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/TLC.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module IOUtils
Semantic processing of module RaftMongo
Semantic processing of module Trace
Starting... (2020-01-06 20:49:39)
Failed to match TLCExt!AssertError operator override from jar:file:/home/markus/src/TLA/_specs/models/tlcbugs/Github413/CommunityModules-202001070430.jar!/tlc2/overrides/TLCExt.class with signature: <Java Method: public static synchronized tlc2.value.impl.Value tlc2.overrides.TLCExt.assertError(tlc2.tool.impl.Tool,tla2sany.semantic.ExprOrOpArgNode[],tlc2.util.Context,tlc2.tool.TLCState,tlc2.tool.TLCState,int,tlc2.tool.coverage.CostModel)> (no such module).
Failed to match TLCExt!PickSuccessor operator override from jar:file:/home/markus/src/TLA/_specs/models/tlcbugs/Github413/CommunityModules-202001070430.jar!/tlc2/overrides/TLCExt.class with signature: <Java Method: public static synchronized tlc2.value.impl.Value tlc2.overrides.TLCExt.pickSuccessor(tlc2.tool.impl.Tool,tla2sany.semantic.ExprOrOpArgNode[],tlc2.util.Context,tlc2.tool.TLCState,tlc2.tool.TLCState,int,tlc2.tool.coverage.CostModel)> (no such module).
Loading IODeserialize operator override from tlc2.overrides.IOUtils with signature: <Java Method: public static final tlc2.value.IValue tlc2.overrides.IOUtils.deserialize(tlc2.value.impl.StringValue,tlc2.value.impl.BoolValue) throws java.io.IOException>.
Loading IOSerialize operator override from tlc2.overrides.IOUtils with signature: <Java Method: public static final tlc2.value.IValue tlc2.overrides.IOUtils.serialize(tlc2.value.IValue,tlc2.value.impl.StringValue,tlc2.value.impl.BoolValue) throws java.io.IOException>.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2020-01-06 20:49:42.
Error: Action property line 268, col 25 to line 268, col 37 of module RaftMongo is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ globalCurrentTerm = 0
/\ log = <<<<>>, <<>>, <<>>>>
/\ i = 1
/\ state = <<"Follower", "Follower", "Follower">>
/\ commitPoint = << [index |-> 0, term |-> 0],
[index |-> 0, term |-> 0],
[index |-> 0, term |-> 0] >>
State 2: <Next line 39, col 12 to line 39, col 51 of module Trace>
/\ globalCurrentTerm = 1
/\ log = <<<<>>, <<>>, <<>>>>
/\ i = 2
/\ state = <<"Leader", "Follower", "Follower">>
/\ commitPoint = << [index |-> 0, term |-> 0],
[index |-> 0, term |-> 0],
[index |-> 0, term |-> 0] >>
State 3: <Next line 39, col 12 to line 39, col 51 of module Trace>
/\ globalCurrentTerm = 1
/\ log = <<<<[term |-> 1], [term |-> 1], [term |-> 1], [term |-> 1]>>, <<>>, <<>>>>
/\ i = 3
/\ state = <<"Leader", "Follower", "Follower">>
/\ commitPoint = << [index |-> 0, term |-> 0],
[index |-> 0, term |-> 0],
[index |-> 0, term |-> 0] >>
State 4: <Next line 39, col 12 to line 39, col 51 of module Trace>
/\ globalCurrentTerm = 1
/\ log = <<<<[term |-> 1], [term |-> 1], [term |-> 1], [term |-> 1]>>, <<>>, <<>>>>
/\ i = 4
/\ state = <<"Leader", "Follower", "Follower">>
/\ commitPoint = << [index |-> 4, term |-> 1],
[index |-> 0, term |-> 0],
[index |-> 0, term |-> 0] >>
6 states generated, 4 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 4.
The average outdegree of the complete state graph is 1 (minimum is 1, the maximum 1 and the 95th percentile is 1).
Finished in 03s at (2020-01-06 20:49:42)Note that the Mongo2TLA hack should eventually be simplified into/merged with your Python script, i.e. a JSon2TLA script. |
|
@ajdavis When you merge the log files based on the timestamps, do you just assume perfectly synchronized clocks? Why don't you use logical clocks? Also, has logging been built into your app just to validate traces or was it already available? What I'm getting at is, how to design a TLA+ specific logging API that is linked to the actual implementation and that creates the Trace.out file. Another variant of this logging API could even validate impl traces on-line by (asynchronously) sending each new log statement to a running TLC. Provided its overhead is negligible, this could then run as a monitor in production. The tricky part is to make this logging API convenient to use. |
|
We run our test servers as processes on a single machine so that they have access to a synchronized clock. To ensure that causally-related events have properly ordered timestamps, our test servers pause 1ms before logging each event. Obviously, our approach wouldn't be appropriate for trace checking in production. We considered logical clocks, but the solution we chose is much simpler. MongoDB has a typical logging framework for a database server; we added some custom code for TLA+ trace logging. It's an interesting idea to directly write the Trace.out file from MongoDB's C++ code instead of post-processing MongoDB logs with Python to produce the trace. There would still need to be a step at some point in the pipeline for merging event streams from multiple processes. |
|
Cannot one of your MongoDBs be the sink for the event stream that merges the log data, followed by writing Trace.out? At any rate, an offline API seems better suited for trace validation of single process apps. In the on-line case on the other hand, TLC could directly act as the sink for all MongoDBs. |
|
Thanks for your advice, and thanks especially for providing us with TLC optimizations and a module for speeding up trace checking! We've concluded our research for now. Unfortunately, we've concluded that model-based trace-checking is more effort than it's worth for our particular scenario. TLC has the features we need, thanks to you. But getting our TLA+ specification to match the output of MongoDB's trace logging is too much trouble. We'll be analyzing our results and publishing later this year, stay tuned. |
|
I have another question, however, if you're willing to answer it. I want to measure how much RaftMongo.tla coverage this trace achieved. When I follow your instructions and include I do not see any lines in RaftMongo.tla covered, only the Trace module, which imports RaftMongo. Is there a way to measure the coverage within RaftMongo.tla? Thanks! |
|
Try this build: https://tla.msr-inria.inria.fr/kuppe/tla2tools-413.jar |
|
Terrific! Now I see coverage lines logged on the imported module, RaftMongo.tla. Since this requires a newer tla2tools.jar than what we have bundled in the TLA+ Toolbox, must I rebuild the Toolbox in order to see this coverage visualized in the Toolbox? Or is there a way to import coverage into the Toolbox? (I see we can't yet use a custom tla2tools.jar with the Toolbox #406). |
lemmy
added a commit
that referenced
this issue
Jan 23, 2020
implied actions (INSTANCE). Activate with "-Dtlc2.tool.coverage.CostModelCreator.implied=true" JVM property when running TLC. In the Toolbox, go to the TLC Options page of the Model and paste the property into the JVM arguments box. Seehttps://github.com//issues/413#issuecomment-577304602 for background. [Feature][TLC]
|
https://nightly.tlapl.us/products/ will soon (~1h) have a build with change.
|
|
Thanks for the video, this is super-helpful. I've just downloaded the latest TLA+ Toolbox and I seem to have a different bundled version of the tools than you, commit hash 6232c31 rather than your f30148c. My coverage output still doesn't include RaftMongo.tla. Here's my TLC console output:
|
|
Works here (see below). Might it be possible that you missed to set |
|
I misspelled it |
|
FWIW: Trace validation applied to a concurrent (Java) app: https://github.com/lemmy/BlockingQueue#v16-traces-print-partial-implementation-executions |
|
That's a spectacularly useful tutorial, especially with the addition of trace-checking! |
quaeler
added a commit
that referenced
this issue
Jan 29, 2020
. Minor improvements on the Validator performance for the usecase of specs with verbosity prefixing the module . Performance unit test . Comments on where further efforts could be made. [Feature][Tools]
|
Hey @ajdavis it looks like the dropbox links are dead, is it possible for you to repost the specs somehow? Would like to see how the tree-sitter grammar fares on them. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hello, I'm continuing development of my trace-checker. (We began discussion in #367, I'm following Ron Pressler's method from "Verifying Software Traces Against a Formal Specification
with TLA+ and TLC".)
Currently, I have a Python script that parses a MongoDB log file and generates a TLA+ spec with a tuple of 6532 states. Each state is a tuple of variable values. Some of these values are large, including tuples up to 1014 elements long. The whole spec is 130MB of TLA+.
Here is the spec and config file.
TLC can parse this file, although it takes some time. The problem is this: TLC runs out of memory during model-checking. This surprises me, because there are only 6532 states. I increased the heap size to nearly the size of my physical RAM with
-Xmx60g. That didn't prevent the crash, it only delayed it.Is there a way to diagnose why TLC needs so much memory, so I can determine a solution to the problem? Do you think I should use a different data structure rather than a tuple of tuples?
The text was updated successfully, but these errors were encountered: