JS-SAM: cross-platform sandbox, Opus 4.8, and real Phase-3 spin traces

config/models.yaml

@@ -26,13 +26,14 @@ models:
   # Anthropic Claude
   claude:
     provider: "anthropic"
-    model_name: "claude-sonnet-4-20250514"
+    # Sonnet 4 (claude-sonnet-4-20250514) retired 2026-06-15; switched to the
+    # current Opus tier on 2026-06-30. Opus 4.8 removes the sampling params:
+    # temperature/top_p/top_k now return a 400, so they are intentionally absent.
+    model_name: "claude-opus-4-8"
     api_key_env: "ANTHROPIC_API_KEY"
-    temperature: 0.1
-    # claude-sonnet-4 rejects max_tokens > 64000 (API: "maximum allowed
-    # number of output tokens for claude-sonnet-4-20250514"); probed 2026-06-09.
+    # Opus 4.8 supports up to 128000 output tokens; kept at 64000 to match the
+    # prior run's cap and stay within non-streaming timeout limits.
     max_tokens: 64000
-    top_p: 0.9
 
   deepseek_tencent:
     provider: "deepseek"

data/patches/spin_2thread_ktest.patch

@@ -0,0 +1,46 @@
+--- a/ostd/src/sync/spin_trace_tests.rs
++++ b/ostd/src/sync/spin_trace_tests.rs
+@@ -98,7 +98,35 @@
+         crate::early_println!("Expected trace count: 18 events");
+         crate::early_println!("- 6 tests × 3 events each (TryAcquire + Success + Release) = 18 total");
+     }
+-    
++
++    /// Two-actor contention scenario matching the JS-SAM 2-thread spin model.
++    /// A single-CPU ktest can't spawn a real 2nd thread that blocks (a blocking
++    /// lock() from actor 1 while actor 0 holds would spin forever), so the 2nd
++    /// actor's contention is expressed via try_lock, which fails without blocking.
++    #[ktest]
++    fn test_spin_2thread() {
++        crate::early_println!("=== 2-Thread SpinLock Trace Start ===");
++        let lock = Arc::new(SpinTrace::<u32, PreemptDisabled>::new(0));
++
++        // actor 0 acquires (blocking): TryAcquireBlocking(0) + AcquireSuccess(0)
++        let g0 = lock.lock_with_thread_id(0);
++        // actor 1 attempts while 0 holds -> AcquireFail(1) (contention, no deadlock)
++        assert!(lock.try_lock_with_thread_id(1).is_none());
++        // actor 0 releases: Release(0)
++        drop(g0);
++        // actor 1 acquires (blocking): TryAcquireBlocking(1) + AcquireSuccess(1)
++        let g1 = lock.lock_with_thread_id(1);
++        // actor 0 attempts while 1 holds -> AcquireFail(0)
++        assert!(lock.try_lock_with_thread_id(0).is_none());
++        // actor 1 releases: Release(1)
++        drop(g1);
++        // actor 0 non-blocking acquire when free -> AcquireSuccess(0)
++        let g0b = lock.try_lock_with_thread_id(0).expect("lock is free");
++        drop(g0b); // Release(0)
++
++        crate::early_println!("=== 2-Thread SpinLock Trace Complete ===");
++    }
++
+     #[ktest]
+     fn test_tla_trace_simple() {
+         crate::early_println!("=== TLA+ SpinLock Randomized Trace Test Start ===");
+@@ -212,4 +240,4 @@
+             _ => unreachable!(),
+         }
+     }
+-}
++}
+\ No newline at end of file

data/sys_traces/spin/spin_2thread.ndjson

