Filtration by memory model

_CoqProject

@@ -21,3 +21,4 @@ prime_eventstruct.v
 eventstructure.v
 transitionsystem.v
 regmachine.v
+memory_model.v

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.
@@ -106,6 +107,8 @@ Notation "w << r" := (write_read_from w r) (at level 0).
 Lemma rf_thrdend w : w << ThreadEnd = false.
 Proof. by case: w. Qed.
 
+Definition same_loc l l' := lloc l == lloc l'.
+
 
 (* ************************************************************************* *)
 (*     Exec Event Structure                                                  *)
@@ -512,7 +515,7 @@ Lemma cfE e1 e2: e1 # e2 = cf_step e1 e2.
 Proof.
   apply/idP/idP; last by apply: cf_step_cf.
   case/cfP=> e1' [e2' [[]]].
-  case: (boolP (e1' == e1))=> [/eqP-> _|].
+  case: (boolP (e1' == e1))=> [/eqP-> _ |].
   - case: (boolP (e2' == e2))=> [/eqP->_->|]; first (apply/orP; by left).
     move/ca_step_last/[apply] => [[x /and3P[/cf_consistr H N + /icf_cf/H]]].
     rewrite lt_neqAle=> /andP[] *.
@@ -548,10 +551,10 @@ Proof.
   suff C: ~ m # (fpred m).
   case: (boolP (frf m == m))=> [/eqP fE|?].
   - rewrite cfE => /orP; rewrite orbb icfxx => [[]] //=.
-  rewrite fE; case: ifP=> [/eqP//|_]; case: ifP=>//= _; by rewrite orbF => /C.
+  rewrite fE; case: ifP=> [/eqP//| _]; case: ifP=>//= _; by rewrite orbF => /C.
   rewrite cfE icfxx orbb=> /hasP[? /(mem_subseq (filter_subseq _ _))] /=.
   by rewrite ?inE=> /orP[/eqP->|/eqP->/C]//; rewrite rff_consist.
-  move=> /cfP[x [y [[]]]]; case: (eqVneq x m)=> [-> _|].
+  move=> /cfP[x [y [[]]]]; case: (eqVneq x m)=> [-> _ |].
   - by move=> /ca_le L /and4P[_ /eqP<- _ /(le_lt_trans L)]; rewrite ltxx.
   move/ca_step_last=> /[apply] [[z /and3P[/[swap]]]].
   rewrite /ica !inE=> /pred2P[]-> Cx L.
@@ -561,6 +564,76 @@ Proof.
   by move=> Cy /icf_cf/cf_consist2/(_ Cx Cy); exact/IHm.
 Qed.
 
+(* ************************************************************************* *)
+(*     Writes-Before relation                                                *)
+(* ************************************************************************* *)
+
+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.
 
 Canonical es_eqMixin disp E := EqMixin (@eqesP disp E).

memory_model.v

@@ -0,0 +1,42 @@
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq.
+From mathcomp Require Import eqtype choice finfun finmap tuple.
+From event_struct Require Import utilities eventstructure inhtype relations.
+From event_struct Require Import transitionsystem ident regmachine.
+
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Section MMConsist.
+
+Context {V : inhType} {disp} {E : identType disp}.
+
+(*Notation n := (@n val).*)
+Notation exec_event_struct := (@fin_exec_event_struct V _ E).
+Notation cexec_event_struct := (@cexec_event_struct V _ E).
+
+Section GeneralDef.
+
+Variable mm_pred : pred cexec_event_struct.
+
+Inductive mm_config := MMConsist (c : config) of mm_pred (evstr c).
+
+Coercion config_of (mmc : mm_config) :=
+  let '(MMConsist c _) := mmc in c.
+
+Canonical config_subType := [subType for config_of].
+
+Lemma consist_inj : injective config_of.
+Proof. exact: val_inj. Qed.
+
+Variable pgm : parprog (V := V).
+
+Definition mm_eval_ster mmc pr : seq mm_config := 
+  pmap insub (eval_step pgm mmc pr).
+
+End GeneralDef.
+
+Export FinClosure.
+
+End MMConsist.

regmachine.v

@@ -140,6 +140,8 @@ Definition ltr_thrd_sem (l : option (@label V V)) pgm st1 st2 : bool :=
   | _, _                                     => false
   end.
 
+Section AddHole.
+
 Variable (es : cexec_event_struct).
 Notation ffpred   := (fpred es).
 Notation ffrf     := (frf es).
@@ -223,22 +225,24 @@ Definition add_hole
     end
   else [::].
 
+End AddHole.
+
 Variable prog : parprog.
 
 Definition fresh_tid (c : config) := 
   foldr maxn 0 [seq (snd x).+1 | x <- fgraph (fmap_of_fsfun c)].
 
 Definition eval_step (c : config) pr : seq config := 
-  let: Config es tmap := c in
-  let: (conf, tid)    := tmap pr in
-  let: tid            := if pr \in dom es then tid else fresh_tid c in
-  let: (l, cont_st)   := thrd_sem (nth empty_prog prog tid) conf in
+  let: Config ces tmap := c in
+  let: (conf, tid)     := tmap pr in
+  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 
-      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)]]
+        [:: Config e  [fsfun c with (fresh_seq (dom ces)) |-> (cont_st v, tid)]]
     else
-      [:: Config es [fsfun c with pr |-> (cont_st inh, tid)]].
+      [:: Config ces [fsfun c with pr |-> (cont_st inh, tid)]].
 
 End RegMachine.
 

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,12 +39,13 @@ 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].
 
-
-
 Section Strictify.
 
 Context {T : eqType}.
@@ -361,3 +363,24 @@ End FinRTClosure.
 
 End FinClosure.
 
+Section Operations.
+
+Context {T : Type}.
+Variables (f g : T -> M T) (p : pred T).
+
+Definition composition := g >=> f.
+
+Definition fun_of_pred := 
+  fun x => if p x then [:: x] else [::].
+
+Definition funion := 
+  fun x => f x ++ g x.
+
+End Operations.
+
+(*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).*)
+
+
+