Skip to content

Generations and mutation

Random generation rarely produces a module whose state changes in interesting ways. A run therefore proceeds in generations. After each generation, a quality gate keeps the agreeing entries that show a behaviour or cover code that the kept entries lack. The next generation is partly mutated from those entries and partly generated by PBT.

1. How a run proceeds

  1. Admit. The input stage admits up to generation_size entries. A feedback_ratio share of them are mutants of entries in 04quality-pass, and the rest are generated by PBT. Before any entry has passed the gate, PBT generates the whole generation.
  2. Look ahead. Once the generation is admitted, the PBT share of the next generation is admitted too, while this generation's checkers are still running. Its mutant share cannot follow yet — it depends on a selection that has not happened — so only one generation is ever open ahead of the one being gated. Work and CPU from the older generation are served first.
  3. Settle. The parser, TLC, Apalache and the aggregator process every entry of the generation. An entry the parser rejects, and one a checker crashes on, settles where it is.
  4. Select. The quality gate moves each entry of the generation from 03aggregator-pass to 04quality-pass or 04quality-fail.
  5. Repeat for the next generation, until every generation that fits in workflow.max_entries has run.

The run length is counted in generations, not in stored entries: a run ends after ceil(workflow.max_entries / generation_size) generations. A generation that ends up short — because the run was interrupted, or because the corpus was written with a different generation_size — leaves the corpus below workflow.max_entries, and the run still reports that it completed.

Every entry records the generation that admitted it in gen.generation. A mutant also records gen.parent, the hash of the entry it was mutated from, and gen.operators, the edits applied:

$ fuzztla print --corpus corpus --envelope corpus/04quality-pass/<hash>.cbor
kind: module
gen:
  generation: 3
  cohort: 4
  richness: 2.0
  parent: <hash of the parent>
  operators: random_byte
…

An interrupted or stopped run resumes at the oldest generation that still lacks entries, still has work in flight, or has not been gated — at most one before the highest generation the corpus records, since only one generation is ever admitted ahead. It admits what that generation is missing, keeping the configured share of mutants, drains the pending work, and reruns the gate, which completes an interrupted selection exactly. The startup scan reconstructs this from the corpus itself; no inventory is taken between generations afterwards.

Each generation numbers its targets from 0, mutants first and PBT after, and a target's ordinal seeds the stream it draws from. A resumed generation reserves the ordinals its stored entries already used, so the entries it adds draw fresh streams. A corpus does not store target ordinals, so after an interruption the reservation is reconstructed from the counts, not from the original assignment: the entries already admitted are unaffected, but the exact streams of an interrupted run's remaining targets cannot always be replayed.

workflow.max_entries may be raised between runs to continue a corpus.

A run requires gen.generation on every entry, so a corpus written before generations existed cannot continue. fuzztla print and fuzztla export-db still read it once 04quality-pass and 04quality-fail exist.

2. Configuration

fuzztla init writes the [mutator] table with these defaults:

[mutator]
generation_size = 1000
select_fraction = 0.05
feedback_ratio = 0.5
max_edits = 1
weights = { random_byte = 8, bitflip = 8, parity_flip = 8, copy = 4, duplicate = 1, insert = 1, erase = 1, splice = 1 }
shallow_patterns = ["vacuous_pass", "initial_state_violation", "early_failure", "no_discovering_action", "counter_only_progress"]
cell_capacity = 4
feature_coverage = true
Key Meaning
generation_size Entries each generation admits, and the unit the run length is counted in. With generation_size ≥ workflow.max_entries, a run is one generation.
select_fraction Upper bound on the share of a generation's agreeing entries kept in 04quality-pass, rounded up. Must be in (0, 1].
feedback_ratio Share of a generation that is mutated. 0 disables mutation; the gate still runs.
max_edits Cap on stacked edits per mutant. A mutant gets 1 edit, plus one more with probability ½ each, up to the cap.
weights Relative weight of each operator. An omitted operator has weight 0.
shallow_patterns Patterns of the exploration-metrics manual that exclude an entry from 04quality-pass.
cell_capacity Entries of 04quality-pass per behaviour cell (section 3). 0 removes the bound.
feature_coverage Also keep an entry that adds an operator-edge coverage feature (section 3).

With cell_capacity = 0 and feature_coverage = false, the gate keeps the best select_fraction of every generation.

The defaults come from one experiment on one corpus. Calibrate select_fraction and feedback_ratio against your corpus with the queries in section 4.

3. What the gate keeps

