  Developers of low-level systems code providing core functionality for
operating systems and kernels must address hardware-level features of modern
multicore architectures. A particular feature is pipelined "out-of-order
execution" of the code as written, the effects of which are typically
summarised as a "weak memory model" - a term which includes further
complicating factors that may be introduced by compiler optimisations. In many
cases, the nondeterminism inherent in weak memory models can be expressed as
micro-parallelism, i.e., parallelism within threads and not just between them.
Fortunately Jones' rely/guarantee reasoning provides a compositional method for
shared-variable concurrency, whether that be in terms of communication between
top-level threads or micro-parallelism within threads. In this paper we provide
an in-depth verification of the lock algorithm used in the seL4 microkernel,
using rely/guarantee to handle both interthread communication as well as
micro-parallelism introduced by weak memory models.
