Posts

The M/M/1 queue's 1/(1-rho) blowup. Why a service at 80% load is fine and at 95% is on fire.

L = lambda W, with essentially no assumptions. Capacity planning from one line of algebra.

Convince someone you know a secret while revealing nothing. The most counterintuitive constructive result in the series.

All of modern crypto rests on an unproven assumption. Why P != NP would still not be enough to secure anything.

Security lives in the key; and Shannon's proof that the one-time pad is unbreakable and impractical for the same reason.

O(log n) proof that one item belongs to a huge set. Git, certificate transparency, and every blockchain are the same data structure.

Your hardware and compiler reorder your program. What, fences, and acquire/release actually guarantee.

2PL produces exactly the serializable schedules; anomalies are precisely what you buy by weakening it.

The correctness condition for concurrent objects, and how it differs from serializability (Conflict serializability and two-phase locking) and sequential...

Atomic registers cannot implement consensus for two threads; compare-and-swap does it for any number. Why your CPU has CAS.

Peterson's algorithm and Lamport's bakery. Correct mutual exclusion from plain reads and writes, and why modern hardware still breaks it (see Memory models and...

A randomized scheduler with a provable bound on both time and space, and why every modern runtime converged on it.

SAT is NP-complete (The Cook–Levin theorem) yet solvers handle millions of variables.

A named theory result sitting in the middle of every compiler backend, plus why the NP-hardness does not stop anyone. Part V's counterweight to all the type theory.

Exhaustively verifying concurrent systems by turning "always eventually" into an automaton, and the state-explosion wall.

Reasoning about programs as a proof system; loop invariants as the hard part, and why they can't be inferred in general.

Constant space, no false negatives, a tunable false-positive rate, and the exact formula for the tradeoff.

Relational algebra and relational calculus have equal expressive power. Why SQL is declarative and why a query planner can exist at all.

Adding a node should move 1/n of the keys, not all of them. One idea, and virtual nodes to fix its variance (Balls into bins and the power of two choices).

Sound approximation, made rigorous. The principled answer to the tradeoff Rice's theorem forces on you.