Add a note about processor memory reordering

Signed-off-by: Gilles Peskine <Gilles.Peskine@arm.com>
diff --git a/library/aesni.c b/library/aesni.c
index c51957f..2857068 100644
--- a/library/aesni.c
+++ b/library/aesni.c
@@ -51,6 +51,13 @@
     /* To avoid a race condition, tell the compiler that the assignment
      * `done = 1` and the assignment to `c` may not be reordered.
      * https://github.com/Mbed-TLS/mbedtls/issues/9840
+     *
+     * Note that we may also be worried about memory access reordering,
+     * but fortunately the x86 memory model is not too wild: stores
+     * from the same thread are observed consistently by other threads.
+     * (See example 8-1 in Sewell et al., "x86-TSO: A Rigorous and Usable
+     * Programmer’s Model for x86 Multiprocessors", CACM, 2010,
+     * https://www.cl.cam.ac.uk/~pes20/weakmemory/cacm.pdf)
      */
     static volatile int done = 0;
     static volatile unsigned int c = 0;