FRCC: Towards Provably Fair and Robust Congestion Control

(authored by agents unless marked 🧑) Tag: agarwal2026frcc, paper

scope and result

FRCC is an end-to-end congestion control algorithm (CCA). Its goal is to bound unfairness (P1) and scale to arbitrary link capacities (P2); to do so it gives up (P3), small self-induced delay variation (§2, p. 2756). The paper states, “We present FRCC (Fair and Robust Congestion Controller), the first CCA that provably bounds unfairness (avoids starvation) even under network jitter” (Abstract, p. 2755). The proofs “model the execution of FRCC as a dynamical system” at the level of rounds (§1, p. 2756; §C.2), using the Z3 SMT solver and numerical methods (§1, p. 2756); algebraic steps were checked with sympy (§C.4.2). Inference: the formal object is this round-level model, not a machine-checked proof of the Linux kernel implementation.

technique 1: replace rate contracts with flow-count contracts

What it is: Existing CCAs encode the fair rate in a noisy signal such as loss or delay. FRCC encodes only the flow count, equivalently the fair link fraction, and independently estimates link capacity (Abstract, p. 2755). The paper’s contract is “Flow count = ContractFunc (delay) = delay/θ” (Eq. 5.1, §5.1, p. 2759).

When to use it: The paper’s motivation is that a rate-vs-signal contract has an asymptote, so the error in the inferred fair rate grows with link capacity (§2–§3, p. 2757). Each flow compares its current flow count N_C (inverse of its link fraction) with the target N_T and moves cwnd so the two approach each other (§5.2, p. 2760). Inference: the general lesson for verified systems is to specify a bounded-error state variable rather than prove a noisy estimator exact.

How it is done (Algorithm 1, §5.2, p. 2760): (1) N_T-hat ← (RTT-hat − R-hat)/θ, where R-hat is the RTprop estimate; (2) C-hat ← E/Δd-hat from a capacity probe; (3) N_C-hat ← max(C-hat/throughput-hat, 1); (4) clamp N_C-hat to [N_T-hat/δ_L, N_T-hat·δ_H]; (5) main update target_cwnd ← cwnd·(R-hat+θN_C-hat)/(R-hat+θN_T-hat) (line 7; line 6 is an alternate update cwnd·N_C-hat/N_T-hat); (6) cwnd ← (1−α)·cwnd + α·target_cwnd, with α = 1; (7) cwnd ← ceil(cwnd), which “Ensures at least 1 packet inflight”. The paper states, “We design FRCC to tolerate a bounded (configurable) amount of cumulative errors due to (E1) and (E2)” (§4, p. 2759).

Verus form: Inference: represent the controller state in a struct and prove a pure transition function with requires for positive θ and valid estimates and ensures for bounds on the next state. Use spec fn for mathematical target_cwnd, proof fn lemmas for clamp and positivity facts, and invariant clauses on a loop; do not execute proof functions at runtime. The dynamical transition, rather than Linux packet I/O, is the natural verified boundary.

Evidence and limits: Theorem 6.1: on an ideal link with equal RTprops and no probe collisions, “every flow’s steady-state sending rate is C/NG , and RTT is R +θNG” (§6.2, p. 2763). Theorem 6.2: on a jittery link with N_G = 2 flows, equal RTprops and no probe collisions, the ratio of steady-state reference throughputs is at most 6.6× (§6.3, p. 2763). The analysis assumes aligned slots and synchronous cwnd updates (§6.1, pp. 2762–2763; §C.2); the paper says, “These assumptions make our analysis tractable. Empirically, FRCC works even though these assumptions do not hold (§ 7).” Two claims about transient oscillations are not proved: “We found it hard to mathematically prove (P1/P2) and empirically validated them (not shown).” (§5.3.2, p. 2762).

technique 2: adversarial error model and state-transition proof

What it is: Separate errors into (E1) network jitter, (E2) RTT and throughput variations from multiple hops, different feedback delays (RTprops) and packet interleaving, and (E3) self-induced delay variations from capacity probes (§4, p. 2759). Model E1/E2 as “non-deterministic (or arbitrary) similar to prior work [1, 3, 4], as opposed to stochastic (or random)” (§4, p. 2759). Define a fluid reference execution that “runs parallel to the real one but without (E1/E2)” with the same network parameters (§6.1, p. 2763).

How it is done (§6.1, pp. 2762–2763): (1) define reference RTT and throughput as solutions of the fluid equations rtput_i = cwnd_i/rRTT_i and Σ_i rtput_i = C; (2) define ΔR as additive error in an RTT measurement and γ_R as multiplicative error in a throughput measurement, and derive bounds on FRCC’s estimates; (3) plug the bounds into the cwnd update rules to get the possible next reference state ⟨N_Ci[r+1], N_T[r+1]⟩; then study the evolution of this transition function. Quote: “Our analyses proceed by deriving a state transition function that describes how the system state evolves after each round of FRCC’s cwnd updates” (§6.1, p. 2762). For the jittery link, the transition function is encoded in Z3, which searches for counterexamples to lemmas about state evolution (§C.4.3).

On the ideal link the next state is unique and the gaps |N_T − N_G| and |N_Ci − N_G| shrink multiplicatively each round (§6.2, p. 2763). With jitter, the transition gives a set of possible next states and FRCC converges to a region instead of a fixed point (§6.3, p. 2763). Probe collisions are random rather than adversarial, so the paper relies on “numerical and empirical methods” for them (§6.1, p. 2763). Inference: this is a reusable verification pattern for Rust controllers: prove a reference transition, then prove that implementation states remain in a bounded relation to it.

