MPRI 2.37.1 - 2015, Exercices on Hardware Memory Models ******************************************************* x86-TSO ******* For each of the following Litmus Tests, state if the final state is allowed or forbidden by the SC and by the x86-TSO memory models. All memory locations are initialised with 0. 1) MOV [x] <- 1 | MOV [y] <-1 MOV eax <- [y] | MOV ebx <- [x] Final state : 0:eax = 0; 1:ebx = 0 2) MOV [x] <- 1 | MOV [x] <-2 MOV eax <- [x] | MOV ebx <- [x] Final state : 0:eax = 2; 1:ebx = 1 3) MOV eax <- [x] | MOV ecx <- [x] MOV [x] <- 1 | MOV [x] <-2 MOV ebx <- [x] | MOV edx <- [x] Final state : 0:eax = 2; 0:ebx = 1; 1:ecx = 1; 1:edx = 2 4) MOV [x] <- 1 | MOV [y] <- 1 | MOV ecx <- [y] MOV eax <- [x] | | MOV edx <- [x] MOV ebx <- [y] | | Final state : 0:eax = 1; 0: ebx = 0; 2: ecx = 1; 2: edx = 0 Validate experimentally your guess by running the test on your machine via the litmus tool: sources: http://diy.inria.fr/sources/litmus.tar.gz doc : http://diy.inria.fr/doc/litmus.html ARMv7/Power *********** Validate the following Litmus Tests using the Power Memory Model simulator: http://www.cl.cam.ac.uk/~pes20/ppcmem/index.html#PPC 1) PPC MP { 0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x; } P0 | P1 ; li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwz r3,0(r4) ; li r3,1 | ; stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0) 2) PPC R { 0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x; } P0 | P1 ; li r1,1 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) ; li r3,1 | lwz r3,0(r4) ; stw r3,0(r4) | ; exists (y=2 /\ 1:r3=0) 3) PPC IRIW { 0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x; } P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) 4) PPC Z6.0 { 0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x; } P0 | P1 | P2 ; li r1,1 | lwz r1,0(r2) | li r1,2 ; stw r1,0(r2) | li r3,1 | stw r1,0(r2) ; li r3,1 | stw r3,0(r4) | lwz r3,0(r4) ; stw r3,0(r4) | | ; exists (z=2 /\ 1:r1=1 /\ 2:r3=0)