Draft chapter in thesis register. Numbers measured on a single VM (Xeon 2.80 GHz, 1 core, 4 GB, GCC -O2); every claim is labelled proved, measured, or conjectured. Citation keys marked [verify] should be checked against the published record before submission.
A transcoder is an unusually favourable object of study. Its specification is fixed by an external standard [Uni; RFC3629], its inputs are unstructured byte strings, and its performance is measured in bytes per second on hardware whose limits can be probed directly. It is therefore possible — and this chapter argues, worthwhile — to ask not merely how fast is this implementation? but what is the largest speed any implementation of this specification could attain on this machine, and which resource forbids the rest?
The question is not rhetorical. Modern transcoders are written against vector instruction sets whose value proposition is precisely that they eliminate a resource bottleneck: data-dependent branching. Establishing that the bottleneck exists, that it is the binding one, and that no cheaper remedy suffices, is a prerequisite for justifying the engineering effort that SIMD kernels represent. In the absence of such an argument, vectorisation is folklore.
This chapter develops a small framework of resource certificates for transcoding kernels and applies it to the scalar reference implementations in the present work. A certificate here is a claim about resource use — buffer capacity, memory footprint, cache transfers, access-pattern class — together with a checking procedure that is (i) independent of the implementation it judges, (ii) quantifier-free, and (iii) cheap enough to run in continuous integration. The style is borrowed from proof-carrying code [NL97], where an expensive proof obligation discharged by the producer is replaced, at the consumer, by a linear-time check.
Four results are reported.
- The reference transcoder's declared output-buffer bound is exhaustively verified and shown tight (§N.4.1).
- The reference transcoder is I/O-optimal in the cache-line (external-memory) model, with matching upper and lower bounds (§N.5).
- The reference transcoder fails a data-obliviousness certificate, and the failure predicts an input class on which throughput degrades by a measured factor of 6.4 (§N.4.3).
- That degradation is not recoverable by scalar means: two interventions — a hand-vectorised ASCII path and a superoptimised branchless width classifier — are reported, one rejected on correctness grounds and one verified but throughput-negative on ASCII inputs (§N.6).
Taken together the four results form an argument of a shape that is rare in performance engineering: the memory-side behaviour of the scalar reference is provably optimal and provably irrelevant, and the residual gap to the machine's roofline [WWP09] is localised to the branch unit — which is exactly the resource the vector kernels of this thesis are built to eliminate. The certificates thus supply the missing justification for the architecture, and, as a by-product, an adversarial input class on which its advantage should be demonstrated.
Transcoding and validation with SIMD. The performance case for vectorised Unicode processing is developed by Keiser and Lemire for UTF-8 validation [KL21] and transcoding [KL22][verify], building on the branch-elimination methodology of simdjson [LL19]. The present work's kernels stand in that lineage; this chapter supplies resource-bound certificates for the scalar references against which those kernels are measured.
External-memory and cache-oblivious analysis. The DAM model of
Aggarwal and Vitter [AV88] counts block transfers between a memory
of size
Proof-carrying artefacts. Necula and Lee [NL97] introduced the
asymmetry exploited here — costly proof at the producer, linear
check at the consumer. Amortised resource analysis in the sense of
Hofmann and Jost [HJ03] places potential functions in types; the
buffer certificates of §N.4.1 are the same idea specialised to
output-length bounds, and are already present, informally, in this
codebase as the *_buflen_* and *_safe_length_* functions.
Superoptimisation. Exhaustive search for minimal instruction sequences originates with Massalin [Mas87]; goal-directed and peephole variants are due to Joshi et al. [JNR02] and Bansal and Aiken [BA06]. §N.6.2 applies the technique in its original form — enumerate a structured family, verify against the specification on the entire input domain — to the lead-byte width classifier.
Roofline analysis. The ceiling-versus-attained framing of §N.4.2 follows Williams et al. [WWP09].
Let a kernel be a function
C1 (Buffer). A function
C2 (Memory rung). Kernels are graded by the shape of their working state: rung 0 (a constant number of scalars), rung 1 (one carried item), rung 2p (a buffer bounded by an invocation parameter), rung 2 (a bounded ledger), rung 3 (unbounded, declared). Rung 0 and 1 are established by inspection of the state type; higher rungs require a prefix-sum ledger over allocation events with three obligations: never negative, never above capacity, zero at exit.
C3 (Access class). In the DAM model, a kernel is scan-class if
its access trace decomposes into finitely many index-monotone
streams. A scan-class kernel with
C4 (Obliviousness). A kernel is data-oblivious (STATIC) if its
control-flow and address traces are functions of
The certificates are ordered by what they exclude. C1–C3 constrain the memory system; C4 constrains the control path. A kernel may satisfy C1–C3 optimally and still be slow, and §N.4 shows that the scalar reference is exactly such a kernel.
The reference transcoder ships its own buffer certificate in the
form of utf8_to_utf16le_buflen_ref. Checking it against
utf8_to_utf16le_ref over the complete domain of two-byte inputs:
| inputs tested | declared bound | observed maximum | inputs attaining it |
|---|---|---|---|
| 65 536 (all) | 2 code units | 2 | 16 384 |
The bound holds on every input and is attained by a quarter of them:
it is correct and cannot be improved at
Memory (C2). Neither the reference transcoder nor the
safe_length routines allocate: all state is scalar locals over
caller-owned buffers. Rung 0, by inspection.
Ceilings were probed on the same machine in the same session.
| quantity | measured |
|---|---|
memcpy bandwidth (4 MiB) |
13 987 MB/s |
| reference, ASCII, |
1 802.6 MB/s |
| reference, ASCII, |
1 830.9 MB/s |
| reference, ASCII, |
1 537.2 MB/s |
The reference attains ≈13 % of the memory roofline. It is therefore compute-bound, not bandwidth-bound, and the mild decline at 1 MiB is attributable to the output buffer (twice the input in bytes) leaving the last-level cache rather than to any defect of the code. Throughput is flat from 4 KiB to 64 KiB, so the scalar epilogue contributes no measurable per-call overhead at these sizes.
The reference's control flow branches on the width class of each lead byte; it is therefore not data-oblivious, and C4 fails. The certificate's failure is predictive: it identifies as adversarial any input whose width sequence is unpredictable. Constructing such an input (a random interleaving of one- and two-byte characters, so that memory traffic is essentially unchanged):
| input, 1 MiB | throughput |
|---|---|
| ASCII (perfectly predictable) | 1 819.5 MB/s |
| regular two-byte/ASCII pattern (predictable) | 1 575.2 MB/s |
| random width mix (unpredictable) | 285.1 MB/s |
The regular mixed pattern is the control: it contains the same proportion of multibyte characters as the random mix and costs almost nothing, which isolates predictability — not multibyte handling — as the cause of the 6.4× degradation.
At line granularity the transcoder is a fold over
Lower bound. Every input byte is load-bearing. Empirically, for
a 63-byte mixed string, each of the
Upper bound. The reference is scan-class (C3) with two monotone
streams and no resident working set beyond the carry, so it incurs
compulsory transfers only, for every
Composition is free. The carry is at most three bytes and hence register-resident, so combining the results of adjacent chunks costs no transfers. The same fact is the content of the kernel's chunk-partition invariance: the fold commutes with any chunking of the input precisely because the carry is total.
Upper and lower bounds coincide: the reference is I/O-optimal at cache-line granularity, and cache-obliviously so.
The practical content of this result is negative and, for that reason, useful. No layout transformation, blocking scheme, or prefetch schedule can improve this function's memory behaviour, because its memory behaviour is already optimal for every cache geometry. Combined with §N.4.2 — 13 % of roofline — the conclusion is that the entire residual gap lies in the arithmetic and control path.
The obvious intervention combines a word-at-a-time ASCII fast path with a flattened width dispatch:
/* eight bytes per iteration while the high bits are clear */
while (i + 8 <= len) {
uint64_t w; memcpy(&w, in + i, 8);
if (w & 0x8080808080808080ull) break;
for (int k = 0; k < 8; k++) out[o + k] = in[i + k];
i += 8; o += 8;
}Exhaustive differential testing against the reference on all 65 536
two-byte inputs produced 6 272 mismatches. The simplified
dispatch does not reproduce the reference's treatment of truncated
sequences and overlong encodings. The variant was rejected before
performance was considered; for the record it was also slower
(1 666.9 vs 1 819.5 MB/s on ASCII), because GCC already
auto-vectorises the reference's inner loop at -O2 and the manual
word loop with byte stores defeats that vectorisation.
The episode motivates a discipline adopted throughout: an optimisation is admitted only after exhaustive equivalence checking on a bounded domain, and correctness failures are reported irrespective of the measured speed.
The branch tree indicted in §N.4.3 computes the width class of a lead byte. Exhaustive search over shift-mask-lookup forms yields a four-operation branchless equivalent:
/* width ∈ {0,1,2,3,4}; 0 denotes continuation or invalid.
W is a 96-bit constant: two uint64_t, or a 32-byte table. */
unsigned idx = c0 >> 3; /* shr */
unsigned width = (W >> (idx * 3)) & 7; /* lea; shr; and */with W = 0x11b492000000249249249249. Two properties were
established by exhaustive check over all 256 byte values: the
classifier agrees with the reference's width semantics everywhere,
and the coarser nibble index c0 >> 4 is provably inadmissible,
because 0xF0–0xF7 and 0xF8–0xFF fall in a single slot with
different widths. The search therefore also establishes the minimal
index granularity.
Integrated behind a fallback to the reference for width-0 and width-4 lead bytes and for tails, the classifier passes the exhaustive two-byte differential test (0 of 65 536 mismatches). Measured:
| input, 1 MiB | reference | branchless |
|---|---|---|
| ASCII | 1 485.8 MB/s | 265.3 MB/s |
| random width mix | 296.0 MB/s | 306.5 MB/s |
The result is a genuine split. On the adversarial class the branchless classifier is faster, which is causal evidence for the diagnosis of §N.4.3: removing the branches improves precisely the input class the certificate predicted. On ASCII it is far slower, because computing all candidate code points unconditionally defeats the compiler's vectorised copy. The engineering conclusion is that branchless dispatch belongs only inside the multibyte region, behind a vectorised ASCII skip-ahead — and, more importantly, that the scalar path cannot recover the factor of 6.4 by itself.
The four certificates decompose the performance question into parts with different epistemic status. Buffer and memory bounds are proved on bounded domains and cheap to re-check in CI. I/O optimality is proved for all cache geometries, and its consequence — that memory-side optimisation is exhausted — is permanent. Obliviousness fails, and the failure is not a defect of the implementation but a property of scalar UTF-8 decoding: any implementation that branches on width will exhibit the same cliff. The measured 6.4× is thus a lower bound on what a data-oblivious kernel stands to gain on adversarial input, and the ≈7× roofline gap is an upper bound on what any implementation can gain in total.
This is the argument the vector kernels require. Their advantage is not merely that they process sixteen or sixty-four bytes per instruction; it is that they do so obliviously, and the certificate framework makes that the load-bearing claim, testable independently of instruction counts.
Measurements are single-machine, single-thread, one compiler at one optimisation level; absolute figures will not transfer, though the ratios between input classes on one machine are the quantities relied upon. Exhaustive verification is complete only on the two-byte domain; three- and four-byte domains are mechanical but were not run. The 6.4× figure depends on a specific adversarial distribution; real corpora will fall between the ASCII and random extremes, and a corpus study is future work. Finally, the AVX-512 kernels were not benchmarked here: the evaluation machine lacks the instruction set, and the comparison must be repeated on hardware that supports it or under an emulator.
Extend the exhaustive differential domain to three and four bytes; certify chunk-partition invariance mechanically rather than by argument; run the obliviousness and roofline certificates against the AVX-512 and NEON kernels on appropriate hardware, where the prediction is a flat throughput profile across all three input classes; and measure buffer-bound slack on natural-language corpora, where the worst-case-tight bound over-allocates for ASCII-dominant text.
- [AV88] A. Aggarwal and J. S. Vitter. The input/output complexity of sorting and related problems. Communications of the ACM, 31(9):1116–1127, 1988.
- [BA06] S. Bansal and A. Aiken. Automatic generation of peephole superoptimizers. ASPLOS, 2006.
- [FLPR99] M. Frigo, C. E. Leiserson, H. Prokop, S. Ramachandran. Cache-oblivious algorithms. FOCS, 1999.
- [HJ03] M. Hofmann and S. Jost. Static prediction of heap space usage for first-order functional programs. POPL, 2003.
- [JNR02] R. Joshi, G. Nelson, K. Randall. Denali: a goal-directed superoptimizer. PLDI, 2002.
- [KL21] J. Keiser and D. Lemire. Validating UTF-8 in less than one instruction per byte. Software: Practice and Experience, 51(5):950–964, 2021.
- [KL22] Transcoding billions of Unicode characters per second with SIMD instructions. Software: Practice and Experience, 2022. [verify author list and volume]
- [LL19] G. Langdale and D. Lemire. Parsing gigabytes of JSON per second. The VLDB Journal, 28:941–960, 2019.
- [Mas87] H. Massalin. Superoptimizer: a look at the smallest program. ASPLOS, 1987.
- [NL97] G. C. Necula and P. Lee. Proof-carrying code. POPL, 1997. [verify venue: POPL 1997 for the paper, OSDI 1996 for the safe-kernel-extensions application]
- [RFC3629] F. Yergeau. UTF-8, a transformation format of ISO 10646. RFC 3629, 2003.
- [Uni] The Unicode Consortium. The Unicode Standard. [cite the edition used]
- [WWP09] S. Williams, A. Waterman, D. Patterson. Roofline: an insightful visual performance model for multicore architectures. Communications of the ACM, 52(4):65–76, 2009.