From c93ba5863dadf2b9ecb51efc977675f5da169bf0 Mon Sep 17 00:00:00 2001 From: kizo-core Date: Tue, 30 Jun 2026 17:06:00 -0700 Subject: [PATCH 1/8] js_sam: make the Docker sandbox cross-platform (Windows host support) _run_helper assumed a POSIX host: it called os.getuid()/os.getgid() (absent on Windows) and mounted the helper and spec at their host paths, which are invalid container destinations for Windows C:\ paths. Decouple host paths from fixed in-container mount points (/opt/js-sam, /work), normalize -v sources to forward slashes, rewrite specPath to the container path, and pick a non-root --user via a hasattr(os, "getuid") guard (host uid:gid on POSIX, fixed 1000:1000 on Windows). Behavior is unchanged on Linux/macOS; the JS-SAM backend now runs on a Windows host against Docker Desktop. Verified by the existing container integration tests plus a real Phase 1/2 sandbox run. --- tla_eval/languages/js_sam.py | 55 ++++++++++++++++++++++++++++++------ 1 file changed, 46 insertions(+), 9 deletions(-) diff --git a/tla_eval/languages/js_sam.py b/tla_eval/languages/js_sam.py index 00ec74d..227c34d 100644 --- a/tla_eval/languages/js_sam.py +++ b/tla_eval/languages/js_sam.py @@ -65,6 +65,13 @@ _SANDBOX_CPUS = "2" _SANDBOX_PIDS = "256" +# Fixed in-container mount points, kept independent of the host paths so the +# sandbox works regardless of host path shape (POSIX paths and Windows C:\ +# paths alike). cli.mjs resolves node_modules from its own location, so the +# whole helper dir is mounted and the spec is mounted under a separate dir. +_CONTAINER_HELPER_DIR = "/opt/js-sam" +_CONTAINER_WORK_DIR = "/work" + # Bench-wide exploration depth for the sam-pattern behavior explorer # (Phases 2 and 4). Deliberately a single constant rather than per-task # config: revisit when a second task lands (spec Open Question 3). @@ -113,6 +120,29 @@ def _force_remove_container(name: str) -> None: _helper_call_counter = 0 +def _docker_mount_source(path: Path) -> str: + """Host path for a ``docker -v`` source, normalized to forward slashes. + + Docker accepts forward-slash paths on every platform; on Windows this + avoids backslash ambiguity in the ``-v src:dst`` argument (the drive-letter + colon, e.g. ``C:``, is handled by Docker Desktop's volume parser). + """ + return str(path).replace("\\", "/") + + +def _sandbox_user_args() -> List[str]: + """``--user`` args that run the sandbox as a non-root user. + + On POSIX hosts, match the host uid:gid so the read-only bind mounts are + guaranteed readable. Windows has no ``os.getuid``/``getgid`` and Docker + Desktop maps bind mounts readable to any container user, so fall back to a + fixed non-root uid there. + """ + if hasattr(os, "getuid"): + return ["--user", f"{os.getuid()}:{os.getgid()}"] + return ["--user", "1000:1000"] + + def _run_helper( subcommand: str, request: Dict[str, Any], timeout: int ) -> Tuple[Optional[Dict[str, Any]], Optional[str]]: @@ -133,21 +163,28 @@ def _run_helper( _helper_call_counter += 1 container_name = f"sysmobench-jssam-{os.getpid()}-{_helper_call_counter}" - # The helper (cli.mjs + node_modules) and, for spec-bound subcommands, the - # single generated spec file. The helper only reads these; all output is - # JSON on stdout. cli.mjs resolves node_modules from its own location, so - # mounting HELPER_DIR at the same path keeps that working in-container. - mounts = ["-v", f"{HELPER_DIR}:{HELPER_DIR}:ro"] + # Mount the helper (cli.mjs + node_modules) at a fixed container path; the + # in-container layout is then independent of the host path shape, and the + # spec is mounted under a separate dir below. The helper only reads these; + # all output is JSON on stdout. cli.mjs resolves node_modules from its own + # location (its NODE_PATH setup), so any consistent mount point works. + mounts = ["-v", f"{_docker_mount_source(HELPER_DIR)}:{_CONTAINER_HELPER_DIR}:ro"] + + # Rewrite specPath to where the spec is mounted *inside* the container. + # Copy the request so the caller's dict is not mutated. + request = dict(request) spec_path = request.get("specPath") if spec_path: sp = Path(spec_path).resolve() - mounts += ["-v", f"{sp}:{sp}:ro"] + container_spec = f"{_CONTAINER_WORK_DIR}/{sp.name}" + mounts += ["-v", f"{_docker_mount_source(sp)}:{container_spec}:ro"] + request["specPath"] = container_spec cmd = [ "docker", "run", "--rm", "-i", "--name", container_name, "--network", "none", - "--user", f"{os.getuid()}:{os.getgid()}", + *_sandbox_user_args(), "--read-only", "--tmpfs", "/tmp", "-e", "HOME=/tmp", @@ -155,9 +192,9 @@ def _run_helper( "--cpus", _SANDBOX_CPUS, "--pids-limit", _SANDBOX_PIDS, *mounts, - "-w", str(HELPER_DIR), + "-w", _CONTAINER_HELPER_DIR, DOCKER_IMAGE, - "node", str(HELPER_CLI), subcommand, + "node", f"{_CONTAINER_HELPER_DIR}/cli.mjs", subcommand, ] try: proc = subprocess.run( From 7b6d1550341cd422c752cf7882e1db6eedcf606a Mon Sep 17 00:00:00 2001 From: kizo-core Date: Tue, 30 Jun 2026 17:06:11 -0700 Subject: [PATCH 2/8] models: point `claude` at Opus 4.8; omit sampling params for Opus 4.7+ MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit claude-sonnet-4-20250514 retired 2026-06-15, so the `claude` entry returned not_found. Repoint it to claude-opus-4-8. Opus 4.7+, Fable 5, and Mythos 5 removed temperature/top_p/top_k and return a 400 if any are sent. Dropping them from models.yaml is not enough — the adapter falls back to GenerationConfig defaults and sent temperature unconditionally, and litellm's drop_params does not yet cover these newer models. Add _should_omit_sampling_params() (mirroring _should_omit_top_p) and guard both temperature and top_p with it. Verified end to end: get_configured_model("claude").generate_direct(...) succeeds, and a full spin/JS-SAM run passes Phases 1, 2, and 4. --- config/models.yaml | 11 ++++++----- tla_eval/models/litellm_adapter.py | 25 +++++++++++++++++++++++-- 2 files changed, 29 insertions(+), 7 deletions(-) diff --git a/config/models.yaml b/config/models.yaml index af2af4b..f8cb770 100644 --- a/config/models.yaml +++ b/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" diff --git a/tla_eval/models/litellm_adapter.py b/tla_eval/models/litellm_adapter.py index 0914509..db2de8d 100644 --- a/tla_eval/models/litellm_adapter.py +++ b/tla_eval/models/litellm_adapter.py @@ -281,6 +281,25 @@ def _supports_missing_api_key(self) -> bool: def _should_omit_top_p(self) -> bool: return self.litellm_model.startswith("openai/gpt-5") + def _should_omit_sampling_params(self) -> bool: + """Whether to drop temperature/top_p/top_k for this model. + + Claude Opus 4.7+, Fable 5, and Mythos 5 removed the sampling + parameters and return a 400 ("`temperature` is deprecated for this + model") if any are sent. litellm's drop_params does not yet cover + these newer models, so the request must omit them here. + """ + model = self.litellm_model.lower() + return any( + tag in model + for tag in ( + "claude-opus-4-8", + "claude-opus-4-7", + "claude-fable-5", + "claude-mythos-5", + ) + ) + def _build_completion_params( self, prompt: str, @@ -312,15 +331,17 @@ def _build_completion_params( if model_max_tokens is not None: params["max_tokens"] = model_max_tokens + omit_sampling = self._should_omit_sampling_params() + model_temperature = self.config.get( "temperature", generation_config.temperature, ) - if model_temperature is not None: + if model_temperature is not None and not omit_sampling: params["temperature"] = model_temperature model_top_p = self.config.get("top_p", generation_config.top_p) - if model_top_p is not None and not self._should_omit_top_p(): + if model_top_p is not None and not self._should_omit_top_p() and not omit_sampling: params["top_p"] = model_top_p if generation_config.stop_sequences: From c900040ddd06bcd93f61462d325d8c9532498dbf Mon Sep 17 00:00:00 2001 From: kizo-core Date: Tue, 30 Jun 2026 17:23:02 -0700 Subject: [PATCH 3/8] run_benchmark: force UTF-8 std streams so status glyphs don't crash MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit _display_evaluation_results prints ✓/✗ status glyphs, which raise UnicodeEncodeError on consoles whose default encoding can't represent them (e.g. Windows cp1252) — the evaluation succeeds, then the final summary print crashes. Reconfigure sys.stdout/sys.stderr to UTF-8 at startup; a no-op where they already speak it. --- scripts/run_benchmark.py | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/scripts/run_benchmark.py b/scripts/run_benchmark.py index 865b400..be0d80f 100644 --- a/scripts/run_benchmark.py +++ b/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.""" From eaed4b6dada79790b07fea7019886cf6d6979b4c Mon Sep 17 00:00:00 2001 From: kizo-core Date: Tue, 30 Jun 2026 17:23:12 -0700 Subject: [PATCH 4/8] eval: report states_explored for non-TLA+ backends MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit "States explored" was hardcoded to 0 for any backend that isn't TLA+: runtime_check only parsed it from TLC output, and the invariant evaluator never set the top-level field at all (so even TLA+ Phase 4 showed 0). The JS-SAM helper already returns stepsExplored — it just wasn't threaded through. Add states_explored to ModelCheckOutcome and populate it from the JS-SAM check response; seed runtime_check's states from the backend outcome (TLA+ still overrides via its own parse); and set the invariant evaluator's top-level states_explored to the sum across cases. Also fix the JS-SAM Phase-4 metadata key (steps_explored -> states_explored) so the evaluator actually reads it. Verified on spin/JS-SAM: Phase 2 reports 326592 steps (depthMax 6), Phase 4 reports 979776 (326592 x 3 invariants). --- tla_eval/evaluation/semantics/manual_invariant_evaluator.py | 3 +++ tla_eval/evaluation/semantics/runtime_check.py | 2 +- tla_eval/languages/js_sam.py | 3 ++- tla_eval/languages/result_types.py | 1 + 4 files changed, 7 insertions(+), 2 deletions(-) diff --git a/tla_eval/evaluation/semantics/manual_invariant_evaluator.py b/tla_eval/evaluation/semantics/manual_invariant_evaluator.py index c040e48..7322327 100644 --- a/tla_eval/evaluation/semantics/manual_invariant_evaluator.py +++ b/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) diff --git a/tla_eval/evaluation/semantics/runtime_check.py b/tla_eval/evaluation/semantics/runtime_check.py index 2c7bea6..d06ce2f 100644 --- a/tla_eval/evaluation/semantics/runtime_check.py +++ b/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) diff --git a/tla_eval/languages/js_sam.py b/tla_eval/languages/js_sam.py index 227c34d..a2534bd 100644 --- a/tla_eval/languages/js_sam.py +++ b/tla_eval/languages/js_sam.py @@ -408,6 +408,7 @@ def run_model_checker( elapsed_seconds=elapsed, error_message="; ".join(errors) if errors else None, classification=response.get("classification"), + states_explored=response.get("stepsExplored"), ) # ---- Phase 3 (direct path) ------------------------------------------ @@ -584,7 +585,7 @@ def check_invariants( if r.get("counterexample"): metadata["counterexample"] = r["counterexample"] if r.get("stepsExplored") is not None: - metadata["steps_explored"] = r["stepsExplored"] + metadata["states_explored"] = r["stepsExplored"] outcome.cases.append( InvariantCaseResult( diff --git a/tla_eval/languages/result_types.py b/tla_eval/languages/result_types.py index b757f8e..46a8ce4 100644 --- a/tla_eval/languages/result_types.py +++ b/tla_eval/languages/result_types.py @@ -31,6 +31,7 @@ class ModelCheckOutcome: elapsed_seconds: float = 0.0 error_message: Optional[str] = None classification: Optional[str] = None # e.g. "violation", "deadlock", "timeout", "parse_error" + states_explored: Optional[int] = None # steps/states the checker explored, when the backend reports it @dataclass From d9f82f741c08c83014d4474f4be2485e6f811d3c Mon Sep 17 00:00:00 2001 From: kizo-core Date: Tue, 30 Jun 2026 21:41:52 -0700 Subject: [PATCH 5/8] spin harness: capture real 2-thread traces for JS-SAM Phase 3 Adds the trace-capture harness for the spin task so JS-SAM Phase 3 (transition validation) runs against real Asterinas spinlock behavior rather than being blocked on missing traces. - scripts/harness/spin/run.sh: clone Asterinas v0.16.0 (LF), apply the reference instrumentation + the 2-thread ktest patch, build+run under QEMU-TCG on an ext4 docker volume, parse serial JSON into NDJSON. - scripts/harness/spin/build_and_test.sh: in-container build+run. - scripts/harness/spin/parse_traces.py: folds kernel events (TryAcquireBlocking/AcquireSuccess/AcquireFail/Release) into (pre, post) windows keyed on the objective {lockHeld, lockHolder} state; JS-SAM's projection rule ignores model-internal bookkeeping. - data/patches/spin_2thread_ktest.patch: adds test_spin_2thread, a 2-actor contention scenario (try_lock avoids single-CPU deadlock); the reference ktests are single-actor. - data/sys_traces/spin/spin_2thread.ndjson: the captured 8-window trace set (force-added; traces are normally generated, not checked in). The v0.16.0 pin (patch doesn't apply to main), LF normalization of the clone and patches, and the ext4 build volume (host FS lacks fallocate) are what make this Linux-oriented flow run under Docker Desktop on Windows. Verified: Phase 3 scores 87.5% (7/8) on the Opus 4.8 spin model. Co-Authored-By: Claude Opus 4.8 (1M context) --- data/patches/spin_2thread_ktest.patch | 46 +++++++++ data/sys_traces/spin/spin_2thread.ndjson | 8 ++ scripts/harness/spin/.gitattributes | 4 + scripts/harness/spin/build_and_test.sh | 33 +++++++ scripts/harness/spin/parse_traces.py | 120 +++++++++++++++++++++++ scripts/harness/spin/run.sh | 64 ++++++++++++ 6 files changed, 275 insertions(+) create mode 100644 data/patches/spin_2thread_ktest.patch create mode 100644 data/sys_traces/spin/spin_2thread.ndjson create mode 100644 scripts/harness/spin/.gitattributes create mode 100644 scripts/harness/spin/build_and_test.sh create mode 100644 scripts/harness/spin/parse_traces.py create mode 100644 scripts/harness/spin/run.sh diff --git a/data/patches/spin_2thread_ktest.patch b/data/patches/spin_2thread_ktest.patch new file mode 100644 index 0000000..133570a --- /dev/null +++ b/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::::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 diff --git a/data/sys_traces/spin/spin_2thread.ndjson b/data/sys_traces/spin/spin_2thread.ndjson new file mode 100644 index 0000000..a4788a6 --- /dev/null +++ b/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}} diff --git a/scripts/harness/spin/.gitattributes b/scripts/harness/spin/.gitattributes new file mode 100644 index 0000000..048c212 --- /dev/null +++ b/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 diff --git a/scripts/harness/spin/build_and_test.sh b/scripts/harness/spin/build_and_test.sh new file mode 100644 index 0000000..8a67f2a --- /dev/null +++ b/scripts/harness/spin/build_and_test.sh @@ -0,0 +1,33 @@ +#!/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 +timeout 1200 cargo osdk test --features tla-trace --target-arch x86_64 \ + --qemu-args='-accel tcg' test_spin_2thread 2>&1 +echo "===== DONE rc=$? =====" diff --git a/scripts/harness/spin/parse_traces.py b/scripts/harness/spin/parse_traces.py new file mode 100644 index 0000000..a156e34 --- /dev/null +++ b/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 +""" + +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() diff --git a/scripts/harness/spin/run.sh b/scripts/harness/spin/run.sh new file mode 100644 index 0000000..416f132 --- /dev/null +++ b/scripts/harness/spin/run.sh @@ -0,0 +1,64 @@ +#!/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). +if [ ! -e "$SRC/ostd/src/sync/spin_trace.rs" ]; 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 +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 From f402e9f5bfd2e26123f075fd7c208ec3b4dc4246 Mon Sep 17 00:00:00 2001 From: kizo-core Date: Tue, 30 Jun 2026 21:48:06 -0700 Subject: [PATCH 6/8] docs: research report for the first end-to-end JS-SAM experiment Documents the first four-phase JS-SAM run on the spin task (Opus 4.8): method, the Phase 3 kernel trace-capture pipeline, results (Phase 3 87.5%, with the try_lock-from-free modeling discrepancy), the cross-platform fixes, limitations, and reproduction steps. Co-Authored-By: Claude Opus 4.8 (1M context) --- docs/js_sam_first_experiment.md | 323 ++++++++++++++++++++++++++++++++ 1 file changed, 323 insertions(+) create mode 100644 docs/js_sam_first_experiment.md diff --git a/docs/js_sam_first_experiment.md b/docs/js_sam_first_experiment.md new file mode 100644 index 0000000..1430847 --- /dev/null +++ b/docs/js_sam_first_experiment.md @@ -0,0 +1,323 @@ +# First End-to-End JS-SAM Experiment on SysMoBench + +**Task:** `spin` (Asterinas OS spinlock) · **Backend:** JS-SAM · **Model:** Claude +Opus 4.8 · **Method:** `direct_call` +**Date:** 2026-06-30 · **Host:** Windows 11, Docker Desktop 4.80 (engine 29.6.1) + +--- + +## Abstract + +We ran the first complete, four-phase SysMoBench evaluation of the **JS-SAM** +backend — JavaScript specifications written in the [SAM +pattern](https://sam.js.org) — on the `spin` task, using Claude Opus 4.8 to +generate the specification. All four phases produced real results: syntax +(Phase 1), bounded model checking (Phase 2), transition validation against +**real kernel-captured traces** (Phase 3), and invariant verification (Phase 4). + +The headline result is a **Phase 3 score of 87.5% (7/8 trace windows)**. The +single failing window is diagnostic rather than incidental: the generated model +reproduces blocking `lock()` acquisitions correctly but its non-blocking +`try_lock` acquire never actually takes the lock — a defect observable only when +acquiring from a free state, and caught precisely because the model was replayed +against transitions captured from the real Asterinas spinlock. + +Reaching a real Phase 3 number required standing up a kernel trace-capture +harness from scratch (the trace corpus is not shipped with the benchmark) and +authoring a 2-thread instrumentation scenario matching what the JS-SAM prompt +models. Several cross-platform defects in the harness were fixed along the way, +making JS-SAM runnable on a Windows host. + +--- + +## 1. Background and objective + +SysMoBench evaluates AI systems on formally modeling real concurrent/distributed +systems across four automated phases. JS-SAM is the benchmark's first +**non-formal-language** backend: instead of TLA+/Alloy/CSP, the model emits an +executable JavaScript module following the SAM pattern (actions propose, a model +accepts, state is a pure function of the model). It tests a distinct hypothesis: + +> Can an LLM produce a correct system specification in a pattern it sees +> constantly in training (JavaScript) more readily than in formal languages it +> rarely sees? + +This experiment is the first data point toward that question: a full run of one +model on one task, establishing that the JS-SAM pipeline works end-to-end and +producing a per-phase score profile for later comparison against the formal +backends. + +### Integration decisions (from the maintainers) + +Four open questions from the JS-SAM spec were resolved by the upstream +maintainer prior to this run, and shaped it: + +1. **In scope** — JS-SAM is a valid leaderboard backend. +2. **Traces** — trace sets are not fixed data; they are generated on demand by + instrumenting the real system. The maintainers' `spin` captures use three + threads; the JS-SAM prompt models two. The two cannot share a trace set, so + **JS-SAM must generate its own traces at the granularity it models** (two + threads), using the existing instrumentation + (`data/patches/asterinas_tla_trace.patch`, `task.yaml > tv.harness`) as a + reference. This directly motivated the Phase 3 work below. +3. **Depth bound** — `depthMax` is a per-task config value with a documented + default; 6 is the default for `spin`. +4. **Shared invariant translation** — only TLA+ has the agent-based invariant + translator; Alloy, PAT, and JS-SAM fall back to a direct API call. + Generalizing the agent translator is deferred future work. + +--- + +## 2. Environment and configuration + +| Component | Value | +|---|---| +| Host OS | Windows 11, Git Bash + PowerShell | +| Container runtime | Docker Desktop 4.80, engine 29.6.1 (WSL2 backend) | +| JS-SAM sandbox image | `node:20-slim` (throwaway container per helper call) | +| Generation model | `claude` → `claude-opus-4-8` (Anthropic API via LiteLLM) | +| Task | `spin` — Asterinas `ostd/src/sync/spin.rs` | +| Generation method | `direct_call` (single prompt) | +| Exploration depth (Phase 2/4) | `depthMax = 6` | + +Two configuration corrections were required before any run: + +- The `claude` model entry pointed at `claude-sonnet-4-20250514`, which + **retired 2026-06-15** and returned `not_found_error`. Repointed to + `claude-opus-4-8`. +- Opus 4.8 rejects `temperature`/`top_p`/`top_k` (HTTP 400); the LiteLLM adapter + was sending them unconditionally. Both fixes are described in §5. + +--- + +## 3. Method + +Each phase evaluates the **same** generated specification (`spin.js`, produced +once by Opus 4.8 in Phase 1) so the four scores describe one artifact. The +JS-SAM backend shells out to a Node helper (`tools/js-sam/cli.mjs`) inside a +locked-down Docker container (`--network none`, read-only rootfs, non-root user, +CPU/memory/PID caps); the container is the trust boundary for model-generated +JavaScript. + +- **Phase 1 — compilation_check:** parse + module-load + structural contract + check of the generated module. +- **Phase 2 — runtime_check:** bounded exploration of the model's own state + space by the sam-pattern explorer at `depthMax 6`; a second identical + exploration detects nondeterminism. +- **Phase 3 — transition_validation (direct path):** each captured + `(pre_state, action, post_state)` window is replayed — + `setState(pre)`, `actions[name](data)`, then `getState()` is diffed against + `post` under the projection rule (only keys present in the trace's post-state + must match; model-only bookkeeping is ignored). This is the direct path — no + coding-agent orchestration — because SAM *is* `model.present(action(data))`. +- **Phase 4 — invariant_verification:** three expert spinlock invariants are + translated to JavaScript predicates (direct API call) and checked by the + explorer. + +--- + +## 4. Phase 3: capturing real spinlock traces + +Phase 3 is the only phase requiring data external to the model, and no `spin` +trace corpus ships with the benchmark. Producing a legitimate trace set meant +building and running the instrumented Asterinas kernel and folding its output +into the JS-SAM state schema. This section documents that pipeline because it is +the experiment's main methodological contribution. + +### 4.1 Pipeline + +1. **Source at a compatible revision.** The reference instrumentation patch does + **not** apply to Asterinas `main`; it applies cleanly at tag **v0.16.0**, + which also matches the toolchain bundled in the + `asterinas/asterinas:0.16.0-20250822` image. We clone v0.16.0. +2. **Instrumentation.** Apply `data/patches/asterinas_tla_trace.patch` (the + reference TLA+-trace instrumentation, which adds `ostd/src/sync/spin_trace.rs` + emitting serial JSON events) plus a new **2-thread ktest** (§4.2). +3. **Build + run.** Inside the image: install `cargo-osdk`, `make initramfs`, + and `cargo osdk test --features tla-trace --qemu-args='-accel tcg' + test_spin_2thread`. The kernel boots under QEMU (software TCG) and the ktest + emits trace events over the serial port. +4. **Parse.** `scripts/harness/spin/parse_traces.py` folds the event stream into + `(pre, post)` NDJSON windows. + +### 4.2 Authoring a 2-thread contention scenario + +The reference spin ktests are **single-actor** (all operations attributed to +thread 0), so they never exercise the contention (`trying`/failed-acquire) +behavior the JS-SAM model represents across two threads. A blocking `lock()` +from a second actor in a single-CPU ktest would spin forever (deadlock), so the +new `test_spin_2thread` expresses the second actor's contention with a +**non-blocking `try_lock`** that fails without blocking: + +``` +actor0.lock() -> TryAcquireBlocking(0), AcquireSuccess(0) // 0 holds +actor1.try_lock() -> AcquireFail(1) // contention, no deadlock +actor0.release() -> Release(0) +actor1.lock() -> TryAcquireBlocking(1), AcquireSuccess(1) // 1 holds +actor0.try_lock() -> AcquireFail(0) // contention +actor1.release() -> Release(1) +actor0.try_lock() -> AcquireSuccess(0) // try from free succeeds +actor0.release() -> Release(0) +``` + +### 4.3 Event → state mapping + +The kernel emits low-level events +(`TryAcquireBlocking`, `AcquireSuccess`, `AcquireFail`, `Release`). The parser +folds them into windows keyed on the **objective, model-independent** spinlock +state `{lockHeld, lockHolder}` — the real observable lock ownership — and lets +the projection rule ignore the model's internal `threadStatus`/`callType` +bookkeeping. This keeps the traces faithful to the *system* rather than tailored +to any one model: + +| Kernel event | Model window | +|---|---| +| `TryAcquireBlocking(t)` | folded (pre-step of a blocking acquire; emits no window) | +| `AcquireSuccess(t)` | `AcquireLock` → lock held by `t` (`callType` `lock` if preceded by `TryAcquireBlocking`, else `try`) | +| `AcquireFail(t)` | `AcquireLock` (`callType` `try`) → ownership unchanged (contention does not steal the lock) | +| `Release(t)` | `ReleaseLock` → lock free | + +The 10 emitted events fold to **8 windows** at +`data/sys_traces/spin/spin_2thread.ndjson`. + +The whole capture is reproducible via `scripts/harness/spin/run.sh`. + +--- + +## 5. Engineering contributions + +The following defects were found and fixed to make the run possible; each is a +self-contained commit on the `full-stack` branch. + +1. **Cross-platform JS-SAM Docker sandbox** (`tla_eval/languages/js_sam.py`). + The sandbox was POSIX-host-only: it called `os.getuid()`/`getgid()` (absent + on Windows) and mounted the helper and spec at their host paths (invalid + container destinations for Windows `C:\` paths). Fixed by decoupling host + paths from fixed in-container mount points (`/opt/js-sam`, `/work`), + normalizing `-v` sources to forward slashes, rewriting `specPath` to the + container path, and selecting a non-root `--user` behind a + `hasattr(os, "getuid")` guard. Behavior is unchanged on Linux/macOS; the + backend now runs on a Windows host. (Upstreamable.) +2. **Model refresh** (`config/models.yaml`, `tla_eval/models/litellm_adapter.py`). + Repointed `claude` to `claude-opus-4-8` and added + `_should_omit_sampling_params()` so `temperature`/`top_p`/`top_k` are dropped + for models that reject them (Opus 4.7+, Fable 5, Mythos 5) — LiteLLM's + `drop_params` does not yet cover these models. +3. **UTF-8 console output** (`scripts/run_benchmark.py`). The result summary + printed `✓`/`✗`, which raised `UnicodeEncodeError` on a Windows cp1252 + console after a successful evaluation; std streams are now reconfigured to + UTF-8. +4. **`states_explored` for non-TLA+ backends** (`ModelCheckOutcome`, + `js_sam.py`, `runtime_check.py`, `manual_invariant_evaluator.py`). The metric + was hardcoded to 0 for any non-TLA+ backend even though the JS-SAM helper + already reports `stepsExplored`; it is now threaded through (and the invariant + evaluator's top-level field, previously 0 for all backends, is populated). +5. **Spin Phase-3 trace harness** (`scripts/harness/spin/*`, + `data/patches/spin_2thread_ktest.patch`, `data/sys_traces/spin/*`). §4. + +Cross-platform frictions resolved during the capture: patch pinned to v0.16.0; +CRLF normalization of both the Asterinas clone (`core.autocrlf`) and the patch +files; and building on an ext4 docker volume because the Windows bind-mount does +not support `fallocate` (needed to build the initramfs image). + +--- + +## 6. Results + +All four phases evaluate the same Opus 4.8 `spin.js`. + +| Phase | Metric | Result | Detail | +|---|---|---|---| +| 1 | compilation_check | **PASS** | 0 syntax errors, 0 semantic errors | +| 2 | runtime_check | **PASS** | 326,592 states explored (`depthMax 6`), 0 violations, no deadlock | +| 3 | transition_validation | **PASS** | **87.5% (7/8 windows)** — AcquireLock 80% (4/5), ReleaseLock 100% (3/3) | +| 4 | invariant_verification | **PASS** | 3/3 invariants: MutualExclusion, LockStatusConsistency, NoDeadlock | + +### The Phase 3 discrepancy + +The single failing window is an `AcquireLock` where the trace expects +`{lockHeld: true, lockHolder: 0}` but the model produced `{lockHeld: false, +lockHolder: null}` — i.e., the model failed to acquire a **free** lock via the +`try_lock` (`callType: "try"`) path. The pattern is precise: + +- Blocking `lock()` acquisitions (`callType: "lock"`) reproduce correctly. +- A failed `try_lock` under contention passes (ownership is unchanged either + way, so the mismatch is masked). +- A `try_lock` that **should succeed** from a free lock exposes the defect: the + generated model's `try` acquire never takes the lock. + +This is a genuine modeling gap in the Opus 4.8 specification, surfaced only +because the model was checked against transitions observed in the real kernel — +the intended value of transition validation. + +--- + +## 7. Discussion + +- **The JS-SAM pipeline is viable end-to-end**, including on a non-Linux host, + and produces a full four-phase score profile suitable for later comparison + against the formal-language backends. +- **Phase 3 has teeth.** Even a small, deterministic trace set (8 windows) + discriminated correct from incorrect transitions and localized a specific + defect in the generated model. The `try_lock`-from-free case is a good example + of a transition that syntactic and self-consistency checks (Phases 1–2) and + invariant checking (Phase 4) all pass while the model is still wrong about + real behavior. +- **Objective-state windows are robust.** Keying traces on `{lockHeld, + lockHolder}` and relying on the projection rule kept the trace corpus + independent of the model under test, which is the correct stance for a + ground-truth oracle. + +--- + +## 8. Limitations and threats to validity + +- **Single model, single task, single generation.** No cross-model or + cross-language comparison yet; the central JS-SAM hypothesis is not answered by + one data point. +- **Small, single-scenario trace set.** Eight windows from one deterministic + ktest. Contention is expressed via `try_lock` on a single CPU rather than true + SMP concurrency, so scenarios like a thread blocking-then-acquiring on release + are not represented. Broader coverage (more scenarios, more interleavings) + would strengthen Phase 3. +- **Invariant translation used the direct API call**, per JS-SAM's current + policy, not the agent-based translator TLA+ uses (Open Question 4). +- **Non-blocking-only second actor.** The 2-thread ktest models contention + faithfully for lock ownership but does not capture a real waiter's blocking + wakeup. + +--- + +## 9. Future work + +1. **Broaden the spin trace corpus** — additional `test_spin_*` scenarios + (blocking waiter released and acquiring, longer interleavings) for richer + Phase 3 coverage. +2. **Run additional models and record the score profiles** to begin answering + the JS-SAM hypothesis (e.g., Sonnet 4.6, Haiku 4.5). +3. **A second JS-SAM task** with richer control state (`ringbuffer`/`locksvc`) + once trace harnesses exist for them. +4. **Generalize the agent invariant translator** so JS-SAM (and Alloy/PAT) can + share the TLA+ approach instead of falling back to a direct call. + +--- + +## 10. Reproducibility + +```bash +# Phases 1/2/4 (generation + evaluation), one metric per invocation: +python scripts/run_benchmark.py --task spin --method direct_call \ + --model claude --language JS-SAM --metric compilation_check +# ... runtime_check / invariant_verification + +# Phase 3: capture traces, then validate. +bash scripts/harness/spin/run.sh # -> data/sys_traces/spin/spin_2thread.ndjson +python scripts/run_benchmark.py --task spin --method direct_call \ + --model claude --language JS-SAM --metric transition_validation --yes \ + --spec-file +``` + +Requirements: Docker (with the `node:20-slim` and +`asterinas/asterinas:0.16.0-20250822` images), Node ≥ 20, `ANTHROPIC_API_KEY` in +`.env`. The JS-SAM sandbox and the Phase-3 capture both run under Docker Desktop +on Windows after the fixes in §5. From 81abd0f66b5aac6634b237ab08fba878ed52cef9 Mon Sep 17 00:00:00 2001 From: kizo-core Date: Sat, 11 Jul 2026 06:39:47 -0700 Subject: [PATCH 7/8] =?UTF-8?q?harness/spin:=20address=20review=20?= =?UTF-8?q?=E2=80=94=20self-healing=20patch=20guard,=20real=20test=20rc?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - run.sh: key the clone+patch idempotency guard on a sentinel written only after both patches apply, so a partial apply self-heals on re-run instead of skipping the 2-thread ktest patch forever (review: Qian-Cheng-nju). - build_and_test.sh: capture the cargo osdk test exit code explicitly (set +e / rc=$? / set -e) and re-exit with it, so the DONE line reports the real result instead of always rc=0 under set -e (review: Qian-Cheng-nju). Co-Authored-By: Claude Fable 5 --- scripts/harness/spin/build_and_test.sh | 9 ++++++++- scripts/harness/spin/run.sh | 9 +++++++-- 2 files changed, 15 insertions(+), 3 deletions(-) diff --git a/scripts/harness/spin/build_and_test.sh b/scripts/harness/spin/build_and_test.sh index 8a67f2a..23209c7 100644 --- a/scripts/harness/spin/build_and_test.sh +++ b/scripts/harness/spin/build_and_test.sh @@ -28,6 +28,13 @@ 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 -echo "===== DONE rc=$? =====" +rc=$? +set -e +echo "===== DONE rc=$rc =====" +exit "$rc" diff --git a/scripts/harness/spin/run.sh b/scripts/harness/spin/run.sh index 416f132..7d0c0c9 100644 --- a/scripts/harness/spin/run.sh +++ b/scripts/harness/spin/run.sh @@ -31,8 +31,12 @@ 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). -if [ ! -e "$SRC/ostd/src/sync/spin_trace.rs" ]; then +# 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 \ @@ -43,6 +47,7 @@ if [ ! -e "$SRC/ostd/src/sync/spin_trace.rs" ]; then 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 From 78a40d87f51b8e41976bc41bcd7ae26bd83f9d55 Mon Sep 17 00:00:00 2001 From: Qian-Cheng-nju Date: Mon, 13 Jul 2026 11:44:30 +0000 Subject: [PATCH 8/8] test: mock missing spin traces --- tests/test_evaluation/test_trace_loader.py | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/tests/test_evaluation/test_trace_loader.py b/tests/test_evaluation/test_trace_loader.py index 1fbc678..eacdbef 100644 --- a/tests/test_evaluation/test_trace_loader.py +++ b/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",