Files
zeekay 6cd94a29f7 Initial: 8 formal proofs accompanying papers/
Each proof is a standalone LaTeX document with theorems, lemmas, and
explicit advantage bounds / reductions. All compile under TeX Live 2025.
2026-05-06 12:50:48 -07:00

327 lines
12 KiB
TeX

\documentclass[11pt]{article}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amsthm,amssymb}
\usepackage{mathtools}
\usepackage{microtype}
\usepackage{hyperref}
\usepackage[capitalize,noabbrev]{cleveref}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem*{remark}{Remark}
\title{Proofs for the ZAP Zero-Copy Throughput Paper}
\author{ZAP Protocol Authors\\\texttt{zap-proto.io}}
\date{2026}
\begin{document}
\maketitle
\begin{abstract}
This document gives full proofs of the two theorems stated in the
companion paper, plus the supporting lemmas. We work in a
unit-cost RAM model augmented with a two-level I/O budget that
distinguishes cache-resident from main-memory accesses. We assume
schemas are known to both endpoints at compile time, that pointers
are 8-byte aligned, and that the network presents bytes already
deposited into a contiguous arena (the standard \texttt{recvmmsg}
plus \texttt{mmap}-friendly pattern).
\end{abstract}
\section{Model}
\label{sec:model}
\begin{definition}[Unit-cost RAM with cache budget]
We use a RAM machine with word size $w=64$. Each instruction
(arithmetic, branch, register-to-register move) costs $1$ unit.
Memory accesses cost $c_h$ for L1-resident data and $c_m$ for main
memory, with $c_m \gg c_h$. Cache lines are $64$ bytes. Any byte
range of length $\ell$ touched once costs at most
$\lceil \ell/64 \rceil$ cold lines plus $O(\ell/w)$ instructions.
\end{definition}
\begin{definition}[Arena allocator]
An arena is a contiguous byte range with a bump pointer. Allocation
of an aligned $k$-byte object costs $O(1)$: one compare against the
arena end, one add to the bump pointer, one alignment mask.
\end{definition}
\begin{definition}[Wire formats]
We consider four wire formats:
\begin{itemize}
\item \textbf{ZAP}: arena of segments; structs are positional;
pointers are relative.
\item \textbf{Protobuf (PB)}: tag-length-value records; varint tags
and lengths.
\item \textbf{JSON}: textual key-value pairs; numbers are decimal
strings.
\item \textbf{FlatBuffers (FB)}: positional like ZAP but with a
vtable indirection per struct (included for context).
\end{itemize}
\end{definition}
\begin{definition}[Workload parameters]
A request has $f$ logical fields, total wire size $n$ bytes, and $p$
of those bytes are variable-length payload (strings, blobs, lists)
that the sender chose to allocate inside the request arena.
\end{definition}
\section{Constant-time arena allocation}
\label{sec:arena}
\begin{lemma}[Arena allocation is $O(1)$]
\label{lem:arena}
Allocating an aligned struct of size $k \leq 2^{16}$ in an arena
takes $O(1)$ instructions and $O(1)$ cache lines amortized.
\end{lemma}
\begin{proof}
The bump pointer $b$ and the arena end $e$ both fit in registers.
The allocation is
\[
b' \;=\; \mathrm{align}_8(b + k);\quad
\text{if } b' > e \text{ go to overflow path};\quad
b \;\leftarrow\; b'.
\]
Three arithmetic operations and one branch: $O(1)$ instructions.
The cache cost is incurred only on the first byte of the next cache
line, so amortized over $64/k$ allocations it is $O(1/k)$ lines.
The overflow path falls through to a fresh segment allocation, which
is itself $O(1)$ (a single \texttt{mmap}-style call to a free list).
\end{proof}
\begin{lemma}[Field access is $O(1)$ in field count]
\label{lem:fieldaccess}
For a ZAP struct, reading or writing field $f_k$ takes $O(1)$
instructions independent of the total number of fields $f$.
\end{lemma}
\begin{proof}
Compile-time generated accessors compute the offset $\mathrm{off}(f_k)$
as a constant. The access is then a single load from
$\mathrm{base} + \mathrm{off}(f_k)$ (one displacement-mode memory
operation on x86\_64). No tag decoding, no table lookup, no
indirection.
\end{proof}
\begin{remark}
This is the property that distinguishes ZAP from FlatBuffers, which
performs a vtable lookup adding a load and an addition per field
access. The asymptotic class is the same ($O(1)$) but the constant
is roughly $2\times$ smaller for ZAP.
\end{remark}
\section{Per-format serialization cost}
\label{sec:performat}
\begin{lemma}[ZAP serialization cost]
\label{lem:zapser}
Constructing a ZAP message containing $f$ fixed-layout fields and $p$
bytes of variable payload costs
$L_{\textit{ser}}^{\mathrm{ZAP}}(f,p) = O(f) + \Theta(p)$
in instructions, and the $O(f)$ term is a sum of independent stores
that the writer issues anyway.
\end{lemma}
\begin{proof}
By \Cref{lem:arena} the arena is initialized in $O(1)$. By
\Cref{lem:fieldaccess} each fixed field is one store. The writer
must store each field at least once, so this is the same cost as
``writing the answer''---there is no \emph{additional} marshaling
work. Variable-length payload is copied byte-by-byte at $\Theta(p)$.
The amortized cost over a request that already produces these bytes
is therefore $L_{\textit{ser}}^{\mathrm{ZAP}}(f,p) = \Theta(p) + O(1)$
beyond the unavoidable field stores.
\end{proof}
\begin{lemma}[Protobuf serialization cost]
\label{lem:pbser}
Encoding a Protobuf message with $f$ fields and $p$ payload bytes
costs $L_{\textit{ser}}^{\mathrm{PB}}(f,p) \;=\; \Omega(f) + \Theta(p)$,
and the $\Omega(f)$ term cannot be eliminated by a positional
representation because the wire format \emph{itself} requires per-field
tag bytes.
\end{lemma}
\begin{proof}
Each present field $f_k$ contributes at least one varint tag byte
plus, for length-delimited types, a varint length prefix. Computing
the varint requires a loop bounded by 5 bytes for 32-bit tags but
constant for any specific tag; nevertheless it is $\geq 1$ store
\emph{per field}, even when the field value is otherwise free.
Therefore the wire-format definition forces $\Omega(f)$ stores, and
no encoder can do fewer.
\end{proof}
\begin{lemma}[JSON serialization cost]
\label{lem:jsonser}
Canonical JSON encoding of $f$ fields with $p$ payload bytes costs
$L_{\textit{ser}}^{\mathrm{JSON}}(f,p) = \Theta(n + f \log f)$ where $n$ is
the total output size.
\end{lemma}
\begin{proof}
Each field contributes its key as text, a colon, the value, and a
comma; this is $\Theta(n)$ in output bytes. Canonical JSON requires
keys to be sorted; sorting $f$ keys is $\Theta(f \log f)$. Number
formatting (\texttt{double}-to-decimal-string with round-trip
guarantee) is $\Theta(1)$ per number but with a much larger
constant than a memory store.
\end{proof}
\section{Throughput Theorem}
\label{sec:thmthroughput}
\begin{theorem}[Throughput bound for zero-copy wire]
\label{thm:throughput}
Consider a workload offering requests of size $n$ bytes at offered
load $\lambda$, with link bandwidth $B$ and per-request fixed CPU
cost $\sigma$ (framing, dispatch, scheduler entry). The achievable
steady-state throughput $T$ for a wire format with serialization cost
$L_{\textit{ser}}(n,f)$, deserialization cost $L_{\textit{de}}(n,f)$, and per-message
header overhead $h$ satisfies
\begin{equation}
T \;\leq\; \min\!\Big(
\tfrac{B}{n+h},\;
\tfrac{1}{\sigma + L_{\textit{ser}}(n,f) + L_{\textit{de}}(n,f)}
\Big).
\label{eq:throughput}
\end{equation}
For ZAP under fixed-layout structs,
$L_{\textit{ser}}(n,f)=L_{\textit{de}}(n,f)=O(1)$ and $h=O(w)$, so as $n \to
\infty$, $T \to B/n$. For Protobuf-over-HTTP/2 with HPACK,
$h \geq h_{\mathrm{HPACK}} + h_{\mathrm{frame}}$ and the CPU bound binds first
at small $n$, so $T \leq r \cdot B/n$ for some $r \in [0.6, 0.7]$
on standard hardware.
\end{theorem}
\begin{proof}
The link cannot deliver more than $B$ bytes per second; therefore at
most $B/(n+h)$ messages per second can cross the wire. This is the
first term of the $\min$.
The CPU pipeline must (i) pay the per-request fixed cost $\sigma$,
(ii) serialize, (iii) deserialize. By Little's law on a single core,
the steady-state rate cannot exceed
$1/(\sigma + L_{\textit{ser}} + L_{\textit{de}})$. This is the second term.
For ZAP, by \Cref{lem:zapser} and the symmetric statement for
deserialization (which is the identity function on the byte buffer
plus the constant-cost root pointer chase), $L_{\textit{ser}}+L_{\textit{de}}=O(1)$.
The header overhead is the segment table plus root pointer, which is
$O(w)$ words. Therefore the second term is $\Theta(1/\sigma)$,
independent of $n$, and the first term dominates as $n \to \infty$.
For Protobuf-over-HTTP/2, by \Cref{lem:pbser},
$L_{\textit{ser}}(n,f)+L_{\textit{de}}(n,f) = \Omega(f) + \Theta(n)$. HPACK
header decoding contributes a per-message constant
$\sigma_{\mathrm{HPACK}}$ that is non-negligible (measured in published
benchmarks at $0.5$--$1.5\,\mu$s). The CPU bound is therefore
$1/(\sigma + \sigma_{\mathrm{HPACK}} + \Omega(f))$, which on commodity
hardware empirically binds at $0.6$--$0.7$ of the link bound for
$n \in [128, 8192]$ bytes. Hence $T \leq r \cdot B/n$ with $r$ in that
range.
\end{proof}
\begin{corollary}
The crossover point at which ZAP saturates the link, while Protobuf
remains CPU-bound, is approximately
$n^* \;=\; \big(\sigma_{\mathrm{HPACK}} + \alpha f\big) \cdot B / (1-r)$,
where $\alpha$ is the per-field cost. For $\sigma_{\mathrm{HPACK}}=1\,\mu$s,
$\alpha=10$\,ns, $f=32$, $B=10$\,Gbps, $r=0.65$, we get
$n^* \approx 3.7$\,KiB.
\end{corollary}
\section{Tail-Latency Independence Theorem}
\label{sec:thmtail}
\begin{theorem}[Tail-latency independence from field count]
\label{thm:tail}
Let $L^{(q)}(f,p)$ denote the $q$-th quantile of single-RPC latency
under i.i.d.\ payloads with $f$ fields and bounded payload bytes
$p$. For ZAP,
\[
L^{(q)}_{\mathrm{ZAP}}(f,p) \;=\; L^{(q)}_{\mathrm{ZAP}}(p) + O(1),
\]
i.e.\ the $q$-th quantile is asymptotically independent of $f$.
For Protobuf and JSON,
\[
L^{(q)}_{\mathrm{PB}}(f,p) \;=\; \Omega(f) + L^{(q)}_{\mathrm{PB}}(p),
\]
and the slope at $q=0.999$ exceeds the slope at $q=0.5$ by a
multiplicative factor that grows with allocator and HPACK
dynamic-table state.
\end{theorem}
\begin{proof}
By \Cref{lem:zapser}, ZAP serialization cost is $O(1)$ in field
count plus $\Theta(p)$ in payload bytes. The same holds for
deserialization (identity map). The variance contribution to any
quantile is therefore bounded by the variance of the constant-time
fixed cost, which is $O(1)$ regardless of $f$.
For Protobuf, by \Cref{lem:pbser}, each field contributes at least
one tag-byte store and, for length-delimited fields, one varint
length-prefix store. These stores can each miss the L1 cache, and
the probability that at least one of $f$ such stores misses grows as
$1 - (1-m)^f \approx mf$ for small per-store miss probability $m$.
Therefore the expected number of L1 misses scales with $f$, and at
high quantiles the realized number of misses scales faster than at
the median due to the heavy-tailed distribution of cache-miss
penalties.
For JSON, the canonical-key sort is $\Theta(f \log f)$ in the median
case, and adversarial input can push it toward $\Theta(f^2)$ in
quicksort-based implementations, dominating high quantiles.
For the HPACK component, dynamic-table eviction during congestion
adds tail-only latency proportional to header set cardinality, which
correlates with $f$ when each field becomes a header (gRPC trailers,
metadata, etc.).
\end{proof}
\begin{corollary}
The $p999/p50$ ratio for ZAP is bounded by the noise floor of the
network and scheduler, typically $3$--$5\times$. For Protobuf-over-HTTP/2
under congestion, the same ratio observed in fleet measurements
exceeds $20$--$50\times$.
\end{corollary}
\section{Discussion of Lower Bounds}
\label{sec:lowerbounds}
\begin{remark}
The throughput bound \Cref{eq:throughput} is tight in the sense that
ZAP achieves the $B/(n+h)$ term up to a small constant in practice.
The Protobuf bound is also tight: there is no encoder that avoids the
per-field tag byte without changing the wire format itself, and
changing the wire format yields a different protocol (which is
what ZAP and FlatBuffers are).
\end{remark}
\begin{remark}
The tail bound \Cref{thm:tail} relies on the i.i.d.\ assumption.
Adversarial workloads can be constructed to make ZAP's tail worse,
e.g.\ by forcing arena overflow at every request to trigger segment
allocation. The expected behavior under realistic load remains as
stated.
\end{remark}
\section{Summary}
\label{sec:summary}
We have proved that ZAP's serialization and deserialization costs are
constant in field count, that the resulting throughput approaches
link rate as message size grows, and that tail latency is
asymptotically independent of field count. These bounds match the
predicted speedups in the companion paper. The proofs make explicit
their model assumptions; relaxing them (e.g.\ allowing adversarial
arena overflow) changes constants but not asymptotics.
\end{document}