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 . Is it unique? c) By enumerating the possible whole-system transitions (without giving their derivations in detail), or otherwise, prove that cannot reach a state of the form . 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/