Yup, these are great slides, especially pg 11-14 about memory models.
Weakly consistent memory models contain all sorts of horrors for programmers that think sequentially consistently. Can the following program throw an assertion error?
//Initially, x = y = 0
Processor 1: x = 1;
Processor 2: while (x == 0) {/*do nothing*/}; y = 1;
Processor 3: while (y == 0) {/*do nothing*/}; assert (x == 1);
(On an ARM processor this assertion can legally fire (x can equal 0 for Processor 3); and you can s/Processor/Thread/ and still have this result hold)Volume 3A of the Intel Architecture Manual is worth a read if you like these type of puzzles (http://www.intel.com/products/processor/manuals/).
For those that want a formal approach then good things are happening in Cambridge: http://www.cl.cam.ac.uk/~pes20/weakmemory/