Fix spin transition-validation example and trace capture

.github/workflows/tests.yml

@@ -69,6 +69,8 @@ jobs:
           mkdir -p lib
           curl -fL --retry 3 -o lib/tla2tools.jar \
             https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
+          curl -fL --retry 3 -o lib/CommunityModules-deps.jar \
+            https://github.com/tlaplus/CommunityModules/releases/download/202505152026/CommunityModules-deps.jar
 
       - name: Run tests
         # test_model_connection.py is an interactive live-provider check that

.gitignore

@@ -45,6 +45,7 @@ systems/asterinas/asterinas/
 *.fp
 states/
 traces/
+!tla_eval/skills/tv-eval/examples/spin/traces/
 **/output/
 generation_summary.json
 specula

data/patches/asterinas_tla_trace.patch

@@ -1843,10 +1843,10 @@ index 0000000..c902814
 \ No newline at end of file
 diff --git a/ostd/src/sync/spin_trace.rs b/ostd/src/sync/spin_trace.rs
 new file mode 100644
-index 0000000..8ca98ee
+index 0000000..0106a41
 --- /dev/null
 +++ b/ostd/src/sync/spin_trace.rs
-@@ -0,0 +1,525 @@
+@@ -0,0 +1,550 @@
 +// SPDX-License-Identifier: MPL-2.0
 +
 +use alloc::sync::Arc;
@@ -2038,6 +2038,7 @@ index 0000000..8ca98ee
 +        // Record RequestTryLock (after setting state to trying_nonblocking)
 +        let lock_addr = self as *const Self as *const () as usize;
 +        let current_state = self.inner.lock.load(Ordering::Relaxed);
++        trace_event("TryAcquireNonBlocking", lock_addr, thread_id, current_state);
 +        
 +        if self.try_acquire_lock_with_id(thread_id) {
 +            let lock_guard = SpinTraceGuard_ {
@@ -2047,8 +2048,8 @@ index 0000000..8ca98ee
 +            };
 +            return Some(lock_guard);
 +        } else {
-+            // Explicitly record failure
-+            trace_event("AcquireFail", lock_addr, thread_id, false);
++            // A failed compare_exchange(false, true) observed a held lock.
++            trace_event("AcquireFail", lock_addr, thread_id, true);
 +            None
 +        }
 +    }
@@ -2075,13 +2076,13 @@ index 0000000..8ca98ee
 +            core::hint::spin_loop();
 +        }
 +
++        // Record successful lock acquisition (after execution)
++        trace_event("AcquireSuccess", lock_addr, thread_id, true);
++
 +        if spinning {
-+            // Record end of spinning (if we did spin)
++            // The lock is already held; this event does not change its state.
 +            trace_event("StopSpinning", lock_addr, thread_id, true);
 +        }
-+
-+        // Record successful lock acquisition (after execution)
-+        trace_event("AcquireSuccess", lock_addr, thread_id, true);
 +    }
 +
 +    fn try_acquire_lock_internal(&self) -> bool {
@@ -2208,6 +2209,30 @@ index 0000000..8ca98ee
 +        *seed
 +    }
 +
