lib/machine/src/explore/root.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

  1 //! Some bugs show up only under one particular order of inputs, scheduling, and
  2 //! faults, so finding one means running a deterministic machine many times with
  3 //! different choices, checking each run against rules written beforehand, and
  4 //! keeping every bound fixed in advance. At each step the namespace offers the
  5 //! possible next inputs, scheduling choices, sets of participating nodes, and
  6 //! faults, and the same seed always offers the same possibilities. It checks
  7 //! the events of a run against two kinds of rule: an event that must never
  8 //! happen, and a triggering event that must be answered within a bound. It
  9 //! searches the possibilities, keeps every settled run together with the path
 10 //! that reached it, and resumes after an interruption. It keeps a failing run
 11 //! in a form that replays exactly and shrinks to the steps the failure needs.
 12 //! It records what happened in a run, step by step, so a caller can ask which
 13 //! step caused what and where two runs first differ. It demonstrates all of
 14 //! this on a three-node protocol with a bug planted in it: the bug is found,
 15 //! shrunk, replayed, and the fixed protocol is checked under the same search.
 16 //!
 17 //! A failing run can be repeated only when every place where two runs could
 18 //! differ is under explicit control, so each offered possibility has to say
 19 //! which of those places it stands for, and under which version. Fixed bounds
 20 //! mean a generator, an event list, or a search can run out of room, and
 21 //! running out has to read differently from finishing. A rule checked against a
 22 //! run that was cut short cannot report that the rule holds, and a rule whose
 23 //! trigger never happened says nothing about its response. A rule written after
 24 //! seeing the failure proves nothing, so each rule has to be declared in the
 25 //! event list ahead of the events it judges. Time in these runs is a simulated
 26 //! clock that moves forward only, and a response bound may count either steps
 27 //! or ticks of that clock.
 28 //!
 29 //! The namespace keeps what can happen next apart from which run to try next:
 30 //! four bounded, stateful generators, one each for inputs, scheduling,
 31 //! participating nodes, and faults, offer the alternatives for one kind of
 32 //! choice, one step at a time (each a *tactic*), and a separate search decides
 33 //! which of them to run. At each step a generator offers a numbered list of
 34 //! alternatives, marks the one the seed suggests, and moves on only when the
 35 //! caller picks one of the alternatives it offered. Each alternative names the
 36 //! place it draws on, a place where two runs of the same program could differ
 37 //! (a *divergence source*), with the version that the machine's declared list
 38 //! of those places gives it. A generator that has used up its steps or its
 39 //! clock window reports itself exhausted, and one whose capacity cannot hold
 40 //! its plan reports itself incomplete with the reason.
 41 //!
 42 //! Runs are checked over a fixed-capacity list of numbered, timestamped events
 43 //! (each a *semantic event*): the choices taken, observations, rule
 44 //! declarations and verdicts, injected faults, diagnostics, outside admissions,
 45 //! and operation outcomes. The rules come in two kinds, each a rule over a
 46 //! run's events (a *temporal invariant*): a safety rule forbids an event
 47 //! pattern after its declaration, and a bounded liveness rule requires every
 48 //! trigger to be answered by a response within a bound of steps or clock ticks.
 49 //! A check returns one of four verdicts: holds, violated, unreached, or
 50 //! incomplete, each with a reason and, where one exists, the number of the
 51 //! event that decided it. An event list appended past its capacity turns
 52 //! incomplete, and a check over it reports incomplete where the full list might
 53 //! have held.
 54 //!
 55 //! The search keeps every settled run as the exact position the run reached,
 56 //! and it never merges two runs whose digests agree. A failing run becomes a
 57 //! self-contained record of fixed capacity that replays exactly and shrinks one
 58 //! step at a time, a *capsule*. A run's record becomes a sealed history with
 59 //! its own identity, built append-only step by step (a *causal history*), and
 60 //! bounded queries and comparisons read it through references into it. The
 61 //! `distributed` namespace carries a three-node commit protocol with a planted
 62 //! bug through the whole path, and the `query` namespace holds the histories,
 63 //! queries, and comparisons.
 64 //!
 65 //! - *choice site*: one step at which a generator offers a numbered list of
 66 //!   alternatives, identified by its kind of choice, its step number, and its
 67 //!   clock tick, with one alternative marked as the seed's suggestion.
 68 //! - *moment*: a position in one world's history, pairing the world root the
 69 //!   world grew from with the ledger root it has reached since.
 70 //! - *trace* (the code's `EventSequence`): the fixed-capacity event list
 71 //!   itself, open until finished as exhausted or incomplete.
 72 
 73 const capsule_owner = @import("capsule/root.zig");
 74 const fault_owner = @import("fault.zig");
 75 const input_owner = @import("input.zig");
 76 const model = @import("model.zig");
 77 const schedule_owner = @import("schedule.zig");
 78 const search_owner = @import("search/root.zig");
 79 const temporal_owner = @import("temporal.zig");
 80 const topology_owner = @import("topology.zig");
 81 
 82 pub const distributed = @import("distributed/root.zig");
 83 pub const query = @import("query/root.zig");
 84 
 85 pub const Bound = model.Bound;
 86 pub const BoundedLiveness = model.BoundedLiveness;
 87 pub const Capsule = capsule_owner.Capsule;
 88 pub const CapsuleBuildIdentity = capsule_owner.BuildIdentity;
 89 pub const CapsuleCapacity = capsule_owner.Capacity;
 90 pub const CapsuleError = capsule_owner.Error;
 91 pub const CapsuleExternalResult = capsule_owner.ExternalResult;
 92 pub const CapsuleFrame = capsule_owner.Frame;
 93 pub const CapsuleIdentity = capsule_owner.Identity;
 94 pub const CapsulePreparation = capsule_owner.Preparation;
 95 pub const CapsuleReducer = capsule_owner.Reducer;
 96 pub const CapsuleRejection = capsule_owner.Rejection;
 97 pub const CapsuleRejectionReason = capsule_owner.RejectionReason;
 98 pub const CapsuleReplay = capsule_owner.Replay;
 99 pub const CapsuleRunner = capsule_owner.Runner;
