diff --git a/docs/guides/native-candidate.md b/docs/guides/native-candidate.md index 0d778fd12..51ec9bf11 100644 --- a/docs/guides/native-candidate.md +++ b/docs/guides/native-candidate.md @@ -503,6 +503,19 @@ linked, mode-`0600` file owned by you): stops the client's whole process group; so does the time budget (default 30 minutes, at most 2 hours). Both also apply while base images resolve, before the client starts: the budget covers the whole operation. +- 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. 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 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..2db9b9fb8 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; 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. | @@ -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 b088e78d8..371484822 100644 --- a/packages/runtime-core/src/provider/image_build.rs +++ b/packages/runtime-core/src/provider/image_build.rs @@ -69,6 +69,7 @@ use std::{ }; mod output; +pub mod reclaim; #[cfg(test)] mod tests; @@ -91,6 +92,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] = [ @@ -169,6 +177,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. @@ -195,6 +207,10 @@ pub(super) struct Receipt { phase: Phase, #[serde(default, skip_serializing_if = "Option::is_none")] image_id: Option, + /// 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, } @@ -228,6 +244,17 @@ pub(super) trait BuildPool { fn builder(&self) -> Result; /// Where the client's filtered output goes. fn output(&self) -> Box; + /// 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. @@ -757,6 +784,7 @@ pub(super) fn run( tag: inputs.tag(), reused: true, base_pins: previous.base_pins.clone(), + cache_reclaimed_bytes: None, }); } } @@ -769,6 +797,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. @@ -809,6 +838,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(), @@ -819,6 +854,9 @@ pub(super) fn run( engine_id: identity.engine_id.clone(), phase: Phase::Building, image_id: 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,10 +940,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. @@ -920,7 +958,10 @@ pub(super) fn run( }; receipt.phase = Phase::ContentIdVerified; receipt.image_id = Some(id.clone()); + 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(); drop(lease); Ok(BuildOutcome { image_id: id, @@ -928,6 +969,7 @@ pub(super) fn run( tag: inputs.tag(), reused: false, base_pins: pins, + cache_reclaimed_bytes, }) } @@ -1369,6 +1411,53 @@ impl<'a> BuildPool for LivePool<'a> { fn output(&self) -> Box { Box::new(std::io::stderr()) } + 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.", + ) + }) } /// Run a blocking, effect-free network step on its own thread and wait for it until 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..4e19e718d --- /dev/null +++ b/packages/runtime-core/src/provider/image_build/reclaim.rs @@ -0,0 +1,433 @@ +//! `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. 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 +//! 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, &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), + Err(error) => Err(error), + } + } +} + +/// 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 }) +} + +#[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 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(); + 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 9e44f6e46..921b3d97c 100644 --- a/packages/runtime-core/src/provider/image_build/tests.rs +++ b/packages/runtime-core/src/provider/image_build/tests.rs @@ -141,10 +141,14 @@ 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>, resolve_delay: Duration, resolve_deadlines: RefCell>, output: Arc>>, @@ -152,10 +156,14 @@ struct FakePool { 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()), resolve_delay: Duration::ZERO, resolve_deadlines: RefCell::new(Vec::new()), output: Arc::default(), @@ -170,7 +178,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}}), ); } } @@ -212,6 +220,13 @@ impl BuildPool for FakePool { fn output(&self) -> Box { Box::new(Captured(Arc::clone(&self.output))) } + 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) + } } /// The caller's stream as the fake pool sees it. @@ -439,6 +454,7 @@ fn receipts_with_the_most_and_longest_accepted_pins_stay_readable() { engine_id: "e".repeat(128), phase: Phase::ContentIdVerified, image_id: Some(IMAGE.into()), + image_bytes: Some(5 * GIB), base_pins: BTreeMap::new(), }; // The scanner's bounds: 32 images, Docker Hub paths up to 200 bytes, tags up to @@ -917,6 +933,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(); @@ -1240,3 +1257,130 @@ 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); + + // 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 { + 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..f9b3f87ee 100644 --- a/tests/models/tla/README.md +++ b/tests/models/tla/README.md @@ -1049,3 +1049,28 @@ 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 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. 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