Skip to content

5.2 Checkpoint Resume Property Suite

Jump to bottom
Raul Cardenas Montoya edited this page Sep 19, 2026 · 1 revision

Checkpoint Resume Property Suite

Relevant source files

The following files were used as context for generating this wiki page:

Purpose and Scope

The Checkpoint Resume Property Suite (tests/checkpoint_resume/) verifies state persistence and restoration invariants for SynapticMesh tests/checkpoint_resume/main.rs:3-9. It asserts that a SynapticMesh restored from a serialized checkpoint continues to execute tick-for-tick identically to an uninterrupted live mesh tests/checkpoint_resume/main.rs:3-4. The suite tests both JSON and postcard (binary) serialization formats across bounded CI runs and extensive nightly property-testing profiles tests/checkpoint_resume/compare.rs:10-36, tests/checkpoint_resume/main.rs:21-38.

Sources:

Harness Architecture and Configuration

The test harness is structured across multiple submodules in tests/checkpoint_resume/:

Configuration Constants

The suite defines execution caps and environment overrides in tests/checkpoint_resume/harness.rs:

graph TD
    A["resume_equivalence_seeded_ci"] --> B["Scenario::from_seed"]
    B --> C["Scenario::mesh"]
    C --> D["apply_event Prefix"]
    D --> E["SerdeFormat::restore"]
    E --> F["meshes_equivalent"]
    F --> G["apply_event Suffix Tick"]
    G --> H["meshes_equivalent Final"]
    
    subGraph "Harness Modules"
        M1["tests/checkpoint_resume/main.rs"]
        M2["tests/checkpoint_resume/harness.rs"]
        M3["tests/checkpoint_resume/generate.rs"]
        M4["tests/checkpoint_resume/compare.rs"]
        M5["tests/checkpoint_resume/recipes.rs"]
    end
Loading

Figure 1: Checkpoint-resume execution flow from seed generation to live-vs-restored equivalence verification.

Sources:

Scenario Generation and Recipe System

Scenarios are built deterministically using a custom SplitMix64 pseudo-random number generator seeded by an integer index tests/checkpoint_resume/harness.rs:129-166, tests/checkpoint_resume/generate.rs:12-29. Each seed maps to one of ten distinct architectural Recipe variants defined in tests/checkpoint_resume/harness.rs tests/checkpoint_resume/harness.rs:25-56:

  1. EmptyGraph: Zero-neuron topology with idle ticks tests/checkpoint_resume/generate.rs:43-53
  2. SingleNeuron: Single neuron with optional self-loop and variable axonal delay tests/checkpoint_resume/recipes.rs:10-31
  3. DelayZero: Multi-neuron graphs with zero-delay synaptic connections tests/checkpoint_resume/recipes.rs:33-56
  4. DelayCapacity: Ring-buffer saturation and capacity boundary testing tests/checkpoint_resume/recipes.rs:58-81
  5. MultiSpikeSameSlot: Multiple spikes arriving at identical ring-buffer delay slots tests/checkpoint_resume/recipes.rs:83-106
  6. CheckpointBeforeDelivery: Checkpointing precisely one tick before in-flight spike delivery tests/checkpoint_resume/recipes.rs:108-128
  7. SignedWeights: Interleaved excitatory and inhibitory polarities with graded and binary activations tests/checkpoint_resume/recipes.rs:130-151
  8. EmptyTicks: Extended sequences of empty propagation ticks tests/checkpoint_resume/recipes.rs:153-168
  9. GeneratedRandom: Erdos-Renyi random topology generation via generate_random tests/checkpoint_resume/recipes.rs:170-177
  10. GeneratedSmallWorld: Watts-Strogatz small-world topology generation via generate_small_world tests/checkpoint_resume/recipes.rs:179-187 
graph TD
    Seed["u64 seed"] --> RecipeSel["Recipe::from_seed"]
    RecipeSel --> SplitGen["SplitMix64::new"]
    SplitGen --> ScenGen["Scenario::from_seed"]
    
    subGraph "Recipes [tests/checkpoint_resume/recipes.rs]"
        ScenGen --> R1["EmptyGraph"]
        ScenGen --> R2["SingleNeuron"]
        ScenGen --> R3["DelayZero"]
        ScenGen --> R4["DelayCapacity"]
        ScenGen --> R5["MultiSpikeSameSlot"]
        ScenGen --> R6["CheckpointBeforeDelivery"]
        ScenGen --> R7["SignedWeights"]
        ScenGen --> R8["EmptyTicks"]
        ScenGen --> R9["GeneratedRandom"]
        ScenGen --> R10["GeneratedSmallWorld"]
    end
Loading

Figure 2: Mapping from seed space to structural recipes within tests/checkpoint_resume/recipes.rs.

Sources:

Equivalence Checking and Serde Formats

The comparison module (tests/checkpoint_resume/compare.rs) defines the SerdeFormat enum supporting Json and Postcard tests/checkpoint_resume/compare.rs:9-13.

Restoration and Validation Pipeline

The restoration method serializes a live SynapticMesh into a byte vector or string, then deserializes it into a distinct restored instance tests/checkpoint_resume/compare.rs:23-35.

The meshes_equivalent function serializes both live and restored meshes into serde_json::Value snapshots to compare graph layout, internal ring buffer slots, and current ticks tests/checkpoint_resume/compare.rs:42-79. If discrepancies occur, it generates a comprehensive diff summary reporting differing fields, ticks, and queued deliveries tests/checkpoint_resume/compare.rs:48-77.

graph TD
    LiveMesh["SynapticMesh live"] --> SerdeAction["SerdeFormat::restore"]
    SerdeAction -->|Json / Postcard| RestoredMesh["SynapticMesh restored"]
    LiveMesh --> SnapLive["checkpoint_snapshot"]
    RestoredMesh --> SnapRest["checkpoint_snapshot"]
    SnapLive --> Comp["meshes_equivalent"]
    SnapRest --> Comp
    Comp -->|Match| Success["Ok(())"]
    Comp -->|Mismatch| Err["Err(String diff)"]
Loading

Figure 3: Live-vs-restored equivalence check pipeline in tests/checkpoint_resume/compare.rs.

Sources:

Greedy Shrinker

When property tests encounter a failure, the harness invokes a greedy minimization shrinker (shrink) to reduce counterexamples before panicking tests/checkpoint_resume/compare.rs:126-134.

The shrinking loop (shrink_step) attempts three reduction strategies sequentially tests/checkpoint_resume/compare.rs:136-140:

  1. shrink_remove_one_event: Iteratively removes individual tick events from the prefix sequence tests/checkpoint_resume/compare.rs:142-159.
  2. shrink_remove_one_event: Iteratively removes individual tick events from the suffix sequence tests/checkpoint_resume/compare.rs:142-159.
  3. shrink_remove_one_descriptor: Iteratively removes individual SynapseDescriptor entries from the graph topology while updating buffer_max_delay tests/checkpoint_resume/compare.rs:161-180.

Sources:

Key Test Cases and Regression Fixtures

The test suite includes explicit regression tests and frozen snapshots in tests/checkpoint_resume/main.rs:

Sources:

synaptic-wiring DeepWiki

Clone this wiki locally