Skip to content

Commit

Permalink
Add pre-processing for realistic scenarios (#5825)
Browse files Browse the repository at this point in the history
  • Loading branch information
achamayou authored Nov 10, 2023
1 parent 8f6d14c commit 7230570
Show file tree
Hide file tree
Showing 19 changed files with 46 additions and 15 deletions.
24 changes: 12 additions & 12 deletions .azure-pipelines-templates/trace_validation.yml
Original file line number Diff line number Diff line change
Expand Up @@ -10,16 +10,16 @@ steps:
set -ex
cd tla/
parallel 'JSON={} ./tlc.sh consensus/Traceccfraft.tla' ::: \
../build/replicate.ndjson \
../build/election.ndjson \
../build/multi_election.ndjson \
../build/check_quorum.ndjson \
../build/reconnect.ndjson \
../build/reconnect_node.ndjson \
../build/bad_network.ndjson \
../build/fancy_election.1.ndjson \
../build/fancy_election.2.ndjson \
../build/suffix_collision.1.ndjson \
../build/suffix_collision.2.ndjson \
../build/suffix_collision.3.ndjson
../build/replicate_deprecated.ndjson \
../build/election_deprecated.ndjson \
../build/multi_election_deprecated.ndjson \
../build/check_quorum_deprecated.ndjson \
../build/reconnect_deprecated.ndjson \
../build/reconnect_node_deprecated.ndjson \
../build/bad_network_deprecated.ndjson \
../build/fancy_election.1_deprecated.ndjson \
../build/fancy_election.2_deprecated.ndjson \
../build/suffix_collision.1_deprecated.ndjson \
../build/suffix_collision.2_deprecated.ndjson \
../build/suffix_collision.3_deprecated.ndjson
displayName: "Run trace validation"
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
37 changes: 34 additions & 3 deletions tests/raft_scenarios_runner.py
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,12 @@
import argparse
import sys
import os
import json
from subprocess import Popen, PIPE
from raft_scenarios_gen import generate_scenarios
from contextlib import contextmanager
from collections import defaultdict
from heapq import merge


@contextmanager
Expand Down Expand Up @@ -33,15 +36,40 @@ def write_error_report(errors=None):
print("??? success \n")


def separate_log_lines(text):
def remove_reconfiguration_replicates(log):

This comment has been minimized.

Copy link
@lemmy

lemmy Dec 27, 2023

Contributor

Removing superfluous replicate and execute_append_entries_sync could be left to non-determinism with:

 IsChangeConfiguration ==
    \/ /\ \/ IsEvent("replicate")
          \/ IsEvent("execute_append_entries_sync")
       \* This lookahead is an optimization.  It only slashes runtime of suffix_collision.2 significantly.
       /\ logline'.msg.function = "add_configuration"
       /\ UNCHANGED vars
    \/ /\ IsEvent("add_configuration")
       /\ state[logline.msg.state.node_id] = Leader
       /\ LET i == logline.msg.state.node_id
             newConfiguration == DOMAIN logline.msg.new_configuration.nodes
          IN ChangeConfigurationInt(i, newConfiguration)
       /\ committableIndices[logline.msg.state.node_id] = Range(logline.msg.state.committable_indices)

This comment has been minimized.

Copy link
@achamayou

achamayou Jan 5, 2024

Author Member

Happy to discuss this more, but I would like to avoid non-determinism as much as possible, partly to keep the spec simple and partly to make debugging easier when we have mismatches.

log_by_node = defaultdict(list)
for line in log:
entry = json.loads(line)
node = entry["msg"]["state"]["node_id"]
if entry["msg"]["function"] == "add_configuration":
removed = log_by_node[node].pop()
assert removed["msg"]["function"] in (
"replicate",
"execute_append_entries_sync",
), removed
log_by_node[node].append(entry)
return [
json.dumps(e)
for e in merge(*log_by_node.values(), key=lambda e: int(e["h_ts"]))
]


def noop(log):
return log


def separate_log_lines(text, preprocess):
mermaid = []
log = []
for line in text.split(os.linesep):
if line.startswith("<RaftDriver>"):
mermaid.append(line[len("<RaftDriver>") :])
elif '"raft_trace"' in line:
log.append(line)
return (os.linesep.join(mermaid) + os.linesep, os.linesep.join(log) + os.linesep)
return (
os.linesep.join(mermaid) + os.linesep,
os.linesep.join(preprocess(log)) + os.linesep,
)


def expand_files(files):
Expand Down Expand Up @@ -94,7 +122,10 @@ def expand_files(files):
with block(ostream, "stderr", 3):
ostream.write(err.decode())

mermaid, log = separate_log_lines(out.decode())
mermaid, log = separate_log_lines(
out.decode(),
noop if "deprecated" in scenario else remove_reconfiguration_replicates,
)

with block(ostream, "diagram", 3, "mermaid", ["sequenceDiagram"]):
ostream.write(mermaid)
Expand Down

0 comments on commit 7230570

Please sign in to comment.