MemSynth results: x86

Initial synthesized model

(define ppo (& po (- (-> MemoryEvent (+ Writes Reads)) (-> (- Writes Atomics) Reads))))

(define grf (- rf (join proc (~ proc))))

(define fences (-> none none))

(define TSO_0 (make-model ppo grf fences))

This model is incorrect: it allows the test x86/ambig/4 below, which should be forbidden by x86. MemSynth’s ambiguity query automatically identifies this additional test for the user to resolve.

Distinguishing litmus tests

Also available in Herd format: browse.

Test x86/ambig/1
=============================
P0            | P1           
-----------------------------
r1 <- [A]     | [B] <- 1     
r2 <- [B]     | LOCK [A] <- 1
=============================
r1=1 /\ r2=0

Test x86/ambig/2
=============================
P0            | P1           
-----------------------------
r1 <- [B]     | LOCK [A] <- 1
r2 <- [A]     | LOCK [B] <- 1
=============================
r1=1 /\ r2=0

Test x86/ambig/3
=============================
P0            | P1           
-----------------------------
r1 <- [B]     | r2 <- [A]    
LOCK [A] <- 1 | [B] <- 1     
=============================
r1=1 /\ r2=1

Test x86/ambig/4
=============================
P0            | P1           
-----------------------------
[A] <- 1      | LOCK [B] <- 1
MFENCE        | r2 <- [A]    
r1 <- [B]     |              
=============================
r1=0 /\ r2=0

Final synthesized model

(define ppo (- po (-> (- Writes Atomics) Reads)))

(define grf (- rf (join proc (~ proc))))

(define fences (-> none none))

(define TSO_4 (make-model ppo grf fences))

This model correctly specifies the intent of x86’s TSO memory model: all program-order edges are preserved, except that non-atomic writes (i.e., xchg operations) can be reordered after later reads