++    // A deterministic, single-CPU scenario with overlapping lock lifetimes.
++    // Every event comes from an executed operation; no synthetic contention.
++    #[ktest]
++    fn test_spin_tv_contract() {
++        TRACE_SEQUENCE.store(0, Ordering::Relaxed);
++        crate::early_println!("=== SPIN_TV_BEGIN ===");
++        let lock = SpinTrace::<u32, PreemptDisabled>::new(0);
++
++        let mut holder = lock.lock_with_thread_id(0);
++        *holder = 1;
++        assert!(lock.try_lock_with_thread_id(1).is_none());
++        drop(holder);
++
++        let mut next = lock.try_lock_with_thread_id(1).unwrap();
++        assert_eq!(*next, 1);
++        *next = 2;
++        drop(next);
++
++        let final_guard = lock.lock_with_thread_id(2);
++        assert_eq!(*final_guard, 2);
++        drop(final_guard);
++        crate::early_println!("=== SPIN_TV_END ===");
++    }
++
 +    #[ktest]
 +    fn test_spin_trace() {
 +        crate::early_println!("=== Starting 20 SpinTrace TLA+ Traces: Single Lock, 3-Thread Contention ===");

scripts/harness/spin_tv/parse_trace.py

@@ -0,0 +1,53 @@
+#!/usr/bin/env python3
+"""Extract the successful spin TV kernel test without synthesizing events."""
+
+import argparse
+import json
+import re
+from pathlib import Path
+
+BEGIN = "=== SPIN_TV_BEGIN ==="
+END = "=== SPIN_TV_END ==="
+
+
+def extract_trace(text):
+    text = re.sub(r"\x1b\[[0-9;]*m", "", text)
+    if text.count(BEGIN) != 1 or text.count(END) != 1:
+        raise ValueError("expected exactly one complete spin TV test")
+    if "test result: ok. 1 passed; 0 failed;" not in text:
+        raise ValueError("kernel test did not report success")
+    body = text.split(BEGIN, 1)[1].split(END, 1)[0]
+    events = []
+    for line in body.splitlines():
+        if not line.strip():
+            continue
+        event = json.loads(line)
+        if (
+            not isinstance(event, dict)
+            or not {"seq", "actor", "action", "state", "lock"} <= event.keys()
+        ):
+            raise ValueError("incomplete kernel event")
+        events.append(event)
+    if not events:
+        raise ValueError("no kernel events")
+    if [event["seq"] for event in events] != list(range(len(events))):
+        raise ValueError("kernel event sequence is incomplete or out of order")
+    return events
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("log", type=Path)
+    parser.add_argument("output", type=Path)
+    args = parser.parse_args()
+    try:
+        events = extract_trace(args.log.read_text())
+    except (OSError, ValueError) as exc:
+        parser.error(str(exc))
+    args.output.parent.mkdir(parents=True, exist_ok=True)
+    args.output.write_text("".join(json.dumps(event) + "\n" for event in events))
+    print(f"Captured {len(events)} kernel events in {args.output}")
+
+
+if __name__ == "__main__":
+    main()

scripts/harness/spin_tv/run.sh

@@ -0,0 +1,62 @@
+#!/usr/bin/env bash
+# Capture the focused spin TV contract test from an isolated Asterinas checkout.
+set -euo pipefail
+SCRIPT_DIR=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)
+PROJECT_ROOT=$(cd "$SCRIPT_DIR/../../.." && pwd)
+SOURCE_COMMIT=d73f1016a1d0cfb7b1f2ea72d2e9dd67ced0e0fa
+IMAGE=asterinas/asterinas:0.16.0-20250822@sha256:10d52ce84f72116ca2e41d6170f8882893592ccfc166d6b7d2262ccfeedacab2
+OUT=${1:-"$PROJECT_ROOT/tla_eval/skills/tv-eval/examples/spin/traces"}
+mkdir -p "$PROJECT_ROOT/artifacts" "$OUT"
+OUT=$(cd "$OUT" && pwd)
+WORK=$(mktemp -d "$PROJECT_ROOT/artifacts/spin-tv.XXXXXX")
+PATCH="$PROJECT_ROOT/data/patches/asterinas_tla_trace.patch"
+cleanup() {
+    if [[ -s "$WORK/container-id" ]]; then
+        docker rm -f "$(cat "$WORK/container-id")" >/dev/null 2>&1 || true
+    fi
+}
+trap cleanup EXIT
+printf 'Capture workspace: %s\n' "$WORK"
+git init -q "$WORK/source"
+git -C "$WORK/source" fetch --depth 1 https://github.com/asterinas/asterinas.git "$SOURCE_COMMIT"
+git -C "$WORK/source" checkout -q --detach FETCH_HEAD
+git -C "$WORK/source" apply --whitespace=nowarn "$PATCH"
+# No host checkout, cargo installation, or other container is modified.
+# --locked preserves the OSDK tool's dependency versions; make initramfs also
+# prepares the disk images referenced by the pinned OSDK configuration.
+timeout 1200 docker run --rm --cidfile "$WORK/container-id" --cpus 8 \
+    -e CARGO_BUILD_JOBS=8 -v "$WORK/source:/build" "$IMAGE" bash -c '
+        set -e
+        cd /build
+        OSDK_LOCAL_DEV=1 cargo install cargo-osdk --path osdk --locked
+        make initramfs
+        cd ostd
+        timeout 900 cargo osdk test --features tla-trace --target-arch x86_64 \
+            --qemu-args="-accel tcg" test_spin_tv_contract
+    ' > "$WORK/kernel.log" 2>&1 || {
+    tail -40 "$WORK/kernel.log" >&2
+    exit 1
+}
+python3 "$SCRIPT_DIR/parse_trace.py" "$WORK/kernel.log" "$OUT/trace_01.jsonl"
+python3 - "$OUT" "$SOURCE_COMMIT" "$IMAGE" "$PATCH" "$WORK/kernel.log" <<'PY'
+import hashlib, json, sys
+from pathlib import Path
+out, commit, image, patch, log = sys.argv[1:]
+out = Path(out)
+text = Path(log).read_text()
+# Keep the test output and result, without the large dependency/build log.
+start = text.index("=== SPIN_TV_BEGIN ===")
+(out / "kernel-test.txt").write_text(text[start:])
+manifest = {
+    "source_repository": "https://github.com/asterinas/asterinas",
+    "source_commit": commit,
+    "docker_image": image,
+    "patch": "data/patches/asterinas_tla_trace.patch",
+    "patch_sha256": hashlib.sha256(Path(patch).read_bytes()).hexdigest(),
+    "trace_sha256": hashlib.sha256((out / "trace_01.jsonl").read_bytes()).hexdigest(),
+    "test": "test_spin_tv_contract",
+    "capture_command": "bash scripts/harness/spin_tv/run.sh",
+    "scope": "Executed SpinTrace operations with three logical actors on one CPU; no synthetic events or blocking contention."
+}
+(out / "manifest.json").write_text(json.dumps(manifest, indent=2) + "\n")
+PY

