Mips

LeanCats.lean

@@ -9,10 +9,12 @@ import LeanCats.CatPreprocessor
 import LeanCats.Macro
 import LeanCats.Theorems
 import LeanCats.TsoWeakerThanSc
+import LeanCats.mipsWeakerThanTSO
 import LeanCats.ModelReader
 import LeanCats.Litmus
 import LeanCats.LitmusParser
 import LeanCats.LitmusGraph
 import LeanCats.LitmusGraphBridge
 import LeanCats.LitmusReader
 import LeanCats.Linux.CoRR_poonceonce_Once
+import LeanCats.Linux.X86_SB_rfi_pos

LeanCats/Basic.lean

@@ -24,6 +24,10 @@ structure CandidateExecution (evts : Events) where
   ctrl' : SetRel Event Event := ∅
   fence' : SetRel Event Event := ∅
   mb' : SetRel Event Event := ∅
+  SYNC' : Set Event := ∅
+  -- Specific fence event sets depend on the test architecture,
+  -- their name is always uppercase and derives from the mnemonic of the instruction that generates them.
+  syncInF : ∀ (e : Event), e ∈ SYNC' → e ∈ evts.F
   uniqueId : ∀ (e₁ e₂ : Event),
     e₁ ∈ evts.all → e₂ ∈ evts.all
     -> e₁ ≠ e₂
@@ -34,11 +38,6 @@ structure CandidateExecution (evts : Events) where
     (w, r) ∈ rf'
     → w.t_id = r.t_id
     → (w, r) ∈ evts.po