@@ -0,0 +1,8 @@
+{"action": "AcquireLock", "data": {"thread": 0, "callType": "lock"}, "pre_state": {"lockHeld": false, "lockHolder": null}, "post_state": {"lockHeld": true, "lockHolder": 0}}
+{"action": "AcquireLock", "data": {"thread": 1, "callType": "try"}, "pre_state": {"lockHeld": true, "lockHolder": 0}, "post_state": {"lockHeld": true, "lockHolder": 0}}
+{"action": "ReleaseLock", "data": {"thread": 0}, "pre_state": {"lockHeld": true, "lockHolder": 0}, "post_state": {"lockHeld": false, "lockHolder": null}}
+{"action": "AcquireLock", "data": {"thread": 1, "callType": "lock"}, "pre_state": {"lockHeld": false, "lockHolder": null}, "post_state": {"lockHeld": true, "lockHolder": 1}}
+{"action": "AcquireLock", "data": {"thread": 0, "callType": "try"}, "pre_state": {"lockHeld": true, "lockHolder": 1}, "post_state": {"lockHeld": true, "lockHolder": 1}}
+{"action": "ReleaseLock", "data": {"thread": 1}, "pre_state": {"lockHeld": true, "lockHolder": 1}, "post_state": {"lockHeld": false, "lockHolder": null}}
+{"action": "AcquireLock", "data": {"thread": 0, "callType": "try"}, "pre_state": {"lockHeld": false, "lockHolder": null}, "post_state": {"lockHeld": true, "lockHolder": 0}}
+{"action": "ReleaseLock", "data": {"thread": 0}, "pre_state": {"lockHeld": true, "lockHolder": 0}, "post_state": {"lockHeld": false, "lockHolder": null}}

scripts/harness/spin/.gitattributes

@@ -0,0 +1,4 @@
+# These scripts run inside a Linux container (build_and_test.sh) or drive it
+# (run.sh); they must keep LF endings even when checked out on Windows, or bash
+# fails on the CR (`$'\r': command not found`).
+*.sh text eol=lf

scripts/harness/spin/build_and_test.sh

@@ -0,0 +1,40 @@
+#!/bin/bash
+# In-container build + run of the Asterinas 2-thread spin trace ktest.
+#
+# Runs inside asterinas/asterinas:0.16.0-20250822. The patched source is
+# bind-mounted read-only at /src (host FS — may not support fallocate), so we
+# build on an ext4 docker volume at /build where mke2fs/fallocate work. /build
+# persists across runs, so re-runs after editing the ktest are incremental.
+#
+# Emits kernel serial JSON on stdout: lines like
+#   {"seq":N,"thread":T,"lock":0,"state":"locked|unlocked","action":A,"actor":T}
+# which scripts/harness/spin/parse_traces.py folds into NDJSON windows.
+set -e
+export PATH=/nix/store/4zpvbvn0cvmmn9k05b1qgr5xh7i6r9ka-nix-2.31.1/bin:$PATH
+echo 'connect-timeout = 60000' >> /etc/nix/nix.conf
+
+if [ ! -f /build/Makefile ]; then
+  echo "===== populating /build from /src (first run) ====="
+  cp -a /src/. /build/
+fi
+# Refresh instrumentation + tests so edits take effect on incremental re-runs.
+cp -f /src/ostd/src/sync/spin_trace.rs       /build/ostd/src/sync/spin_trace.rs
+cp -f /src/ostd/src/sync/spin_trace_tests.rs /build/ostd/src/sync/spin_trace_tests.rs
+
+cd /build
+echo "===== installing cargo-osdk ====="
+OSDK_LOCAL_DEV=1 cargo install cargo-osdk --path osdk --locked
+echo "===== make initramfs ====="
+make initramfs
+echo "===== cargo osdk test (test_spin_2thread) ====="
+cd ostd
+# Capture the test's real exit code: under set -e a bare $? after a failing
+# command is unreachable (the script would have aborted), so the DONE line
+# would always print rc=0. Disable -e around the call, record rc, re-exit.
+set +e
+timeout 1200 cargo osdk test --features tla-trace --target-arch x86_64 \
+  --qemu-args='-accel tcg' test_spin_2thread 2>&1
+rc=$?
+set -e
+echo "===== DONE rc=$rc ====="
+exit "$rc"

scripts/harness/spin/parse_traces.py

