MemSynth results

This page hosts the full synthesis results—specifications and litmus tests–for MemSynth. We synthesized correct specifications for both the PowerPC and x86 memory models, and discovered several ambiguities in each.

Results for PowerPC

Initial synthesized model

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

(define grf
  (-> none none))

; let-expressions inserted manually for readability
(define fences
  (let ([poFpo (join (:> po Syncs) po)]
        [poLFpo (join (:> po Lwsyncs) po)]
        [RE+WW (+ (-> Reads MemoryEvent) (-> Writes Writes))])
    (+
     (<:
      (+ Reads (join (+ rf poFpo) (+ Reads Writes)))
      (+ (:> (join poFpo rf) Reads) (+ poFpo (join rf poFpo))))
     (:> (<: (+ Reads Writes)
             (+ (& RE+WW poLFpo) (join (& RE+WW poLFpo) rf)))
         (+ (+ Writes (join (& RE+WW poLFpo) Writes))
            (:> (join Reads (& RE+WW poLFpo)) Reads))))))

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

Distinguishing litmus tests

Also available in Herd format.

Test ppc/ambig/1
=============================
P0            | P1           
-----------------------------
r1 <- [B]     | r2 <- [A]    
sync          | r3 <- r2 ^ r2
[A] <- 1      | [B+r3] <- 1  
=============================
r1=1 /\ r2=1

Test ppc/ambig/2
=============================
P0            | P1           
-----------------------------
r1 <- [B]     | r2 <- [A]    
lwsync        | r3 <- r2 ^ r2
[A] <- 1      | [B+r3] <- 1  
=============================
r1=1 /\ r2=1

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

Test ppc/ambig/4
=============================
P0            | P1           
-----------------------------
r1 <- [B]     | r3 <- [A]    
sync          | lwsync       
r2 <- r1 ^ r1 | [B] <- 1     
[A+r2] <- 1   |              
=============================
r1=1 /\ r3=1

Test ppc/ambig/5
=============================
P0            | P1           
-----------------------------
r1 <- [A]     | [B] <- 1     
r2 <- r1 ^ r1 | lwsync       
r3 <- [B+r2]  | [A] <- 1     
r4 <- [B]     |              
=============================
r1=1 /\ r3=0 /\ r4=1

Test ppc/ambig/6
=============================
P0            | P1           
-----------------------------
r1 <- [B]     | r2 <- [A]    
sync          | r3 <- r2 ^ r2
lwsync        | [B+r3] <- 1  
[A] <- 1      |              
=============================
r1=1 /\ r2=1

Test ppc/ambig/7
=============================
P0            | P1           
-----------------------------
r1 <- [B]     | r3 <- [A]    
r2 <- r1 ^ r1 | r4 <- r3 ^ r3
[A+r2] <- 1   | [B+r4] <- 1  
sync          |              
[A] <- 1      |              
=============================
r1=1 /\ r3=1

Test ppc/ambig/8
=============================
P0            | P1           
-----------------------------
r1 <- [B]     | r4 <- [A]    
sync          | r5 <- r4 ^ r4
[A] <- 1      | [B+r5] <- 1  
r2 <- r1 ^ r1 |              
r3 <- [A+r2]  |              
=============================
r1=1 /\ r3=1 /\ r4=1

Test ppc/ambig/9
=============================
P0            | P1           
-----------------------------
[B] <- 1      | r2 <- [A]    
r1 <- [B]     | r3 <- r2 ^ r2
lwsync        | r4 <- [B+r3]
[A] <- 1      |              
=============================
r1=1 /\ r2=1 /\ r4=0

Final synthesized model

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

(define grf
  (-> none none))

; let-expressions inserted manually for readability
(define fences
  (let ([poFpo (join (:> po Syncs) po)]
        [poLFpo (join (:> po Lwsyncs) po)]
        [RE+WW (+ (-> Reads MemoryEvent) (-> Writes Writes))])
  (+
   (:>
    (+ (+ (join rf poFpo) (<: Writes poFpo))
       (join poFpo (+ rf poFpo)))
    (+ (join (+ Reads Writes) (+ rf poFpo))
       (<: Reads (join poFpo Writes))))
   (:> (:> (+ (:> (& RE+WW poLFpo) Writes)
              (join rf (& RE+WW poLFpo)))
           (+ Reads Writes))
       (:> (+ Writes (join (& RE+WW poLFpo) Writes))
           (join (+ Reads Writes) (+ rf (& RE+WW poLFpo))))))))

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

Results for 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.

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