The universal machine, the halting problem, Rice on schedulers, and deadlock detection as the approximation a kernel can afford.
Turing, 1936: one machine, handed the description of any other, does what that one does. The emulator of week 3 is that machine, and the program it is handed is data. A universal machine cannot be specialised to safe programs only, because it must accept every description.
So the machine will run programs that loop, that address memory they do not own, that never yield. Nothing can screen them out in advance, and something has to deal with them at run time. That something is the kernel. Operating systems are what universality makes necessary.
The kernel is not a collection of workarounds for badly written programs. It is the run-time consequence of three theorems about what cannot be known at design time. Each theorem, each consequence, on the next slides.
Suppose H decides halting. Build D: run H on its own input, loop if H says halt, halt if it says loop. Run D on D: either answer contradicts itself. Cantor's diagonal, on programs.
The kernel's answer, week 5: do not decide, bound. The timer guarantees that every context yields, by preempting the ones that would not.
Fork, week 7, is the construction made literal: a process that runs a copy of itself. The kernel copes because the copy is isolated; isolation keeps self-reference from becoming a contradiction.
| the kernel would like to know | a property of | what it does instead |
|---|---|---|
| will this process yield? | behaviour | timer interrupt · week 5 |
| how long will this job run? | behaviour | a policy, round robin · week 5 |
| will this process touch that page? | behaviour | page faults on demand · week 4 |
| will this block be used again? | behaviour | reachability · week 9 |
| will these threads deadlock? | behaviour | detect the cycle when it exists · today |
| is this program safe to run? | behaviour | isolate it, and bound it · every week |
| has this process called exit? | the door | decided, exactly · week 7 |
The last row is the pattern: what happens at the interface is syntax, recorded and decidable. What happens inside is semantics, and Rice says the kernel may not know it. Every mechanism in the class sits in the right-hand column.
Four conditions, all necessary: mutual exclusion, hold and wait, no preemption of held resources, and a circular wait. Break any one by design and deadlock is impossible. Ordering all locks breaks the fourth: a proof obligation on the programmer, not the machine.
Whether a program will deadlock is a behaviour property: Rice. Whether the system is deadlocked now is a fact about the current state: a cycle in the waits-for graph. Linear time. The kernel checks the present because it cannot see the future.
Detection tells you a cycle exists. Recovery is killing a process in it: preempt what cannot be reasoned with. Or do what most systems do, and let the user notice. Detection is an approximation the kernel can afford; prevention is a proof it cannot make.
Week 6 said it for hypster: isolation comes from a ground the kernel does not control, hardware privilege or a smaller kernel beneath. Gödel's second theorem, run as a system. The trusted computing base is the axiom set, and the verified kernels of the world are proofs relative to it.
The same theorem applies to any system that is universal, including the ones that next week will run as processes under your kernel. A system cannot certify itself; the certificate has to come from outside, from something smaller, that somebody understands.
Agents as processes. A generator produces programs; a kernel runs them under isolation and bounds. Sandboxing is virtualization, and the gate is everything this class built.
Wagner · Tannhäuser — Colin Davis, Bayreuth 1978. Rome’s verdict: the papal staff will sprout leaves before Tannhäuser is forgiven, a decision made from a bound rather than from the man. Then the staff sprouts. The undecidable question, answered from outside.
Plato and the Nerd — Lee, 2017: models, machines and what universality does and does not buy, by someone who builds both. And, more technical, System Deadlocks — Coffman, Elphick and Shoshani, 1971: the four conditions, prevention, avoidance and detection, the survey this week’s slide condensed.