@@ -0,0 +1,120 @@
+#!/usr/bin/env python3
+"""Fold Asterinas spin-trace serial events into JS-SAM (pre, post) NDJSON windows.
+
+Input: the docker/QEMU run log (mixed build output + kernel serial JSON events of
+the form emitted by ostd/src/sync/spin_trace.rs):
+
+    {"seq":N,"thread":T,"lock":0,"state":"locked|unlocked","action":A,"actor":T}
+
+Output: one NDJSON file of event-form windows (see
+tla_eval/evaluation/semantics/trace_loader.py), each line:
+
+    {"action": "AcquireLock"|"ReleaseLock", "data": {...},
+     "pre_state": {...}, "post_state": {...}}
+
+The window state is the *objective, model-independent* spinlock state
+{lockHeld, lockHolder} — the real lock ownership observed by the kernel. JS-SAM's
+Phase-3 projection rule only requires the trace's post_state keys to match the
+model, so the model's internal threadStatus/callType bookkeeping is ignored and
+the traces stay faithful to the system rather than tailored to any one model.
+
+Event -> model action mapping:
+  TryAcquireBlocking(t)  pre-step of a blocking lock(); folded, emits no window
+  AcquireSuccess(t)      AcquireLock: lock becomes held by t
+                         (callType "lock" if preceded by TryAcquireBlocking, else "try")
+  AcquireFail(t)         AcquireLock (callType "try"): contention — ownership unchanged
+  Release(t)             ReleaseLock: lock becomes free
+  StopSpinning(t)        internal spin step; skipped
+
+Usage:
+  parse_traces.py <input_log> <output_ndjson>
+"""
+
+import json
+import re
+import sys
+from pathlib import Path
+
+EVENT_RE = re.compile(r'\{"seq":\d+[^{}]*"action":"[^"]*"[^{}]*\}')
+
+
+def extract_events(log_text):
+    events = []
+    for match in EVENT_RE.findall(log_text):
+        try:
+            event = json.loads(match)
+        except json.JSONDecodeError:
+            continue
+        if "action" in event and "thread" in event:
+            events.append(event)
+    return events
+
+
+def fold_windows(events):
+    lock_held = False
+    lock_holder = None
+    blocking = {}  # thread -> True after a TryAcquireBlocking, cleared on its acquire
+    windows = []
+
+    for event in events:
+        action = event["action"]
+        thread = event["thread"]
+
+        if action == "TryAcquireBlocking":
+            blocking[thread] = True
+            continue
+        if action == "StopSpinning":
+            continue
+
+        pre = {"lockHeld": lock_held, "lockHolder": lock_holder}
+
+        if action == "AcquireSuccess":
+            call_type = "lock" if blocking.pop(thread, False) else "try"
+            lock_held, lock_holder = True, thread
+            windows.append({
+                "action": "AcquireLock",
+                "data": {"thread": thread, "callType": call_type},
+                "pre_state": pre,
+                "post_state": {"lockHeld": lock_held, "lockHolder": lock_holder},
+            })
+        elif action == "AcquireFail":
+            blocking.pop(thread, None)
+            # Failed contention: the lock stays with its current holder.
+            windows.append({
+                "action": "AcquireLock",
+                "data": {"thread": thread, "callType": "try"},
+                "pre_state": pre,
+                "post_state": {"lockHeld": lock_held, "lockHolder": lock_holder},
+            })
+        elif action == "Release":
+            lock_held, lock_holder = False, None
+            windows.append({
+                "action": "ReleaseLock",
+                "data": {"thread": thread},
+                "pre_state": pre,
+                "post_state": {"lockHeld": lock_held, "lockHolder": lock_holder},
+            })
+
+    return windows
+
+
+def main():
+    if len(sys.argv) != 3:
+        print(__doc__)
+        sys.exit(2)
+    log_path = Path(sys.argv[1])
+    out_path = Path(sys.argv[2])
+
+    events = extract_events(log_path.read_text(encoding="utf-8", errors="replace"))
+    windows = fold_windows(events)
+
+    out_path.parent.mkdir(parents=True, exist_ok=True)
+    with out_path.open("w", encoding="utf-8") as f:
+        for window in windows:
+            f.write(json.dumps(window) + "\n")
+
+    print(f"wrote {len(windows)} windows from {len(events)} events -> {out_path}")
+
+
+if __name__ == "__main__":
+    main()

