From 64ac8dab940746f38534ac33a1f1fb86ad6a84d9 Mon Sep 17 00:00:00 2001 From: Dimitri Kennedy <344842+roodboi@users.noreply.github.com> Date: Thu, 5 Nov 2026 17:56:38 -0500 Subject: [PATCH 1/3] feat(native): admit build storage, prune build cache and reclaim superseded build images - A cold native build needs at least 6 GiB free on the guest storage disk, or twice the last verified image of the same key; otherwise it refuses with native_build_storage before any receipt or client effect. Nothing is deleted to make room. Receipts record the verified image size. - After each verified build, BuildKit cache is pruned to 8 GiB through the engine's build-prune endpoint (cache records only). A failed prune leaves the build result in place. - runtime reclaim-build-images --json removes, without force, only build images that carry exactly this pool's ownership labels, that no build receipt names as current, and that no retained graph state (graphs, native graphs, archive) mentions. It runs under the provider lease, refuses while a build is admitted, and removes nothing when the graph state scan meets a symlink, special file, unreadable entry or bound. The engine's own refusal keeps images any container uses. Every kept image is reported with its reason. - New TLA+ model tests/models/tla/native-build-retention (6,181 states) with three guard-removal controls: reclaim ignoring retained references, adoption without the label/incarnation check, down ignoring the build fence. Registered in the runtime model contracts and coverage reference. Refs HACK-1270 Co-Authored-By: Claude Opus 5.5 --- docs/guides/native-candidate.md | 12 + docs/reference/v5-model-coverage.md | 2 + packages/runtime-core/README.md | 6 +- packages/runtime-core/src/main.rs | 8 + .../runtime-core/src/provider/image_build.rs | 92 +++- .../src/provider/image_build/reclaim.rs | 423 ++++++++++++++++++ .../src/provider/image_build/tests.rs | 133 +++++- scripts/lib/tla-runtime-models.ts | 36 ++ tests/models/tla/README.md | 24 + .../native-build-retention/BuildRetention.tla | 115 +++++ .../down-under-build.cfg | 4 + .../foreign-adoption.cfg | 4 + .../tla/native-build-retention/negative.cfg | 4 + .../tla/native-build-retention/positive.cfg | 4 + 14 files changed, 862 insertions(+), 5 deletions(-) create mode 100644 packages/runtime-core/src/provider/image_build/reclaim.rs create mode 100644 tests/models/tla/native-build-retention/BuildRetention.tla create mode 100644 tests/models/tla/native-build-retention/down-under-build.cfg create mode 100644 tests/models/tla/native-build-retention/foreign-adoption.cfg create mode 100644 tests/models/tla/native-build-retention/negative.cfg create mode 100644 tests/models/tla/native-build-retention/positive.cfg diff --git a/docs/guides/native-candidate.md b/docs/guides/native-candidate.md index 74caf19b2..9f4f986fb 100644 --- a/docs/guides/native-candidate.md +++ b/docs/guides/native-candidate.md @@ -485,6 +485,18 @@ linked, mode-`0600` file owned by you), because build-argument values are in it: - `runtime down` refuses while a build runs. Ctrl-C or SIGTERM cancels the build and stops the client's whole process group; so does the time budget (default 30 minutes, at most 2 hours). +- A cold build needs at least 6 GiB free on the runtime's storage disk, or twice the + last image of the same build if that is larger; otherwise it refuses with + `native_build_storage` and deletes nothing. After each successful build, BuildKit's + cache is pruned to 8 GiB. The cache holds only build steps; pruning never removes + images, containers or volumes. + +`runtime reclaim-build-images --json` removes build images that a newer build of the +same key replaced. It keeps every image a build receipt names as current, every image +that any retained run's saved state mentions, every image a container still uses (the +engine refuses those), and every image whose ownership labels are not exactly this +runtime's. It refuses while a build runs, and removes nothing if it cannot read all +saved run state. The report lists removed images and why each other one was kept. Before startup, network-tool preparation additionally requires all four pinned Alpine aarch64 APKs in a current-user-owned private directory (mode `0700`), with diff --git a/docs/reference/v5-model-coverage.md b/docs/reference/v5-model-coverage.md index 9f229fe79..973afee48 100644 --- a/docs/reference/v5-model-coverage.md +++ b/docs/reference/v5-model-coverage.md @@ -44,6 +44,7 @@ must be attached to the eventual exact integration revision. | Concurrent stop/publication; route claim and relay lifetime | native-route-stop, shared-https-lifetime, previous-boot-shared-https, relay-lifecycle-barrier, relay-authorization, relay-staging, relay-fence | Fenced route removal, relay owner, ready/removed protocol, authenticated observations | Native DNS/TLS/browser behavior; old-boot uncertainty and external routing. | | Shared host helper instance: overlapping ups, session adoption, stale create decisions, replacement before finalize, epoch-record failure, interrupted cleanup, concurrent down, displaced launches, failed down session stop | shared-helper-instance | `src/lib/project-shared-helpers.ts` (shutdown generation, `assertCurrent`, `SharedHelperSessionOwnership`); `src/lib/project-lifecycle-controller.ts` session decision, the locked creation transaction (revalidate, publish, create, environment, record, stop on failure, all under one lock), launches fenced by the lock and a token check, abort and signal cleanup through the same epoch decision (`runIfOwned`), an unknown exact-presence answer failing the inspection, and the locked conditional finalize; `stopSessionBeforeReleasingHelpers` (down, restart, native retirement keep holders when the session stop fails); `runMuxCommand` bounds every lifecycle and backend mux call so it settles before the lock is released, and reports a timeout as unknown (never absence); `tests/mux-command-timeout.test.ts`; `tests/project-lifecycle-controller-ownership.test.ts`, `tests/project-shared-helpers.test.ts`, `tests/native-project-down.test.ts`, e2e `shared-host-helpers` | Helper holder/rollback and claim protocol are not modeled (claim fixtures cover them); timeout settlement is an assumption the code does not guarantee (a killed tmux client's queued command may still apply, so a late kill or window command can reach a newer session; consequences and the session-ID fence, not in this slice, are in the README); zellij is refused for shared-helper lifecycle sessions (token written after creation); the gap between a down's session stop and its release (an up that captured after the stopping mark can still succeed there) is a documented first-slice limitation; real mux/process/lock-file behavior. | | Dependency rebind, incomplete initializer, terminal reuse | dependency-rebind, stopped-pool-startup, restore-history | Dependency claim/readiness, saved execution, restore history and source convergence tests | Actual installer failure, cache corruption, retained application state and resource plateau. | +| Native image builds: unleased build versus engine stop, crash mid-build, storage recreation, foreign or forged images, reclamation versus retained graph references | native-build-retention | `provider::image_build` (shared build fence, per-key lock, incarnation/boot/engine recheck and label check at adoption, dead-attempt recording) and `image_build::reclaim` (owned labels, current receipts, retained graph state scan, engine non-force removal); `image_build` regressions | One key and namespace; an orphaned client after a host crash is not modeled (the fence is released with its holder); real BuildKit, engine removal semantics and guest storage are host evidence. | | MCP cold start, cancellation and duplicate launches | mcp-startup, mcp-startup-cancellation | Shared MCP bundle identity, startup deduplication and cancellation regressions | Fresh supported client sessions, full workflow coverage and measured overhead (WU16/WU20/WU28). | | Software install/upgrade/rollback, active launcher versus selection, compatibility | **Coverage gap:** no maintained model here is an installer/selection refinement | `scripts/install-prerelease.py`, prerelease-install/Python installer tests, candidate-install contract | Add a bounded selection/lock/crash/compatibility model before primary-driver promotion; real official-artifact upgrade/rollback still required. | | Primary-driver promotion and rollback to stable | **Coverage gap:** staged readiness policy is not an implemented state machine proof | Reviewed release manifest, per-project opt-in, explicit stable/candidate ownership records | No active-project switch until exact candidate/artifact and rollback/data compatibility are qualified. | @@ -86,6 +87,7 @@ liveness/reachability controls have their own documented assumptions. | [fence-pending](../../tests/models/tla/fence-pending/Fence.tla) | 7 | 2 | | [relay-staging](../../tests/models/tla/relay-staging/Stage.tla) | 9 | 2 | | [relay-fence](../../tests/models/tla/relay-fence/RelayFence.tla) | 16 | 2 | +| [native-build-retention](../../tests/models/tla/native-build-retention/BuildRetention.tla) | 6,181 | 4 | | [shared-helper-instance](../../tests/models/tla/shared-helper-instance/Instance.tla) | 7,649 | 11 | | [restore-history](../../tests/models/tla/restore-history/RestoreHistory.tla) | See named result contract | 2 | | [graph-admission](../../tests/models/tla/graph-admission/Admission.tla) | See named result contract | 2 | diff --git a/packages/runtime-core/README.md b/packages/runtime-core/README.md index db8af2a41..aca2f2762 100644 --- a/packages/runtime-core/README.md +++ b/packages/runtime-core/README.md @@ -485,7 +485,11 @@ build fence, cancellation and timeout rules are documented in that module. Egres pools give dockerd a fixed default bridge (`10.213.255.0/24`, `icc=false`) that only BuildKit `RUN` steps use; `guest-build-network.sh` isolates it from the guest, the host gateway and link-local metadata, and the engine client refuses any container create -that does not name an owned network or `none`. Native `up` does not call the build +that does not name an owned network or `none`. Cold builds need free guest storage +(at least 6 GiB, or twice the key's last image), successful builds prune BuildKit +cache to 8 GiB, and `runtime reclaim-build-images` removes only owned, superseded, +unreferenced images (`provider/image_build/reclaim.rs`; model +`tests/models/tla/native-build-retention`). Native `up` does not call the build operation yet. Source binaries embed their build checkout. If a copied Cargo target directory diff --git a/packages/runtime-core/src/main.rs b/packages/runtime-core/src/main.rs index a10acd084..5b9fdcb7f 100644 --- a/packages/runtime-core/src/main.rs +++ b/packages/runtime-core/src/main.rs @@ -103,6 +103,7 @@ Usage: hack-local runtime prepared-base remove --base-id [--store ] [--json] hack-local runtime admit-image --reference <[namespace/]repository[:tag][@sha256:digest]|sha256:image-id> --json hack-local runtime build-image --request --json + hack-local runtime reclaim-build-images --json hack-local runtime ensure-image --reference <[namespace/]repository[:tag]|[namespace/]repository@sha256:digest> --json hack-local runtime resolve-image --reference <[namespace/]repository[:tag]> --json hack-local runtime fetch-image --reference <[namespace/]repository@sha256:digest> --archive [--json] @@ -956,6 +957,13 @@ fn run() -> Result<(), CandidateError> { Path::new(request), )?)?; } + ["runtime", "reclaim-build-images", "--json"] => { + print_json( + &hack_runtime_core::provider::image_build::reclaim::reclaim_build_images( + &discover_candidate(&requested)?, + )?, + )?; + } ["runtime", "admit-image", "--reference", reference, "--json"] => { // Pure: no candidate discovery, network, credentials or runtime effects. print_json(&hack_runtime_core::provider::registry_image::admit( diff --git a/packages/runtime-core/src/provider/image_build.rs b/packages/runtime-core/src/provider/image_build.rs index ff6268d46..bd305f905 100644 --- a/packages/runtime-core/src/provider/image_build.rs +++ b/packages/runtime-core/src/provider/image_build.rs @@ -53,6 +53,7 @@ use std::{ time::{Duration, Instant}, }; +pub mod reclaim; #[cfg(test)] mod tests; @@ -73,6 +74,13 @@ const MAX_METADATA_BYTES: u64 = 1024 * 1024; const MAX_IGNORE_BYTES: u64 = 1024 * 1024; const MAX_ARGS: usize = 64; const MAX_ARG_BYTES: usize = 64 * 1024; +const GIB: u64 = 1024 * 1024 * 1024; +/// A cold build needs this much free guest storage, or twice the key's last verified +/// image size when that is larger. Admission refuses; it never deletes to make room. +const STORAGE_FLOOR: u64 = 6 * GIB; +/// BuildKit cache kept after each successful build. The cache in this engine is created +/// only by Hack builds and is regenerable; pruning never touches images or volumes. +pub(super) const CACHE_BUDGET: u64 = 8 * GIB; /// Labels a Dockerfile (or a base image) must not set on an image Hack runs: the same /// reserved ownership namespaces the frontend refuses on authored services. const RESERVED_LABEL_PREFIXES: [&str; 5] = [ @@ -150,6 +158,10 @@ pub struct BuildOutcome { pub reused: bool, /// Named build context to the pinned reference it resolved to, for this image. pub base_pins: BTreeMap, + /// Build cache bytes the post-build prune reclaimed; `None` when no prune ran or + /// it failed (the build result stands either way). + #[serde(skip_serializing_if = "Option::is_none")] + pub cache_reclaimed_bytes: Option, } /// Receipt phases. `building` with no live holder of the key lock is a dead attempt. @@ -176,6 +188,9 @@ pub(super) struct Receipt { phase: Phase, #[serde(default, skip_serializing_if = "Option::is_none")] image_id: Option, + /// Engine-reported size of the verified image, for the next cold build's admission. + #[serde(default, skip_serializing_if = "Option::is_none")] + image_bytes: Option, base_pins: BTreeMap, } @@ -201,6 +216,17 @@ pub(super) trait BuildPool { fn resolve(&self, base: &BaseImage) -> Result; /// The verified builder executable. fn builder(&self) -> Result; + /// Free bytes on the guest storage disk that holds images and build cache. + fn storage_available(&self, lease: &Self::Lease) -> Result; + /// Prune BuildKit cache down to `max_used` bytes; returns the bytes reclaimed. + fn prune_cache(&self, lease: &Self::Lease, max_used: u64) -> Result; +} + +/// Free storage a cold build of a key requires. +pub(super) fn storage_required(previous_image_bytes: Option) -> u64 { + previous_image_bytes + .map_or(0, |bytes| bytes.saturating_mul(2)) + .max(STORAGE_FLOOR) } /// Validated local inputs and the build key derived from them. @@ -683,6 +709,7 @@ pub(super) fn run( tag: inputs.tag(), reused: true, base_pins: previous.base_pins.clone(), + cache_reclaimed_bytes: None, }); } } @@ -695,6 +722,7 @@ pub(super) fn run( state::write(&receipt_path, &dead)?; } } + let previous_bytes = previous.as_ref().and_then(|receipt| receipt.image_bytes); drop(lease); // Step 2, unleased: resolve every base image to a pinned manifest. @@ -729,6 +757,12 @@ pub(super) fn run( "The runtime changed before the build started; no build was run.", )); } + if pool.storage_available(&lease)? < storage_required(previous_bytes) { + return Err(refusal( + "native_build_storage", + "The native runtime's storage disk has too little free space for this build (at least 6 GiB, or twice the last image of this build). Inspect it with `runtime guest-disk-usage` and remove unused images or data; nothing was deleted.", + )); + } let mut receipt = Receipt { version: 1, checkout: candidate.checkout.clone(), @@ -739,6 +773,7 @@ pub(super) fn run( engine_id: identity.engine_id.clone(), phase: Phase::Building, image_id: None, + image_bytes: None, base_pins: pins.clone(), }; state::write(&receipt_path, &receipt)?; @@ -814,10 +849,10 @@ pub(super) fn run( ) })?; owned_image(&inspected, &id, &expected)?; - Ok(id) + Ok((id, inspected["Size"].as_u64())) }); - let id = match adopted { - Ok(id) => id, + let (id, image_bytes) = match adopted { + Ok(adopted) => adopted, Err(error) => { // A refused or missing result is a failed build; an engine or transport // error leaves the outcome unknown. @@ -832,7 +867,10 @@ pub(super) fn run( }; receipt.phase = Phase::ContentIdVerified; receipt.image_id = Some(id.clone()); + receipt.image_bytes = image_bytes; state::write(&receipt_path, &receipt)?; + // The verified image is recorded first; a failed prune leaves only extra cache. + let cache_reclaimed_bytes = pool.prune_cache(&lease, CACHE_BUDGET).ok(); drop(lease); Ok(BuildOutcome { image_id: id, @@ -840,6 +878,7 @@ pub(super) fn run( tag: inputs.tag(), reused: false, base_pins: pins, + cache_reclaimed_bytes, }) } @@ -1128,6 +1167,53 @@ impl<'a> BuildPool for LivePool<'a> { artifact::verify_builder(self.candidate)?; Ok(artifact::builder_executable(self.candidate)) } + fn storage_available(&self, lease: &Self::Lease) -> Result { + guest_storage_available(lease) + } + fn prune_cache(&self, lease: &Self::Lease, max_used: u64) -> Result { + prune_build_cache(lease, max_used) + } +} + +/// Free bytes on the guest `/storage` ext4 disk, which holds `/var/lib/docker`. +pub(super) fn guest_storage_available( + engine: &super::engine::Engine<'_>, +) -> Result { + let output = + engine + .guest() + .execute("df -Pk /storage | awk 'NR == 2 { print $4 }'", &[], None)?; + output + .trim() + .parse::() + .ok() + .and_then(|kib| kib.checked_mul(1024)) + .ok_or_else(|| { + refusal( + "guest_protocol", + "The guest reported no usable free-space value.", + ) + }) +} + +/// Prune the engine's BuildKit cache to at most `max_used` bytes. Cache records only: +/// the build-prune endpoint never removes images, containers or volumes, and BuildKit +/// keeps records an active build uses. +pub(super) fn prune_build_cache( + engine: &super::engine::Engine<'_>, + max_used: u64, +) -> Result { + let value = engine.request( + reqwest::Method::POST, + &format!("/v1.53/build/prune?max-used-space={max_used}"), + None, + )?; + value["SpaceReclaimed"].as_u64().ok_or_else(|| { + refusal( + "engine_protocol", + "The engine reported no reclaimed build-cache size.", + ) + }) } /// `runtime build-image --request `: build or reuse one native image. diff --git a/packages/runtime-core/src/provider/image_build/reclaim.rs b/packages/runtime-core/src/provider/image_build/reclaim.rs new file mode 100644 index 000000000..e903240a8 --- /dev/null +++ b/packages/runtime-core/src/provider/image_build/reclaim.rs @@ -0,0 +1,423 @@ +//! `runtime reclaim-build-images`: remove superseded Hack-built images and trim cache. +//! +//! An image is removed only when every one of these holds; anything else is retained +//! and reported: +//! +//! - it carries exactly this pool's build ownership labels (kind, owner digest of the +//! current incarnation, a namespace and a build key) and no other reserved labels; +//! - no build receipt of any namespace names it as its verified image; +//! - no retained graph state (`run/graphs`, `run/native-graphs`, `run/graph-archive`) +//! mentions its content ID anywhere, whatever the graph's phase or branch; +//! - the engine agrees to remove it without force, which it refuses while any +//! container, running or stopped, uses the image. +//! +//! The operation runs under the provider lease and refuses while a build is admitted, +//! so no build can adopt an image between the reference scan and the removal. If the +//! reference scan cannot read every retained graph record safely, nothing is removed. +//! BuildKit cache is then pruned to the build cache budget; that never removes images. +use super::{ + BuildPool, CACHE_BUDGET, LivePool, Phase, RESERVED_LABEL_PREFIXES, Receipt, builds_root, hex64, + image_id, owner_label, refusal, require_no_active_build, +}; +use crate::{Candidate, CandidateError}; +use serde::Serialize; +use serde_json::Value; +use std::{ + collections::{BTreeMap, BTreeSet}, + fs::{self, OpenOptions}, + io::Read, + os::unix::fs::{FileTypeExt, MetadataExt, OpenOptionsExt}, + path::Path, +}; + +const MAX_SCAN_ENTRIES: usize = 20_000; +const MAX_SCAN_DEPTH: usize = 8; +const MAX_SCAN_FILE: u64 = 16 * 1024 * 1024; +const MAX_BUILD_IMAGES: usize = 4096; + +/// Why an owned-looking image was kept. +#[derive(Debug, Serialize, Clone, Copy, Eq, PartialEq, Ord, PartialOrd)] +#[serde(rename_all = "kebab-case")] +pub enum Retained { + /// Its labels are not exactly this pool's build ownership labels. + NotOwned, + /// A build receipt names it as a key's current image. + Current, + /// Retained graph state references it. + Referenced, + /// The engine refused removal (in use by a container) or the outcome is unknown. + EngineRefused, +} + +#[derive(Debug, Serialize)] +pub struct ReclaimReport { + pub removed: Vec, + pub retained: BTreeMap, + /// Build cache bytes reclaimed; `None` when the prune failed (images unaffected). + pub cache_reclaimed_bytes: Option, +} + +/// Engine effects reclamation needs beyond a build pool. +pub(super) trait ReclaimPool: BuildPool { + /// Images labeled `io.hack-local.kind=build-image`, as the engine lists them. + fn build_images(&self, lease: &Self::Lease) -> Result, CandidateError>; + /// Remove one image by content ID without force. `Ok(false)` when the engine refuses. + fn remove(&self, lease: &Self::Lease, image: &str) -> Result; +} + +fn unprovable() -> CandidateError { + refusal( + "native_build_reclaim_unprovable", + "Retained graph state could not be read completely; no build image was removed.", + ) +} + +/// Every `sha256:<64 hex>` token in the bytes. +fn image_tokens(bytes: &[u8], into: &mut BTreeSet) { + const PREFIX: &[u8] = b"sha256:"; + let mut index = 0; + while let Some(offset) = bytes[index..] + .windows(PREFIX.len()) + .position(|window| window == PREFIX) + { + let start = index + offset + PREFIX.len(); + if let Some(hex) = bytes.get(start..start + 64) + && let Ok(hex) = std::str::from_utf8(hex) + && hex64(hex) + && !bytes.get(start + 64).is_some_and(|b| b.is_ascii_hexdigit()) + { + into.insert(format!("sha256:{hex}")); + } + index = start; + } +} + +/// Collect every image ID retained graph state mentions. Symlinks, special files, +/// unreadable entries or exceeded bounds refuse: reclamation needs a complete scan. +pub(super) fn referenced_images(candidate: &Candidate) -> Result, CandidateError> { + let mut found = BTreeSet::new(); + let mut entries = 0; + for name in ["run/graphs", "run/native-graphs", "run/graph-archive"] { + let root = candidate.state_root.join(name); + match fs::symlink_metadata(&root) { + Err(error) if error.kind() == std::io::ErrorKind::NotFound => continue, + Err(_) => return Err(unprovable()), + Ok(metadata) if !metadata.is_dir() => return Err(unprovable()), + Ok(_) => {} + } + scan_directory(&root, 0, &mut entries, &mut found)?; + } + Ok(found) +} + +fn scan_directory( + directory: &Path, + depth: usize, + entries: &mut usize, + found: &mut BTreeSet, +) -> Result<(), CandidateError> { + if depth > MAX_SCAN_DEPTH { + return Err(unprovable()); + } + for entry in fs::read_dir(directory).map_err(|_| unprovable())? { + *entries += 1; + if *entries > MAX_SCAN_ENTRIES { + return Err(unprovable()); + } + let path = entry.map_err(|_| unprovable())?.path(); + let metadata = fs::symlink_metadata(&path).map_err(|_| unprovable())?; + if metadata.is_dir() { + scan_directory(&path, depth + 1, entries, found)?; + } else if metadata.is_file() { + if metadata.len() > MAX_SCAN_FILE { + return Err(unprovable()); + } + let file = OpenOptions::new() + .read(true) + .custom_flags(libc::O_NOFOLLOW | libc::O_NONBLOCK) + .open(&path) + .map_err(|_| unprovable())?; + let opened = file.metadata().map_err(|_| unprovable())?; + if !opened.is_file() || (opened.dev(), opened.ino()) != (metadata.dev(), metadata.ino()) + { + return Err(unprovable()); + } + let mut bytes = Vec::new(); + file.take(MAX_SCAN_FILE + 1) + .read_to_end(&mut bytes) + .map_err(|_| unprovable())?; + if bytes.len() as u64 > MAX_SCAN_FILE { + return Err(unprovable()); + } + image_tokens(&bytes, found); + } else if !metadata.file_type().is_socket() { + // Sockets carry no records; anything else is unexpected in graph state. + return Err(unprovable()); + } + } + Ok(()) +} + +/// Image IDs that build receipts of every namespace record as verified. +fn current_images(candidate: &Candidate) -> Result, CandidateError> { + let root = builds_root(candidate); + let mut current = BTreeSet::new(); + let namespaces = match fs::read_dir(&root) { + Ok(namespaces) => namespaces, + Err(error) if error.kind() == std::io::ErrorKind::NotFound => return Ok(current), + Err(_) => return Err(unprovable()), + }; + for namespace in namespaces { + let namespace = namespace.map_err(|_| unprovable())?.path(); + let name = namespace.file_name().and_then(|n| n.to_str()).unwrap_or(""); + let metadata = fs::symlink_metadata(&namespace).map_err(|_| unprovable())?; + if name == "active.lock" && metadata.is_file() { + continue; + } + if !hex64(name) || !metadata.is_dir() { + return Err(unprovable()); + } + for entry in fs::read_dir(&namespace).map_err(|_| unprovable())? { + let path = entry.map_err(|_| unprovable())?.path(); + if path.extension().and_then(|e| e.to_str()) != Some("json") { + continue; + } + let receipt: Receipt = + crate::provider::state::read_bounded(&path, super::MAX_RECEIPT_BYTES) + .map_err(|_| unprovable())?; + if receipt.phase == Phase::ContentIdVerified + && let Some(id) = receipt.image_id + { + current.insert(id); + } + } + } + Ok(current) +} + +/// Whether listed labels are exactly this pool's build ownership labels. +fn owned_by(labels: &Value, owner: &str) -> bool { + let Some(labels) = labels.as_object() else { + return false; + }; + let text = |key: &str| labels.get(key).and_then(Value::as_str); + let reserved_extra = labels.keys().any(|key| { + RESERVED_LABEL_PREFIXES + .iter() + .any(|prefix| key.starts_with(prefix)) + && ![ + "io.hack-local.build-key", + "io.hack-local.kind", + "io.hack-local.namespace", + "io.hack-local.owner", + ] + .contains(&key.as_str()) + }); + text("io.hack-local.kind") == Some(super::KIND) + && text("io.hack-local.owner") == Some(owner) + && text("io.hack-local.namespace").is_some_and(hex64) + && text("io.hack-local.build-key").is_some_and(hex64) + && !reserved_extra +} + +/// The removal decision for each listed image, before any engine effect. +pub(super) fn plan( + images: &[Value], + owner: &str, + current: &BTreeSet, + referenced: &BTreeSet, +) -> Result<(Vec, BTreeMap), CandidateError> { + if images.len() > MAX_BUILD_IMAGES { + return Err(refusal( + "native_build_reclaim_bounds", + "Too many build images to reclaim in one operation; nothing was removed.", + )); + } + let mut remove = Vec::new(); + let mut retained = BTreeMap::new(); + for image in images { + let id = image["Id"] + .as_str() + .filter(|id| image_id(id)) + .ok_or_else(|| { + refusal( + "engine_protocol", + "The engine listed a build image without a content ID.", + ) + })? + .to_owned(); + let reason = if !owned_by(&image["Labels"], owner) { + Some(Retained::NotOwned) + } else if current.contains(&id) { + Some(Retained::Current) + } else if referenced.contains(&id) { + Some(Retained::Referenced) + } else { + None + }; + match reason { + Some(reason) => { + retained.insert(id, reason); + } + None => remove.push(id), + } + } + remove.sort(); + remove.dedup(); + Ok((remove, retained)) +} + +pub(super) fn run( + candidate: &Candidate, + pool: &P, +) -> Result { + let (lease, identity) = pool.lease()?; + require_no_active_build(candidate)?; + // Under the lease no build can start, adopt or write a receipt. + let current = current_images(candidate)?; + let referenced = referenced_images(candidate)?; + let images = pool.build_images(&lease)?; + let (candidates, mut retained) = plan( + &images, + &owner_label(&identity.incarnation), + ¤t, + &referenced, + )?; + let mut removed = Vec::new(); + for id in candidates { + match pool.remove(&lease, &id) { + Ok(true) => removed.push(id), + Ok(false) | Err(_) => { + retained.insert(id, Retained::EngineRefused); + } + } + } + let cache_reclaimed_bytes = pool.prune_cache(&lease, CACHE_BUDGET).ok(); + Ok(ReclaimReport { + removed, + retained, + cache_reclaimed_bytes, + }) +} + +impl ReclaimPool for LivePool<'_> { + fn build_images(&self, lease: &Self::Lease) -> Result, CandidateError> { + // `{"label":["io.hack-local.kind=build-image"]}`, percent-encoded. + let value = lease.request( + reqwest::Method::GET, + "/v1.53/images/json?all=true&filters=%7B%22label%22%3A%5B%22io.hack-local.kind%3Dbuild-image%22%5D%7D", + None, + )?; + value + .as_array() + .cloned() + .ok_or_else(|| refusal("engine_protocol", "The engine image list is not an array.")) + } + fn remove(&self, lease: &Self::Lease, image: &str) -> Result { + match lease.request( + reqwest::Method::DELETE, + &format!("/v1.53/images/{image}?force=false&noprune=false"), + None, + ) { + Ok(_) => Ok(true), + Err(error) if error.code == "engine_not_found" => Ok(true), + Err(error) if error.code == "engine_rejected" => Ok(false), + Err(error) => Err(error), + } + } +} + +/// `runtime reclaim-build-images`: see the module documentation. +pub fn reclaim_build_images(candidate: &Candidate) -> Result { + run(candidate, &LivePool { candidate }) +} + +#[cfg(test)] +mod tests { + use super::*; + + const A: &str = "sha256:aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"; + const B: &str = "sha256:bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb"; + const C: &str = "sha256:cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc"; + const D: &str = "sha256:dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd"; + + fn image(id: &str, owner: &str) -> Value { + serde_json::json!({"Id": id, "Labels": { + "io.hack-local.kind": "build-image", + "io.hack-local.owner": owner, + "io.hack-local.namespace": "1".repeat(64), + "io.hack-local.build-key": "2".repeat(64), + }}) + } + + #[test] + fn only_unreferenced_superseded_images_of_this_pool_are_removal_candidates() { + let owner = owner_label("pool"); + let mut forged = image(D, &owner); + forged["Labels"]["io.hack-local.graph"] = "x".into(); + let images = [ + image(A, &owner), + image(B, &owner), + image(C, &owner), + forged, + image( + "sha256:eeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee", + &owner_label("other-pool"), + ), + ]; + let current = BTreeSet::from([B.to_owned()]); + let referenced = BTreeSet::from([C.to_owned()]); + let (remove, retained) = plan(&images, &owner, ¤t, &referenced).unwrap(); + assert_eq!(remove, vec![A.to_owned()]); + assert_eq!(retained[B], Retained::Current); + assert_eq!(retained[C], Retained::Referenced); + assert_eq!(retained[D], Retained::NotOwned); + assert_eq!(retained.len(), 4); + assert!( + plan( + &[serde_json::json!({"Id": "bad"})], + &owner, + ¤t, + &referenced + ) + .is_err() + ); + } + + #[test] + fn image_tokens_find_exact_content_ids_only() { + let mut found = BTreeSet::new(); + image_tokens( + format!("{{\"image\":\"{A}\"}} x{B}f sha256:short {C}").as_bytes(), + &mut found, + ); + // B is followed by another hex digit, so it is not an exact ID. + assert_eq!(found, BTreeSet::from([A.to_owned(), C.to_owned()])); + } + + #[test] + fn retained_graph_state_is_scanned_completely_or_not_at_all() { + let tmp = std::env::temp_dir().canonicalize().unwrap(); + let root = crate::test_root::private_test_root(&tmp, "hack-build-reclaim"); + let checkout = root.join("checkout"); + crate::provider::state::private_directory(&checkout).unwrap(); + let candidate = Candidate::discover(&checkout).unwrap(); + assert!(referenced_images(&candidate).unwrap().is_empty()); + let run = candidate.state_root.join("run/native-graphs/r1/nested"); + crate::provider::state::private_directory(&run).unwrap(); + fs::write(run.join("receipt.json"), format!("{{\"image\":\"{A}\"}}")).unwrap(); + let archive = candidate.state_root.join("run/graph-archive"); + crate::provider::state::private_directory(&archive).unwrap(); + fs::write(archive.join("old.json"), format!("[\"{B}\"]")).unwrap(); + assert_eq!( + referenced_images(&candidate).unwrap(), + BTreeSet::from([A.to_owned(), B.to_owned()]) + ); + std::os::unix::fs::symlink(run.join("receipt.json"), archive.join("alias")).unwrap(); + assert_eq!( + referenced_images(&candidate).unwrap_err().code, + "native_build_reclaim_unprovable" + ); + fs::remove_dir_all(&root).unwrap(); + } +} diff --git a/packages/runtime-core/src/provider/image_build/tests.rs b/packages/runtime-core/src/provider/image_build/tests.rs index eeec6f91b..054cef1b0 100644 --- a/packages/runtime-core/src/provider/image_build/tests.rs +++ b/packages/runtime-core/src/provider/image_build/tests.rs @@ -116,18 +116,26 @@ fn identity(incarnation: &str) -> PoolIdentity { /// A fake pool: identities returned per lease in order (the last repeats), images by ID. struct FakePool { + removable: RefCell>, + removed: RefCell>, identities: RefCell>, images: RefCell>, leases: RefCell, resolve_error: bool, + available: RefCell, + prunes: RefCell>, } impl FakePool { fn new(incarnation: &str) -> Self { Self { + removable: RefCell::new(BTreeMap::new()), + removed: RefCell::new(Vec::new()), identities: RefCell::new(vec![identity(incarnation)]), images: RefCell::new(BTreeMap::new()), leases: RefCell::new(0), resolve_error: false, + available: RefCell::new(64 * GIB), + prunes: RefCell::new(Vec::new()), } } /// Register the image the fake client "builds", with the labels the build expects. @@ -139,7 +147,7 @@ impl FakePool { self.images.borrow_mut().insert( IMAGE.into(), serde_json::json!({"Id": IMAGE, "Architecture": "arm64", "Os": "linux", - "Config": {"Labels": labels, "Volumes": null}}), + "Size": 5 * GIB, "Config": {"Labels": labels, "Volumes": null}}), ); } } @@ -171,6 +179,13 @@ impl BuildPool for FakePool { fn builder(&self) -> Result { Ok(PathBuf::from("/bin/sh")) } + fn storage_available(&self, _: &()) -> Result { + Ok(*self.available.borrow()) + } + fn prune_cache(&self, _: &(), max_used: u64) -> Result { + self.prunes.borrow_mut().push(max_used); + Ok(7) + } } fn never() -> bool { @@ -417,6 +432,7 @@ fn a_dead_attempt_is_recorded_indeterminate_and_built_again() { engine_id: "engine-1".into(), phase: Phase::Building, image_id: None, + image_bytes: None, base_pins: BTreeMap::new(), }; state::write(&path, &leftover).unwrap(); @@ -745,3 +761,118 @@ fn build_network_script_parses_and_ignores_isolated_pools() { assert_eq!(run(&[]), Some(64)); assert!(script.contains(BUILD_NETWORK_MARKER)); } + +#[test] +fn cold_builds_need_free_storage_and_successful_builds_prune_the_cache() { + assert_eq!(storage_required(None), 6 * GIB); + assert_eq!(storage_required(Some(GIB)), 6 * GIB); + assert_eq!(storage_required(Some(5 * GIB)), 10 * GIB); + assert_eq!(storage_required(Some(u64::MAX)), u64::MAX); + + let fixture = Fixture::new(); + let inputs = fixture.inputs(Policy::Missing); + fixture.client(&inputs, "ok"); + let pool = FakePool::new("pool-1"); + pool.built(&inputs, "pool-1", serde_json::json!({})); + *pool.available.borrow_mut() = 6 * GIB - 1; + let error = run(&fixture.candidate, &pool, &inputs, &never).unwrap_err(); + assert_eq!(error.code, "native_build_storage"); + assert_eq!(fixture.calls(&inputs), 0); + + *pool.available.borrow_mut() = 6 * GIB; + let outcome = run(&fixture.candidate, &pool, &inputs, &never).unwrap(); + assert_eq!(outcome.cache_reclaimed_bytes, Some(7)); + assert_eq!(*pool.prunes.borrow(), vec![CACHE_BUDGET]); + assert_eq!(fixture.receipt(&inputs).image_bytes, Some(5 * GIB)); + + // The next cold build of this key needs twice the last verified image. + let rebuild = fixture.inputs(Policy::Rebuild); + let error = run(&fixture.candidate, &pool, &rebuild, &never).unwrap_err(); + assert_eq!(error.code, "native_build_storage"); + // A warm reuse needs no free-space headroom. + let reused = run(&fixture.candidate, &pool, &inputs, &never).unwrap(); + assert!(reused.reused); + assert_eq!(pool.prunes.borrow().len(), 1); +} + +impl reclaim::ReclaimPool for FakePool { + fn build_images(&self, _: &()) -> Result, CandidateError> { + Ok(self + .images + .borrow() + .values() + .map( + |image| serde_json::json!({"Id": image["Id"], "Labels": image["Config"]["Labels"]}), + ) + .collect()) + } + fn remove(&self, _: &(), image: &str) -> Result { + let allowed = self.removable.borrow().get(image).copied().unwrap_or(true); + if allowed { + self.removed.borrow_mut().push(image.to_owned()); + self.images.borrow_mut().remove(image); + } + Ok(allowed) + } +} + +#[test] +fn reclamation_keeps_current_referenced_in_use_and_foreign_images() { + const OLD: &str = "sha256:1111111111111111111111111111111111111111111111111111111111111111"; + const KEPT: &str = "sha256:2222222222222222222222222222222222222222222222222222222222222222"; + const BUSY: &str = "sha256:3333333333333333333333333333333333333333333333333333333333333333"; + let fixture = Fixture::new(); + let inputs = fixture.inputs(Policy::Missing); + fixture.client(&inputs, "ok"); + let pool = FakePool::new("pool-1"); + pool.built(&inputs, "pool-1", serde_json::json!({})); + run(&fixture.candidate, &pool, &inputs, &never).unwrap(); + let current = pool.images.borrow()[IMAGE].clone(); + for id in [OLD, KEPT, BUSY] { + let mut superseded = current.clone(); + superseded["Id"] = id.into(); + pool.images.borrow_mut().insert(id.into(), superseded); + } + pool.removable.borrow_mut().insert(BUSY.into(), false); + let graphs = fixture.candidate.state_root.join("run/graphs/0123"); + state::private_directory(&graphs).unwrap(); + fs::write( + graphs.join("receipt.json"), + format!("{{\"image\":\"{KEPT}\"}}"), + ) + .unwrap(); + + // Nothing is removed while a build is admitted. + let build = Flock::try_lock( + Flock::open(&builds_root(&fixture.candidate).join("active.lock")).unwrap(), + libc::LOCK_SH, + ) + .unwrap() + .unwrap(); + assert_eq!( + reclaim::run(&fixture.candidate, &pool).unwrap_err().code, + "provider_busy" + ); + drop(build); + + let report = reclaim::run(&fixture.candidate, &pool).unwrap(); + assert_eq!(report.removed, vec![OLD.to_owned()]); + assert_eq!(report.retained[IMAGE], reclaim::Retained::Current); + assert_eq!(report.retained[KEPT], reclaim::Retained::Referenced); + assert_eq!(report.retained[BUSY], reclaim::Retained::EngineRefused); + assert_eq!(report.cache_reclaimed_bytes, Some(7)); + // Another pool's images are never this pool's to remove. + let other = FakePool::new("pool-2"); + other + .images + .borrow_mut() + .extend(pool.images.borrow().clone()); + let report = reclaim::run(&fixture.candidate, &other).unwrap(); + assert!(report.removed.is_empty()); + assert!( + report + .retained + .values() + .all(|r| *r == reclaim::Retained::NotOwned) + ); +} diff --git a/scripts/lib/tla-runtime-models.ts b/scripts/lib/tla-runtime-models.ts index 3da1f022a..1f6360c2f 100644 --- a/scripts/lib/tla-runtime-models.ts +++ b/scripts/lib/tla-runtime-models.ts @@ -1440,6 +1440,42 @@ const contracts: readonly ModelContract[] = [ }, ], }, + { + name: "native-build-retention", + module: "BuildRetention", + states: 6181, + invariant: "NoReclaimReferenced", + action: "Reclaim", + fields: ["refs = {1}", "removed = 1", "fence = FALSE"], + additionalControls: [ + { + name: "foreign-adoption", + negative: true, + invariant: "NoForeignAdoption", + action: "CompleteBuild", + fields: [ + 'receipt = [phase |-> "verified", image |-> 2, inc |-> 1]', + "owner = <<1, 0, 0>>", + ], + alternativeWitnesses: [ + { + action: "CompleteBuild", + fields: [ + 'receipt = [phase |-> "verified", image |-> 1, inc |-> 1]', + "owner = <<0, 1, 0>>", + ], + }, + ], + }, + { + name: "down-under-build", + negative: true, + invariant: "DownNotUnderBuild", + action: "Down", + fields: ['build = "running"', "engineUp = FALSE", "fence = TRUE"], + }, + ], + }, { name: "relay-fence", module: "RelayFence", diff --git a/tests/models/tla/README.md b/tests/models/tla/README.md index dcc19f977..2ebe1b8f4 100644 --- a/tests/models/tla/README.md +++ b/tests/models/tla/README.md @@ -1049,3 +1049,27 @@ Closing the residual needs a mutation fence rather than a timeout: target tmux mutations by session ID (`#{session_id}`, never reused by a server) captured with the token read. That fence, and full zellij support for shared-helper lifecycle sessions, are tracked in HACK-1849 and are not in this slice. + +## Native image build retention + +`native-build-retention/BuildRetention.tla` follows `provider::image_build` and its +`reclaim` module for one build key in one namespace, with three content IDs and two +storage incarnations. The positive configuration exhausts **6,181 distinct states**. + +| Model operation | Source boundary | +| --- | --- | +| `BeginBuild` | Under the provider lease: shared build fence, per-key lock, `building` receipt. | +| `RunBuild` / `ForeignImage` | Unleased BuildKit run writing an image with this pool's labels; a forged or foreign image may appear at any time. | +| `CompleteBuild` | Under the lease: the reported ID is adopted only with this incarnation's labels and the admitted incarnation; otherwise `failed`. | +| `Cancel` / `CrashHost` / `RecordDeadAttempt` | Cancellation and host death release the fence; a `building` receipt under the key lock is recorded `indeterminate`. | +| `Down` / `RecreateStorage` | `runtime down` refuses while the fence is held; recreated storage is a new incarnation with an empty engine. | +| `StartGraph` / `RemoveContainers` / `Restore` | Graphs use only a verified image of this incarnation and keep a reference to it; data-retaining cleanup removes containers but not the reference; restore never builds. | +| `Reclaim` / `PruneCache` | Owned, non-current, unreferenced, unused images only, with no build admitted; cache pruning never touches images. | + +Three controls each remove one guard and must fail at the named action: +`negative` (reclaim ignores retained references) fails `NoReclaimReferenced` at +`Reclaim`; `foreign-adoption` (adoption without the label/incarnation check) fails +`NoForeignAdoption` at `CompleteBuild`; `down-under-build` (down ignores the fence) +fails `DownNotUnderBuild` at `Down`. The model does not cover an orphaned build client +that outlives a crashed host process, real BuildKit or engine behavior, receipt +durability, or more than one key and namespace. diff --git a/tests/models/tla/native-build-retention/BuildRetention.tla b/tests/models/tla/native-build-retention/BuildRetention.tla new file mode 100644 index 000000000..f9a459253 --- /dev/null +++ b/tests/models/tla/native-build-retention/BuildRetention.tla @@ -0,0 +1,115 @@ +------------------------- MODULE BuildRetention ------------------------- +(***************************************************************************) +(* Native image build retention: `provider::image_build` and its *) +(* `reclaim` module. One build key, one namespace, a bounded supply of *) +(* content IDs. A build is admitted under the provider lease (fence and *) +(* `building` receipt), runs unleased, and is adopted under the lease only *) +(* when the reported image carries this incarnation's labels and the *) +(* incarnation is the one admitted. `runtime down` stops the engine only *) +(* when no build holds the shared fence. Reclamation removes only owned, *) +(* non-current images that no retained graph state references; the engine *) +(* itself refuses images a container uses. Unsafe* constants remove one *) +(* guard each for the negative controls. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets +CONSTANTS UnsafeReclaim, UnsafeAdopt, UnsafeDown +VARIABLES incarnation, engineUp, engine, owner, next, receipt, build, + fence, refs, used, removed +vars == <> +Ids == 1..3 +Phases == {"none", "building", "verified", "failed", "canceled", + "indeterminate"} + +Init == /\ incarnation = 1 /\ engineUp = TRUE /\ engine = {} + /\ owner = [i \in Ids |-> 0] /\ next = 1 + /\ receipt = [phase |-> "none", image |-> 0, inc |-> 0] + /\ build = "idle" /\ fence = FALSE + /\ refs = {} /\ used = {} /\ removed = 0 + +(* Step 1: under the lease, take the fence and record the attempt. *) +BeginBuild == /\ engineUp /\ build = "idle" + /\ build' = "running" /\ fence' = TRUE + /\ receipt' = [phase |-> "building", image |-> 0, inc |-> incarnation] + /\ UNCHANGED <> +(* Step 4, unleased: BuildKit writes a fresh image with this pool's labels. *) +RunBuild == /\ build = "running" /\ engineUp /\ next \in Ids + /\ engine' = engine \cup {next} + /\ owner' = [owner EXCEPT ![next] = incarnation] + /\ next' = next + 1 /\ build' = "done" + /\ UNCHANGED <> +(* A forged or foreign image appears in the engine (Dockerfile labels, other pool). *) +ForeignImage == /\ engineUp /\ next \in Ids + /\ engine' = engine \cup {next} /\ next' = next + 1 + /\ UNCHANGED <> +(* Step 5: the reported ID may be any present image; only an owned one under *) +(* the admitted incarnation is adopted. *) +CompleteBuild == /\ build = "done" /\ engineUp + /\ \E reported \in engine : + receipt' = IF UnsafeAdopt \/ + (owner[reported] = incarnation /\ receipt.inc = incarnation) + THEN [phase |-> "verified", image |-> reported, inc |-> receipt.inc] + ELSE [receipt EXCEPT !.phase = "failed"] + /\ build' = "idle" /\ fence' = FALSE + /\ UNCHANGED <> +Cancel == /\ build \in {"running", "done"} + /\ build' = "idle" /\ fence' = FALSE + /\ receipt' = [receipt EXCEPT !.phase = "canceled"] + /\ UNCHANGED <> +(* hack-native dies: the flock-backed fence and key lock are released; the *) +(* receipt stays `building` and the next attempt records it indeterminate. *) +CrashHost == /\ build # "idle" /\ build' = "idle" /\ fence' = FALSE + /\ UNCHANGED <> +RecordDeadAttempt == /\ build = "idle" /\ receipt.phase = "building" + /\ receipt' = [receipt EXCEPT !.phase = "indeterminate"] + /\ UNCHANGED <> +Down == /\ engineUp /\ (UnsafeDown \/ ~fence) + /\ engineUp' = FALSE + /\ UNCHANGED <> +Up == /\ ~engineUp /\ engineUp' = TRUE + /\ UNCHANGED <> +(* The storage disk is recreated: a new incarnation with an empty engine. *) +RecreateStorage == /\ ~engineUp /\ build = "idle" /\ incarnation = 1 + /\ incarnation' = 2 /\ engine' = {} /\ used' = {} + /\ UNCHANGED <> +(* A graph starts from the verified image of this incarnation and retains a *) +(* reference to it; its containers use it until removed. *) +StartGraph == /\ engineUp /\ receipt.phase = "verified" + /\ receipt.inc = incarnation /\ receipt.image \in engine + /\ owner[receipt.image] = incarnation + /\ refs' = refs \cup {receipt.image} /\ used' = used \cup {receipt.image} + /\ UNCHANGED <> +(* Data-retaining cleanup removes containers but keeps the graph reference. *) +RemoveContainers == /\ used # {} /\ used' = {} + /\ UNCHANGED <> +(* Restore uses retained references only and never builds. *) +Restore == /\ engineUp /\ build = "idle" /\ refs \cap engine # {} + /\ used' = used \cup (refs \cap engine) + /\ UNCHANGED <> +Reclaim == /\ engineUp /\ ~fence + /\ \E image \in engine : + /\ owner[image] = incarnation + /\ ~(receipt.phase = "verified" /\ receipt.image = image) + /\ (UnsafeReclaim \/ image \notin refs) + /\ image \notin used + /\ engine' = engine \ {image} /\ removed' = image + /\ UNCHANGED <> +PruneCache == /\ engineUp /\ UNCHANGED vars +Next == BeginBuild \/ RunBuild \/ ForeignImage \/ CompleteBuild \/ Cancel + \/ CrashHost \/ RecordDeadAttempt \/ Down \/ Up \/ RecreateStorage + \/ StartGraph \/ RemoveContainers \/ Restore \/ Reclaim \/ PruneCache +Spec == Init /\ [][Next]_vars + +TypeOK == /\ incarnation \in {1, 2} /\ engineUp \in BOOLEAN + /\ engine \subseteq Ids /\ owner \in [Ids -> 0..2] /\ next \in 1..4 + /\ receipt.phase \in Phases /\ receipt.image \in 0..3 /\ receipt.inc \in 0..2 + /\ build \in {"idle", "running", "done"} /\ fence \in BOOLEAN + /\ refs \subseteq Ids /\ used \subseteq Ids /\ removed \in 0..3 +(* An image retained graph state references is never reclaimed. *) +NoReclaimReferenced == removed = 0 \/ removed \notin refs +(* A verified receipt names an image produced under its own incarnation. *) +NoForeignAdoption == receipt.phase = "verified" => owner[receipt.image] = receipt.inc +(* The engine never stops under a build its operation still controls. *) +DownNotUnderBuild == build = "running" => engineUp +Safe == NoReclaimReferenced /\ NoForeignAdoption /\ DownNotUnderBuild +============================================================================= diff --git a/tests/models/tla/native-build-retention/down-under-build.cfg b/tests/models/tla/native-build-retention/down-under-build.cfg new file mode 100644 index 000000000..e5a514866 --- /dev/null +++ b/tests/models/tla/native-build-retention/down-under-build.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANTS UnsafeReclaim = FALSE UnsafeAdopt = FALSE UnsafeDown = TRUE +INVARIANT TypeOK +INVARIANT DownNotUnderBuild diff --git a/tests/models/tla/native-build-retention/foreign-adoption.cfg b/tests/models/tla/native-build-retention/foreign-adoption.cfg new file mode 100644 index 000000000..694d3bbf3 --- /dev/null +++ b/tests/models/tla/native-build-retention/foreign-adoption.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANTS UnsafeReclaim = FALSE UnsafeAdopt = TRUE UnsafeDown = FALSE +INVARIANT TypeOK +INVARIANT NoForeignAdoption diff --git a/tests/models/tla/native-build-retention/negative.cfg b/tests/models/tla/native-build-retention/negative.cfg new file mode 100644 index 000000000..595325be5 --- /dev/null +++ b/tests/models/tla/native-build-retention/negative.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANTS UnsafeReclaim = TRUE UnsafeAdopt = FALSE UnsafeDown = FALSE +INVARIANT TypeOK +INVARIANT NoReclaimReferenced diff --git a/tests/models/tla/native-build-retention/positive.cfg b/tests/models/tla/native-build-retention/positive.cfg new file mode 100644 index 000000000..28191ce8d --- /dev/null +++ b/tests/models/tla/native-build-retention/positive.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANTS UnsafeReclaim = FALSE UnsafeAdopt = FALSE UnsafeDown = FALSE +INVARIANT TypeOK +INVARIANT Safe From 7ba0c59189ef9ce3a1638e553e2cecbbbdac7d92 Mon Sep 17 00:00:00 2001 From: Dimitri Kennedy <344842+roodboi@users.noreply.github.com> Date: Thu, 5 Nov 2026 23:11:18 -0500 Subject: [PATCH 2/3] fix(native): never prune parents when reclaiming and keep the last verified image size Reclamation now deletes each candidate with noprune=true, so an untagged parent is never removed without passing the ownership, current-receipt and reference checks itself. A build attempt that verifies no image (failed, canceled, interrupted) now carries the last verified image size forward, so its retry is admitted against twice that size rather than the floor. Co-Authored-By: Claude Opus 5.5 --- docs/guides/native-candidate.md | 3 ++- .../runtime-core/src/provider/image_build.rs | 9 +++++--- .../src/provider/image_build/reclaim.rs | 22 ++++++++++++++----- .../src/provider/image_build/tests.rs | 12 ++++++++++ 4 files changed, 36 insertions(+), 10 deletions(-) diff --git a/docs/guides/native-candidate.md b/docs/guides/native-candidate.md index a80767d12..12f490bea 100644 --- a/docs/guides/native-candidate.md +++ b/docs/guides/native-candidate.md @@ -501,7 +501,8 @@ linked, mode-`0600` file owned by you), because build-argument values are in it: same key replaced. It keeps every image a build receipt names as current, every image that any retained run's saved state mentions, every image a container still uses (the engine refuses those), and every image whose ownership labels are not exactly this -runtime's. It refuses while a build runs, and removes nothing if it cannot read all +runtime's. Each removal deletes that one image only, never its untagged parent +images. It refuses while a build runs, and removes nothing if it cannot read all saved run state. The report lists removed images and why each other one was kept. Before startup, network-tool preparation additionally requires all four pinned diff --git a/packages/runtime-core/src/provider/image_build.rs b/packages/runtime-core/src/provider/image_build.rs index e919fc47a..2a0ba3fb0 100644 --- a/packages/runtime-core/src/provider/image_build.rs +++ b/packages/runtime-core/src/provider/image_build.rs @@ -193,7 +193,8 @@ pub(super) struct Receipt { phase: Phase, #[serde(default, skip_serializing_if = "Option::is_none")] image_id: Option, - /// Engine-reported size of the verified image, for the next cold build's admission. + /// Engine-reported size of the last verified image of this key, for the next cold + /// build's admission. Attempts that verify no image carry it forward unchanged. #[serde(default, skip_serializing_if = "Option::is_none")] image_bytes: Option, base_pins: BTreeMap, @@ -806,7 +807,9 @@ pub(super) fn run( engine_id: identity.engine_id.clone(), phase: Phase::Building, image_id: None, - image_bytes: None, + // Failed, canceled or interrupted attempts keep the last verified size, so a + // retry is admitted against it rather than the floor. + image_bytes: previous_bytes, base_pins: pins.clone(), }; state::write(&receipt_path, &receipt)?; @@ -902,7 +905,7 @@ pub(super) fn run( }; receipt.phase = Phase::ContentIdVerified; receipt.image_id = Some(id.clone()); - receipt.image_bytes = image_bytes; + receipt.image_bytes = image_bytes.or(receipt.image_bytes); state::write(&receipt_path, &receipt)?; // The verified image is recorded first; a failed prune leaves only extra cache. let cache_reclaimed_bytes = pool.prune_cache(&lease, CACHE_BUDGET).ok(); diff --git a/packages/runtime-core/src/provider/image_build/reclaim.rs b/packages/runtime-core/src/provider/image_build/reclaim.rs index e903240a8..4e19e718d 100644 --- a/packages/runtime-core/src/provider/image_build/reclaim.rs +++ b/packages/runtime-core/src/provider/image_build/reclaim.rs @@ -9,7 +9,8 @@ //! - no retained graph state (`run/graphs`, `run/native-graphs`, `run/graph-archive`) //! mentions its content ID anywhere, whatever the graph's phase or branch; //! - the engine agrees to remove it without force, which it refuses while any -//! container, running or stopped, uses the image. +//! container, running or stopped, uses the image. Untagged parent images are never +//! pruned along with it (`noprune=true`); each must pass these checks itself. //! //! The operation runs under the provider lease and refuses while a build is admitted, //! so no build can adopt an image between the reference scan and the removal. If the @@ -314,11 +315,7 @@ impl ReclaimPool for LivePool<'_> { .ok_or_else(|| refusal("engine_protocol", "The engine image list is not an array.")) } fn remove(&self, lease: &Self::Lease, image: &str) -> Result { - match lease.request( - reqwest::Method::DELETE, - &format!("/v1.53/images/{image}?force=false&noprune=false"), - None, - ) { + match lease.request(reqwest::Method::DELETE, &removal_path(image), None) { Ok(_) => Ok(true), Err(error) if error.code == "engine_not_found" => Ok(true), Err(error) if error.code == "engine_rejected" => Ok(false), @@ -327,6 +324,12 @@ impl ReclaimPool for LivePool<'_> { } } +/// Remove exactly one image: never forced, and never its untagged parents +/// (`noprune=true`), so every image the engine deletes has passed [`plan`] itself. +fn removal_path(image: &str) -> String { + format!("/v1.53/images/{image}?force=false&noprune=true") +} + /// `runtime reclaim-build-images`: see the module documentation. pub fn reclaim_build_images(candidate: &Candidate) -> Result { run(candidate, &LivePool { candidate }) @@ -384,6 +387,13 @@ mod tests { ); } + #[test] + fn removal_never_forces_or_prunes_untagged_parents() { + let path = removal_path(A); + assert_eq!(path, format!("/v1.53/images/{A}?force=false&noprune=true")); + assert!(!path.contains("noprune=false") && !path.contains("force=true")); + } + #[test] fn image_tokens_find_exact_content_ids_only() { let mut found = BTreeSet::new(); diff --git a/packages/runtime-core/src/provider/image_build/tests.rs b/packages/runtime-core/src/provider/image_build/tests.rs index f7d898df7..bb2b083eb 100644 --- a/packages/runtime-core/src/provider/image_build/tests.rs +++ b/packages/runtime-core/src/provider/image_build/tests.rs @@ -887,6 +887,18 @@ fn cold_builds_need_free_storage_and_successful_builds_prune_the_cache() { let reused = run(&fixture.candidate, &pool, &inputs, &never).unwrap(); assert!(reused.reused); assert_eq!(pool.prunes.borrow().len(), 1); + + // A rebuild that fails verifies no image: the last verified size still applies. + *pool.available.borrow_mut() = 10 * GIB; + fixture.client(&rebuild, "fail"); + let error = run(&fixture.candidate, &pool, &rebuild, &never).unwrap_err(); + assert_eq!(error.code, "native_build_failed"); + let receipt = fixture.receipt(&rebuild); + assert_eq!(receipt.phase, Phase::Failed); + assert_eq!(receipt.image_bytes, Some(5 * GIB)); + *pool.available.borrow_mut() = 6 * GIB; + let error = run(&fixture.candidate, &pool, &rebuild, &never).unwrap_err(); + assert_eq!(error.code, "native_build_storage"); } impl reclaim::ReclaimPool for FakePool { From 9f33a1d01c4c5a68dd5d4c253937f79ad6863091 Mon Sep 17 00:00:00 2001 From: Dimitri Kennedy <344842+roodboi@users.noreply.github.com> Date: Fri, 6 Nov 2026 19:20:03 -0500 Subject: [PATCH 3/3] docs(native): describe the orphaned build client as fenced in model coverage The native-build-retention coverage row and model README said the fence is released with its holder when the coordinator dies. Since #606 the build client inherits the fence and per-key lock, so both stay held until an orphaned client exits; the model still does not cover that case. Co-Authored-By: Claude Opus 5.5 --- docs/reference/v5-model-coverage.md | 2 +- tests/models/tla/README.md | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/docs/reference/v5-model-coverage.md b/docs/reference/v5-model-coverage.md index 973afee48..2db9b9fb8 100644 --- a/docs/reference/v5-model-coverage.md +++ b/docs/reference/v5-model-coverage.md @@ -44,7 +44,7 @@ must be attached to the eventual exact integration revision. | Concurrent stop/publication; route claim and relay lifetime | native-route-stop, shared-https-lifetime, previous-boot-shared-https, relay-lifecycle-barrier, relay-authorization, relay-staging, relay-fence | Fenced route removal, relay owner, ready/removed protocol, authenticated observations | Native DNS/TLS/browser behavior; old-boot uncertainty and external routing. | | Shared host helper instance: overlapping ups, session adoption, stale create decisions, replacement before finalize, epoch-record failure, interrupted cleanup, concurrent down, displaced launches, failed down session stop | shared-helper-instance | `src/lib/project-shared-helpers.ts` (shutdown generation, `assertCurrent`, `SharedHelperSessionOwnership`); `src/lib/project-lifecycle-controller.ts` session decision, the locked creation transaction (revalidate, publish, create, environment, record, stop on failure, all under one lock), launches fenced by the lock and a token check, abort and signal cleanup through the same epoch decision (`runIfOwned`), an unknown exact-presence answer failing the inspection, and the locked conditional finalize; `stopSessionBeforeReleasingHelpers` (down, restart, native retirement keep holders when the session stop fails); `runMuxCommand` bounds every lifecycle and backend mux call so it settles before the lock is released, and reports a timeout as unknown (never absence); `tests/mux-command-timeout.test.ts`; `tests/project-lifecycle-controller-ownership.test.ts`, `tests/project-shared-helpers.test.ts`, `tests/native-project-down.test.ts`, e2e `shared-host-helpers` | Helper holder/rollback and claim protocol are not modeled (claim fixtures cover them); timeout settlement is an assumption the code does not guarantee (a killed tmux client's queued command may still apply, so a late kill or window command can reach a newer session; consequences and the session-ID fence, not in this slice, are in the README); zellij is refused for shared-helper lifecycle sessions (token written after creation); the gap between a down's session stop and its release (an up that captured after the stopping mark can still succeed there) is a documented first-slice limitation; real mux/process/lock-file behavior. | | Dependency rebind, incomplete initializer, terminal reuse | dependency-rebind, stopped-pool-startup, restore-history | Dependency claim/readiness, saved execution, restore history and source convergence tests | Actual installer failure, cache corruption, retained application state and resource plateau. | -| Native image builds: unleased build versus engine stop, crash mid-build, storage recreation, foreign or forged images, reclamation versus retained graph references | native-build-retention | `provider::image_build` (shared build fence, per-key lock, incarnation/boot/engine recheck and label check at adoption, dead-attempt recording) and `image_build::reclaim` (owned labels, current receipts, retained graph state scan, engine non-force removal); `image_build` regressions | One key and namespace; an orphaned client after a host crash is not modeled (the fence is released with its holder); real BuildKit, engine removal semantics and guest storage are host evidence. | +| Native image builds: unleased build versus engine stop, crash mid-build, storage recreation, foreign or forged images, reclamation versus retained graph references | native-build-retention | `provider::image_build` (shared build fence, per-key lock, incarnation/boot/engine recheck and label check at adoption, dead-attempt recording) and `image_build::reclaim` (owned labels, current receipts, retained graph state scan, engine non-force removal); `image_build` regressions | One key and namespace; a build client orphaned by a killed `hack-native` is not modeled (the client inherits the build fence and per-key lock, so both stay held until it exits: `image_build::tests::a_killed_coordinator_leaves_its_client_fenced`); real BuildKit, engine removal semantics and guest storage are host evidence. | | MCP cold start, cancellation and duplicate launches | mcp-startup, mcp-startup-cancellation | Shared MCP bundle identity, startup deduplication and cancellation regressions | Fresh supported client sessions, full workflow coverage and measured overhead (WU16/WU20/WU28). | | Software install/upgrade/rollback, active launcher versus selection, compatibility | **Coverage gap:** no maintained model here is an installer/selection refinement | `scripts/install-prerelease.py`, prerelease-install/Python installer tests, candidate-install contract | Add a bounded selection/lock/crash/compatibility model before primary-driver promotion; real official-artifact upgrade/rollback still required. | | Primary-driver promotion and rollback to stable | **Coverage gap:** staged readiness policy is not an implemented state machine proof | Reviewed release manifest, per-project opt-in, explicit stable/candidate ownership records | No active-project switch until exact candidate/artifact and rollback/data compatibility are qualified. | diff --git a/tests/models/tla/README.md b/tests/models/tla/README.md index 2ebe1b8f4..f9b3f87ee 100644 --- a/tests/models/tla/README.md +++ b/tests/models/tla/README.md @@ -1070,6 +1070,7 @@ Three controls each remove one guard and must fail at the named action: `negative` (reclaim ignores retained references) fails `NoReclaimReferenced` at `Reclaim`; `foreign-adoption` (adoption without the label/incarnation check) fails `NoForeignAdoption` at `CompleteBuild`; `down-under-build` (down ignores the fence) -fails `DownNotUnderBuild` at `Down`. The model does not cover an orphaned build client -that outlives a crashed host process, real BuildKit or engine behavior, receipt -durability, or more than one key and namespace. +fails `DownNotUnderBuild` at `Down`. The model does not cover a build client that +outlives a killed `hack-native` process (the implementation keeps the fence and key +lock held by the inherited descriptors until that client exits), real BuildKit or +engine behavior, receipt durability, or more than one key and namespace.