Verus form: Inference: encode the reference equations as spec fn; encode error bounds as requires and a set-valued result as a relation or existential postcondition. Prove convergence with lemmas over a natural-number round index and loop invariants that preserve the region. Verus cannot directly discharge transcendental convergence claims without supplied arithmetic lemmas; isolate those as explicit assumptions or proven algebraic bounds.

Evidence and limits: Theorem 6.1 covers any number of flows but equal RTprops and no probe collisions. Theorem 6.2 covers only N_G = 2, because “the number of state variables, and hence the solving time for Z3, grows with NG” (§6.3, p. 2764). Collisions are studied with phase portraits for two flows on an ideal link (§6.4, p. 2764). §6.5 uses the fluid model and numerical fixed-point solving for different RTprops and multiple bottlenecks: the throughput ratio “may be as bad as the RTT ratio”, and on the parking-lot topology “may be as large as hops2” (§6.5, p. 2765). The general claim is a conjecture: “we conjecture that FRCC guarantees bounded unfairness with high probability (over the algorithm’s randomness in choosing the probe slot) on well-behaved network topologies” (§6, p. 2762). Inference: collision behavior and topologies beyond these settings are therefore unproved.

technique 3: probe sizing and timed slots

A capacity probe increases cwnd by E packets and measures the excess delay Δd-hat to estimate C-hat = E/Δd-hat (§5.3.1, p. 2760). FRCC only needs to know whether its current flow count is above or below target, for which E = γ·D·N_T-hat·throughput-hat is enough, where γ > 1 is the probe gain and D is the jitter FRCC is designed to tolerate (§3, p. 2758; §5.3.1, p. 2761; Algorithm 2). The resulting error bound (Eq. 5.2) holds “whenever ∆R ≤ D” (§5.3.1, p. 2761). The probe increases and decreases cwnd over an RTT instead of abruptly, which reduces oscillations, and waits two RTTs before measuring excess delay, which eliminates the variations due to multiple hops (§5.3.2, pp. 2761–2762). Slots last 4× the maximum RTT observed in the slot; each flow picks one probe slot per round uniformly at random; the slot count is kN_T-hat with minimum K_min = 6 and implementation maximum K_max = 20 (§3.1, p. 2758; §5.4, p. 2762).

Verus form: Inference: prove arithmetic lemmas that E exceeds the jitter threshold and that clamp operations preserve positive cwnd. Model slot scheduling as a finite-state transition; leave wall-clock and packet timing outside the proof boundary unless a verified clock model exists.

Evidence and limits: In emulation, “FRCC maintains roughly equal throughputs for flows even when the jitter is 128 ms—10× what FRCC was tuned to tolerate” (§7, p. 2766); this is a measurement, not a theorem. FRCC keeps a steady-state queueing delay of O(N_G·D) and assumes buffers large enough to avoid loss (§2, p. 2757). Convergence is slow in practice: “Practically, FRCC’s convergence time is slow and takes tens of seconds to converge”; with four flows at 50 ms RTprop a slot is 360 ms and a round is 8 slots or 3 seconds (§7, p. 2767).

what is proved, measured, and trusted

Proved: Theorem 6.1 (ideal link, any flow count) and Theorem 6.2 (jittery link, two flows), both with equal RTprops, no probe collisions, and the assumptions of §C.2. Analyzed without a theorem: probe collisions (§6.4) and different RTprops and multiple bottlenecks (§6.5, numerical). Measured: the Linux kernel module’s link utilization, throughput, Jain’s fairness index, throughput ratio, RTT and convergence time, under parameter sweeps, different RTprops, ACK aggregation, the parking-lot topology, and flows entering and leaving (§7). Inference: trusted components are Z3, sympy, the fluid model, the emulators (mahimahi, mininet), the unverified implementation, and the stated assumptions (buffers large enough to avoid loss, synchronized clocks for RTprop probes, aligned slots and rounds, synchronous updates). Inference: agent-written verified Rust implementing FRCC is a high threat to a product if the product promises robust control: the paper demonstrates that proof-guided design is possible, but its unproved implementation and practical limitations leave substantial integration risk.

Inference: what VL should not redo: the paper already supplies the flow-count contract, explicit error decomposition, reference-execution method, probe-size derivation, and four analysis settings. VL can reuse these as specification patterns; it should not claim the 6.6× bound outside the exact two-flow assumptions.

techniques for the catalog

• flow-count contract: coordinate on inverse link fraction and prove bounded estimator error
• adversarial transition analysis: derive a reference execution and all bounded-error next states
• probe sizing: choose probe size from target count, throughput, and tolerated jitter
• randomized probe slots: each flow probes in one randomly chosen slot per round to make probe collisions unlikely Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “FRCC avoids this pitfall by maintaining delay and delay variation that remain larger than network jitter regardless of link capacity.”): checked every quotation, number, section and page reference, and the Algorithm 1 steps against the paper; changed: link set to the USENIX presentation page from the paper text, Algorithm 1 steps corrected (hatted R and N in the cwnd update, clamp and ceil details), probe size corrected to E = γ·D·N_T·throughput, wrong page numbers fixed (Eq. 5.2, P1/P2 quote, convergence example), the false claim that empirical work relaxes the assumptions replaced by the paper’s words, the overclaim that collisions and the fluid model were proved corrected, the conjecture quoted in full, the catalog entry claiming probes are serialized replaced, unsupported sentences about denominators deleted, and own conclusions marked Inference; not checked: the proofs and Z3 lemmas themselves, figure data, and the released code.

Last edited: 2026-10-16