Status: Superseded by ADR-296 — its D1-D7 are D9-D15 there
Related: ADR-007 (the grammar protocol), ADR-008
(container-level tethering, which is why a chunked parse costs no atomics),
ADR-005 D5 (sync and scoped parallelism),
ADR-010 (settles §5’s first item)
Splitting a buffer at line boundaries, one chunk per core, can be written by hand:
let chunks = data.split_aligned(cpu::count(), "\n")
let summaries = chunks.par_iter().map fn { dsl Measurements from a } .collect()Specifying split_aligned would close that gap and get the shape wrong. The
user is asked to restate, as an argument, something the grammar already
knows — that a measurement ends at "\n" — and then to hand-write the
pipeline that follows mechanically from it.
The fast reference implementations of this workload all rest on format assumptions exploited at the byte level: the separator can be found without parsing, fields are short, numbers are fixed width, keys are few. Those assumptions are legitimate. The question for a language is where they may be written down, and hand-written SWAR in user code is not an answer: unreadable, unportable, unverifiable.
The grammar is the right place, because it is already the file’s specification. This ADR decides which assumptions a grammar may state, what the compiler may then generate, and what it must verify first.
@frame declares a resynchronisation unit, and the compiler checks it.@frame(boundary: "\n")
rule MEASUREMENT -> Reading = name:NAME ";" => temp:TENTHS frame_end -> { … }@frame says: an occurrence of this rule can be found from an arbitrary offset
by scanning to the next boundary — no parse state from earlier in the file is
needed.
Not a promise the user makes; a property the compiler checks.
Resynchronisation is sound exactly when the boundary cannot occur inside a
frame. The frontend walks the terminals reachable from the frame rule and
rejects the marker otherwise. The canonical failure is CSV with quoted fields: a
newline inside "…" means the split lands mid-record. That grammar gets a
diagnostic naming the rule that can swallow the boundary, not a data-dependent
wrong answer at 3 a.m.
Two verdicts, and no third:
| construct | verdict |
|---|---|
a literal without the boundary; a built-in whose alphabet excludes it (digit1, ident); lookahead |
safe |
until(t) whose terminator covers the boundary — an alternative is frame_end, the boundary literal or a prefix of it, or line_ending for a newline |
safe |
a literal containing the boundary; a built-in that can consume it (any, multispace0); the implicit whitespace of a syntactic rule |
rejected, naming rule and pattern |
until(t) that does not cover the boundary |
rejected — the message says until(… \| frame_end) |
recover(…) |
rejected — the skip would have to stop at the boundary and the sync token consume it. Recover per frame instead: (item \| until(frame_end)) frame_end |
The compiler checks the grammar; it never rewrites it. The naive version of
the check rejects the grammar it exists for, because NAME = until(";")
consumes a newline too. The tempting repair is to generate an until reached
from a "\n" frame as “until ; or newline” without the grammar saying so.
That is refused: it makes the same rule text parse differently depending on what
reached it, changes a rule shared between a frame and something else for the
something else, and needs per-rule mutable state in the generator. It is the
parsing-side twin of “Nikaia never inserts a clone the user didn’t write” — a
pattern means what it says, wherever it is written.
frame_end is the built-in that resolves this honestly: it names the
boundary of the frame the rule is reached from, written once in the attribute
and referenced rather than copied. As an until alternative it covers the
boundary by construction. It resolves statically — writing it outside a frame is
an error, and so is being reached from two frames with different boundaries.
Writing the literal stays legal and means the same.
The attribute is keyed, and has an escape hatch. @frame, @frame(boundary:
"\n"), @frame(boundary: "\n", unchecked). unchecked skips the walk: the
author asserts the invariant, and the word is greppable — it is to a frame what
the reserved unsafe is to FFI. It is needed because a boundary is a byte
string, and formats exist whose cut points cannot be found by searching for one:
quoted fields (quote parity is a stateful pre-scan, not a search), records
recognisable by how they start, escaped boundaries, a scanner of the author’s
own. Each is a future key (quote, start, escape, scan) that changes
nothing about the existing ones; until one exists, such a grammar says so in the
grammar.
Two consequences stay normative. A frame rule and everything it reaches is
lexical (uppercase, or wrapped in lex(…)) unless the grammar defines a WS
that leaves the boundary alone — which for a data format with no whitespace
between fields is the honest spelling anyway. A frame must end in its
boundary, so that the piece that finds a frame’s end is the one that owns it
(D3).
Named @frame rather than sync rule: sync already means “pure CPU, cannot
pause” and names the resynchronisation token of recover(rule, sync). A third
meaning would be the worst kind of overload.
par_fold.pub rule file -> Summary =
par_fold(MEASUREMENT, Summary::new, fn(acc, m) { acc.record(m) }, Summary::merge)par_fold is fold plus a merge, and requires its item rule to be
@frame. Given both, the whole pipeline is generated — split, seam repair, one
accumulator per chunk, merge — and the user’s main is
let totals = dsl Measurements from data.
Parallelism stays opt-in, deliberately. The compiler could infer that a
fold with an associative step may run in parallel, and must not: a merge over
f64 is not associative, so the chunk count would silently change the output.
par_fold is the user saying “results from different chunk counts are the same
to me” — which a program earns by accumulating in integer tenths and converting
at print time.
Chunk count changes neither what is accepted nor what is rejected. A
par_fold rule’s entry point skips no whitespace on either side. The obvious
implementation skips it once per piece rather than once per input, which loses
a leading space in whichever piece happens to start there and tolerates
whitespace-only text between frames that a single-piece parse rejects. The
property is asserted over accept and reject, against awkward inputs at one to
eight pieces.
It degrades rather than failing. At user_parallelism = no, par_fold is a sequential
fold — same accumulator, same merge, same result, no threads — which is the
spawn pattern applied to parsing, and keeps a par_fold grammar compiling for
wasm32-*.
Normative, because the edge cases are where a chunked parser silently loses or double-counts rows:
cpu::count() by
default. No scan.recover, a chunk-local failure does not abort the others.This is the reference implementations’ trick — split blindly, repair the seam — with the correctness conditions written down rather than left to the reader.
A par_fold rule generates a cut, a merge and a driver that parses each piece
with the rule’s own parser and reports a failing piece at its offset in the
whole input. The driver takes Parallelism::Off | Pieces(n) | Auto, and Off
is defined to be identical to the plain parser. Nikaia chooses that value from
user_parallelism; the cut and merge are public so the pieces can run on Nikaia’s own
pool rather than the backend’s.
Finding a boundary or an until terminator lowers to a word-at-a-time scan:
a u64 load, an XOR against the broadcast byte, the standard
(x - 0x01..) & ~x & 0x80.. mask, a trailing-zero count. Portable SWAR — no
target feature, no runtime detection, works on wasm32 and therefore under
wasm32. Target-gated SIMD is a multiversioning layer on top, never the baseline,
so a program’s performance story does not fork by target.
until accepts an alternation, and up to three fixed alternatives are scanned
in one pass; more take the position-by-position path.
The guarantee is stated as complexity, not instruction selection: scanning for
a byte terminator never inspects one byte at a time. The same primitive
removes recover’s byte-by-byte skip — one scan primitive, two callers.
rule TENTHS -> i32 = neg:"-"? whole:digit{1,2} "." frac:digit -> { … }The branchless integer trick is sound only where the field’s width is bounded.
digit+ says unbounded, so a compiler emitting the fixed-width path would be
inventing a constraint the grammar never stated. p{n,m} is the only sanctioned
route: the format assumption is written by the person who knows it, checked by
the parser, exploited by codegen.
Ordinary branch elimination needs none of this and is already the backend’s job.
A view key may be hashed from its first 8 bytes mixed with its length — sound as a hash. What several reference implementations additionally do, comparing only the first 8 or 16 bytes on a probe hit, is not sound: two keys sharing a 16-byte prefix merge silently.
ADR-008 D4 already fixed equality on views as content-based. This is stated separately because the tempting optimisation is the one that produces a plausible wrong answer rather than a crash.
A read-only mapping with no Cleanup and nothing observable attached to it
may be left to the kernel at process exit. At thirteen gigabytes, unmapping
page by page is measurable and changes nothing a program can see.
This is the one place ADR-006’s “cleanup always runs” is relaxed, and it is relaxed by proof of non-observability, not by a flag.
sync rule as the frame marker — keyword collision (D1).split_aligned(n, "\n") as the sanctioned form — it asks the user to
repeat what the grammar states and to write the pipeline that follows. A raw
chunking primitive on Bytes may still be specified for non-grammar uses.fold — float merges
would make output depend on core count (D2).@frame could often also find one, but then a grammar that happens
to be splittable today would silently stop being parallel after an unrelated
edit. An explicit marker fails loudly.dsl backend::… (ADR-007 D6); D4’s guarantee is what a parser
author gets instead.The user writes down the format: a record ends at a newline, summaries combine, a name runs to the semicolon, a temperature has one decimal. Everything the reference implementations hand-code, the compiler now has grounds to generate — blind split and seam repair (D3), word-at-a-time scanning (D4), per-worker accumulators with no shared state (D2), and zero allocation and zero refcount traffic per row (ADR-008).
cpu::count(): NUMA, heterogeneous cores, an
oversubscribed container’s CPU quota.par_fold over a stream rather than a mapped buffer. Splitting needs
random access, so the parallel form is buffer-only; this is about a pipe.