scripts/harness/spin/run.sh

@@ -0,0 +1,69 @@
+#!/usr/bin/env bash
+# scripts/harness/spin/run.sh — capture Asterinas spinlock execution traces for
+# the JS-SAM Phase-3 (transition validation) direct path.
+#
+# Produces a 2-thread (pre, post) NDJSON trace set at
+#   data/sys_traces/spin/spin_2thread.ndjson
+# from a real run of the instrumented Asterinas spinlock under QEMU.
+#
+# Pipeline:
+#   1. Clone Asterinas at v0.16.0 (matches the docker image toolchain; the
+#      reference patch does not apply to current main) with LF line endings.
+#   2. Apply data/patches/asterinas_tla_trace.patch (reference TLA+ trace
+#      instrumentation) + data/patches/spin_2thread_ktest.patch (adds the
+#      2-actor `test_spin_2thread` ktest — the reference tests are single-actor).
+#   3. Build + run the ktest under QEMU-TCG inside the asterinas image, on an
+#      ext4 docker volume (the source may be on a host FS without fallocate).
+#   4. Fold the kernel serial JSON into JS-SAM windows via parse_traces.py.
+#
+# Requires: docker, the asterinas/asterinas:0.16.0-20250822 image, git, python3.
+# Windows note: run from Git Bash with Docker Desktop; the CRLF and fallocate
+# handling below is what makes the Linux-oriented flow work on a Windows host.
+set -euo pipefail
+
+SCRIPT_DIR=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)
+PROJECT_ROOT=$(cd "$SCRIPT_DIR/../../.." && pwd)
+
+SRC="${ASTERINAS_SOURCE_DIR:-$PROJECT_ROOT/artifacts/spin}"
+IMAGE="${ASTERINAS_DOCKER_IMAGE:-asterinas/asterinas:0.16.0-20250822}"
+REF_PATCH="$PROJECT_ROOT/data/patches/asterinas_tla_trace.patch"
+ADD_PATCH="$PROJECT_ROOT/data/patches/spin_2thread_ktest.patch"
+TRACES_OUT="${TRACES_OUT:-$PROJECT_ROOT/data/sys_traces/spin/spin_2thread.ndjson}"
+LOG="${LOG:-$PROJECT_ROOT/artifacts/spin_capture.log}"
+
+# 1-2. Clone + patch (idempotent: skip if already instrumented). The guard is
+# a sentinel written only after BOTH patches apply — checking for a file the
+# first patch creates would leave a half-patched checkout unrecoverable if the
+# second apply fails (set -e aborts, the next run would skip the whole block).
+SENTINEL="$SRC/.sysmobench_instrumented"
+if [ ! -e "$SENTINEL" ]; then
+  echo "[run.sh] cloning asterinas v0.16.0 (LF) into $SRC" >&2
+  rm -rf "$SRC"
+  git -c core.autocrlf=false clone --depth 1 --branch v0.16.0 \
+    https://github.com/asterinas/asterinas.git "$SRC"
+  git -C "$SRC" config core.autocrlf false
+  # Patches (and the sysmobench checkout) may carry CRLF on Windows; normalize
+  # to LF before applying so the emitted Rust/shell files build in Linux.
+  echo "[run.sh] applying reference + 2-thread patches" >&2
+  tr -d '\r' < "$REF_PATCH" | git -C "$SRC" apply --whitespace=nowarn
+  tr -d '\r' < "$ADD_PATCH" | git -C "$SRC" apply --whitespace=nowarn
+  touch "$SENTINEL"
+fi
+
+# 3. Build + run under QEMU, capturing serial output. Source is read-only; the
+# build happens on the ext4 volume `spin-work`; cargo cache on `spin-cargo`.
+echo "[run.sh] building + running test_spin_2thread under QEMU (see $LOG)" >&2
+docker run --rm --privileged \
+  -v "$SRC:/src:ro" \
+  -v "$SCRIPT_DIR:/harness:ro" \
+  -v "spin-work:/build" \
+  -v "spin-cargo:/root/.cargo" \
+  "$IMAGE" bash /harness/build_and_test.sh > "$LOG" 2>&1 || {
+    echo "[run.sh] docker run failed; tail of $LOG:" >&2
+    tail -40 "$LOG" >&2
+    exit 1
+  }
+
+# 4. Parse serial JSON -> NDJSON windows.
+python3 "$SCRIPT_DIR/parse_traces.py" "$LOG" "$TRACES_OUT"
+echo "[run.sh] traces written to $TRACES_OUT" >&2