100 pub const CapsuleStatistics = capsule_owner.Statistics;
101 pub const ChoiceSite = model.ChoiceSite;
102 pub const Diagnostic = model.Diagnostic;
103 pub const EvaluationPattern = model.EvaluationPattern;
104 pub const EvaluationReason = model.EvaluationReason;
105 pub const Event = model.Event;
106 pub const EventCapacity = model.EventCapacity;
107 pub const EventClass = model.EventClass;
108 pub const EventSequence = temporal_owner.Sequence;
109 pub const EventValue = model.EventValue;
110 pub const ExternalAdmission = model.ExternalAdmission;
111 pub const FaultAction = model.FaultAction;
112 pub const FaultAlternative = model.FaultAlternative;
113 pub const FaultCapacity = model.FaultCapacity;
114 pub const FaultGenerator = fault_owner.Generator;
115 pub const FaultPlan = model.FaultPlan;
116 pub const GeneratedFault = model.GeneratedFault;
117 pub const GeneratedInput = model.GeneratedInput;
118 pub const GeneratedSchedule = model.GeneratedSchedule;
119 pub const GeneratedTopology = model.GeneratedTopology;
120 pub const Generation = model.Generation;
121 pub const GeneratorError = model.GeneratorError;
122 pub const IncompleteReason = model.IncompleteReason;
123 pub const InputAlternative = model.InputAlternative;
124 pub const InputCapacity = model.InputCapacity;
125 pub const InputGenerator = input_owner.Generator;
126 pub const InputKind = model.InputKind;
127 pub const InputPhase = model.InputPhase;
128 pub const InputValue = model.InputValue;
129 pub const Observation = model.Observation;
130 pub const Operation = model.Operation;
131 pub const OperationOutcome = model.OperationOutcome;
132 pub const OperationPattern = model.OperationPattern;
133 pub const Origin = model.Origin;
134 pub const Pattern = model.Pattern;
135 pub const PropertyDeclaration = model.PropertyDeclaration;
136 pub const PropertyEvaluation = model.PropertyEvaluation;
137 pub const PropertyKind = model.PropertyKind;
138 pub const Safety = model.Safety;
139 pub const ScheduleAlternative = model.ScheduleAlternative;
140 pub const ScheduleCapacity = model.ScheduleCapacity;
141 pub const ScheduleGenerator = schedule_owner.Generator;
142 pub const ScheduleKind = model.ScheduleKind;
143 pub const SchedulePlan = model.SchedulePlan;
144 pub const ScheduleValue = model.ScheduleValue;
145 pub const Search = search_owner.Search;
146 pub const SearchBranch = search_owner.Branch;
147 pub const SearchBranchId = search_owner.BranchId;
148 pub const SearchBudget = search_owner.Budget;
149 pub const SearchCandidate = search_owner.Candidate;
150 pub const SearchCapacity = search_owner.Capacity;
151 pub const SearchChoice = search_owner.Choice;
152 pub const SearchDecision = search_owner.Decision;
153 pub const SearchError = search_owner.Error;
154 pub const SearchExhaustedReason = search_owner.ExhaustedReason;
155 pub const SearchExecution = search_owner.Execution;
156 pub const SearchExecutionIncomplete = search_owner.ExecutionIncomplete;
157 pub const SearchExpansion = search_owner.Expansion;
158 pub const SearchIncompleteReason = search_owner.IncompleteReason;
159 pub const SearchOutcome = search_owner.Outcome;
160 pub const SearchProgress = search_owner.Progress;
161 pub const SearchPrunedReason = search_owner.PrunedReason;
162 pub const SearchRunner = search_owner.Runner;
163 pub const SearchSettlement = search_owner.Settlement;
164 pub const Seed = model.Seed;
165 pub const SeedDialect = model.SeedDialect;
166 pub const SemanticId = model.SemanticId;
167 pub const SiteId = model.SiteId;
168 pub const Stream = model.Stream;
169 pub const TemporalPlan = model.TemporalPlan;
170 pub const TopologyAlternative = model.TopologyAlternative;
171 pub const TopologyCapacity = model.TopologyCapacity;
172 pub const TopologyGenerator = topology_owner.Generator;
173 pub const TopologyKind = model.TopologyKind;
174 pub const TopologyNode = model.TopologyNode;
175 pub const TopologyPlan = model.TopologyPlan;
176 pub const TopologyValue = model.TopologyValue;
177 pub const TraceCompletion = model.TraceCompletion;
178 pub const TraceState = model.TraceState;
179 pub const Verdict = model.Verdict;
180 pub const evaluateLiveness = temporal_owner.evaluateLiveness;
181 pub const evaluateSafety = temporal_owner.evaluateSafety;
182 pub const matchesEvent = temporal_owner.matches;
183 pub const faultOrigin = model.faultOrigin;
184 pub const origin = model.origin;