zacheryasc/swactor
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(provisioning): stateful conformance kit for reconciler and plugins

Browse source 
Replace pointwise scenario testing with a reusable conformance kit in
tests/common: a deterministic trace harness (input alphabet, seeded
generator, naive shrinker), an invariant oracle covering twenty black-box
guarantees (identity, correlation, dead-hold, attempt-fact ownership,
quiescence no-op, monotonic generation, fair convergence, bounded
replacement), and a fair-scheduler tail asserting eventual reconciliation.

Three conformance levels run the same battery:
- FakeBackend: the reference in-memory substrate (256 seeds x 2 modes)
- PluginBackendAdapter over FakePlugin: seam contracts plus the battery
- ProcessPlugin: real child processes, faults as real signals/errors;
  "no double-create" and "converged leaks nothing" verified by counting
  live PIDs (16 seeds)

Also documents two seam findings the battery surfaced: ProvisionPlugin
cannot express ambiguity (kit convention: AMBIGUOUS_FAULT_MARKER error
reclassified by the adapter; definite classification leaks provider
resources) and spawn_effect closures form a spawner Arc cycle that leaks
backends under queue-based spawners (kit breaks it at harness drop).
This commit is contained in:
Zachery Aaron Shores-Chmielewski 2026-08-14 19:21:46 +04:00
parent b8aff00dc1
commit 9ea17edec1
6 changed files with 1958 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
crates/provisioning/Cargo.toml
View file

@ -9,4 +9,5 @@ publish = false
serde = { version = "1", features = ["derive"] } serde = { version = "1", features = ["derive"] }
[dev-dependencies] [dev-dependencies]
parking_lot = "0.12"
serde_json = "1" serde_json = "1"

226
crates/provisioning/README.md Normal file
View file

