MemSynth results: PowerPC

(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))

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

(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))