lib/machine/src/explore/distributed/root.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

  1 //! A tool that searches for bugs earns trust by finding a real one in a running
  2 //! system and replaying it on demand. This namespace runs a small three-node
  3 //! commit protocol with a bug planted on purpose, and a gate that has to find
  4 //! the bug, shrink it, replay it, and show that the fixed protocol survives the
  5 //! same search.
  6 //!
  7 //! In the protocol, node 0 coordinates rounds. Opening a round sends a proposal
  8 //! to the other two nodes, a node that receives the proposal accepts it and
  9 //! replies with an acknowledgement, and the coordinator announces a commit once
 10 //! its own vote plus the acknowledgements it counted reach two. Two safety
 11 //! rules are declared before any search runs: a commit needs two nodes that
 12 //! accepted the current round's value, and a node never accepts a proposal from
 13 //! an older round. The gate answers by passing or failing the package tests,
 14 //! and on success it returns a report for a renderer to show.
 15 //!
 16 //! A rule or a seed picked after seeing the failure proves nothing, so the
 17 //! rules are fixed ahead of the search and the seed comes from the machine
 18 //! configuration alone. A bug that one fault can trigger exercises little, so
 19 //! the planted bug needs two faults acting together across steps. A search that
 20 //! stops at the first failure, or whose result depends on the order it tries
 21 //! things in, can miss the bug or misreport it, so the search has to cover one
 22 //! fixed tree completely and keep going after each failure. A fix is believable
 23 //! only when it survives the same search that found the bug.
 24 //!
 25 //! The planted bug (the *seeded defect*) lives in how the coordinator counts.
 26 //! The defective variant counts every acknowledgement, a late one from a closed
 27 //! round and a repeat from the same node alike, so it can announce a commit
 28 //! that fewer than two nodes back. The bug needs two facts at once, a *stateful
 29 //! conjunction*: a node stays hung across two fault steps, so the coordinator
 30 //! suspects it and opens a new round, and an acknowledgement from the closed
 31 //! round arrives afterward. Every search walks the same six levels of choices,
 32 //! a *frozen choice tree*, in the order input, schedule, fault, fault,
 33 //! schedule, schedule, under a budget of 4096 executions. The seed is a SHA-256
 34 //! digest over the identities of the machine configuration, its shared
 35 //! execution rules, and its list of places where two runs could differ,
 36 //! together with the protocol's encoding version.
 37 //!
 38 //! The defective search covers the tree in 3017 executions with nothing pruned,
 39 //! and it settles nine failing branches, each of which carries both facts. Two
 40 //! single-fault variants run the same budget and fail nowhere: one delivers
 41 //! every acknowledgement the moment it is sent, and the other never lets a hang
 42 //! last. The repaired variant counts an acknowledgement only for the current
 43 //! round and only once per node, reaches both facts together in 17 branches,
 44 //! and violates neither rule.
 45 //!
 46 //! The first failure shrinks to five steps, and the gate confirms that none of
 47 //! them can be removed: a terminal input, a step for a node other than the
 48 //! coordinator, an injected crash, the crash held for another step, and a step
 49 //! for the coordinator. The shortened record replays twice to one history
 50 //! identity and survives a round trip through its byte encoding. A sibling path
 51 //! that takes another alternative at the last choice gives the first step where
 52 //! two recorded histories differ, as one stable *first divergence* at that
 53 //! choice, encoded as a reference, and it records the reason and which fields
 54 //! of the two reached positions differ. The report carries where the seed came
 55 //! from, the four search summaries, the shrinking statistics, the replay
 56 //! identities, and the signature of that first divergence.
 57 //!
 58 //! - *workload*: the three-node replicated-commit protocol the gate explores,
 59 //!   in a defective, a repaired, or a single-fault variant.
 60 //! - *witness gate*: the run that finds the defect, shrinks its capsule,
 61 //!   replays it twice, branches from it, and checks the single-fault and
 62 //!   repaired variants.
 63 //! - *capsule*: a fixed-capacity record of one failing run that replays it
 64 //!   exactly.
 65 //! - *seed provenance*: the record of where the gate's seed came from: the
 66 //!   profile fingerprint, the contract fingerprint, the inventory identity, the
 67 //!   encoding version, and the seed itself.
 68 
 69 const canon = @import("canon.zig");
 70 const driver = @import("driver.zig");
 71 const property = @import("property.zig");
 72 const queue = @import("queue.zig");
 73 const replay = @import("replay.zig");
 74 const seed = @import("seed.zig");
 75 const state = @import("state.zig");
 76 const types = @import("types.zig");
 77 const witness = @import("witness.zig");
 78 const workload = @import("workload.zig");
 79 
 80 pub const Capsule = replay.Capsule;
 81 pub const Config = types.Config;
 82 pub const Conjunct = types.Conjunct;
 83 pub const Cursors = driver.Cursors;
 84 pub const Delivery = types.Delivery;
 85 pub const Diagnostic = types.Diagnostic;
 86 pub const Diff = replay.Diff;
 87 pub const Driver = driver.Driver;
 88 pub const Error = types.Error;
 89 pub const Events = types.Events;
 90 pub const Exploration = types.Exploration;
 91 pub const History = replay.History;
 92 pub const Message = types.Message;
 93 pub const MessageKind = types.MessageKind;
 94 pub const Node = types.Node;
 95 pub const Persistence = types.Persistence;
 96 pub const Property = types.Property;
 97 pub const Provenance = types.Provenance;
 98 pub const Queue = queue.Queue;
 99 pub const Reducer = replay.Reducer;
100 pub const Reduction = types.Reduction;
101 pub const Replay = types.Replay;
102 pub const Replayer = replay.Replayer;
103 pub const Report = types.Report;
104 pub const Search = driver.Search;
105 pub const Semantic = types.Semantic;
106 pub const Signature = types.Signature;
107 pub const State = state.State;
108 pub const Variant = types.Variant;
109 pub const Witness = witness.Witness;
110 pub const budget = types.budget;
111 pub const capsule_capacity = types.capsule_capacity;
112 pub const coordinator = types.coordinator;
113 pub const declarations = property.declarations;
114 pub const defective = types.defective;
115 pub const delayed_only = types.delayed_only;
116 pub const depth = types.depth;
117 pub const freshness_rule = property.freshness_rule;
118 pub const history_capacity = types.history_capacity;
119 pub const kinds = types.kinds;
120 pub const node_count = types.node_count;
121 pub const persistent_only = types.persistent_only;
122 pub const quorum = types.quorum;
123 pub const quorum_rule = property.quorum_rule;
124 pub const repaired = types.repaired;
125 pub const search_capacity = types.search_capacity;
126 pub const suspicion_steps = types.suspicion_steps;
127 pub const tree = types.tree;
128 pub const builds = canon.builds;
129 pub const initialRoot = canon.initialRoot;
130 pub const origin = canon.origin;
131 pub const seedProvenance = seed.provenance;
132 pub const selectedProfile = seed.selected;
133 pub const step = workload.step;