-  coWR : ∀ (w r w' : Event),
-    (w, r) ∈ evts.po
-    → w.effect.location = r.effect.location
-    → (w', r) ∈ rf'
-    → (w, w') ∈ co' ∨ w = w'
 
 /-- from-reads: always defined as rf⁻¹ ; co, so it is transparent to the kernel. -/
 @[simp] def CandidateExecution.fr' {evts : Events} (X : CandidateExecution evts) : SetRel Event Event :=

LeanCats/Cats/examples/models/bpf.cat

@@ -0,0 +1,81 @@
+(*************)
+(* Utilities *)
+(*************)
+
+(* Single event atomic ops are marked with both R and W.
+ * These events are marked with SC if the op returns a value.
+ *)
+let RMW = [R & W] & [SC]
+
+(* Atomic ops with separate R and W events are related by the amo relation.
+ * both of these R and W events are  marked with SC if the op returns a value.
+ *)
+let SRMW = (SC * SC) & amo
+
+(* Ignore the SRCU part *)
+let po_amo_fetch = ([M];po;RMW) | (RMW;po;[M])
+
+show po_amo_fetch as atomicfetch
+
+(* Release Consistency processor consistent (RCpc) *)
+let load_acquire = ([AQ];po;[M])
+let store_release = ([M];po;[RL])
+let rcpc = load_acquire | store_release
+
+(****************)
+(* Dependencies *)
+(****************)
+
+let addr_dep = [R];addr;[M]
+let data_dep = [R];data;[W]
+let ctrl_dep = [R];ctrl;[W]
+
+show addr_dep as addr
+show data_dep as data
+show ctrl_dep as ctrl
+
+(**********************)
+(* ppo and prop rules *)
+(**********************)
+
+(* Compute coherence relation *)
+include "cos-opt.cat"
+let com = co | rf | fr
+
+let ppo =
+(* Explicit synchronization *)
+ po_amo_fetch | rcpc
+(* Syntactic Dependencies *)
+| addr_dep
+| data_dep
+| ctrl_dep
+(* Pipeline Dependencies *)
+| [M];(addr|data);[W];rfi;[R]
+| [M];addr;[M];po;[W]
+(* Overlapping-address ordering *)
+| (coi | fri)
+
+(* Propagation ordering from SC and release operations *)
+let A-cumul = rfe? ; (po_amo_fetch | store_release)
+let prop = (coe | fre)? ; A-cumul* ; rfe?
+
+(**********)
+(* Axioms *)
+(**********)
+
+(* Sc per location *)
+acyclic com | po-loc as Coherence
+
+(* No-Thin-Air and Observation *)
+let hb = ppo | rfe | ((prop \ id) & int)
+acyclic hb as Happens-before
+
+(* Propagation *)
+let pb = prop ; po_amo_fetch ; hb*
+acyclic pb as Propagation
+
+(* Atomicity *)
+empty rmw & (fre;coe) as Atomic
+
+(* Atomic fetch as a fence *)
+acyclic po_amo_fetch | com

LeanCats/Cats/examples/models/mips.cat

@@ -0,0 +1,12 @@
+let fencerel(r) = (po & (_ * r)) ;  po
+let com = rf | fr | co
+acyclic po_loc | com as uniproc
+
+let sync = try fencerel(SYNC) with 0
+
+empty rmw & (fre;coe) as atomic
+
+let ppo = po & (R * M) | sync
+
+let ghb = ppo | rfe | fr | co
+acyclic ghb as pso

LeanCats/Cats/tso.cat → LeanCats/Cats/examples/models/tso.cat

@@ -1,5 +1,7 @@
 include "cos.cat"
 
+empty rmw & (fre;coe)
+
 let xppo = ((W*W) | (R*W) | (R*R)) & po
 let At = domain(rmw) | range(rmw)
 let implied = po;[At | F] | [At | F];po

LeanCats/Cats/examples/models/tsox.cat

@@ -0,0 +1,4 @@
+let xppo = ((W*W) | (R*W) | (R*R)) & po
+let At = domain(rmw) | range(rmw)
+let implied = po;[At | F] | [At | F];po
+acyclic (implied | xppo | rfe | fr | co) as tso

LeanCats/Cats/examples/models/x86.cat

@@ -0,0 +1,5 @@
+let xppo = ((W*W) | (R*W) | (R*R)) & po
+let At = domain(rmw) | range(rmw)
+let implied = po;[At | F] | [At | F];po
+acyclic (implied | xppo | rfe | fr | co) as tso
+acyclic (po_loc | rf | fr | co) as uniproc

LeanCats/Data.lean

@@ -72,10 +72,9 @@ structure Events where
   (B : Set Event)
   (F : Set Event)
   (RMW : Set Event)
-  (M : Set Event)
 
 @[simp] def Events.all (evts : Events) :=
-  evts.IW ∪ evts.R ∪ evts.W ∪ evts.B ∪ evts.F ∪ evts.RMW ∪ evts.M
+  evts.IW ∪ evts.R ∪ evts.W ∪ evts.B ∪ evts.F ∪ evts.RMW
 
 instance : Membership Event Events where
   mem := fun es e => e ∈ es.all

LeanCats/Linux/CoRR_poonceonce_Once.lean

@@ -29,10 +29,10 @@ abbrev x := 0
 @[simp] abbrev p1r0 : Data.Event :=
   Data.Event.mk 2 1 rOpX1 ⟨lkmm.Accesses, lkmm.Accesses.ONCE'⟩
 @[simp] abbrev p1r1 : Data.Event :=
-  Data.Event.mk 3 2 rOpX0 ⟨lkmm.Accesses, lkmm.Accesses.ONCE'⟩
+  Data.Event.mk 3 1 rOpX0 ⟨lkmm.Accesses, lkmm.Accesses.ONCE'⟩
 
 @[simp] abbrev corr_evts : Data.Events :=
-  Data.Events.mk {initWx} {p1r0, p1r1} {initWx, p0wX} {} {} {} {}
+  Data.Events.mk {initWx} {p1r0, p1r1} {initWx, p0wX} {} {} {}
 
 @[simp] def corr_co : SetRel Event Event := {(initWx, p0wX)}
 @[simp] def corr_po : SetRel Event Event := {(p1r0, p1r1)}
@@ -65,17 +65,20 @@ Chosen rf edges: `p0wX -> p1r0` and `initWx -> p1r1`. -/
 
 def corr_test : CandidateExecution corr_evts :=
   {
+    evts := corr_evts
     po' := corr_po
     prePo := by candidateExecution_wf
     rf' := corr_rf
     rfInst := corr_rfInst
     co' := corr_co
+    rmw' := ∅
     preRMW := instWellformedRmwEmpty corr_evts
+    syncInF := by
+      intro e h
+      contradiction
     uniqueId := uniqueId_by_id corr_evts
     rfiPo := by
       candidateExecution_wf
-    coWR := by
-      candidateExecution_wf
   }
 
 theorem corr_FindCycle : ¬ (lkmm.coherence corr_evts corr_test) := by