From 0376b90176b423811804858d2e66494c6f9d2673 Mon Sep 17 00:00:00 2001 From: volodeyka Date: Thu, 1 Apr 2021 11:53:27 +0300 Subject: [PATCH 1/6] fix: do-notation level --- utilities.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/utilities.v b/utilities.v index 3cdeeb7b..2a25b15f 100644 --- a/utilities.v +++ b/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. From 0eb6fed09ece10999052ff47590515a5e8973b7c Mon Sep 17 00:00:00 2001 From: volodeyka Date: Thu, 1 Apr 2021 11:56:14 +0300 Subject: [PATCH 2/6] fix: variabels of eval_step --- regmachine.v | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/regmachine.v b/regmachine.v index 2ae7e368..e370e128 100644 --- a/regmachine.v +++ b/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. From 4fc3268d22a3436dc825d625e8e162bc2a5b1885 Mon Sep 17 00:00:00 2001 From: volodeyka Date: Thu, 1 Apr 2021 11:57:38 +0300 Subject: [PATCH 3/6] feat: add utilities for 'T -> seq T' function --- relations.v | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/relations.v b/relations.v index 38639140..dc157eac 100644 --- a/relations.v +++ b/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). + + + From af5819ffe286133a292999ea34781b77b88a3c42 Mon Sep 17 00:00:00 2001 From: volodeyka Date: Thu, 1 Apr 2021 11:59:30 +0300 Subject: [PATCH 4/6] feat: add writes-berofe relation --- eventstructure.v | 34 +++++++++++++++++++++++++++++++--- 1 file changed, 31 insertions(+), 3 deletions(-) diff --git a/eventstructure.v b/eventstructure.v index 72798878..4e81ef43 100644 --- a/eventstructure.v +++ b/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). From de88ae1c562e1e905e1af461be33b79fb398c16f Mon Sep 17 00:00:00 2001 From: volodeyka Date: Thu, 1 Apr 2021 12:11:15 +0300 Subject: [PATCH 5/6] feat: add filtration on memory model predicate --- _CoqProject | 1 + memory_model.v | 45 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 46 insertions(+) create mode 100644 memory_model.v diff --git a/_CoqProject b/_CoqProject index 33cb5f26..50fb8b64 100644 --- a/_CoqProject +++ b/_CoqProject @@ -20,3 +20,4 @@ prime_eventstruct.v eventstructure.v transitionsystem.v regmachine.v +memory_model.v diff --git a/memory_model.v b/memory_model.v new file mode 100644 index 00000000..69936c08 --- /dev/null +++ b/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. From a7f48271b98dd164ebef6ebc5a1ac984b600be78 Mon Sep 17 00:00:00 2001 From: volodeyka Date: Tue, 27 Apr 2021 19:32:48 +0300 Subject: [PATCH 6/6] feat: prepare for RA consistency --- eventstructure.v | 87 ++++++++++++++++++++++++++++++++++++------------ memory_model.v | 3 -- regmachine.v | 9 ++--- relations.v | 13 +++++--- utilities.v | 5 --- 5 files changed, 76 insertions(+), 41 deletions(-) diff --git a/eventstructure.v b/eventstructure.v index 4e81ef43..79582203 100644 --- a/eventstructure.v +++ b/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. diff --git a/memory_model.v b/memory_model.v index 69936c08..3b283bde 100644 --- a/memory_model.v +++ b/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. diff --git a/regmachine.v b/regmachine.v index 0621c890..ffcf85d2 100644 --- a/regmachine.v +++ b/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)]]. diff --git a/relations.v b/relations.v index fca64086..b8584195 100644 --- a/relations.v +++ b/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).*) diff --git a/utilities.v b/utilities.v index 45230e0c..9a089ae5 100644 --- a/utilities.v +++ b/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)