scripts/run_benchmark.py

@@ -43,6 +43,15 @@
 logging.basicConfig(level=logging.INFO, format='[%(levelname)s] %(message)s')
 logger = logging.getLogger(__name__)
 
+# The result summaries print status glyphs (✓ / ✗ / ⏭) that crash on consoles
+# whose default encoding can't represent them (e.g. Windows cp1252). Force the
+# std streams to UTF-8; a no-op where they already speak it.
+for _stream in (sys.stdout, sys.stderr):
+    try:
+        _stream.reconfigure(encoding="utf-8")
+    except (AttributeError, ValueError):
+        pass
+
 
 def _display_evaluation_results(eval_result):
     """Print a unified summary across SyntaxEvaluationResult / SemanticEvaluationResult / TransitionValidationResult."""

tests/test_evaluation/test_trace_loader.py

@@ -113,17 +113,20 @@ def test_direct_path_dispatches_to_backend(self, tmp_path, monkeypatch):
         assert result.per_action_pass_rates == {"AcquireLock": 1.0}
 
     def test_missing_traces_reported_cleanly(self, tmp_path, monkeypatch):
+        from tla_eval.evaluation.semantics import trace_loader
         from tla_eval.evaluation.semantics.transition_validation import (
             TransitionValidationEvaluator,
         )
 
+        def raise_missing_traces(task_name):
+            raise FileNotFoundError(f"Trace folder not found for task '{task_name}'")
+
+        monkeypatch.setattr(trace_loader, "load_trace_windows", raise_missing_traces)
+
         spec = PROJECT_ROOT / "tests" / "fixtures" / "js_sam" / "specs" / "spin-good.js"
         evaluator = TransitionValidationEvaluator(
             language="JS-SAM", workspace_root=str(tmp_path)
         )
-        # No monkeypatch: the real spin traces_folder (data/sys_traces/spin)
-        # is not checked into the repository, so the loader must fail with an
-        # actionable message rather than a crash.
         result = evaluator.evaluate(
             generation_result=SimpleNamespace(metadata={}),
             task_name="spin",

tla_eval/evaluation/semantics/manual_invariant_evaluator.py

@@ -949,6 +949,9 @@ def evaluate(self,
             invariant_results = outcome.cases
             result.model_checking_successful = any(c.success for c in invariant_results)
             result.model_checking_time = sum(c.elapsed_seconds for c in invariant_results)
+            result.states_explored = sum(
+                c.metadata.get("states_explored", 0) for c in invariant_results
+            )
 
             passed_count = sum(1 for c in invariant_results if c.success)
             total_count = len(invariant_results)

tla_eval/evaluation/semantics/runtime_check.py

@@ -646,7 +646,7 @@ def evaluate(self,
             # Other backends may not provide these; default to safe values.
             violations: List[str] = []
             deadlock = False
-            states = 0
+            states = mc_outcome.states_explored or 0
             if self.language.lower() in ("tla+", "tla", "tlaplus", "tla_plus"):
                 try:
                     runner = TLCRunner(timeout=self.timeout)