feat: prepare for RA consistency

Author: volodeyka

eventstructure.v

@@ -1,5 +1,5 @@
 From Coq Require Import Relations Relation_Operators.
-From RelationAlgebra Require Import lattice rel kat_tac.
+From RelationAlgebra Require Import lattice monoid rel kat_tac rel.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq path.
 From mathcomp Require Import eqtype choice order finmap fintype.
 From event_struct Require Import utilities relations wftype ident.
@@ -38,6 +38,7 @@ From event_struct Require Import utilities relations wftype ident.
 
 Import Order.LTheory.
 Open Scope order_scope.
+Local Open Scope ra_terms.
 Import WfClosure.
 
 Set Implicit Arguments.
@@ -567,26 +568,70 @@ Qed.
 (*     Writes-Before relation                                                *)
 (* ************************************************************************* *)
 
-Definition sca_suffix : E -> seq E := suffix (fica_lt).
-
-Definition contr_loc f : E -> seq E := 
-  fun e => (f ∘ (same_loc (lab e) \o lab)ᶠ) e.
-
-Definition contr_wrire f : E -> seq E := 
-  (is_write \o lab)ᶠ ∘ f ∘ (is_write \o lab)ᶠ.
-
-Definition frf_inv : E -> seq E := 
-  fun e => [seq x <- dom | frf x == e].
-
-(* wb := [W] ; (po ∪ rf)⁺ |loc ; [W] ∪ [W]; (po ∪ rf)⁺ ; rf⁻ ; [W] \ id *)
-
-Definition fwb : {fsfun E -> seq E with [::]} := 
-  [fsfun x in (seq_fset tt dom) => 
-    (
-      contr_wrire (contr_loc sca_suffix) 
-      ∪
-      strictify (contr_wrire (frf_inv ∘ (contr_loc sca_suffix)))
-    ) x].
+Definition sca : hrel E E := (ca : hrel E E) ∩ (fun x y => x <> y).
+
+Definition rf_inv : hrel E E := fun x y => frf x = y.
+
+Definition wb1 : hrel E E := fun e1 e2 =>
+  (
+    ((same_loc (lab e1) (lab e2)) *
+    (is_write (lab e1))) * 
+    ((is_write (lab e2)) *
+    ((sca e1 e2)))
+  )%type.
+
+Definition wb2 : hrel E E := fun e1 e2 =>
+  (
+    ((same_loc (lab e1) (lab e2)) *
+    (is_write (lab e1))) * 
+    ((is_write (lab e2)) *
+    (((hrel_dot _ _ _ sca rf_inv) e1 e2) * (e1 <> e2)))
+  )%type.
+
+(* wb := [W] ; (po ∪ rf)⁺ |loc ; [W] ∪ [W]; (po ∪ rf)⁺ |loc ; rf⁻ ; [W] \ id *)
+
+Definition wb := wb1 ⊔ wb2.
+
+Definition rwb1 e1 e2 := 
+  (
+    ((same_loc (lab e1) (lab e2)) *
+    (is_read (lab e1))) * 
+    ((is_read (lab e2)) *
+    ((frf e1) <> (frf e2))) *
+    (sca (frf e1) e2)
+  )%type.
+
+Definition rwb2 e1 e2 := 
+  (
+    ((same_loc (lab e1) (lab e2)) *
+    (is_read (lab e1))) * 
+    ((is_read (lab e2)) *
+    ((wb1 ⋅ sca) (frf e1) e2))
+  )%type.
+
+Definition rwb : hrel E E := rwb1 ⊔ rwb2.
+
+Lemma wb_rbw : 
+  (exists x, wb^* x x) <->
+  exists x, rwb^* x x.
+Proof. Admitted.
+
+Definition frwb : {fsfun E -> seq E with [::]}. Admitted.
+
+Lemma frwbP e1 e2: 
+  reflect (rwb e1 e2) (e2 \in frwb e1).
+Proof. Admitted.
+
+Definition seq_contr (f : E -> seq E) (xs : seq E): {fsfun E -> seq E with [::]} :=
+  [fsfun x in seq_fset tt dom => [seq y <- f x | y \in xs]] .
+
+Export FinClosure.
+
+Definition fwb_cf (rs : seq E) := 
+  if rs is r :: _ then
+    (t_closure (seq_contr frwb rs) r r) ||
+    (~~ allrel (fun e1 e2 => ~~ e1 # e2) rs rs)
+  else false.
 
 
 End ExecEventStructure.

memory_model.v

@@ -39,7 +39,4 @@ End GeneralDef.
 
 Export FinClosure.
 
-Definition ra_consist (es : cexec_event_struct):= 
-  all (fun x => x \notin t_closure (fwb es) x) (dom es).
-
 End MMConsist.

regmachine.v

@@ -238,14 +238,9 @@ Definition eval_step (c : config) pr : seq config :=
   let: tid             := if pr \in dom ces then tid else fresh_tid c in
   let: (l, cont_st)    := thrd_sem (nth empty_prog prog tid) conf in
     if l is Some l then do 
-<<<<<<< HEAD
-      (e, v) <- add_hole ces l pr;
-      [:: Config e  [fsfun c with (fresh_seq (dom ces)) |-> (cont_st v, tid)]]
-=======
-      ev <- add_hole l pr : M _;
+      ev <- add_hole ces l pr : M _;
       let '(e, v) := ev in
-        [:: Config e  [fsfun c with fresh_id |-> (cont_st v, tid)]]
->>>>>>> 01e861d77835d84e8e68fa729a27cee3c3d06ebb
+        [:: Config e  [fsfun c with (fresh_seq (dom ces)) |-> (cont_st v, tid)]]
     else
       [:: Config ces [fsfun c with pr |-> (cont_st inh, tid)]].
 

relations.v

@@ -2,6 +2,7 @@ From Coq Require Import Relations Relation_Operators.
 From RelationAlgebra Require Import lattice monoid rel kat_tac.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype seq order choice.
 From mathcomp Require Import finmap fingraph fintype finfun ssrnat path.
+From monae Require Import hierarchy monad_model.
 From Equations Require Import Equations.
 From event_struct Require Import utilities wftype monad.
 
@@ -38,6 +39,9 @@ Set Equations Transparent.
 Import Order.LTheory.
 Local Open Scope order_scope.
 Local Open Scope ra_terms.
+Open Scope monae.
+
+Local Notation M := ModelMonad.ListMonad.t.
 
 Definition sfrel {T : eqType} (f : T -> seq T) : rel T :=
   [rel a b | a \in f b].
@@ -362,10 +366,9 @@ End FinClosure.
 Section Operations.
 
 Context {T : Type}.
-Variables (f g : T -> seq T) (p : pred T).
+Variables (f g : T -> M T) (p : pred T).
 
-Definition composition := 
-  fun x => do y <- g x; f y.
+Definition composition := g >=> f.
 
 Definition fun_of_pred := 
   fun x => if p x then [:: x] else [::].
@@ -375,9 +378,9 @@ Definition funion :=
 
 End Operations.
 
-Notation "p 'ᶠ'" := (fun_of_pred p) (at level 10).
+(*Notation "p 'ᶠ'" := (fun_of_pred p) (at level 10).
 Notation "f ∘ g" := (composition f g) (at level 100, right associativity).
-Notation "f ∪ g" := (funion f g) (at level 100).
+Notation "f ∪ g" := (funion f g) (at level 100).*)
 
 
 

utilities.v

@@ -381,11 +381,6 @@ Qed.
 
 End ReflectConnectives.
 
-<<<<<<< HEAD
-Notation "'do' i <- s ; E" := (flatten (map (fun i => E) s)) (at level 100, i pattern).
-
-=======
->>>>>>> 01e861d77835d84e8e68fa729a27cee3c3d06ebb
 Section RelationOnSeq.
 
 Lemma rfoldl {A B C D} (r : A -> C -> bool) (r' : B -> D -> bool)