MPhil course in Multicore Programming - Exercise Sheet 1

      Version of Mon Oct 25 12:43:31 BST 2010

Due: Wednesday November 11th (Revised date - originally Monday
November 8th). Please hand to student admin, with a
coversheet.



1.   In terms of the semantics on Slides 4-10:

a) Give two different transitions, with derivations using the rules in
the notes, of the process t1:(*x=(*y=*z)).

b) Give a complete transition sequence of the whole-system state 
<t1:(*x=(*y=*z)), {x=1,y=2,z=3}>.  Is it unique? 

c) By enumerating the possible whole-system transitions (without
giving their derivations in detail), or otherwise, prove that
<t1:(*x=1);*y | t2:(*y=1);*x, {x=0,y=0}> cannot reach a state of the
form <t1:0 | t2:0, M>.




2.  Consider the following tiny fragment of x86 assembly language.

thread id, t

value, x, v, n            word32 value

register, r ::= EAX | EBX | ECX | EDX

instruction, i ::= 
 | MOV [x] <- r
 | MOV [x] <- v
 | MOV r <-[x]
 | INC [x]
 | LOCK INC [x]
 | MFENCE

instruction_sequence, is ::=
 | stop
 | i ; is

register_environment, R    function from registers to values,
e.g. {EAX=0, EBX=1, ECX=38, EDX=0}

process, p ::=
 |  t:R:is            thread with id t, register environment R, and body is
 |  p | p             parallel composition of two threads


a) Define an operational semantics for processes that is suitable for
composing with the x86-TSO abstract machine, with a transition
judgement

     p --l--> p'

where l is a label from the grammar on Slide 45.

b) Describe the possible transition sequences of the process

   t2:R0: MOV [y]<-1; MOV ECX<-[x]; stop

where the initial register environment is R0 =
{EAX=0,EBX=1,ECX=2;EDX=3}.




3.  Read the chapters of the Intel SDM and AMD APM cited on Slide 35. 

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.

d) Is it allowed with respect to a semantics that only guarantees
coherence?




4. Consider the n6 example from Slide 33.

a) Give a transition sequence of the x86-TSO abstract machine that
proves that this behaviour is allowed there. 

b) Give an E and X that show that it is allowed with respect to the
x86-TSO axiomatic model, checking each of the axioms carefully. 




5. Suppose you have a single-threaded axiomatic-model E, in which
which all events are by a single thread and where po_iico is a strict
total order. Consider an arbitrary execution witness X such that
valid_execution E X.  Prove that X is SC in the sense that each read
reads from the most recent write to the same location w.r.t. po_iico,
or from the initial state if there is one. 



6. Discuss the issues (pro and con) involved in adopting TSO as a
programming-language memory model. 



A. (Optional)

a) Think of a new interesting x86 example that would be worth testing
on actual hardware.

b) Is your specified behaviour allowed or not with respect to x86-TSO?

c) Test it using the Litmus tool, distributed as part of diy here:
   http://diy.inria.fr/