From 197f068093a64cce89d9d44a3f8d2295fdb6faa8 Mon Sep 17 00:00:00 2001 From: Rain Date: Mon, 26 Oct 2026 16:19:37 -0700 Subject: [PATCH 1/2] [trust-quorum] tla: download jar, add check.sh, and add a no-crash model exposing a model bug --- dev-tools/downloader/src/lib.rs | 32 ++++++ tools/tla2tools_checksums | 1 + tools/tla2tools_version | 1 + trust-quorum/tla/check.sh | 121 ++++++++++++++++++++++ trust-quorum/tla/trust_quorum.tla | 21 ++-- trust-quorum/tla/trust_quorum_nocrash.cfg | 35 +++++++ 6 files changed, 204 insertions(+), 7 deletions(-) create mode 100644 tools/tla2tools_checksums create mode 100644 tools/tla2tools_version create mode 100755 trust-quorum/tla/check.sh create mode 100644 trust-quorum/tla/trust_quorum_nocrash.cfg diff --git a/dev-tools/downloader/src/lib.rs b/dev-tools/downloader/src/lib.rs index 7e3dca4201a..4411248dee5 100644 --- a/dev-tools/downloader/src/lib.rs +++ b/dev-tools/downloader/src/lib.rs @@ -34,6 +34,8 @@ const BUILDOMAT_URL: &'static str = const CARGO_HACK_URL: &'static str = "https://github.com/taiki-e/cargo-hack/releases/download"; const MACOS_AARCH64_SERIES: &'static str = "macos-aarch64"; +const TLA2TOOLS_URL: &'static str = + "https://github.com/tlaplus/tlaplus/releases/download"; const RETRY_ATTEMPTS: usize = 3; @@ -78,6 +80,9 @@ enum Target { /// SoftNPU, an admin program (scadm) and a pre-compiled P4 program. Softnpu, + /// TLA+ tools jar (`tla2tools.jar`), used by `trust-quorum/tla/check.sh`. + Tla2tools, + /// Transceiver Control binary TransceiverControl, } @@ -145,6 +150,7 @@ pub async fn run_cmd(args: DownloadArgs) -> Result<()> { Target::MaghemiteMgd => downloader.download_maghemite_mgd().await, Target::MaghemiteDdmd => downloader.download_maghemite_ddmd().await, Target::Softnpu => downloader.download_softnpu().await, + Target::Tla2tools => downloader.download_tla2tools().await, Target::TransceiverControl => { downloader.download_transceiver_control().await } @@ -1046,6 +1052,32 @@ impl Downloader<'_> { Ok(()) } + async fn download_tla2tools(&self) -> Result<()> { + let download_dir = self.output_dir.join("downloads"); + let destination_dir = self.output_dir.join("tla2tools"); + + let checksums = + KvFile::read(self.versions_dir.join("tla2tools_checksums")).await?; + let checksum = checksums.get_sha256_value("CIDL_SHA256")?; + + let version = self.read_version_file("tla2tools_version").await?; + let jar_url = format!("{TLA2TOOLS_URL}/v{version}/tla2tools.jar"); + + tokio::fs::create_dir_all(&download_dir).await?; + tokio::fs::create_dir_all(&destination_dir).await?; + + let download_path = download_dir.join("tla2tools.jar"); + download_file_and_verify(&self.log, &download_path, &jar_url, checksum) + .await?; + + let dest = destination_dir.join("tla2tools.jar"); + tokio::fs::copy(&download_path, &dest).await.with_context(|| { + format!("Failed to copy {download_path} to {dest}") + })?; + + Ok(()) + } + async fn download_transceiver_control(&self) -> Result<()> { let destination_dir = self.output_dir.join("transceiver-control"); let download_dir = self.output_dir.join("downloads"); diff --git a/tools/tla2tools_checksums b/tools/tla2tools_checksums new file mode 100644 index 00000000000..1be7515ae9d --- /dev/null +++ b/tools/tla2tools_checksums @@ -0,0 +1 @@ +CIDL_SHA256="936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88" diff --git a/tools/tla2tools_version b/tools/tla2tools_version new file mode 100644 index 00000000000..10c088013f8 --- /dev/null +++ b/tools/tla2tools_version @@ -0,0 +1 @@ +1.7.4 diff --git a/trust-quorum/tla/check.sh b/trust-quorum/tla/check.sh new file mode 100755 index 00000000000..f6595791799 --- /dev/null +++ b/trust-quorum/tla/check.sh @@ -0,0 +1,121 @@ +#!/usr/bin/env bash +# TLA+ check script. +# +# This script runs all, or the defined, configurations through TLC, and compares +# TLC's exit status with the table below. +# +# The exit codes are: +# +# * 0: the properties are satisfied. +# * 12: safety violation. +# * 13: temporal/action violation. +# +# A non-zero entry indicates a configuration that is expected to fail. This +# could either be an expected failure (i.e., a precondition which we know does +# not satisfy the properties), or a current issue that a subsequent commit will +# fix. +set -euo pipefail + +cd "$(dirname "$0")" + +REPO_ROOT="$(cd ../.. && pwd)" +DEFAULT_JAR="$REPO_ROOT/out/tla2tools/tla2tools.jar" + +usage() { + cat </dev/null 2>&1; then + echo "error: java not found in PATH (TLC requires a Java runtime)" >&2 + exit 2 +fi + +TLA2TOOLS_JAR="${TLA2TOOLS_JAR:-$DEFAULT_JAR}" +if [[ ! -f "$TLA2TOOLS_JAR" ]]; then + echo "error: TLA+ tools jar not found at $TLA2TOOLS_JAR" >&2 + if [[ "$TLA2TOOLS_JAR" == "$DEFAULT_JAR" ]]; then + echo "To download it, run \`cargo xtask download tla2tools\` from $REPO_ROOT." >&2 + else + echo "Check TLA2TOOLS_JAR, or unset it to use $DEFAULT_JAR." >&2 + fi + exit 2 +fi +echo "tla2tools: $TLA2TOOLS_JAR" + +WORKERS="${TLC_WORKERS:-auto}" + +# cfg module expected-exit-status +EXPECTED=( + "trust_quorum.cfg trust_quorum 0" + "trust_quorum_nocrash.cfg trust_quorum 13" +) + +selected=("$@") +want() { + [[ ${#selected[@]} -eq 0 ]] && return 0 + local s + for s in "${selected[@]}"; do + [[ "$s" == "$1" ]] && return 0 + done + return 1 +} + +outdir="$(mktemp -d "${TMPDIR:-/tmp}/tlc-check.XXXXXX")" +echo "output: $outdir" + +failures=0 +ran=0 +for entry in "${EXPECTED[@]}"; do + read -r cfg module expected <<<"$entry" + want "$cfg" || continue + ran=$((ran + 1)) + name="${cfg%.cfg}" + log="$outdir/$name.log" + start=$SECONDS + set +e + java -XX:+UseParallelGC -cp "$TLA2TOOLS_JAR" tlc2.TLC \ + -workers "$WORKERS" \ + -metadir "$outdir/$name.states" \ + -config "$cfg" "$module.tla" >"$log" 2>&1 + actual=$? + set -e + elapsed=$((SECONDS - start)) + if [[ "$actual" == "$expected" ]]; then + status="ok" + else + status="FAIL" + failures=$((failures + 1)) + fi + printf '%-4s %-28s expected %-3s got %-3s %4ds %s\n' \ + "$status" "$cfg" "$expected" "$actual" "$elapsed" "$log" +done + +if [[ $ran -eq 0 ]]; then + echo "error: no cfg matched: ${selected[*]}" >&2 + exit 2 +fi + +if [[ $failures -ne 0 ]]; then + echo "$failures of $ran cfg(s) did not produce the expected exit status" >&2 + exit 1 +fi diff --git a/trust-quorum/tla/trust_quorum.tla b/trust-quorum/tla/trust_quorum.tla index 3f2a513c9f2..739aabcc355 100644 --- a/trust-quorum/tla/trust_quorum.tla +++ b/trust-quorum/tla/trust_quorum.tla @@ -23,7 +23,7 @@ the state space. *) -EXTENDS Integers, FiniteSets, TLC, TLCExt +EXTENDS Integers, FiniteSets, TLC CONSTANTS (* The set of trust quorum nodes *) @@ -249,7 +249,7 @@ Msgs == care which message they receive first, but whether they have received enough messages. In any case, even if there were a few concurrency bugs that could possibly be exposed via use of `\E \in msgs`, it would still be too expensive - to use. + to use. Therefore, we instead filter down the set of valid messages, and choose one one from the set. The `valid(_)` operator must ensure that the same message @@ -302,7 +302,7 @@ UpAndUnlocked(id) == \/ nodeOp[id] = "Idle" \/ nodeOp[id] = "CoordinatePrepare" \/ nodeOp[id] = "CoordinateCollectShares" - \/ nodeOp[id] = "ComputeShare" + \/ nodeOp[id] = "ComputeShare" ChooseCoordinator(members) == IF nexus.last_committed_config = NONE THEN @@ -411,7 +411,14 @@ CommittedNodesHaveShares == ----------------------------------------------------------------------------- (* Temporal properties *) -AllNodesUnlock == <>[](\A id \in nexus.config.members: nodeOp[id] # "Unlock") +AllNodesUnlock == <>[](\A id \in nexus.config.members: nodeOp[id] # "Unlock") + +\* This is currently expected to FAIL under trust_quorum_nocrash.cfg, because +\* RecvCommit never fires for the coordinator (it stays in CoordinatePrepare), +\* so NexusRecvCommitAck never reaches Idle and epoch 2 never starts. +\* trust_quorum.cfg only gets there because n1 is in CRASHSET and commits after +\* restarting. +ReconfigurationStarts == <>(nexus.config.epoch = 2) ----------------------------------------------------------------------------- (* The initial state predicate that sets the initial state of the system. *) @@ -664,7 +671,7 @@ RecvPrepare(id) == all the other nodes transiently reboot, we'd mask the retries that we get for free by keeping all the messages ever sent in `msgs`. - + This is one of the few places where explict retries would be handy, but the whole spec would have to change again to support that. *) @@ -774,7 +781,7 @@ RecvGetConfig(id) == /\ \/ nodes[m.from] = NONE \/ /\ nodes[m.from] # NONE /\ nodes[m.from].config.epoch # m.epoch - + m == Recv(valid) IN /\ m # NONE @@ -797,7 +804,7 @@ RecvGetShare(id) == \* Commit occurred, but this node hasn't learned of it yet. \* It must return the share so a crashed node that did learn \* can unlock. - \/ /\ m.epoch = nodes[id].config.epoch + \/ /\ m.epoch = nodes[id].config.epoch /\ m.from \in nodes[id].config.members m == Recv(valid) IN diff --git a/trust-quorum/tla/trust_quorum_nocrash.cfg b/trust-quorum/tla/trust_quorum_nocrash.cfg new file mode 100644 index 00000000000..7ecfc8f98c5 --- /dev/null +++ b/trust-quorum/tla/trust_quorum_nocrash.cfg @@ -0,0 +1,35 @@ +\* SPECIFICATION +\* Uncomment the previous line and provide the specification name if it's declared +\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION. + +CONSTANTS + NONE = NONE + n1 = n1 + n2 = n2 + n3 = n3 + n4 = n4 + n5 = n5 + NODES = {n1,n2,n3,n4,n5} + ALL_CONFIGS = AllConfigs + MAX_EPOCH = 3 + MAX_CRASHES_PER_NODE = 1 + MAX_NEXUS_CRASHES = 1 + CRASHSET = {} + +PROPERTY + AllNodesUnlock + ReconfigurationStarts + +SPECIFICATION FairSpec + + +INVARIANTS +TypeOK +NexusCoordinatorIsPartOfConfig +NodeConfigsMatchNexus +NodesThatHaveAckedCommitsHaveActuallyCommitted +LastCommittedConfigLessThanEqualConfig +CommittedNodesHaveShares + +CONSTRAINT +MaxEpochConstraint From 4fd8d81a1803f12c5ef2187299d01e7397cbde72 Mon Sep 17 00:00:00 2001 From: Rain Date: Tue, 27 Oct 2026 09:51:14 -0700 Subject: [PATCH 2/2] license header --- trust-quorum/tla/check.sh | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/trust-quorum/tla/check.sh b/trust-quorum/tla/check.sh index f6595791799..1f74d0ba5e7 100755 --- a/trust-quorum/tla/check.sh +++ b/trust-quorum/tla/check.sh @@ -1,4 +1,8 @@ #!/usr/bin/env bash +# This Source Code Form is subject to the terms of the Mozilla Public +# License, v. 2.0. If a copy of the MPL was not distributed with this +# file, You can obtain one at https://mozilla.org/MPL/2.0/. + # TLA+ check script. # # This script runs all, or the defined, configurations through TLC, and compares