An entry of 03aggregator-pass is admissible when all of these hold:

  • its TLC verdict is pass or counterexample;
  • TLC recorded exploration metrics;
  • it matches none of shallow_patterns.

The gate ranks admissible entries by TLC's exploration metrics, compared in this order, higher first:

  1. projectedDepth;
  2. projectedStates, by power of two;
  3. actionsDiscovering;
  4. maxStateNodes, by power of two;
  5. maxCardinality, by power of two;
  6. maxNesting.

Ties go to the shorter input. A gbt corpus ranks by action coverage instead (ADR 0024): dataActions by power of two, projectedStates by power of two, projectedDepth, then the last three as above. Its metrics project out pc as well as step, so they measure the data a graph entry computes rather than the length of its walks.

The gate walks the admissible entries in this order and keeps an entry while it has kept fewer than ceil(select_fraction × agreeing entries of the generation) and either of these holds:

  • Behaviour. The entry's cell holds fewer than cell_capacity kept entries. The cell is the TLC verdict together with the six metrics of the corpus's ranking, each compared as in the ranking (states, nodes and cardinality by power of two, and, under action coverage, dataActions too).
  • Coverage. feature_coverage is enabled and the entry has a feature that no kept entry has.

"Kept" counts 04quality-pass over every earlier generation plus the entries this generation has kept so far. Every other entry of the generation, admissible or not, moves to 04quality-fail. The mutator's parent pool is all of 04quality-pass, over every generation.

The features of an entry come from the code the checkers evaluate, the same code that the expr table of the corpus database counts. Constructs are operator applications, LET-IN, and literal kinds. The features are:

  • a construct and how often it occurs;
  • an edge, meaning a construct and a construct that is its immediate argument (SET_IN → FUN_APP, for example), and how often it occurs.

Counts are bucketed as in AFL: 1, 2, 3, 4–7, 8–15, 16–31, 32–127, 128 or more. The gate computes features by replaying the input through the generator, as fuzztla export-db does. An input that fails to replay has no features.

An expr corpus is always shallow: its module has no transitions. To exercise mutation on one, set shallow_patterns = [].

4. Mutation operators

Operator Edit
random_byte Replaces one byte with a random byte.
bitflip Flips one bit.
parity_flip Flips the low bit of one byte. On a continuation marker it adds or removes an element of a structural list; on the size byte of a set or sequence literal it changes the size by one (collection sizes).
copy Copies up to 32 bytes over another offset.
duplicate Repeats a block of up to 32 bytes in place.
insert Inserts up to 8 random bytes.
erase Deletes up to 16 bytes.
splice Joins a prefix of the parent with a suffix of another parent.

A mutant is truncated to pbt.max_input_bytes. It passes the same admission as a PBT candidate: the worker request-frame limit, duplicate detection and the known-defect signatures. The richness cohorts do not apply. A mutant whose TLA+ module is identical to its parent's is a clone and is discarded; the run table counts these as mutant clones. If a target entry cannot be filled within 10,000 candidates, the run stops with a diagnostic that names the parent pool size and the rejection counts.

After fuzztla export-db (corpus-database manual), the yield of each generation and operator is a query:

SELECT e.generation, count(*) AS entries, sum(e.parent IS NOT NULL) AS mutants,
       sum(e.directory = '04quality-pass') AS selected
FROM entry e
WHERE e.directory NOT LIKE '02apa-%' AND e.directory <> '00-known-defects'
GROUP BY e.generation ORDER BY e.generation;

SELECT e.generation, count(DISTINCT x.parentName || ' ' || x.childName) AS edges
FROM entry e JOIN exprEdge x ON x.entryId = e.id
WHERE e.directory = '04quality-pass'
GROUP BY e.generation ORDER BY e.generation;

SELECT m.operator, count(DISTINCT e.id) AS mutants,
       count(DISTINCT CASE WHEN e.directory = '04quality-pass' THEN e.id END) AS selected
FROM mutationOperator m JOIN entry e ON e.id = m.entryId
GROUP BY m.operator ORDER BY selected DESC;

5. Determinism

A run replays given the same seed, configuration and starting corpus, for any --max-cpus: every target entry draws from a stream seeded by the run seed, its generation and its position in the generation. The one exception is two targets that draw identical bytes, where scheduling decides which one stores them. A resumed generation is not a replay of the uninterrupted one.

Background

ADR 0010 records the design and the experiment behind it. ADR 0013 revises the quality gate: behaviour cells and operator-edge coverage.