Filtration by memory model

_CoqProject

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

eventstructure.v

@@ -106,6 +106,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 +514,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 +550,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 +563,32 @@ Proof.
   by move=> Cy /icf_cf/cf_consist2/(_ Cx Cy); exact/IHm.
 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].
+
+
 End ExecEventStructure.
 
 Canonical es_eqMixin disp E := EqMixin (@eqesP disp E).

memory_model.v

@@ -0,0 +1,45 @@
+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.
+
+Definition ra_consist (es : cexec_event_struct):= 
+  all (fun x => x \notin t_closure (fwb es) x) (dom es).
+
+End MMConsist.

regmachine.v

@@ -135,6 +135,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).
@@ -218,21 +220,23 @@ 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 
-      (e, v) <- add_hole l pr;
-      [:: Config e  [fsfun c with fresh_id |-> (cont_st v, tid)]]
+      (e, v) <- add_hole ces l pr;
+      [:: 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

@@ -42,8 +42,6 @@ Local Open Scope ra_terms.
 Definition sfrel {T : eqType} (f : T -> seq T) : rel T :=
   [rel a b | a \in f b].
 
-
-
 Section Strictify.
 
 Context {T : eqType}.
@@ -361,3 +359,25 @@ End FinRTClosure.
 
 End FinClosure.
 
+Section Operations.
+
+Context {T : Type}.
+Variables (f g : T -> seq T) (p : pred T).
+
+Definition composition := 
+  fun x => do y <- g x; f y.
+
+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).
+
+
+

utilities.v

@@ -381,7 +381,7 @@ Qed.
 
 End ReflectConnectives.
 
-Notation "'do' i <- s ; E" := (flatten (map (fun i => E) s)) (at level 10, i pattern).
+Notation "'do' i <- s ; E" := (flatten (map (fun i => E) s)) (at level 100, i pattern).
 
 Section RelationOnSeq.