A corpus
Each fact about a system is a claim. A claim has a unit, the conditions where it is true, its sources and its grade of evidence.
systems
A client holds a connection, and its peer goes silent. When does the client know? This site computes the answer, and then it measures the answer.
One question, three answers
Section titled “One question, three answers”Linux 6.6 has default settings for each TCP timer. With these settings, an idle connection learns of a black hole after 2 h 11 min 15 s. A connection with a request in flight learns after 924.6 s. A connection to a frozen process does not learn of the failure at the TCP level.
The lab below computes these times from the rules of the kernel. Select a harness cell to see the runs that the harness measured. Change a setting to see the new prediction.
Kernel clock
- First detector
- keepalive
- Closed form
- 11 s
- Lands in
- 10.996 s to 11.352 s
- Measured
- 11.054 s to 11.269 s
Keepalive tells the client after 11 s, at most 352 ms late.
- Prediction
- Keepalive probes
- Measured runs
The whole timeline
Near the prediction
The parts of the program
Section titled “The parts of the program”An algebra
The algebra reads the state machines and the settings. It gives each timer a closed form, and a band for how late the timer fires.
A harness
The harness starts each cell in fresh containers. It injects a fault, measures the result on one clock, and compares the result with the prediction.
A prober
The prober is an eBPF program. It records what the kernel does to each socket, to the nanosecond.
Where to go next
Section titled “Where to go next”- The thesis tells why a connection is a chain of state machines.
- The detection lab computes the first detector for your settings.
- The results show each harness cell against its prediction.