Oops!
Build an x86 memory model!
How well do you know x86? In this demo, you'll use MemSynth to interactively synthesize a (simplified) specification of the x86 memory consistency model.
MemSynth will generate new litmus tests—small multi-threaded programs—and ask you whether the behavior they describe should be allowed or forbidden. Once you've seen enough tests, MemSynth will synthesize a memory model specification consistent with your answers, and compare it to the actual x86 model.
Tests so far
MemSynth is thinking...
MemSynth built your memory model!
But is it x86? Let's compare to the Intel manual (big PDF).
| Litmus test | x86 | You said |
|---|
What about this test?
[A] <- 1 writes 1 to shared variable A.r1 <- [A] reads from shared variable A into local register r1.
X86 disambig2
{ A=0; B=0; }
P0 | P1 ;
MOV [A],$1 | MOV EAX,[B] ;
MOV [B],$1 | MOV EBX,[A] ;
exists (1:EAX = 1 /\ 1:EBX = 0)