MPhil course in Multicore Programming - Exercise Sheet 1

      Version of 7 Oct 2016

Please hand to student admin, with a coversheet. Deadline noon,
December 5, 2016.



1.  Read the chapters of the Intel SDM and AMD APM about memory
ordering pointed to in the slides.  

Consider this x86 example:

  Initially all registers and [x] and [y] are 0. 

    Thread 0         Thread 1           Thread 2

    MOV [x] <- 1     MOV EAX <- [x]     MOV [y] <- 1
                     MOV EBX <- [y]     MOV ECX <- [x]

  Finally: 
    Thread 1: EAX=1
    Thread 1: EBX=0
    Thread 2: ECX=0

a) Is this allowed with respect to an SC semantics?

b) Can you argue whether this is allowed or not with respect to each of
those chapters?

c) Prove whether or not it is allowed with respect to the x86-TSO
abstract machine.




2. Using ppcmem, http://www.cl.cam.ac.uk/~pes20/ppcmem, for each of
the following tests, either explain why it doesn't have any non-SC
behaviour or describe the abstract-machine trace of one non-SC
behaviour (explain what's going on, but don't write out the full state
after each step of the trace in excruciating detail).

a) WRC+lwsync+isync
b) IRIW+lwsync+lwsync
c) MP+lwsync+addr
d) SB+sync+lwsync


3. Either prove or give a counterexample for the conjecture that any
candidate execution in which the reads and writes are all to the same
location and that does not contain any of the five coherence shapes is
SC-L.


4. Consider the C11 stack-weak.c implementation.  

a) Discuss, in terms of C11 litmus-test shapes, the properties that it
depends.

b) Explain (informally, but in some detail) why those hold, in terms
of the corresponding properties for the POWER, ARMv8, and x86
mappings.