tests/test_tv_examples/spin_contention.rs

@@ -0,0 +1,72 @@
+// Execute the patched acquisition/release methods with a deterministic CAS race.
+use std::sync::atomic::{AtomicBool, AtomicU64, Ordering};
+use std::sync::{Arc, Barrier};
+
+static FAILED_CAS: Barrier = Barrier::new(2);
+static RESUME_WAITER: Barrier = Barrier::new(2);
+static SEQUENCE: AtomicU64 = AtomicU64::new(0);
+
+struct ObservedLock(AtomicBool);
+
+impl ObservedLock {
+    fn compare_exchange(
+        &self,
+        current: bool,
+        new: bool,
+        success: Ordering,
+        failure: Ordering,
+    ) -> Result<bool, bool> {
+        let result = self.0.compare_exchange(current, new, success, failure);
+        if result.is_err() {
+            // Pause immediately after the failed atomic operation so the holder
+            // can release and finish logging before the waiter retries.
+            FAILED_CAS.wait();
+            RESUME_WAITER.wait();
+        }
+        result
+    }
+
+    fn store(&self, value: bool, order: Ordering) {
+        self.0.store(value, order);
+    }
+}
+
+struct SpinLockInner {
+    lock: ObservedLock,
+}
+
+struct SpinTrace {
+    inner: SpinLockInner,
+}
+
+impl SpinTrace {
+    // SPIN_TRACE_METHODS
+}
+
+fn trace_event(action: &str, _address: usize, actor: usize, held: bool) {
+    let seq = SEQUENCE.fetch_add(1, Ordering::Relaxed);
+    let state = if held { "locked" } else { "unlocked" };
+    println!(
+        "{{\"seq\":{seq},\"action\":\"{action}\",\"actor\":{actor},\"state\":\"{state}\",\"lock\":0}}"
+    );
+}
+
+fn main() {
+    let lock = Arc::new(SpinTrace {
+        inner: SpinLockInner {
+            lock: ObservedLock(AtomicBool::new(false)),
+        },
+    });
+    trace_event("TryAcquireBlocking", 0, 0, false);
+    lock.acquire_lock_with_id(0);
+    let waiter_lock = Arc::clone(&lock);
+    let waiter = std::thread::spawn(move || {
+        trace_event("TryAcquireBlocking", 0, 1, true);
+        waiter_lock.acquire_lock_with_id(1);
+        waiter_lock.release_lock(1);
+    });
+    FAILED_CAS.wait();
+    lock.release_lock(0);
+    RESUME_WAITER.wait();
+    waiter.join().unwrap();
+}