Linux-kernel memory model

The Linux-kernel memory model is currently defined very informally in the memory-barriers.txt, atomic_ops.rst, atomic_bitops.txt, atomic_t.txt, and refcount-vs-atomic.rst files in the source tree. Although these two files appear to have been reasonably effective at helping kernel hackers understand what is and is not permitted, they are not necessarily sufficient for deriving the corresponding formal model. This document is a first attempt to bridge this gap.