From 57e20a8df005ca36d614b2927410bf71423196cb Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:07:48 +0000 Subject: [PATCH 1/3] feat(publish): prototype generation-directory publish, with experiments and a model check MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PROTOTYPE, not wired into any subcommand. It follows the maintainer's decision on #264 to replace per-file writes with a generation-directory publish. It is here so the design can be judged on evidence before any output path uses it. - src/publish.rs: write a generation into .gen/.partial/, rename it complete, then under an advisory lock move the CURRENT manifest (JCS, with SHA-256 per file) unless a newer generation is already current. Mirrors at the old paths are refreshed by hard link and rename; old generations are collected. Lock-free readers retry when a generation is collected under them. - examples/publish_stress.rs: multi-process race, kill -9 crash and latency experiments comparing in-place fs::write, per-file rename and generation publish. - tests/publish_model.rs: an exhaustive explicit-state check of the protocol (up to 3 writers, 1 reader, a crash at every step, garbage collection of live and crashed writers' partial generations). P1–P3 hold. P4 (mirrors consistent after a crash) fails as expected, matching the crash experiment. Three mutants show the checker detects broken protocols. Two defects the experiments found are fixed here, each with a test that fails without the fix: GC raced a writer's rename of its own partial directory, and a reader could lose a generation to GC. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PFaqv6iBXrt3W5Akd1Fq5k --- examples/publish_stress.rs | 285 +++++++++++++++++++++ src/lib.rs | 1 + src/publish.rs | 508 +++++++++++++++++++++++++++++++++++++ tests/publish_model.rs | 365 ++++++++++++++++++++++++++ 4 files changed, 1159 insertions(+) create mode 100644 examples/publish_stress.rs create mode 100644 src/publish.rs create mode 100644 tests/publish_model.rs diff --git a/examples/publish_stress.rs b/examples/publish_stress.rs new file mode 100644 index 0000000..ffaf0c1 --- /dev/null +++ b/examples/publish_stress.rs @@ -0,0 +1,285 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +//! Experiments for `docs/design/GENERATION-PUBLISH.adoc`. +//! +//! Three ways to write the report set `S.json`, `S.kyaml`, +//! `S.attestation.json` are compared: +//! +//! - `inplace`: `fs::write` each file (main today); +//! - `perfile`: temp file + rename for each file (the withdrawn +//! `atomic_write` approach); +//! - `genset`: `panic_attack::publish` generation directories. +//! +//! ```text +//! cargo run --release --example publish_stress -- race +//! cargo run --release --example publish_stress -- crash +//! cargo run --release --example publish_stress -- bench +//! ``` +//! +//! Every count printed is measured; none is estimated. + +use panic_attack::publish::{self, Generation, Options}; +use sha2::{Digest, Sha256}; +use std::fs; +use std::path::{Path, PathBuf}; +use std::process::{Child, Command, Stdio}; +use std::time::{Duration, Instant}; + +const NAMES: [&str; 3] = ["S.json", "S.kyaml", "S.attestation.json"]; +const PAD: usize = 256 * 1024; + +fn main() { + let args: Vec = std::env::args().skip(1).collect(); + let a = |i: usize| args.get(i).map(String::as_str).unwrap_or(""); + let n = |i: usize| a(i).parse::().expect("number"); + match a(0) { + "race" => race(a(1), n(2), n(3), n(4)), + "crash" => crash(a(1), n(2)), + "bench" => bench(a(1), n(2) as usize, n(3)), + "writer" => writer(a(1), Path::new(a(2)), a(3), n(4), PAD), + "reader" => reader(a(1), Path::new(a(2)), n(3)), + _ => eprintln!("usage: see the module comment"), + } +} + +fn set_for(run: &str, pad: usize) -> [(String, Vec); 3] { + let json = format!("{{\"pad\":\"{}\",\"run\":\"{run}\"}}\n", "x".repeat(pad)); + let sha = hex::encode(Sha256::digest(json.as_bytes())); + let kyaml = format!( + "{{\n pad: \"{}\",\n run: \"{run}\",\n}}\n", + "x".repeat(pad) + ); + let sidecar = format!("{{\"report_sha256\":\"{sha}\",\"run\":\"{run}\"}}\n"); + [ + (NAMES[0].into(), json.into_bytes()), + (NAMES[1].into(), kyaml.into_bytes()), + (NAMES[2].into(), sidecar.into_bytes()), + ] +} + +fn write_set(mode: &str, dir: &Path, run: &str, pad: usize) { + let files = set_for(run, pad); + match mode { + "inplace" => { + for (name, bytes) in &files { + fs::write(dir.join(name), bytes).unwrap(); + } + } + "perfile" => { + for (name, bytes) in &files { + let tmp = dir.join(format!(".{name}.{}.tmp", publish::new_id().unwrap())); + let mut f = fs::File::create_new(&tmp).unwrap(); + std::io::Write::write_all(&mut f, bytes).unwrap(); + f.sync_all().unwrap(); + fs::rename(&tmp, dir.join(name)).unwrap(); + } + } + "genset" => { + let mut g = Generation::begin(&dir.join("S.json"), publish::new_id().unwrap()).unwrap(); + for (name, bytes) in &files { + g.write(name, bytes).unwrap(); + } + g.publish(&Options::default()).unwrap(); + } + other => panic!("unknown mode {other}"), + } +} + +fn writer(mode: &str, dir: &Path, id: &str, iters: u64, pad: usize) { + for i in 0..iters { + write_set(mode, dir, &format!("{id}-{i}"), pad); + } +} + +#[derive(Default, Debug)] +struct Tally { + reads: u64, + partial: u64, + torn: u64, + missing: u64, +} + +/// Classify one set of three byte strings. +fn classify(files: &[Vec], t: &mut Tally) { + t.reads += 1; + let json: Option = serde_json::from_slice(&files[0]).ok(); + let side: Option = serde_json::from_slice(&files[2]).ok(); + let kyaml_ok = files[1].ends_with(b"}\n"); + let (Some(json), Some(side), true) = (json, side, kyaml_ok) else { + t.partial += 1; + return; + }; + let kyaml = String::from_utf8_lossy(&files[1]); + let run = json["run"].as_str().unwrap_or(""); + let sha = hex::encode(Sha256::digest(&files[0])); + if side["run"] != run + || side["report_sha256"] != sha.as_str() + || !kyaml.contains(&format!("run: \"{run}\"")) + { + t.torn += 1; + } +} + +fn read_once(mode: &str, dir: &Path, t: &mut Tally) { + if mode == "genset-consistent" { + match publish::read_consistent(&publish::root_for(&dir.join("S.json"))) { + Ok(Some((_, files))) => { + let v: Vec> = NAMES.iter().map(|n| files[*n].clone()).collect(); + classify(&v, t) + } + Ok(None) => {} + Err(_) => t.missing += 1, + } + return; + } + let mut v = Vec::new(); + for name in NAMES { + match fs::read(dir.join(name)) { + Ok(b) => v.push(b), + Err(_) => { + t.missing += 1; + return; + } + } + } + classify(&v, t); +} + +fn reader(mode: &str, dir: &Path, millis: u64) { + let mut t = Tally::default(); + let end = Instant::now() + Duration::from_millis(millis); + while Instant::now() < end && !dir.join(".done").exists() { + read_once(mode, dir, &mut t); + } + println!("{} {} {} {}", t.reads, t.partial, t.torn, t.missing); +} + +fn me() -> PathBuf { + std::env::current_exe().unwrap() +} + +fn race(mode: &str, writers: u64, readers: u64, iters: u64) { + let dir = tempfile::tempdir().unwrap(); + write_set(mode, dir.path(), "seed-0", PAD); + let start = Instant::now(); + let ws: Vec = (0..writers) + .map(|w| { + Command::new(me()) + .args(["writer", mode]) + .arg(dir.path()) + .args([format!("w{w}"), iters.to_string()]) + .spawn() + .unwrap() + }) + .collect(); + // Readers of the plain paths, and for genset also manifest readers. + let mut read_modes = vec![mode.to_string()]; + if mode == "genset" { + read_modes.push("genset-consistent".into()); + } + let mut rs = Vec::new(); + for rm in &read_modes { + for _ in 0..readers { + rs.push(( + rm.clone(), + Command::new(me()) + .args(["reader", rm]) + .arg(dir.path()) + .arg("120000") + .stdout(Stdio::piped()) + .spawn() + .unwrap(), + )); + } + } + for mut w in ws { + assert!(w.wait().unwrap().success()); + } + let wall = start.elapsed(); + fs::write(dir.path().join(".done"), b"").unwrap(); + for rm in &read_modes { + let mut sum = [0u64; 4]; + for (m, r) in rs.iter_mut().filter(|(m, _)| m == rm) { + let _ = m; + let out = r.stdout.take().unwrap(); + let s = std::io::read_to_string(out).unwrap(); + for (i, x) in s.split_whitespace().enumerate() { + sum[i] += x.parse::().unwrap(); + } + } + for (_, r) in rs.iter_mut().filter(|(m, _)| m == rm) { + r.wait().unwrap(); + } + println!( + "race mode={mode} readers-of={rm} writers={writers} iters={iters} \ + writer_wall_ms={} reads={} partial={} torn={} missing={}", + wall.as_millis(), + sum[0], + sum[1], + sum[2], + sum[3] + ); + } + let mut t = Tally::default(); + read_once(mode, dir.path(), &mut t); + println!( + "race mode={mode} final-state partial={} torn={} missing={}", + t.partial, t.torn, t.missing + ); +} + +fn crash(mode: &str, trials: u64) { + let mut bad = Tally::default(); + let mut consistent_bad = 0u64; + for trial in 0..trials { + let dir = tempfile::tempdir().unwrap(); + write_set(mode, dir.path(), "seed-0", PAD); + let mut child = Command::new(me()) + .args(["writer", mode]) + .arg(dir.path()) + .args([format!("c{trial}"), "1000".into()]) + .spawn() + .unwrap(); + // Kill somewhere inside the write loop: 1–40 ms in. + std::thread::sleep(Duration::from_micros(1000 + (trial * 7919) % 39000)); + child.kill().unwrap(); + child.wait().unwrap(); + read_once(mode, dir.path(), &mut bad); + if mode == "genset" { + match publish::read_consistent(&publish::root_for(&dir.path().join("S.json"))) { + Ok(Some(_)) => {} + _ => consistent_bad += 1, + } + } + } + println!( + "crash mode={mode} trials={trials} after-kill: partial={} torn={} missing={}{}", + bad.partial, + bad.torn, + bad.missing, + if mode == "genset" { + format!(" manifest-read-failures={consistent_bad}") + } else { + String::new() + } + ); +} + +fn bench(mode: &str, bytes: usize, iters: u64) { + let dir = tempfile::tempdir().unwrap(); + let mut samples = Vec::with_capacity(iters as usize); + for i in 0..iters { + let t0 = Instant::now(); + write_set(mode, dir.path(), &format!("b-{i}"), bytes); + samples.push(t0.elapsed().as_micros() as u64); + } + samples.sort_unstable(); + let pct = |p: f64| samples[((samples.len() - 1) as f64 * p) as usize]; + println!( + "bench mode={mode} pad_bytes={bytes} iters={iters} p50_us={} p90_us={} max_us={}", + pct(0.5), + pct(0.9), + samples[samples.len() - 1] + ); +} diff --git a/src/lib.rs b/src/lib.rs index 6760498..5bfc4f0 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -40,6 +40,7 @@ pub mod kyaml; pub mod mass_panic; pub mod notify; pub mod panll; +pub mod publish; pub mod query; pub mod report; pub mod safe_path; diff --git a/src/publish.rs b/src/publish.rs new file mode 100644 index 0000000..81cdbb4 --- /dev/null +++ b/src/publish.rs @@ -0,0 +1,508 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +//! PROTOTYPE: publish a set of report files as one generation. +//! +//! Status: experimental, not wired into any subcommand. It exists to test +//! the design in `docs/design/GENERATION-PUBLISH.adoc` before anything uses +//! it. The design note records the open questions; the stress harness in +//! `examples/publish_stress.rs` holds the experiments. +//! +//! # Layout +//! +//! For a report named `S.json` in directory `D`: +//! +//! ```text +//! D/S.json, D/S.kyaml, ... mirrors: regular files, hard links into the +//! current generation (copies where links fail) +//! D/S.gen/lock advisory lock taken by publishers +//! D/S.gen/CURRENT JCS manifest naming the current generation +//! and the SHA-256 of each of its files +//! D/S.gen//S.json, ... one complete generation per directory +//! D/S.gen/.partial/ a generation still being written +//! ``` +//! +//! # Protocol +//! +//! 1. `begin`: create `.partial/`, `id` ordered by the run's start time. +//! 2. `write`: each file is created new inside it and synced. +//! 3. `publish`: sync the directory, rename it to `` (complete), then +//! under the lock: refuse if `CURRENT` names a newer generation, else +//! write `CURRENT` by temp-file + rename, sync `S.gen`, refresh the +//! mirrors by link + rename, and collect old generations. +//! +//! The invariants the protocol is meant to keep are stated in the design +//! note and model-checked in `docs/design/GenerationPublish.tla`. + +use serde::{Deserialize, Serialize}; +use sha2::{Digest, Sha256}; +use std::collections::BTreeMap; +use std::fs::{self, File, OpenOptions}; +use std::io::{self, Read, Write}; +use std::path::{Path, PathBuf}; +use std::time::{Duration, SystemTime, UNIX_EPOCH}; + +/// Name of the pointer file inside the generation root. +pub const CURRENT: &str = "CURRENT"; +const LOCK: &str = "lock"; +const PARTIAL: &str = ".partial"; + +/// The `CURRENT` manifest: which generation is current, and what it holds. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct Manifest { + /// The generation's directory name, which orders generations. + pub generation: String, + /// File name → lowercase hex SHA-256 of its bytes. + pub files: BTreeMap, +} + +/// A current generation read whole: its manifest and each file's bytes. +pub type Snapshot = (Manifest, BTreeMap>); + +/// What `publish` did. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Outcome { + /// This generation is now current. + Published, + /// A newer generation was already current; this one was not published. + Superseded { current: String }, +} + +/// Options for `publish`. +#[derive(Debug, Clone)] +pub struct Options { + /// Complete generations kept besides the current one. + pub keep: usize, + /// Partial generations older than this are treated as abandoned. + pub partial_grace: Duration, + /// Refresh the top-level mirrors after moving the pointer. + pub mirror: bool, +} + +impl Default for Options { + fn default() -> Self { + Self { + keep: 1, + partial_grace: Duration::from_secs(3600), + mirror: true, + } + } +} + +/// A generation being written. +#[derive(Debug)] +pub struct Generation { + base_dir: PathBuf, + root: PathBuf, + id: String, + partial: PathBuf, + files: BTreeMap, +} + +/// The generation root for a report at `report`: `.gen` beside it. +pub fn root_for(report: &Path) -> PathBuf { + let stem = report.file_stem().unwrap_or_default().to_string_lossy(); + parent_dir(report).join(format!("{stem}.gen")) +} + +/// A new generation id: 16 hex digits of Unix nanoseconds at the run's +/// start, then 16 random hex digits. Ids sort by start time as strings. +pub fn new_id() -> io::Result { + let nanos = SystemTime::now() + .duration_since(UNIX_EPOCH) + .map_err(io::Error::other)? + .as_nanos() as u64; + let mut random = [0u8; 8]; + getrandom::fill(&mut random).map_err(io::Error::other)?; + Ok(format!("{nanos:016x}{}", hex::encode(random))) +} + +impl Generation { + /// Start a generation for the report at `report`, with id `id` (from + /// [`new_id`], taken when the run started). + pub fn begin(report: &Path, id: String) -> io::Result { + let base_dir = parent_dir(report).to_path_buf(); + let root = root_for(report); + fs::create_dir_all(&root)?; + let partial = root.join(format!("{id}{PARTIAL}")); + fs::create_dir(&partial)?; + Ok(Self { + base_dir, + root, + id, + partial, + files: BTreeMap::new(), + }) + } + + /// The generation id. + pub fn id(&self) -> &str { + &self.id + } + + /// Write one file of the generation. `name` is a bare file name. + pub fn write(&mut self, name: &str, bytes: &[u8]) -> io::Result<()> { + if name.is_empty() || name.contains(['/', '\\']) || name == "." || name == ".." { + return Err(io::Error::new(io::ErrorKind::InvalidInput, "bad file name")); + } + let path = self.partial.join(name); + let mut file = new_file(&path, self.mode_of_current(name))?; + file.write_all(bytes)?; + file.sync_all()?; + self.files + .insert(name.to_owned(), hex::encode(Sha256::digest(bytes))); + Ok(()) + } + + /// The permission bits of `name` in the current generation, so a report + /// made private stays private in the next one. + fn mode_of_current(&self, name: &str) -> Option { + let current = read_current(&self.root).ok()??; + mode_of(&self.root.join(¤t.generation).join(name)) + } + + /// Complete the generation and make it current unless a newer one is. + pub fn publish(self, options: &Options) -> io::Result { + sync_dir(&self.partial)?; + let complete = self.root.join(&self.id); + fs::rename(&self.partial, &complete)?; + sync_dir(&self.root)?; + + let lock = OpenOptions::new() + .create(true) + .truncate(false) + .write(true) + .open(self.root.join(LOCK))?; + lock.lock()?; + + let outcome: io::Result = (|| { + if let Some(current) = read_current(&self.root)? { + if current.generation > self.id { + return Ok(Outcome::Superseded { + current: current.generation, + }); + } + } + let manifest = Manifest { + generation: self.id.clone(), + files: self.files.clone(), + }; + let bytes = crate::json::to_canonical_string(&manifest).map_err(io::Error::other)?; + replace_file(&self.root, CURRENT, bytes.as_bytes())?; + if options.mirror { + for name in self.files.keys() { + mirror(&complete.join(name), &self.base_dir, name)?; + } + sync_dir(&self.base_dir)?; + } + Ok(Outcome::Published) + })(); + if let Ok(Outcome::Superseded { .. }) = &outcome { + let _ = fs::remove_dir_all(&complete); + } + let collected = collect(&self.root, options); + let _ = lock.unlock(); + let outcome = outcome?; + collected?; + Ok(outcome) + } +} + +/// Read the `CURRENT` manifest, or `None` before the first publish. +pub fn read_current(root: &Path) -> io::Result> { + match fs::read(root.join(CURRENT)) { + Ok(bytes) => serde_json::from_slice(&bytes) + .map(Some) + .map_err(|e| io::Error::new(io::ErrorKind::InvalidData, e)), + Err(e) if e.kind() == io::ErrorKind::NotFound => Ok(None), + Err(e) => Err(e), + } +} + +/// Read the whole current generation and check it against its manifest. +/// A reader that wants one consistent set of files uses this, not the +/// mirrors. +/// +/// Readers take no lock. A generation can be collected between reading +/// `CURRENT` and opening its files, but only after a newer one became +/// current, so on "not found" the read starts again from `CURRENT`. It +/// gives up when `CURRENT` has not moved, since then the loss is real. +pub fn read_consistent(root: &Path) -> io::Result> { + const ATTEMPTS: usize = 16; + let mut last_error = None; + for _ in 0..ATTEMPTS { + let Some(manifest) = read_current(root)? else { + return Ok(None); + }; + match read_generation(root, &manifest) { + Ok(files) => return Ok(Some((manifest, files))), + Err(e) if e.kind() == io::ErrorKind::NotFound => { + let moved = + read_current(root)?.map(|m| m.generation) != Some(manifest.generation.clone()); + if !moved { + return Err(e); + } + last_error = Some(e); + } + Err(e) => return Err(e), + } + } + Err(last_error.unwrap_or_else(|| io::Error::other("generation kept moving"))) +} + +fn read_generation(root: &Path, manifest: &Manifest) -> io::Result>> { + let dir = root.join(&manifest.generation); + let mut files = BTreeMap::new(); + for (name, digest) in &manifest.files { + let mut bytes = Vec::new(); + File::open(dir.join(name))?.read_to_end(&mut bytes)?; + if hex::encode(Sha256::digest(&bytes)) != *digest { + return Err(io::Error::new( + io::ErrorKind::InvalidData, + format!("{name} does not match the manifest"), + )); + } + files.insert(name.clone(), bytes); + } + Ok(files) +} + +/// Point `dir/name` at `target` by hard link + rename; copy + rename where +/// the filesystem refuses the link. +fn mirror(target: &Path, dir: &Path, name: &str) -> io::Result<()> { + let tmp = dir.join(format!(".{name}.{}.mirror", new_id()?)); + if fs::hard_link(target, &tmp).is_err() { + fs::copy(target, &tmp)?; + File::open(&tmp)?.sync_all()?; + } + fs::rename(&tmp, dir.join(name)).inspect_err(|_| { + let _ = fs::remove_file(&tmp); + }) +} + +/// Replace `dir/name` with `bytes` by temp file + rename, then sync `dir`. +fn replace_file(dir: &Path, name: &str, bytes: &[u8]) -> io::Result<()> { + let tmp = dir.join(format!(".{name}.{}.tmp", new_id()?)); + let result: io::Result<()> = (|| { + let mut file = new_file(&tmp, None)?; + file.write_all(bytes)?; + file.sync_all()?; + fs::rename(&tmp, dir.join(name)) + })(); + if result.is_err() { + let _ = fs::remove_file(&tmp); + } + result?; + sync_dir(dir) +} + +/// Remove complete generations beyond `keep` older ones, and partial ones +/// past the grace period. Never removes the current generation. Called +/// with the lock held, but other writers create and rename their own +/// generations without it, so an entry can vanish between listing and use: +/// that is treated as already gone, not as an error. +fn collect(root: &Path, options: &Options) -> io::Result<()> { + let current = read_current(root)?.map(|m| m.generation); + let mut complete = Vec::new(); + for entry in fs::read_dir(root)? { + let entry = entry?; + let Some(file_type) = unless_gone(entry.file_type())? else { + continue; + }; + if !file_type.is_dir() { + continue; + } + let name = entry.file_name().to_string_lossy().into_owned(); + if let Some(id) = name.strip_suffix(PARTIAL) { + let Some(meta) = unless_gone(entry.metadata())? else { + continue; + }; + let age = meta.modified()?.elapsed().unwrap_or(Duration::ZERO); + if age > options.partial_grace && Some(id) != current.as_deref() { + unless_gone(fs::remove_dir_all(entry.path()))?; + } + } else { + complete.push(name); + } + } + complete.sort(); + let Some(current) = current else { + return Ok(()); + }; + // Keep the current generation and the `keep` newest older than it. + // Newer complete generations belong to writers waiting for the lock and + // are left alone. An older one not yet published can only be superseded + // (the pointer never moves backwards), so removing it is safe. + let older: Vec<_> = complete.iter().filter(|g| **g < current).collect(); + let keep_from = older.len().saturating_sub(options.keep); + for (i, g) in older.iter().enumerate() { + if i < keep_from { + unless_gone(fs::remove_dir_all(root.join(g)))?; + } + } + Ok(()) +} + +/// `Ok(None)` for "not found", so a vanished entry is skipped. +fn unless_gone(result: io::Result) -> io::Result> { + match result { + Ok(value) => Ok(Some(value)), + Err(e) if e.kind() == io::ErrorKind::NotFound => Ok(None), + Err(e) => Err(e), + } +} + +fn parent_dir(path: &Path) -> &Path { + match path.parent() { + Some(p) if !p.as_os_str().is_empty() => p, + _ => Path::new("."), + } +} + +fn new_file(path: &Path, mode: Option) -> io::Result { + let mut options = OpenOptions::new(); + options.write(true).create_new(true); + #[cfg(unix)] + { + use std::os::unix::fs::OpenOptionsExt; + options.mode(mode.unwrap_or(0o666) & 0o777); + } + #[cfg(not(unix))] + let _ = mode; + options.open(path) +} + +fn mode_of(path: &Path) -> Option { + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + let meta = fs::symlink_metadata(path).ok()?; + meta.is_file().then(|| meta.permissions().mode() & 0o777) + } + #[cfg(not(unix))] + { + let _ = path; + None + } +} + +fn sync_dir(dir: &Path) -> io::Result<()> { + #[cfg(unix)] + { + File::open(dir)?.sync_all() + } + #[cfg(not(unix))] + { + let _ = dir; + Ok(()) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn publish_set(report: &Path, tag: &str) -> Outcome { + let mut generation = Generation::begin(report, new_id().unwrap()).unwrap(); + generation + .write("S.json", format!("{{\"run\":\"{tag}\"}}\n").as_bytes()) + .unwrap(); + generation + .write("S.kyaml", format!("{{run: \"{tag}\"}}\n").as_bytes()) + .unwrap(); + generation.publish(&Options::default()).unwrap() + } + + #[test] + fn publishes_mirrors_and_manifest() { + let dir = tempfile::tempdir().unwrap(); + let report = dir.path().join("S.json"); + assert_eq!(publish_set(&report, "a"), Outcome::Published); + assert_eq!(fs::read_to_string(&report).unwrap(), "{\"run\":\"a\"}\n"); + let (manifest, files) = read_consistent(&root_for(&report)).unwrap().unwrap(); + assert_eq!(files.len(), 2); + assert_eq!(manifest.files.len(), 2); + assert!(fs::symlink_metadata(&report).unwrap().is_file()); + } + + #[test] + fn a_stale_generation_is_superseded() { + let dir = tempfile::tempdir().unwrap(); + let report = dir.path().join("S.json"); + let old_id = new_id().unwrap(); + std::thread::sleep(Duration::from_millis(2)); + publish_set(&report, "new"); + let mut stale = Generation::begin(&report, old_id).unwrap(); + stale.write("S.json", b"{\"run\":\"old\"}\n").unwrap(); + let outcome = stale.publish(&Options::default()).unwrap(); + assert!(matches!(outcome, Outcome::Superseded { .. })); + assert_eq!(fs::read_to_string(&report).unwrap(), "{\"run\":\"new\"}\n"); + } + + #[test] + fn keeps_current_and_one_older_generation() { + let dir = tempfile::tempdir().unwrap(); + let report = dir.path().join("S.json"); + for tag in ["a", "b", "c", "d"] { + publish_set(&report, tag); + } + let root = root_for(&report); + let gens = fs::read_dir(&root) + .unwrap() + .filter(|e| e.as_ref().unwrap().file_type().unwrap().is_dir()) + .count(); + assert_eq!(gens, 2); + } + + #[cfg(unix)] + #[test] + fn a_private_report_stays_private() { + use std::os::unix::fs::PermissionsExt; + let dir = tempfile::tempdir().unwrap(); + let report = dir.path().join("S.json"); + publish_set(&report, "a"); + fs::set_permissions(&report, fs::Permissions::from_mode(0o600)).unwrap(); + publish_set(&report, "b"); + let mode = fs::metadata(&report).unwrap().permissions().mode() & 0o777; + assert_eq!(mode, 0o600); + } + + #[test] + fn collect_skips_generations_renamed_while_it_lists() { + let dir = tempfile::tempdir().unwrap(); + let report = dir.path().join("S.json"); + publish_set(&report, "seed"); + let root = root_for(&report); + let options = Options { + partial_grace: Duration::ZERO, + ..Options::default() + }; + let stop = std::sync::Arc::new(std::sync::atomic::AtomicBool::new(false)); + let renamer = { + let (root, stop) = (root.clone(), stop.clone()); + std::thread::spawn(move || { + while !stop.load(std::sync::atomic::Ordering::Relaxed) { + let id = new_id().unwrap(); + let partial = root.join(format!("{id}{PARTIAL}")); + if fs::create_dir(&partial).is_ok() { + let _ = fs::rename(&partial, root.join(format!("{id}x"))); + let _ = fs::remove_dir(root.join(format!("{id}x"))); + } + } + }) + }; + let result = (0..20_000).try_for_each(|_| collect(&root, &options)); + stop.store(true, std::sync::atomic::Ordering::Relaxed); + renamer.join().unwrap(); + result.unwrap(); + } + + #[test] + fn rejects_path_names() { + let dir = tempfile::tempdir().unwrap(); + let mut generation = + Generation::begin(&dir.path().join("S.json"), new_id().unwrap()).unwrap(); + assert!(generation.write("../x", b"").is_err()); + assert!(generation.write("..", b"").is_err()); + } +} diff --git a/tests/publish_model.rs b/tests/publish_model.rs new file mode 100644 index 0000000..a503995 --- /dev/null +++ b/tests/publish_model.rs @@ -0,0 +1,365 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +//! Exhaustive explicit-state check of the generation-publish protocol in +//! `src/publish.rs` (design: `docs/design/GENERATION-PUBLISH.adoc`). +//! +//! This is an abstract model, not the code: each step below stands for one +//! filesystem operation the code performs, and every interleaving of up to +//! three writers and one reader is explored, with a crash (SIGKILL: the +//! process stops, the kernel drops its lock) allowed at every writer step. +//! It checks process crashes only. Power loss and fsync ordering are out of +//! scope here. +//! +//! Invariants checked in every reachable state: +//! - P1: `CURRENT` only ever names a complete generation. +//! - P2: `CURRENT` never moves to an older generation. +//! - P3: the manifest reader never returns a generation that is not +//! complete, and never fails while `CURRENT` names a readable one. +//! - P4 (expected to FAIL with crashes, see the design note): once no writer +//! is running, the top-level mirrors all name the current generation. + +use std::collections::{HashSet, VecDeque}; + +const FILES: usize = 2; + +#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)] +enum Gen { + Absent, + Partial, + Complete, + Removed, +} + +#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)] +enum Pc { + Start, + Writing, + Renamed, + Locked, + Swapped, + Mirrored(u8), + Superseded, + Collected, + Done, + Crashed, + /// Its partial generation was collected under it, so its next write or + /// rename failed with "not found" and it exited with an error. + Failed, +} + +#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)] +enum Reader { + Idle, + Got(u8), + Missed(u8), + Ok(u8), + Failed, +} + +#[derive(Clone, PartialEq, Eq, Hash, Debug)] +struct State { + gens: Vec, + pc: Vec, + current: Option, + lock: Option, + mirrors: [Option; FILES], + reader: Reader, + retries: u8, +} + +struct Config { + writers: u8, + keep: usize, + crashes: bool, + reader_retries: bool, + /// A deliberate defect, to show the invariants can fail (see the + /// `mutant_*` tests). `None` is the protocol as implemented. + mutant: Option, +} + +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +enum Mutant { + /// Move `CURRENT` without comparing generation ids. + NoSupersedeCheck, + /// Swap the pointer before renaming `.partial` to complete. + SwapBeforeComplete, + /// Collect the current generation along with the older ones. + CollectCurrent, +} + +/// Writer `i` has generation id `i`: ids order generations by start time, +/// and the interleavings decide who finishes first. +fn successors(s: &State, c: &Config) -> Vec { + let mut out = Vec::new(); + for i in 0..c.writers { + let w = i as usize; + let mut n = s.clone(); + let step = match s.pc[w] { + Pc::Start => { + n.gens[w] = Gen::Partial; + n.pc[w] = Pc::Writing; + true + } + Pc::Writing => { + if c.mutant == Some(Mutant::SwapBeforeComplete) && s.lock.is_none() { + // Publish while the generation is still partial. + n.current = Some(i); + } + if s.gens[w] == Gen::Removed { + n.pc[w] = Pc::Failed; + } else { + n.gens[w] = Gen::Complete; + n.pc[w] = Pc::Renamed; + } + true + } + Pc::Renamed if s.lock.is_none() => { + n.lock = Some(i); + n.pc[w] = Pc::Locked; + true + } + Pc::Locked => { + if c.mutant != Some(Mutant::NoSupersedeCheck) && s.current.is_some_and(|g| g > i) { + n.gens[w] = Gen::Removed; + n.pc[w] = Pc::Superseded; + } else { + n.current = Some(i); + n.pc[w] = Pc::Swapped; + } + true + } + Pc::Swapped => { + n.mirrors[0] = Some(i); + n.pc[w] = Pc::Mirrored(1); + true + } + Pc::Mirrored(k) if (k as usize) < FILES => { + n.mirrors[k as usize] = Some(i); + n.pc[w] = Pc::Mirrored(k + 1); + true + } + Pc::Mirrored(_) | Pc::Superseded => { + collect(&mut n, c.keep, c.mutant == Some(Mutant::CollectCurrent)); + n.pc[w] = Pc::Collected; + true + } + Pc::Collected => { + n.lock = None; + n.pc[w] = Pc::Done; + true + } + _ => false, + }; + if step { + out.push(n); + } + if c.crashes && !matches!(s.pc[w], Pc::Done | Pc::Crashed | Pc::Failed) { + let mut n = s.clone(); + n.pc[w] = Pc::Crashed; + if n.lock == Some(i) { + n.lock = None; + } + out.push(n); + } + // Grace-period removal of a partial generation. `collect` cannot tell + // a crashed writer from one that has stalled past the grace period, so + // a live writer's partial generation can be removed too. + if s.gens[w] == Gen::Partial { + let mut n = s.clone(); + n.gens[w] = Gen::Removed; + out.push(n); + } + } + // Reader. + let mut n = s.clone(); + let reader_step = match s.reader { + Reader::Idle => match s.current { + Some(g) => { + n.reader = Reader::Got(g); + true + } + None => false, + }, + Reader::Got(g) => { + n.reader = if s.gens[g as usize] == Gen::Complete { + Reader::Ok(g) + } else { + Reader::Missed(g) + }; + true + } + Reader::Missed(g) => { + n.reader = if c.reader_retries && s.current != Some(g) && s.retries < 3 { + n.retries += 1; + Reader::Idle + } else { + Reader::Failed + }; + true + } + Reader::Ok(_) | Reader::Failed => false, + }; + if reader_step { + out.push(n); + } + out +} + +fn collect(s: &mut State, keep: usize, also_current: bool) { + if also_current { + if let Some(g) = s.current { + s.gens[g as usize] = Gen::Removed; + } + } + let Some(current) = s.current else { return }; + let older: Vec = (0..s.gens.len()) + .filter(|&g| (g as u8) < current && s.gens[g] == Gen::Complete) + .collect(); + let keep_from = older.len().saturating_sub(keep); + for &g in &older[..keep_from] { + s.gens[g] = Gen::Removed; + } +} + +#[derive(Debug, Default)] +struct Report { + states: usize, + p1: Option, + p2: Option<(State, State)>, + p3: Option, + p4: Option, +} + +fn explore(c: &Config) -> Report { + let w = c.writers as usize; + let init = State { + gens: vec![Gen::Absent; w], + pc: vec![Pc::Start; w], + current: None, + lock: None, + mirrors: [None; FILES], + reader: Reader::Idle, + retries: 0, + }; + let mut seen = HashSet::new(); + let mut queue = VecDeque::from([init.clone()]); + seen.insert(init); + let mut r = Report::default(); + while let Some(s) = queue.pop_front() { + r.states += 1; + if let Some(g) = s.current { + if s.gens[g as usize] != Gen::Complete && r.p1.is_none() { + r.p1 = Some(s.clone()); + } + } + if s.reader == Reader::Failed && r.p3.is_none() { + r.p3 = Some(s.clone()); + } + let quiet = s.lock.is_none() + && s.pc + .iter() + .all(|p| matches!(p, Pc::Done | Pc::Crashed | Pc::Failed | Pc::Start)); + if quiet + && s.current.is_some() + && s.mirrors.iter().any(|m| *m != s.current) + && r.p4.is_none() + { + r.p4 = Some(s.clone()); + } + for n in successors(&s, c) { + if let (Some(a), Some(b)) = (s.current, n.current) { + if b < a && r.p2.is_none() { + r.p2 = Some((s.clone(), n.clone())); + } + } + if seen.insert(n.clone()) { + queue.push_back(n); + } + } + } + r +} + +#[test] +fn p1_p2_p3_hold_for_every_interleaving_with_crashes() { + for keep in [0, 1] { + for writers in [2, 3] { + let r = explore(&Config { + writers, + keep, + crashes: true, + reader_retries: true, + mutant: None, + }); + eprintln!("writers={writers} keep={keep} states={}", r.states); + assert!(r.p1.is_none(), "P1 violated: {:?}", r.p1); + assert!(r.p2.is_none(), "P2 violated: {:?}", r.p2); + assert!(r.p3.is_none(), "P3 violated: {:?}", r.p3); + } + } +} + +#[test] +fn without_the_retry_a_reader_can_fail() { + let r = explore(&Config { + writers: 2, + keep: 0, + crashes: false, + reader_retries: false, + mutant: None, + }); + assert!(r.p3.is_some(), "expected a P3 counterexample without retry"); +} + +#[test] +fn mirrors_are_consistent_when_quiet_without_crashes() { + let r = explore(&Config { + writers: 3, + keep: 1, + crashes: false, + reader_retries: true, + mutant: None, + }); + assert!(r.p4.is_none(), "P4 violated: {:?}", r.p4); +} + +#[test] +fn a_crash_can_leave_the_mirrors_torn() { + let r = explore(&Config { + writers: 2, + keep: 1, + crashes: true, + reader_retries: true, + mutant: None, + }); + let s = r.p4.expect("expected the known P4 counterexample"); + eprintln!("P4 counterexample: {s:?}"); +} + +/// Each mutant breaks one step of the protocol. The checker must find a +/// counterexample for each, or the invariants above would prove nothing. +fn mutant(m: Mutant) -> Report { + explore(&Config { + writers: 2, + keep: 1, + crashes: true, + reader_retries: true, + mutant: Some(m), + }) +} + +#[test] +fn mutant_without_the_supersede_check_moves_current_backwards() { + assert!(mutant(Mutant::NoSupersedeCheck).p2.is_some()); +} + +#[test] +fn mutant_swapping_before_completion_points_at_a_partial_generation() { + assert!(mutant(Mutant::SwapBeforeComplete).p1.is_some()); +} + +#[test] +fn mutant_collecting_the_current_generation_breaks_the_pointer() { + assert!(mutant(Mutant::CollectCurrent).p1.is_some()); +} From c851f6e7353cf3a8044f18e30e9009bfaea8f13c Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:22:45 +0000 Subject: [PATCH 2/3] fix(publish): return errors from the stress example instead of panicking Hypatia flagged 25 unwrap() calls, one expect() and one panic! in examples/publish_stress.rs (CWE-754). The example now returns anyhow::Result throughout: bad arguments and I/O failures exit with a message and status 1. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PFaqv6iBXrt3W5Akd1Fq5k --- examples/publish_stress.rs | 155 ++++++++++++++++++++----------------- 1 file changed, 84 insertions(+), 71 deletions(-) diff --git a/examples/publish_stress.rs b/examples/publish_stress.rs index ffaf0c1..be478c5 100644 --- a/examples/publish_stress.rs +++ b/examples/publish_stress.rs @@ -19,6 +19,7 @@ //! //! Every count printed is measured; none is estimated. +use anyhow::{bail, Context, Result}; use panic_attack::publish::{self, Generation, Options}; use sha2::{Digest, Sha256}; use std::fs; @@ -29,17 +30,20 @@ use std::time::{Duration, Instant}; const NAMES: [&str; 3] = ["S.json", "S.kyaml", "S.attestation.json"]; const PAD: usize = 256 * 1024; -fn main() { +fn main() -> Result<()> { let args: Vec = std::env::args().skip(1).collect(); let a = |i: usize| args.get(i).map(String::as_str).unwrap_or(""); - let n = |i: usize| a(i).parse::().expect("number"); + let n = |i: usize| -> Result { + a(i).parse::() + .with_context(|| format!("argument {i} must be a number, got {:?}", a(i))) + }; match a(0) { - "race" => race(a(1), n(2), n(3), n(4)), - "crash" => crash(a(1), n(2)), - "bench" => bench(a(1), n(2) as usize, n(3)), - "writer" => writer(a(1), Path::new(a(2)), a(3), n(4), PAD), - "reader" => reader(a(1), Path::new(a(2)), n(3)), - _ => eprintln!("usage: see the module comment"), + "race" => race(a(1), n(2)?, n(3)?, n(4)?), + "crash" => crash(a(1), n(2)?), + "bench" => bench(a(1), usize::try_from(n(2)?)?, n(3)?), + "writer" => writer(a(1), Path::new(a(2)), a(3), n(4)?, PAD), + "reader" => reader(a(1), Path::new(a(2)), n(3)?), + _ => bail!("usage: see the module comment"), } } @@ -58,38 +62,40 @@ fn set_for(run: &str, pad: usize) -> [(String, Vec); 3] { ] } -fn write_set(mode: &str, dir: &Path, run: &str, pad: usize) { +fn write_set(mode: &str, dir: &Path, run: &str, pad: usize) -> Result<()> { let files = set_for(run, pad); match mode { "inplace" => { for (name, bytes) in &files { - fs::write(dir.join(name), bytes).unwrap(); + fs::write(dir.join(name), bytes)?; } } "perfile" => { for (name, bytes) in &files { - let tmp = dir.join(format!(".{name}.{}.tmp", publish::new_id().unwrap())); - let mut f = fs::File::create_new(&tmp).unwrap(); - std::io::Write::write_all(&mut f, bytes).unwrap(); - f.sync_all().unwrap(); - fs::rename(&tmp, dir.join(name)).unwrap(); + let tmp = dir.join(format!(".{name}.{}.tmp", publish::new_id()?)); + let mut f = fs::File::create_new(&tmp)?; + std::io::Write::write_all(&mut f, bytes)?; + f.sync_all()?; + fs::rename(&tmp, dir.join(name))?; } } "genset" => { - let mut g = Generation::begin(&dir.join("S.json"), publish::new_id().unwrap()).unwrap(); + let mut g = Generation::begin(&dir.join("S.json"), publish::new_id()?)?; for (name, bytes) in &files { - g.write(name, bytes).unwrap(); + g.write(name, bytes)?; } - g.publish(&Options::default()).unwrap(); + g.publish(&Options::default())?; } - other => panic!("unknown mode {other}"), + other => bail!("unknown mode {other}"), } + Ok(()) } -fn writer(mode: &str, dir: &Path, id: &str, iters: u64, pad: usize) { +fn writer(mode: &str, dir: &Path, id: &str, iters: u64, pad: usize) -> Result<()> { for i in 0..iters { - write_set(mode, dir, &format!("{id}-{i}"), pad); + write_set(mode, dir, &format!("{id}-{i}"), pad)?; } + Ok(()) } #[derive(Default, Debug)] @@ -125,7 +131,10 @@ fn read_once(mode: &str, dir: &Path, t: &mut Tally) { if mode == "genset-consistent" { match publish::read_consistent(&publish::root_for(&dir.join("S.json"))) { Ok(Some((_, files))) => { - let v: Vec> = NAMES.iter().map(|n| files[*n].clone()).collect(); + let v: Vec> = NAMES + .iter() + .map(|n| files.get(*n).cloned().unwrap_or_default()) + .collect(); classify(&v, t) } Ok(None) => {} @@ -146,33 +155,34 @@ fn read_once(mode: &str, dir: &Path, t: &mut Tally) { classify(&v, t); } -fn reader(mode: &str, dir: &Path, millis: u64) { +fn reader(mode: &str, dir: &Path, millis: u64) -> Result<()> { let mut t = Tally::default(); let end = Instant::now() + Duration::from_millis(millis); while Instant::now() < end && !dir.join(".done").exists() { read_once(mode, dir, &mut t); } println!("{} {} {} {}", t.reads, t.partial, t.torn, t.missing); + Ok(()) } -fn me() -> PathBuf { - std::env::current_exe().unwrap() +fn me() -> Result { + Ok(std::env::current_exe()?) } -fn race(mode: &str, writers: u64, readers: u64, iters: u64) { - let dir = tempfile::tempdir().unwrap(); - write_set(mode, dir.path(), "seed-0", PAD); +fn race(mode: &str, writers: u64, readers: u64, iters: u64) -> Result<()> { + let dir = tempfile::tempdir()?; + write_set(mode, dir.path(), "seed-0", PAD)?; let start = Instant::now(); - let ws: Vec = (0..writers) + let ws = (0..writers) .map(|w| { - Command::new(me()) + Command::new(me()?) .args(["writer", mode]) .arg(dir.path()) .args([format!("w{w}"), iters.to_string()]) .spawn() - .unwrap() + .context("spawning a writer") }) - .collect(); + .collect::>>()?; // Readers of the plain paths, and for genset also manifest readers. let mut read_modes = vec![mode.to_string()]; if mode == "genset" { @@ -181,35 +191,32 @@ fn race(mode: &str, writers: u64, readers: u64, iters: u64) { let mut rs = Vec::new(); for rm in &read_modes { for _ in 0..readers { - rs.push(( - rm.clone(), - Command::new(me()) - .args(["reader", rm]) - .arg(dir.path()) - .arg("120000") - .stdout(Stdio::piped()) - .spawn() - .unwrap(), - )); + let child = Command::new(me()?) + .args(["reader", rm]) + .arg(dir.path()) + .arg("120000") + .stdout(Stdio::piped()) + .spawn()?; + rs.push((rm.clone(), child)); } } for mut w in ws { - assert!(w.wait().unwrap().success()); + let status = w.wait()?; + if !status.success() { + bail!("a writer failed: {status}"); + } } let wall = start.elapsed(); - fs::write(dir.path().join(".done"), b"").unwrap(); + fs::write(dir.path().join(".done"), b"")?; for rm in &read_modes { let mut sum = [0u64; 4]; - for (m, r) in rs.iter_mut().filter(|(m, _)| m == rm) { - let _ = m; - let out = r.stdout.take().unwrap(); - let s = std::io::read_to_string(out).unwrap(); - for (i, x) in s.split_whitespace().enumerate() { - sum[i] += x.parse::().unwrap(); - } - } for (_, r) in rs.iter_mut().filter(|(m, _)| m == rm) { - r.wait().unwrap(); + let out = r.stdout.take().context("reader stdout")?; + let s = std::io::read_to_string(out)?; + for (slot, x) in sum.iter_mut().zip(s.split_whitespace()) { + *slot += x.parse::()?; + } + r.wait()?; } println!( "race mode={mode} readers-of={rm} writers={writers} iters={iters} \ @@ -227,24 +234,24 @@ fn race(mode: &str, writers: u64, readers: u64, iters: u64) { "race mode={mode} final-state partial={} torn={} missing={}", t.partial, t.torn, t.missing ); + Ok(()) } -fn crash(mode: &str, trials: u64) { +fn crash(mode: &str, trials: u64) -> Result<()> { let mut bad = Tally::default(); let mut consistent_bad = 0u64; for trial in 0..trials { - let dir = tempfile::tempdir().unwrap(); - write_set(mode, dir.path(), "seed-0", PAD); - let mut child = Command::new(me()) + let dir = tempfile::tempdir()?; + write_set(mode, dir.path(), "seed-0", PAD)?; + let mut child = Command::new(me()?) .args(["writer", mode]) .arg(dir.path()) .args([format!("c{trial}"), "1000".into()]) - .spawn() - .unwrap(); + .spawn()?; // Kill somewhere inside the write loop: 1–40 ms in. std::thread::sleep(Duration::from_micros(1000 + (trial * 7919) % 39000)); - child.kill().unwrap(); - child.wait().unwrap(); + child.kill()?; + child.wait()?; read_once(mode, dir.path(), &mut bad); if mode == "genset" { match publish::read_consistent(&publish::root_for(&dir.path().join("S.json"))) { @@ -264,22 +271,28 @@ fn crash(mode: &str, trials: u64) { String::new() } ); + Ok(()) } -fn bench(mode: &str, bytes: usize, iters: u64) { - let dir = tempfile::tempdir().unwrap(); - let mut samples = Vec::with_capacity(iters as usize); +fn bench(mode: &str, bytes: usize, iters: u64) -> Result<()> { + let dir = tempfile::tempdir()?; + let mut samples = Vec::new(); for i in 0..iters { let t0 = Instant::now(); - write_set(mode, dir.path(), &format!("b-{i}"), bytes); - samples.push(t0.elapsed().as_micros() as u64); + write_set(mode, dir.path(), &format!("b-{i}"), bytes)?; + samples.push(t0.elapsed().as_micros()); } samples.sort_unstable(); - let pct = |p: f64| samples[((samples.len() - 1) as f64 * p) as usize]; + let pct = |p: usize| { + samples + .get(samples.len().saturating_sub(1) * p / 100) + .copied() + }; println!( - "bench mode={mode} pad_bytes={bytes} iters={iters} p50_us={} p90_us={} max_us={}", - pct(0.5), - pct(0.9), - samples[samples.len() - 1] + "bench mode={mode} pad_bytes={bytes} iters={iters} p50_us={:?} p90_us={:?} max_us={:?}", + pct(50), + pct(90), + samples.last() ); + Ok(()) } From 48296bb5ae5740f315662ba1f4c11ec0d9ecae55 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:22:21 +0000 Subject: [PATCH 3/3] feat(publish): model-check the protocol with TLC; design note; proof-status rows MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - verification/proofs/tlaplus/GenerationPublish.tla: the protocol for TLC, step for step like tests/publish_model.rs. Eight configs, each stating its expected outcome. P1–P3 pass for 3 writers with keep 0 and 1 (up to 17,744 distinct states). P4 passes without crashes and fails after one, the documented mirror limit. The reader without a retry fails P3. Three mutants each fail P1 or P2. - check.sh checks the jar's SHA-256 (tla2tools v1.7.4, TLC 2.19) and fails on any unexpected outcome. It fails both ways: on a wrong jar, and on a planted wrong expectation. - verify.yml gains a `tlaplus` job that runs it, recording a PROOF-POLICY §6 deviation (TLC is not in Guix or the container yet). actionlint 1.7.7 is clean, and the job uses only the already-locked checkout pin. - The "swap before complete" mutant now moves the pointer when the partial generation is created, in both models, matching its name. - docs/design/GENERATION-PUBLISH.adoc: layout, protocol, guarantees, measurements and open questions. It records the owner's decision to keep hard-link mirrors and document the crash limit. - PROOF-NEEDS.adoc: a TESTED row for the protocol, with bounds and the §4 exception, and an OPEN Creusot/Pearlite + Verus row for the pure decisions. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PFaqv6iBXrt3W5Akd1Fq5k --- .github/workflows/verify.yml | 29 +++ PROOF-NEEDS.adoc | 26 +++ docs/design/GENERATION-PUBLISH.adoc | 144 ++++++++++++++ src/publish.rs | 4 +- tests/publish_model.rs | 14 +- .../proofs/tlaplus/GenerationPublish.tla | 186 ++++++++++++++++++ verification/proofs/tlaplus/MirrorsCrash.cfg | 12 ++ .../proofs/tlaplus/MirrorsNoCrash.cfg | 12 ++ .../proofs/tlaplus/MutantCollectCurrent.cfg | 13 ++ .../proofs/tlaplus/MutantNoSupersede.cfg | 13 ++ .../tlaplus/MutantSwapBeforeComplete.cfg | 13 ++ verification/proofs/tlaplus/NoRetry.cfg | 12 ++ verification/proofs/tlaplus/Safety3Keep0.cfg | 13 ++ verification/proofs/tlaplus/Safety3Keep1.cfg | 13 ++ verification/proofs/tlaplus/check.sh | 55 ++++++ 15 files changed, 552 insertions(+), 7 deletions(-) create mode 100644 docs/design/GENERATION-PUBLISH.adoc create mode 100644 verification/proofs/tlaplus/GenerationPublish.tla create mode 100644 verification/proofs/tlaplus/MirrorsCrash.cfg create mode 100644 verification/proofs/tlaplus/MirrorsNoCrash.cfg create mode 100644 verification/proofs/tlaplus/MutantCollectCurrent.cfg create mode 100644 verification/proofs/tlaplus/MutantNoSupersede.cfg create mode 100644 verification/proofs/tlaplus/MutantSwapBeforeComplete.cfg create mode 100644 verification/proofs/tlaplus/NoRetry.cfg create mode 100644 verification/proofs/tlaplus/Safety3Keep0.cfg create mode 100644 verification/proofs/tlaplus/Safety3Keep1.cfg create mode 100755 verification/proofs/tlaplus/check.sh diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index e133c95..54a38cc 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -242,3 +242,32 @@ jobs: assert any(i.get('status') not in ('analyzed', 'excluded') for i in coverage['inputs']), coverage print(f"coverage={coverage['status']} (gap recorded)") PY + + # The generation-publish protocol (src/publish.rs) is model-checked with TLC, + # PROOF-POLICY §4's worked exception for concurrency protocols. Results are + # TESTED with the bounds in each .cfg, never PROVEN. Every config states its + # expected outcome; the expected violations (the documented mirror limit and + # three mutants) show the invariants can fail. + # + # Deviation (PROOF-POLICY §6), state: open. Leg: protocol model check. Tool: + # tla2tools.jar v1.7.4 (TLC 2.19), SHA-256 below, checked by check.sh. Why not + # Guix or the container: neither provides TLC yet. Java comes from the runner. + tlaplus: + name: TLA+ model check (GenerationPublish) + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Fetch the pinned TLC and model-check every config + shell: bash + run: | + set -euo pipefail + java -version + tools_dir=$(mktemp -d) + trap 'rm -rf "$tools_dir"' EXIT + curl --fail --silent --show-error --location --max-time 120 \ + https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar \ + --output "$tools_dir/tla2tools.jar" + TLA2TOOLS="$tools_dir/tla2tools.jar" bash verification/proofs/tlaplus/check.sh diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index e09653d..cd8d6ca 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -66,11 +66,37 @@ obligation. The gateway octad projection is lossy by design, so this property also does not establish a faithful hexad↔octad map. |=== +=== Model-Checked (TESTED, bounded) + +[width="100%",cols="26%,30%,44%",options="header",] +|=== +|Obligation |Artefact |Status and bounds +|Generation-publish protocol P1–P3 (prototype, `src/publish.rs`; +design `docs/design/GENERATION-PUBLISH.adoc`) |`verification/proofs/tlaplus/GenerationPublish.tla` +(TLC 2.19, tla2tools v1.7.4, run by `verify.yml` job `tlaplus`) and +`tests/publish_model.rs` (independent explicit-state checker) |*TESTED*: up to +3 writers, 1 reader, 2 files, crash at every writer step, collection of crashed +and live writers' partial generations, `keep` 0 and 1. P1 (`CURRENT` names a +complete generation), P2 (never moves backwards) and P3 (manifest reader never +fails) hold. P4 (mirrors consistent once quiet) holds without crashes and +*fails* after a crash, the documented limit. Three mutants each violate P1 or +P2, so the invariants are not vacuous. *PROOF-POLICY §4 exception*: a +concurrency protocol over crash interleavings, which Creusot and Verus do not +state. *§6 deviation (open)*: TLC is fetched from its release, digest-checked, +because neither Guix nor the container provides it yet. +|=== + === What Still Needs Proving [width="100%",cols="51%,27%,22%",options="header",] |=== |Component |What |Why +|Generation publish: pure decisions (`src/publish.rs`) |*OPEN* (PROOF-POLICY +§1.2): Creusot/Pearlite and Verus contracts for the supersede comparison and +the collect selection (never removes the current or a newer generation; keeps +the `keep` newest older ones) |The model check covers the protocol, not the Rust +code; these tie the implementation to P1 and P2 + |*Layer 1.0 — stripBlockComments + Strings + Composition + Position-Preservation* (issue #114) |Block-comment (`+/* */+`) and string-literal (`+"..."+`) strippers with same mutual-recursive shape; diff --git a/docs/design/GENERATION-PUBLISH.adoc b/docs/design/GENERATION-PUBLISH.adoc new file mode 100644 index 0000000..c0e71d1 --- /dev/null +++ b/docs/design/GENERATION-PUBLISH.adoc @@ -0,0 +1,144 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Generation-directory publish +:toc: + +Status: *prototype* (`src/publish.rs`), not wired into any subcommand. + +== Why + +`assail` writes up to three files for one run: the JSON report, its KYAML +copy and the `--attest` sidecar. Writing them one at a time with `fs::write` +leaves three gaps: + +* a crash can leave a partial file; +* two runs into the same paths can interleave, leaving files from different + runs side by side; +* a symbolic link swapped in between the preflight check and the write is + written through. + +hyperpolymath/panic-attack#264 chose to close these for every output mode +with one design: publish each run as a *generation*, and move a single +pointer to it. + +== Layout + +For a report `D/S.json`: + +[cols="1,3"] +|=== +|`D/S.gen/.partial/` |A generation still being written. +|`D/S.gen//` |One complete generation: `S.json`, `S.kyaml`, `S.attestation.json`. +|`D/S.gen/CURRENT` |The pointer: a JCS manifest naming the current generation and the SHA-256 of each file in it. +|`D/S.gen/lock` |An advisory lock (`File::lock`) taken by publishers only. +|`D/S.json`, `D/S.kyaml`, … |Mirrors: hard links into the current generation (copies where linking fails). +|=== + +`` is 16 hex digits of Unix nanoseconds at the run's start followed by 16 +random hex digits, so ids sort by start time. + +== Protocol + +. *Write.* Create `.partial/`. Create each file new inside it and sync it. +. *Complete.* Sync the directory, rename it to ``, sync `S.gen`. +. *Publish, under the lock:* +.. if `CURRENT` names a newer generation, this run is *superseded*: remove + its generation and stop; +.. otherwise replace `CURRENT` (temporary file, sync, rename, sync `S.gen`); +.. refresh each mirror by hard link and rename; +.. collect: remove complete generations older than the current one, except + the newest `keep` (default 1), and partial generations older than the + grace period (default 1 hour). + +*Readers* take no lock. A reader that needs one consistent set reads +`CURRENT`, then the generation's files, and checks each against the +manifest's digest. If the generation was collected in between, it starts +again, but only if `CURRENT` has moved; otherwise the loss is real and it +reports an error. + +== What is guaranteed + +Checked by TLC (`verification/proofs/tlaplus/`) and, independently, by the +explicit-state checker in `tests/publish_model.rs`. Both are `TESTED` under +PROOF-POLICY §4, with the bounds in each configuration: up to 3 writers, +1 reader and 2 files, a crash at every writer step, and collection of the +partial generations of crashed and live writers. + +[cols="1,4,1"] +|=== +|Property |Statement |Result + +|P1 |`CURRENT` only ever names a complete generation. |holds +|P2 |`CURRENT` never moves to an older generation. |holds +|P3 |A manifest reader never fails or returns a mixed set. |holds +|P4 |When no writer is running, every mirror names the current generation. |holds without crashes; *fails after a crash* (see below) +|=== + +Each checker also runs three mutants of the protocol, each with one +defect. Each mutant violates P1 or P2, which shows the invariants are not +vacuous: + +* no supersede check; +* publish before completion; +* collect the current generation. + +Process crashes only: a SIGKILL stops the process and the kernel releases +its lock. Power loss, and the ordering of `fsync` against it, is not modelled +or tested. + +== The mirror limit (owner decision: hard links, documented) + +Mirrors are refreshed one at a time after `CURRENT` moves. A crash between +two refreshes leaves the mirrors from different generations: each file is +complete, but the set is mixed. The checkers find this (P4), and the crash +experiment measured it: 3 torn mirror sets in 300 kills, against none for +manifest readers. + +This is accepted and documented, because: + +* each mirror is always a complete file, never a partial one; +* the attestation sidecar seals the report's SHA-256, so + `attest verify --report` detects a mixed report and sidecar; +* the next successful publish repairs the mirrors; +* a reader that needs a consistent set reads through `CURRENT`. + +The alternative considered was a single `current` symlink with fixed +top-level symlinks through it. It is crash-consistent on Unix, but needs +symlinks (Windows falls back) and must exempt its own links from `assail`'s +symlink refusal. It was not chosen. + +== Measurements + +Measured on Linux 6.18, ext4, 4 cores, with `examples/publish_stress.rs`. +Three strategies are compared: `fs::write` in place, a rename per file, and +generation publish. + +[cols="2,1,1,1,1"] +|=== +| |in place |rename per file |generation, mirrors |generation, manifest + +|race, 3 writers × 150 runs: partial reads |7931 / 8424 |0 / 3209 |0 / 6058 |0 / 2500 +|race: mixed sets read |182 |3008 |67 |0 +|kill -9, 300 trials: partial / mixed left |176 / 13 |0 / 155 |0 / 3 |0 / 0 +|100 races: mixed final state |0 |7 |0 |0 +|p50 latency, 1 KiB / 256 KiB / 4 MiB |0.27 / 1.0 / 12.5 ms |1.2 / 3.2 / 23.8 ms |2.7 / 4.6 / 33.7 ms | +|=== + +The extra cost is mostly the directory syncs. Against a scan that takes +seconds, a few milliseconds is negligible. + +== Open before wiring + +* *Rust verification* (PROOF-POLICY §1.2): Creusot/Pearlite and Verus for + the pure decisions: the supersede comparison, and the collect selection + (never the current generation or a newer one). `OPEN`. +* *Generation id format*: align with the estate identifier policy (UUIDv7 or + v8), keeping the start-time ordering. +* *Windows*: there is no Windows run yet. `std::fs::rename` replaces + directories differently there, and a file that is open cannot be removed. +* *What a replacement keeps*: new files inherit the directory's default ACLs, + not the previous file's ACLs, xattrs, labels or owner. A private report + stays private because each file takes the mode of its predecessor in the + current generation. +* *Wiring*: `assail` (all output modes) and the preflight in + hyperpolymath/panic-attack#264 and hyperpolymath/panic-attack#274. diff --git a/src/publish.rs b/src/publish.rs index 81cdbb4..7f6d4bf 100644 --- a/src/publish.rs +++ b/src/publish.rs @@ -32,7 +32,9 @@ //! mirrors by link + rename, and collect old generations. //! //! The invariants the protocol is meant to keep are stated in the design -//! note and model-checked in `docs/design/GenerationPublish.tla`. +//! note and model-checked with TLC in +//! `verification/proofs/tlaplus/GenerationPublish.tla` and, independently, by +//! the explicit-state checker in `tests/publish_model.rs`. use serde::{Deserialize, Serialize}; use sha2::{Digest, Sha256}; diff --git a/tests/publish_model.rs b/tests/publish_model.rs index a503995..881b10d 100644 --- a/tests/publish_model.rs +++ b/tests/publish_model.rs @@ -2,7 +2,9 @@ // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell //! Exhaustive explicit-state check of the generation-publish protocol in -//! `src/publish.rs` (design: `docs/design/GENERATION-PUBLISH.adoc`). +//! `src/publish.rs` (design: `docs/design/GENERATION-PUBLISH.adoc`). The same +//! model is checked with TLC in `verification/proofs/tlaplus/`; the two are +//! kept step for step alike so each cross-checks the other. //! //! This is an abstract model, not the code: each step below stands for one //! filesystem operation the code performs, and every interleaving of up to @@ -82,7 +84,7 @@ struct Config { enum Mutant { /// Move `CURRENT` without comparing generation ids. NoSupersedeCheck, - /// Swap the pointer before renaming `.partial` to complete. + /// Move `CURRENT` as soon as the partial generation is created. SwapBeforeComplete, /// Collect the current generation along with the older ones. CollectCurrent, @@ -98,14 +100,14 @@ fn successors(s: &State, c: &Config) -> Vec { let step = match s.pc[w] { Pc::Start => { n.gens[w] = Gen::Partial; + if c.mutant == Some(Mutant::SwapBeforeComplete) { + // Publish the generation while it is still partial. + n.current = Some(i); + } n.pc[w] = Pc::Writing; true } Pc::Writing => { - if c.mutant == Some(Mutant::SwapBeforeComplete) && s.lock.is_none() { - // Publish while the generation is still partial. - n.current = Some(i); - } if s.gens[w] == Gen::Removed { n.pc[w] = Pc::Failed; } else { diff --git a/verification/proofs/tlaplus/GenerationPublish.tla b/verification/proofs/tlaplus/GenerationPublish.tla new file mode 100644 index 0000000..f8a46d1 --- /dev/null +++ b/verification/proofs/tlaplus/GenerationPublish.tla @@ -0,0 +1,186 @@ +---------------------------- MODULE GenerationPublish ---------------------------- +\* SPDX-License-Identifier: MPL-2.0 +\* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +\* +\* The generation-publish protocol of src/publish.rs, for TLC. +\* +\* PROOF-POLICY section 4 exception: TLA+ model checking of a concurrency +\* protocol, the policy's worked example. The obligation is a property of +\* interleavings of several processes and of crashes between file-system +\* operations; neither Creusot nor Verus states that. A finite check is +\* reported as TESTED with the bounds in the .cfg files, never as PROVEN. +\* tests/publish_model.rs checks the same model independently in Rust. +\* +\* Each step is one file-system operation of the code. Writer w's generation +\* id is w, so ids order generations by start time and the interleavings +\* decide who finishes first. A crash is SIGKILL: the process stops and the +\* kernel releases its lock. Power loss and fsync ordering are out of scope. + +EXTENDS Naturals, FiniteSets + +CONSTANTS + Writers, \* writer ids, e.g. 1..3 + NFiles, \* files per generation, mirrored one at a time + Keep, \* complete generations kept besides the current one + Crashes, \* TRUE: a writer may crash at any step + Retry, \* TRUE: the reader retries when its generation vanished + MaxRetries, + Mutant \* "none", or one deliberate defect (see the Mutant* configs) + +VARIABLES gen, pc, mi, current, lock, mirror, rpc, rgen, retries + +vars == <> + +None == 0 +Files == 1..NFiles + +TypeOK == + /\ gen \in [Writers -> {"absent", "partial", "complete", "removed"}] + /\ pc \in [Writers -> {"start", "writing", "renamed", "locked", "mirroring", + "superseded", "collected", "done", "crashed", "failed"}] + /\ mi \in [Writers -> 0..NFiles] + /\ current \in Writers \cup {None} + /\ lock \in Writers \cup {None} + /\ mirror \in [Files -> Writers \cup {None}] + /\ rpc \in {"idle", "got", "missed", "ok", "failed"} + /\ rgen \in Writers \cup {None} + /\ retries \in 0..MaxRetries + +Init == + /\ gen = [w \in Writers |-> "absent"] + /\ pc = [w \in Writers |-> "start"] + /\ mi = [w \in Writers |-> 0] + /\ current = None + /\ lock = None + /\ mirror = [f \in Files |-> None] + /\ rpc = "idle" + /\ rgen = None + /\ retries = 0 + +\* Collect: remove complete generations older than the current one, except +\* the Keep newest of them. +Collected(g, cur) == + LET older == {h \in Writers : h < cur /\ g[h] = "complete"} + doomed == {h \in older : Cardinality({k \in older : k > h}) >= Keep} + IN [h \in Writers |-> + IF h \in doomed \/ (Mutant = "collectcurrent" /\ h = cur) + THEN "removed" ELSE g[h]] + +Begin(w) == + /\ pc[w] = "start" + /\ gen' = [gen EXCEPT ![w] = "partial"] + /\ pc' = [pc EXCEPT ![w] = "writing"] + \* Mutant: publish the generation while it is still partial. + /\ current' = IF Mutant = "swapbeforecomplete" THEN w ELSE current + /\ UNCHANGED <> + +\* Rename .partial to . Fails if collect removed the partial +\* generation under a writer that stalled past the grace period. +Rename(w) == + /\ pc[w] = "writing" + /\ IF gen[w] = "removed" + THEN /\ pc' = [pc EXCEPT ![w] = "failed"] + /\ UNCHANGED gen + ELSE /\ gen' = [gen EXCEPT ![w] = "complete"] + /\ pc' = [pc EXCEPT ![w] = "renamed"] + /\ UNCHANGED <> + +Acquire(w) == + /\ pc[w] = "renamed" + /\ lock = None + /\ lock' = w + /\ pc' = [pc EXCEPT ![w] = "locked"] + /\ UNCHANGED <> + +\* Under the lock: refuse if a newer generation is current, else move CURRENT. +Swap(w) == + /\ pc[w] = "locked" + /\ IF Mutant /= "nosupersede" /\ current /= None /\ current > w + THEN /\ gen' = [gen EXCEPT ![w] = "removed"] + /\ pc' = [pc EXCEPT ![w] = "superseded"] + /\ UNCHANGED current + ELSE /\ current' = w + /\ pc' = [pc EXCEPT ![w] = "mirroring"] + /\ UNCHANGED gen + /\ UNCHANGED <> + +MirrorStep(w) == + /\ pc[w] = "mirroring" + /\ mi[w] < NFiles + /\ mirror' = [mirror EXCEPT ![mi[w] + 1] = w] + /\ mi' = [mi EXCEPT ![w] = mi[w] + 1] + /\ UNCHANGED <> + +Collect(w) == + /\ \/ pc[w] = "mirroring" /\ mi[w] = NFiles + \/ pc[w] = "superseded" + /\ gen' = IF current = None THEN gen ELSE Collected(gen, current) + /\ pc' = [pc EXCEPT ![w] = "collected"] + /\ UNCHANGED <> + +Release(w) == + /\ pc[w] = "collected" + /\ lock' = None + /\ pc' = [pc EXCEPT ![w] = "done"] + /\ UNCHANGED <> + +Crash(w) == + /\ Crashes + /\ pc[w] \notin {"done", "crashed", "failed"} + /\ pc' = [pc EXCEPT ![w] = "crashed"] + /\ lock' = IF lock = w THEN None ELSE lock + /\ UNCHANGED <> + +\* Grace-period removal of a partial generation, crashed or merely stalled. +GcPartial(w) == + /\ gen[w] = "partial" + /\ gen' = [gen EXCEPT ![w] = "removed"] + /\ UNCHANGED <> + +\* The lock-free manifest reader: read CURRENT, open its generation, and on +\* "not found" start again only if CURRENT has moved. +ReadPointer == + /\ rpc = "idle" + /\ current /= None + /\ rpc' = "got" + /\ rgen' = current + /\ UNCHANGED <> + +OpenGeneration == + /\ rpc = "got" + /\ rpc' = IF gen[rgen] = "complete" THEN "ok" ELSE "missed" + /\ UNCHANGED <> + +Recheck == + /\ rpc = "missed" + /\ IF Retry /\ current /= rgen /\ retries < MaxRetries + THEN /\ rpc' = "idle" + /\ retries' = retries + 1 + ELSE /\ rpc' = "failed" + /\ UNCHANGED retries + /\ UNCHANGED <> + +Next == + \/ \E w \in Writers : + Begin(w) \/ Rename(w) \/ Acquire(w) \/ Swap(w) \/ MirrorStep(w) + \/ Collect(w) \/ Release(w) \/ Crash(w) \/ GcPartial(w) + \/ ReadPointer \/ OpenGeneration \/ Recheck + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +\* P1: CURRENT only ever names a complete generation. +CurrentIsComplete == current /= None => gen[current] = "complete" + +\* P2: CURRENT never moves to an older generation (an action property). +CurrentMonotone == [][current /= None => current' /= None /\ current' >= current]_vars + +\* P3: the manifest reader never fails. +ReaderNeverFails == rpc /= "failed" + +\* P4: once no writer runs, every mirror names the current generation. +\* Expected to FAIL when Crashes is TRUE (the documented mirror limit). +Quiet == lock = None /\ \A w \in Writers : pc[w] \in {"start", "done", "crashed", "failed"} +MirrorsConsistentWhenQuiet == + (Quiet /\ current /= None) => \A f \in Files : mirror[f] = current +============================================================================= diff --git a/verification/proofs/tlaplus/MirrorsCrash.cfg b/verification/proofs/tlaplus/MirrorsCrash.cfg new file mode 100644 index 0000000..98352fa --- /dev/null +++ b/verification/proofs/tlaplus/MirrorsCrash.cfg @@ -0,0 +1,12 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* Expected: violation of MirrorsConsistentWhenQuiet (documented mirror limit) +CONSTANTS + Writers = {1, 2} + NFiles = 2 + Keep = 1 + Crashes = TRUE + Retry = TRUE + MaxRetries = 3 + Mutant = "none" +SPECIFICATION Spec +INVARIANTS MirrorsConsistentWhenQuiet diff --git a/verification/proofs/tlaplus/MirrorsNoCrash.cfg b/verification/proofs/tlaplus/MirrorsNoCrash.cfg new file mode 100644 index 0000000..0bf8ac4 --- /dev/null +++ b/verification/proofs/tlaplus/MirrorsNoCrash.cfg @@ -0,0 +1,12 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* Expected: pass +CONSTANTS + Writers = {1, 2, 3} + NFiles = 2 + Keep = 1 + Crashes = FALSE + Retry = TRUE + MaxRetries = 3 + Mutant = "none" +SPECIFICATION Spec +INVARIANTS TypeOK MirrorsConsistentWhenQuiet diff --git a/verification/proofs/tlaplus/MutantCollectCurrent.cfg b/verification/proofs/tlaplus/MutantCollectCurrent.cfg new file mode 100644 index 0000000..6b556f4 --- /dev/null +++ b/verification/proofs/tlaplus/MutantCollectCurrent.cfg @@ -0,0 +1,13 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* Expected: violation of CurrentIsComplete +CONSTANTS + Writers = {1, 2} + NFiles = 2 + Keep = 1 + Crashes = TRUE + Retry = TRUE + MaxRetries = 3 + Mutant = "collectcurrent" +SPECIFICATION Spec +INVARIANTS CurrentIsComplete +PROPERTIES CurrentMonotone diff --git a/verification/proofs/tlaplus/MutantNoSupersede.cfg b/verification/proofs/tlaplus/MutantNoSupersede.cfg new file mode 100644 index 0000000..cf5c123 --- /dev/null +++ b/verification/proofs/tlaplus/MutantNoSupersede.cfg @@ -0,0 +1,13 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* Expected: violation of CurrentMonotone +CONSTANTS + Writers = {1, 2} + NFiles = 2 + Keep = 1 + Crashes = TRUE + Retry = TRUE + MaxRetries = 3 + Mutant = "nosupersede" +SPECIFICATION Spec +INVARIANTS CurrentIsComplete +PROPERTIES CurrentMonotone diff --git a/verification/proofs/tlaplus/MutantSwapBeforeComplete.cfg b/verification/proofs/tlaplus/MutantSwapBeforeComplete.cfg new file mode 100644 index 0000000..31d8b83 --- /dev/null +++ b/verification/proofs/tlaplus/MutantSwapBeforeComplete.cfg @@ -0,0 +1,13 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* Expected: violation of CurrentIsComplete +CONSTANTS + Writers = {1, 2} + NFiles = 2 + Keep = 1 + Crashes = TRUE + Retry = TRUE + MaxRetries = 3 + Mutant = "swapbeforecomplete" +SPECIFICATION Spec +INVARIANTS CurrentIsComplete +PROPERTIES CurrentMonotone diff --git a/verification/proofs/tlaplus/NoRetry.cfg b/verification/proofs/tlaplus/NoRetry.cfg new file mode 100644 index 0000000..e5c3a3e --- /dev/null +++ b/verification/proofs/tlaplus/NoRetry.cfg @@ -0,0 +1,12 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* Expected: violation of ReaderNeverFails +CONSTANTS + Writers = {1, 2} + NFiles = 2 + Keep = 0 + Crashes = FALSE + Retry = FALSE + MaxRetries = 3 + Mutant = "none" +SPECIFICATION Spec +INVARIANTS ReaderNeverFails diff --git a/verification/proofs/tlaplus/Safety3Keep0.cfg b/verification/proofs/tlaplus/Safety3Keep0.cfg new file mode 100644 index 0000000..086633d --- /dev/null +++ b/verification/proofs/tlaplus/Safety3Keep0.cfg @@ -0,0 +1,13 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* Expected: pass +CONSTANTS + Writers = {1, 2, 3} + NFiles = 2 + Keep = 0 + Crashes = TRUE + Retry = TRUE + MaxRetries = 3 + Mutant = "none" +SPECIFICATION Spec +INVARIANTS TypeOK CurrentIsComplete ReaderNeverFails +PROPERTIES CurrentMonotone diff --git a/verification/proofs/tlaplus/Safety3Keep1.cfg b/verification/proofs/tlaplus/Safety3Keep1.cfg new file mode 100644 index 0000000..7c27098 --- /dev/null +++ b/verification/proofs/tlaplus/Safety3Keep1.cfg @@ -0,0 +1,13 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* Expected: pass +CONSTANTS + Writers = {1, 2, 3} + NFiles = 2 + Keep = 1 + Crashes = TRUE + Retry = TRUE + MaxRetries = 3 + Mutant = "none" +SPECIFICATION Spec +INVARIANTS TypeOK CurrentIsComplete ReaderNeverFails +PROPERTIES CurrentMonotone diff --git a/verification/proofs/tlaplus/check.sh b/verification/proofs/tlaplus/check.sh new file mode 100755 index 0000000..a390e8c --- /dev/null +++ b/verification/proofs/tlaplus/check.sh @@ -0,0 +1,55 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# Model-check GenerationPublish.tla with every .cfg beside it. +# +# Each .cfg states its expected outcome on its second line: +# "\* Expected: pass" TLC must finish with no error; +# "\* Expected: violation of ..." TLC must report violated. +# The expected violations are the documented mirror limit, the reader +# without a retry, and three deliberate mutants: they show the invariants +# can fail. A config that does anything else fails the run. +# +# Usage: TLA2TOOLS=/path/to/tla2tools.jar verification/proofs/tlaplus/check.sh +# The jar must be the pinned release below; its digest is checked first. +set -euo pipefail + +TLA2TOOLS_VERSION=v1.7.4 +TLA2TOOLS_SHA256=936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88 + +jar=${TLA2TOOLS:?set TLA2TOOLS to tla2tools.jar ($TLA2TOOLS_VERSION)} +dir=$(cd "$(dirname "$0")" && pwd) +echo "$TLA2TOOLS_SHA256 $jar" | sha256sum --check --quiet + +work=$(mktemp -d) +trap 'rm -rf "$work"' EXIT +failures=0 +for cfg in "$dir"/*.cfg; do + name=$(basename "$cfg" .cfg) + expected=$(sed -n '2s/^\\\* Expected: //p' "$cfg") + log="$work/$name.log" + set +e + java -XX:+UseParallelGC -cp "$jar" tlc2.TLC -workers auto -deadlock \ + -metadir "$work/$name.states" -config "$cfg" "$dir/GenerationPublish.tla" >"$log" 2>&1 + set -e + states=$(grep -oE '[0-9]+ distinct states found' "$log" | tail -1 || true) + case "$expected" in + pass) + if grep -q 'No error has been found' "$log"; then + echo "PASS $name: no error ($states)" + else + echo "FAIL $name: expected no error"; sed -n '1,40p' "$log"; failures=$((failures + 1)) + fi ;; + "violation of "*) + prop=${expected#violation of }; prop=${prop%% *} + if grep -qE "(Invariant|Action property) $prop is violated" "$log"; then + echo "PASS $name: $prop violated, as expected ($states)" + else + echo "FAIL $name: expected $prop to be violated"; sed -n '1,40p' "$log"; failures=$((failures + 1)) + fi ;; + *) + echo "FAIL $name: no 'Expected:' line"; failures=$((failures + 1)) ;; + esac +done +exit "$failures"