@ -0,0 +1,226 @@
# provisioning — the cluster reconciler
This crate drives a declared cluster shape toward convergence. A caller states
*what the run should look like* — which node groups, how many of each, with what
provider shape and boot parameters — and the reconciler repeatedly compares that
desired shape against observed reality, taking the next safe step for each node
until the two match. It is modeled on Kubernetes controller mechanics
(level-triggered decisions, spec/status separation, workqueue-style coalescing,
finalizer-style deletion) but runs entirely in-process over the Swactor/Myelin
engine: there is no API server, and no persistence beyond the process lifetime.
The payoff over the imperative lifecycle it replaced: the system converges from
whatever state it is currently in. A reconcile pass is a pure function of
`(observed, desired, now)` — never of the event that triggered it — so missed
events, duplicated events, and crash-of-a-single-pass all heal on the next
pass. Reconcile is a function of state, not events.
## The three roles
One state-ownership rule upholds the design: **only the driver mutates observed
state.**
| Role | Embodiment | Responsibility |
|---|---|---|
| Decider | `reconcile` / `reconcile_node` | Pure, deterministic: reads state snapshots, returns next actions. No I/O, no clocks, no randomness. |
| Driver | `ClusterDriver` | Sole writer of `ClusterState`. Folds observations, coalesces triggers, runs passes, records operations as pending *before* dispatch, schedules requeues. |
| Executor | `EffectExecutor` / `IdempotentEffectExecutor` + a provider `EffectBackend` | Runs provider I/O off the pass, deduplicates by operation identity, adopts resources after ambiguous outcomes. |
## Inputs
**Desired state** — `ClusterShape { run_id, generation, groups }`. It expands to
one `LogicalNodeSpec` per slot named `{group_id}-{index}`; validation rejects
cross-run groups, duplicate group or node IDs, and non-finite shape values.
The driver additionally enforces a revision contract: the run ID is fixed for
its lifetime, `generation` must strictly increase whenever shape content
changes, and changed content at the same generation is rejected. A node's spec
is an immutable attempt template — any drift (image, boot, role, provider,
swarm-join) means *replace the attempt*, never mutate it in place.
**Observed state** — `ClusterState`: the last-evaluated generation, a monotonic
attempt-ID allocator, and one `ManagedNode` per logical slot. A `ManagedNode`
carries its attempt ID, intent (`Active` / `Deleting`), the lifecycle-fact
record (`NodeRecord`), at most **one** pending operation, and per-node retry
state. Identity is layered: a `LogicalNodeId` is the stable slot;
a `NodeAttemptId` names one incarnation of that slot (like a k8s object name
vs its UID); an `OperationId` (attempt + sequence) names one dispatched effect.
Results from an old attempt can never mutate a newer one.
**Events** — executor results, bootstrap stream observations, timeouts, and a
periodic tick. Events carry no decision input; they only mark the cluster
dirty and are folded into observed state before the next pass looks.
## Reconciliation flow
Per node, progress is a ladder of stages crossed by one effect at a time, with
a deletion track that runs to completion once entered:
```mermaid
stateDiagram-v2
[*] --> New : Insert (desired slot, fresh attempt)
New --> LeaseRequested : Dispatch CreateLease
LeaseRequested --> LeaseCreated : lease observed, endpoint unknown
LeaseRequested --> EndpointKnown : lease + endpoint observed
LeaseCreated --> EndpointKnown : LookupEndpoint succeeds
LeaseCreated --> LeaseCreated : LookupEndpoint : not ready yet (probe)
EndpointKnown --> BootstrapRunning : StartBootstrap accepted
BootstrapRunning --> BootstrapRunning : bootstrap stream observations
BootstrapRunning --> SwactorJoined : swactor joins the swarm
SwactorJoined --> Dormant : convergence observed / bootstrap closed
Dormant --> [*] : ready steady state
LeaseRequested --> LeaseRequested : CreateLease fails (backoff, retry)
EndpointKnown --> Failed : bootstrap fails to start
BootstrapRunning --> Failed : bootstrap runtime / join failure
SwactorJoined --> Failed : bootstrap closes before convergence
Failed --> Deleting : BeginDelete (next pass)
New --> Deleting : BeginDelete (slot undesired or spec drifted)
Dormant --> Deleting : BeginDelete (scale-down / replacement)
Deleting --> Deleting : CancelBootstrap → DestroyLease (in order)
Deleting --> Destroyed : cleanup complete (MarkDestroyed)
Destroyed --> [*] : Reap (slot undesired)
Destroyed --> New : Restart after restart_at backoff (still desired)
```
A pass picks **at most one action per node**; a driver transition
(`Insert`, `BeginDelete`, `MarkDestroyed`, `Restart`, `Reap`) completes that
node's step, and its follow-on effect is considered in a later pass. Nodes
progress independently — one node's slow provider I/O never blocks another.
### The per-pass decision ladder
For each node, the decider's rules in priority order (first match wins):
| # | Condition | Action |
|---|---|---|
| 1 | stage `Destroyed`, slot undesired | `Reap` — remove from the map |
| 2 | stage `Destroyed`, slot desired, `restart_at` due | `Restart` — fresh attempt, latest spec |
| 3 | stage `Destroyed`, restart backoff not due | wait until `restart_at` |
| 4 | intent `Active` and (undesired, spec drift, or stage `Failed`) | `BeginDelete` |
| 5 | an operation is pending | wait for its result or stored deadline |
| 6 | intent `Deleting`, ambiguous create/bootstrap remembered | re-dispatch that create (executor adopts) |
| 7 | intent `Deleting`, active bootstrap session | `CancelBootstrap` |
| 8 | intent `Deleting`, lease still live | `DestroyLease` |
| 9 | intent `Deleting`, nothing left to clean | `MarkDestroyed` |
| 10 | retry backoff (`next_effect_at`) not due | wait |
| 11 | ready in `HandedOff` / `Dormant` | none — steady state |
| 12 | no lease | `CreateLease` |
| 13 | lease but no SSH endpoint | `LookupEndpoint` |
| 14 | stage `SwactorJoined` with live session | `BootstrapConvergenceObserved` |
| 15 | bootstrap running, awaiting observations | none — await stream events |
| 16 | lease + endpoint, no bootstrap session | `StartBootstrap` |
Rows 1–4 handle topology (scale up is an `Insert` seen before row 1); rows
5–10 handle in-flight work and deletion; rows 11–16 are the healthy
progression ladder. Cleanup ordering is deliberately sequential — cancel
bootstrap, then destroy the lease, then mark destroyed — so partial success is
never ambiguous.
## Triggers and requeues
The driver is the process-local equivalent of a single-key Kubernetes
workqueue: one pass runs at a time (reentry is an error), triggers while
queued collapse, and a trigger during a pass marks dirty and guarantees exactly
one follow-up pass.
| Trigger | Source | Effect |
|---|---|---|
| Desired shape update | `update_desired` (validated, generation advanced) | queue a pass |
| Executor result | operation completed / failed | fold observation, queue a pass |
| Bootstrap observation | stream stage, swactor join, closure, failure | fold observation, queue a pass |
| Operation timeout | stored pending-operation deadline | fold as ambiguous failure, queue a pass |
| Retry / probe / restart deadline | `trigger_if_due(now)` against `requeue_at` | queue a pass |
| Periodic wake | host tick (safety net, not the progress mechanism) | queue a pass if due |
Every pass recomputes `requeue_at` as the earliest deadline among waiting
nodes (pending-operation deadlines, backoff, probes, restarts). The host
(`apps/myelin`'s `ProvisionedClusterGuard`) drives `drive_until_blocked` on
each wake and re-arms the timer.
## Node conditions
`NodeStage` is the observation ladder; `ready` is the convergence flag:
| Stage | Meaning |
|---|---|
| `New` | slot inserted, nothing dispatched yet |
| `LeaseRequested` | `CreateLease` dispatched, pending |
| `LeaseCreated` | provider lease exists; SSH endpoint not yet known |
| `EndpointKnown` | lease + reachable SSH endpoint recorded |
| `BootstrapRunning` | bootstrap session started; stream observations flowing |
| `SwactorJoined` | the node's swactor joined the swarm |
| `HandedOff` | host marked handoff complete (reserved; the ready-check accepts it) |
| `Dormant` | bootstrap finished, handoff recorded — **ready** steady state |
| `Failed` | attempt-ending failure recorded (`failed_reason`, `failed_at`) |
| `Destroyed` | cleanup finished; awaiting reap or restart |
Bootstrap internals (`BootstrapStage`: SSH connect, boot check, swactor start,
join, converged, plus five failure stages) are facts folded into the record;
they update progress but the reconciler only branches on their failure/converged
classes, never on individual stream events.
## Failure and backoff
Not every failed call kills an attempt. Classification by operation:
| Failure | Retained state | Behavior |
|---|---|---|
| `CreateLease` | nothing | retry after exponential backoff |
| `LookupEndpoint` (not ready) | lease | re-probe on probe interval — not a failure |
| `LookupEndpoint` (error) | lease | retry after backoff |
| `StartBootstrap`, bootstrap runtime, or join | facts for observability | **attempt fails**: cleanup starts immediately; backoff applies to the *restart*, not the cleanup |
| `CancelBootstrap` / `DestroyLease` | stay in `Deleting` | retry after backoff |
| any timeout / ambiguous create | remembered | retry re-issues the same create so the executor adopts first |
Backoff is per node: exponential from 1 s to a 60 s cap (defaults), with
optional jitter sampled *deterministically* from the attempt ID — the decider
never reads randomness or a clock. Deadlines are computed once when an
observation is folded and stored; the pure decider only reads them. Reaching
ready resets the failure count. A failed attempt's `consecutive_failures`
carries into its replacement so hot-restart loops still back off.
## What is guaranteed
| Class | Guarantee |
|---|---|
| Determinism | Identical traces converge to identical state; execution order of independent work doesn't matter; a pass over a settled machine is a no-op. |
| Attempt isolation | Attempt IDs are never reused; results and facts from a superseded or retired attempt are discarded, never folded or leaked into a replacement. |
| No unrecorded effects | Every effect is recorded as pending before submission; one pending operation per node, one running per attempt; a destroyed node holds no lease, session, or pending operation; failed cleanup keeps its live facts. |
| Failure classification | Per-node backoff with one stored deadline; attempt failure cleans up immediately and delays only the restart; endpoint-not-ready is a probe, not a failure; ambiguous outcomes adopt before any destructive step; exhaustion and clock saturation are errors, never spins or panics. |
| Bounded convergence | Converges to the latest desired shape — intermediate generations may be skipped — in bounded rounds once faults stop; scale-down removes only highest-index slots; replacement starts a fresh attempt only after full cleanup; generation regressions and silent shape changes are rejected. |
## Operation identity and idempotency
A deterministic plan is not by itself a safe side effect; safety comes from the
identity contract:
- The driver records an operation as pending **before** dispatch and never
emits a second operation for a node while one is pending. If submission
itself fails, that folds as an operation failure — no unrecorded in-flight
effect is ever observable.
- The executor deduplicates by `OperationId`: resubmitting a completed
operation replays its recorded result; reusing an ID with different input is
rejected; at most one operation runs per attempt at a time.
- Provider backends must key external requests on
`(run_id, logical_node_id, attempt)` and **adopt** an existing resource for
that identity before creating anew; cancel/destroy treat "already absent" as
success.
- Timeouts expire an operation as *ambiguous* only after the executor
classifies it; a late completion is discarded rather than folded.
## Convergence and boundaries
The cluster is converged for a generation when every desired slot holds the
exact desired spec with `ready`, `Active` intent, and no pending operation,
and no undesired or deleting nodes remain. `observed_generation ==
generation` alone means only "the driver has evaluated that shape," not
readiness.
Deliberately out of scope (v1): persistence and crash recovery — the identity
and adoption rules are the shape a later durability guarantee would build on —
leader election, availability-budgeted rollouts, and any provider-specific
behavior (backends live in application crates). The normative design spec,
including the full invariants list, is archived at
`docs/specs/archive/RECONCILER_SPEC.md`.

1320
crates/provisioning/tests/common/mod.rs Normal file
View file

File diff suppressed because it is too large Load diff

25
crates/provisioning/tests/plugin_conformance.rs Normal file
View file

@ -0,0 +1,25 @@
//! Plugin-level conformance: the kit's reference in-memory plugin runs
//! the seam contracts and the full trace battery through the real
//! `PluginBackendAdapter` — one conformance level below the fake
//! backend, still without leaving the crate.
mod common;
use common::{assert_plugin_contracts, run_trace_battery, FakePlugin, PluginBackendAdapter};
#[test]
fn in_memory_plugin_passes_seam_contracts() {
let mut plugin = FakePlugin::default();
assert_plugin_contracts(&mut plugin);
}
#[test]
fn in_memory_plugin_battery_holds_invariants_and_converges() {
run_trace_battery(
|| PluginBackendAdapter::new(FakePlugin::default()),
256,
64,
);
}

169
crates/provisioning/tests/process_conformance.rs Normal file
View file

@ -0,0 +1,169 @@
//! Process-level conformance: a `ProvisionPlugin` whose resources are
//! real OS processes (`sleep infinity` children). The kit battery and
//! seam contracts run against it, so "no double-create", "destroy
//! releases", "ambiguous create adopts", and "converged leaks nothing"
//! are verified by counting actual live PIDs.
mod common;
use std::collections::{BTreeMap, VecDeque};
use std::process::{Child, Command};
use std::sync::Arc;
use parking_lot::Mutex;
use provisioning::plugin::{
NodeProvisionSpec, PluginNodeHandle, PluginSink, ProvisionPlugin,
};
use common::{
assert_plugin_contracts, run_trace_battery, AMBIGUOUS_FAULT_MARKER, Fault, TestablePlugin,
PluginBackendAdapter,
};
struct ProcessPluginState {
faults: VecDeque<Fault>,
/// attempt -> live child, present until stopped.
children: BTreeMap<u64, Child>,
created: usize,
}
/// A process provisioner: create spawns a real child keyed by attempt,
/// stop kills and reaps it, ambiguous faults spawn-then-fail.
struct ProcessPlugin {
state: Arc<Mutex<ProcessPluginState>>,
}
impl Default for ProcessPlugin {
fn default() -> Self {
Self {
state: Arc::new(Mutex::new(ProcessPluginState {
faults: VecDeque::new(),
children: BTreeMap::new(),
created: 0,
})),
}
}
}
impl Drop for ProcessPlugin {
fn drop(&mut self) {
// CI hygiene: never leave children behind, even on failure.
let mut state = self.state.lock();
let children: Vec<Child> = std::mem::take(&mut state.children).into_values().collect();
for mut child in children {
let _ = child.kill();
let _ = child.wait();
}
}
}
impl TestablePlugin for ProcessPlugin {
fn apply_fault(&self, fault: Fault) {
let mut state = self.state.lock();
match fault {
Fault::Heal => state.faults.clear(),
other => state.faults.push_back(other),
}
}
fn leaked_resources(&self, live_handles: &[u64]) -> Vec<String> {
let state = self.state.lock();
state
.children
.keys()
.filter(|attempt| !live_handles.contains(attempt))
.map(|attempt| {
let pid = state
.children
.get(attempt)
.map(|child| child.id())
.unwrap_or_default();
format!("attempt={attempt} pid={pid}")
})
.collect()
}
fn resources_created(&self) -> usize {
self.state.lock().created
}
}
impl ProvisionPlugin for ProcessPlugin {
fn create_node(
&mut self,
spec: NodeProvisionSpec,
_sink: PluginSink,
) -> Result<PluginNodeHandle, String> {
let mut state = self.state.lock();
let attempt = spec.attempt_id;
if let Some(child) = state.children.get(&attempt) {
// Adoption: the child for this attempt already exists.
return Ok(PluginNodeHandle {
id: attempt,
provider_process_id: Some(child.id()),
});
}
let fault = state.faults.pop_front();
if matches!(fault, Some(Fault::Panic)) {
panic!("scripted process plugin panic");
}
if matches!(fault, Some(Fault::Definite)) {
return Err("scripted definite failure".to_owned());
}
let child = Command::new("sleep")
.arg("infinity")
.spawn()
.map_err(|error| format!("spawn failed: {error}"))?;
let pid = child.id();
state.children.insert(attempt, child);
state.created += 1;
if matches!(fault, Some(Fault::Ambiguous)) {
// The child exists but the caller cannot know; a retry with
// the same attempt must adopt it.
return Err(AMBIGUOUS_FAULT_MARKER.to_owned());
}
Ok(PluginNodeHandle {
id: attempt,
provider_process_id: Some(pid),
})
}
fn start_bootstrap(&mut self, _handle: &PluginNodeHandle) -> Result<(), String> {
Ok(())
}
fn cancel_bootstrap(&mut self, _handle: &PluginNodeHandle) -> Result<(), String> {
Ok(())
}
fn complete_bootstrap(&mut self, _handle: &PluginNodeHandle) -> Result<(), String> {
Ok(())
}
fn stop_node(&mut self, handle: &PluginNodeHandle) -> Result<(), String> {
let mut state = self.state.lock();
if let Some(mut child) = state.children.remove(&handle.id) {
child
.kill()
.map_err(|error| format!("kill failed: {error}"))?;
child
.wait()
.map_err(|error| format!("reap failed: {error}"))?;
}
Ok(())
}
}
#[test]
fn process_plugin_passes_seam_contracts() {
let mut plugin = ProcessPlugin::default();
assert_plugin_contracts(&mut plugin);
// Belt and braces: contracts released everything.
assert!(plugin.leaked_resources(&[]).is_empty());
}
#[test]
fn process_plugin_battery_holds_invariants_and_converges() {
run_trace_battery(|| PluginBackendAdapter::new(ProcessPlugin::default()), 16, 28);
}

217
crates/provisioning/tests/reconciler_stateful.rs Normal file
View file

@ -0,0 +1,217 @@
//! Stateful property tests for the cluster reconciler over the kit's
//! reference `FakeBackend`. The harness, oracle, and generator live in
//! `common`; this file is a thin client pinning named guarantees.
mod common;
use std::time::{Duration, UNIX_EPOCH};
use common::{
check_invariants, gen_trace, group, group_with_role, run_trace, sanitized, shape, BootEvent,
Harness, Input, RecordingExecutor, Reply, RunOrder,
};
use provisioning::*;
// ── plain deterministic tests ─────────────────────────────────────────
#[test]
fn replayed_traces_are_identical() {
for seed in 0..32 {
let trace = gen_trace(seed, 48);
let first = run_trace(seed, &trace, false, RunOrder::Fifo);
let second = run_trace(seed, &trace, false, RunOrder::Fifo);
assert_eq!(*first.state(), *second.state(), "seed {seed}");
assert_eq!(first.backend.calls(), second.backend.calls(), "seed {seed}");
}
}
#[test]
fn happy_path_converges() {
let mut harness = Harness::new_with_backend(0, shape(1, vec![group("g0", 1)]), common::FakeBackend::default());
harness.step(Input::Run); // dispatch create lease
harness.step(Input::Run); // execute create, dispatch bootstrap start
harness.step(Input::Run); // execute bootstrap start, session active
harness.step(Input::Boot(BootEvent::Joined));
harness.step(Input::Boot(BootEvent::Closed));
harness.step(Input::Run); // bootstrap convergence accepted
assert!(harness.driver.is_converged());
assert!(harness.backend.calls().iter().any(|effect| {
matches!(effect.command, NodeManagerCommand::CreateLease(_))
}));
}
#[test]
fn ambiguous_create_is_adopted_and_converges() {
let mut harness = Harness::new_with_backend(0, shape(1, vec![group("g0", 1)]), common::FakeBackend::default());
harness.step(Input::Reply(Reply::Ambiguous("create timed out")));
harness.step(Input::Run); // create fails ambiguously, backoff starts
harness.step(Input::Tick(Duration::from_secs(10))); // retry/adopt
harness.fair_tail();
assert!(harness.driver.is_converged());
}
#[test]
fn shape_shrink_mid_lifecycle_converges() {
let mut harness = Harness::new_with_backend(0, shape(1, vec![group("g0", 2)]), common::FakeBackend::default());
harness.step(Input::Run);
harness.step(Input::Run);
harness.step(Input::Boot(BootEvent::Joined));
// Node g0-1 may be mid-bootstrap when the shape shrinks to one node.
harness.step(Input::Shape(shape(2, vec![group("g0", 1)])));
harness.fair_tail();
assert!(harness.driver.is_converged());
assert_eq!(harness.state().nodes.len(), 1);
assert!(harness
.state()
.nodes
.contains_key(&LogicalNodeId("g0-0".to_owned())));
}
#[test]
fn same_generation_same_content_is_accepted() {
let mut driver = ClusterDriver::new(shape(1, vec![group("g0", 1)]), RetryPolicy::default())
.expect("driver builds");
let identical = driver.desired().clone();
assert!(driver.update_desired(identical).is_ok());
let mut changed = driver.desired().clone();
changed.groups[0].count = 2;
assert!(driver.update_desired(changed).is_err());
}
#[test]
fn deadline_expires_exactly_at_deadline() {
let mut harness = Harness::new_with_backend(0, shape(1, vec![group("g0", 1)]), common::FakeBackend::default());
harness.settle(); // create dispatched at the epoch
let timeout = RetryPolicy::default().operation_timeout;
let node = harness.state().nodes.values().next().expect("node exists");
let pending = node.pending.as_ref().expect("create is pending");
assert_eq!(pending.deadline, UNIX_EPOCH + timeout);
// One tick before the deadline: still pending, nothing expired.
harness.step(Input::Tick(timeout - Duration::from_secs(1)));
let node = harness.state().nodes.values().next().expect("node exists");
assert!(node.pending.is_some(), "operation expired before its deadline");
assert_eq!(node.retry.ambiguous_operation, None);
// Exactly at the deadline: expired, classified ambiguous, never ran.
harness.step(Input::Tick(Duration::from_secs(1)));
let node = harness.state().nodes.values().next().expect("node exists");
assert!(node.pending.is_none(), "operation did not expire at its deadline");
assert_eq!(node.retry.ambiguous_operation, Some(OperationKind::CreateLease));
assert!(
harness.backend.calls().is_empty(),
"expired operation must not reach the backend"
);
}
#[test]
fn clock_extremes_do_not_panic_or_corrupt_state() {
// Near the end of representable time the operation timeout saturates
// (deadline collapses to `now`, i.e. immediately due) while retry
// backoffs still fit; the machine must keep making progress without
// panicking and without corrupting state.
let mut now = UNIX_EPOCH + Duration::from_secs(i64::MAX as u64 - 100);
let step = Duration::from_secs(2);
let mut driver = ClusterDriver::new(shape(1, vec![group("g0", 1)]), RetryPolicy::default())
.expect("driver builds");
let mut executor = RecordingExecutor::default();
let mut guard = 0;
while executor.submitted < 8 {
guard += 1;
assert!(guard <= 64, "driver stopped making progress at clock extremes");
driver.trigger_if_due(now);
driver
.drive_until_blocked(now, &mut executor)
.expect("drive near the end of time");
for operation in driver.pending_operations_due(now) {
assert!(driver.operation_timed_out(&operation, "extreme clock", now));
}
check_invariants(driver.state(), &driver.desired().expand().expect("expands"))
.unwrap_or_else(|violation| panic!("invariant broken at clock extreme: {violation}"));
now = now.checked_add(step).expect("probe clock still representable");
if let Some(requeue) = driver.requeue_at()
&& requeue > now
{
now = requeue
.checked_add(step)
.expect("requeue still representable");
}
}
assert_eq!(executor.submitted, 8);
let policy = RetryPolicy::default();
assert_eq!(policy.delay_for_failure(u32::MAX), policy.max_delay);
}
#[test]
fn attempt_allocator_exhaustion_is_reported() {
let observed = ClusterState {
next_attempt_id: u64::MAX,
..ClusterState::default()
};
let error = reconcile(&observed, &shape(1, vec![group("g0", 1)]), UNIX_EPOCH)
.expect_err("allocator must be exhausted");
assert!(
error.reason.contains("exhausted"),
"unexpected error: {error:?}"
);
}
#[test]
fn latest_desired_wins() {
for seed in 0..16 {
let trace = sanitized(&gen_trace(seed, 32));
let mut harness = Harness::new_with_backend(seed, shape(1, vec![group("g0", 1)]), common::FakeBackend::default());
for input in &trace {
harness.step(input.clone());
}
// A late shape change at a higher generation must win: the final
// state converges to it, never to any earlier generation.
let generation = harness.driver.desired().generation + 1;
harness.step(Input::Shape(shape(
generation,
vec![group_with_role("g0", 2, "worker-late")],
)));
harness.fair_tail();
assert!(harness.driver.is_converged(), "seed {seed}");
assert_eq!(harness.driver.state().observed_generation, generation);
assert_eq!(harness.state().nodes.len(), 2, "seed {seed}");
for node in harness.state().nodes.values() {
assert_eq!(
node.record.desired.role,
RoleId("worker-late".to_owned()),
"seed {seed}"
);
}
}
}
#[test]
fn run_order_confluence() {
for seed in 0..16 {
let trace = sanitized(&gen_trace(seed, 48));
let fifo = run_trace(seed, &trace, true, RunOrder::Fifo);
let lifo = run_trace(seed, &trace, true, RunOrder::Lifo);
assert_eq!(*fifo.state(), *lifo.state(), "seed {seed}");
}
}
// ── stateful property tests ───────────────────────────────────────────
const SEEDS: u64 = 256;
const TRACE_LEN: usize = 64;
#[test]
fn adversarial_traces_hold_invariants() {
for seed in 0..SEEDS {
let trace = gen_trace(seed, TRACE_LEN);
common::assert_trace(common::FakeBackend::default, seed, &trace, false);
}
}
#[test]
fn fair_traces_converge() {
for seed in 0..SEEDS {
let trace = gen_trace(seed, TRACE_LEN);
common::assert_trace(common::FakeBackend::default, seed, &trace, true);
}
}