M5 Concurrency

[tamnd]

Roughly eighteen weeks. Ten lessons, C01 to C10, and the riskiest content milestone in the project.

Concurrency is where readers are lost. It is also where Tier 0 hurts most, because v86 is uniprocessor and a uniprocessor emulator cannot show you a race.

The design answer is that Part V is not where concurrency starts. Rule 7 has put a context badge on every frame and CPU lanes on every trace since Part I, so by the time a reader gets here they have been looking at concurrent behaviour for four parts and are already asking the right questions. Part V formalises what they have already seen. If that plan works, this milestone is fine. If it does not, this is where we find out.

The uniprocessor limit is covered two ways. Recorded multi CPU traces from CI on real hardware, and the formal memory model, which is better than an emulator for the specific question of what orderings are allowed. An emulator shows you one execution. herd7 enumerates all of them.

Exit criterion. A reader can take a lock free algorithm out of the tree, prove or refute it under the Linux Kernel Memory Model, and read a lockdep splat unaided.

Lessons

• C01 Why the sequential story was a lie
• C02 Atomics
• C03 Spinlocks
• C04 Mutexes and semaphores
• C05 Per CPU data
• C06 RCU
• C07 Memory ordering
• C08 The formal model
• C09 Lockdep
• C10 PREEMPT_RT

Everything else

• The SMP corpus, recorded on real x86-64 multi core hardware
• The Lock Timeline artifact
• The LockdepSplat and LitmusView widgets
• The Litmus Lab playground
• herd7 wired in, and the question of whether it runs in the browser or ships as precomputed output settled either way
• Six blueprints at complete: atomics, spinlocks, sleeping-locks, rcu, percpu, memory-model
• The RCU grace period animation

The rule this milestone is held to

If beginner completion for Part V comes in under 70 percent, the part gets rewritten rather than shipped. That is the standing rule for every part, and this is the part most likely to trip it.