ASPLOS Paper: Frightening Small Children and Disconcerting Grown-ups: Concurrency in the Linux Kernel.
All in all, our LK model specifies the cumulative effect of a language-level model (the subset of C specific to the LK) and the hardware models targeted by the LK.
Syntax and semantics of the weak consistency model specification language cat
Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory