Commit 14a91e2e authored by Hai Dang's avatar Hai Dang

fix TC divergence in lambda-rust-weak; add hint mode

parent d76571ee
......@@ -10,6 +10,7 @@ Class LocFacts (loc: Type) := {
loc_eqdec :> EqDecision loc;
loc_count :> Countable loc;
}.
Hint Mode LocFacts ! : typeclass_instances.
Class Shift (loc: Type) := {
shift : loc Z loc;
......@@ -17,20 +18,24 @@ Class Shift (loc: Type) := {
shift_nat_assoc l (n1 n2: nat) : shift (shift l n1) n2 = shift l (n1 + n2)%nat;
shift_0 l : shift l 0%nat = l;
}.
Hint Mode Shift ! : typeclass_instances.
Infix ">>" := shift (at level 50, left associativity) : stdpp_scope.
Notation "(>>)" := shift (only parsing) : stdpp_scope.
Notation "( l >>)" := (shift l) (only parsing) : stdpp_scope.
Arguments shift : simpl never.
Class StateFacts `{LocFacts loc} (state : Type):= {
Class StateFacts `{LocFacts loc} (state: Type) := {
state_dom :> Dom state (gset loc);
state_wf :> Wellformed state;
state_dealloc : state gset loc;
state_dealloc_sub σ : state_dealloc σ dom (gset loc) σ;
}.
Arguments StateFacts _ {_} _.
(* Hint Mode StateFacts + + ! : typeclass_instances. *)
Class Allocator (loc state: Type) `{StateFacts loc state} `{Shift loc} := {
Class Allocator `{StateFacts loc state} `{!Shift loc} := {
alloc : state nat loc Prop;
dealloc : state nat loc Prop;
alloc_add_fresh σ l n:
......@@ -41,6 +46,7 @@ Class Allocator (loc state: Type) `{StateFacts loc state} `{Shift loc} := {
(n' : nat), n' < n
l >> n' (dom (gset _) σ state_dealloc σ);
}.
Arguments Allocator {_ _} _ {_ _}.
Arguments alloc {_ _ _ _ _ _}.
Arguments dealloc {_ _ _ _ _ _}.
......@@ -73,7 +79,7 @@ Proof.
Qed.
Section LocPos.
Context `{@StateFacts positive _ state}.
Context `{!StateFacts positive state}.
Implicit Types (σ : state) (l : positive).
......@@ -106,7 +112,8 @@ Section LocPos.
- apply elem_of_cons in InL as [?|InL]; first by (subst max; lia).
assert (HS := StronglySorted_merge_sort Pos.ge (elements (dom (gset positive) σ))).
rewrite HEq in HS.
inversion HS. subst. rewrite -> Forall_forall in H3. apply H3 in InL.
inversion HS as [|?? SS FA]. subst.
rewrite -> Forall_forall in FA. apply FA in InL.
apply Pos.ge_le in InL. by apply Pos.lt_succ_r.
Qed.
......@@ -129,13 +136,14 @@ Section LocPos.
End LocPos.
Program Instance pos_allocator `{@StateFacts positive _ state}: Allocator positive state :=
Program Instance pos_allocator `{!StateFacts positive state}
: Allocator state :=
{| alloc := pos_alloc;
dealloc := pos_dealloc; |}.
Next Obligation. intros. inversion H0. by apply NEW. Qed.
Next Obligation. intros ????? ALL. inversion ALL. by apply NEW. Qed.
Next Obligation.
intros. inversion H0. subst n. apply Nat.lt_1_r in H1.
subst n'. by apply ALLOC.
intros ????? DEL ? Lt. inversion DEL. subst. apply Nat.lt_1_r in Lt. subst.
by apply ALLOC.
Qed.
(** Locations as blocks *)
......@@ -152,7 +160,8 @@ Next Obligation. move => ???. inversion 1. lia. Defined.
Next Obligation. intros. simpl. f_equal. lia. Defined.
Next Obligation. intros []. f_equal. simpl. lia. Defined.
Lemma shift_lblock_assoc (l : lblock) n n':
Implicit Type (l : lblock).
Lemma shift_lblock_assoc l n n':
(l >> n) >> n' = l >> (n+n').
Proof. rewrite /shift /lblock_shift /=. f_equal. lia. Qed.
......@@ -166,9 +175,9 @@ Lemma shift_lblock l n : (l >> n).1 = l.1.
Proof. done. Qed.
Section LocBlock.
Context `{@StateFacts lblock _ state}.
Context `{!StateFacts lblock state}.
Implicit Types (σ : state) (l : lblock).
Implicit Types (σ : state).
Inductive lblock_alloc σ n l : Prop :=
| LBlockAlloc
......@@ -208,7 +217,7 @@ Section LocBlock.
End LocBlock.
Program Instance lblock_allocator `{@StateFacts lblock _ state} : Allocator lblock state :=
Program Instance lblock_allocator `{!StateFacts lblock state} : Allocator state :=
{| alloc := lblock_alloc;
dealloc := lblock_dealloc; |}.
Next Obligation. intros ????? Hl ??. inversion Hl. by apply MAX. Qed.
......
......@@ -3,9 +3,11 @@ From orc11 Require Export view value.
Section Memory.
Context `{LocFacts loc} `{CVAL: Countable VAL}.
Context `{!LocFacts loc} `{CVAL: Countable VAL}.
Notation val := (@val VAL).
Notation view := (view loc).
Implicit Types (V: view).
(** Base messages do not have loc and to fields *)
Record baseMessage :=
......@@ -51,7 +53,7 @@ Section Memory.
defined as maps from time to base messages *)
Notation cell := (gmap time baseMessage) (only parsing).
Implicit Types (t: time) (V: view) (l: loc) (m: baseMessage) (C: cell).
Implicit Types (t: time) (l: loc) (m: baseMessage) (C: cell).
(* Extension on Cell that ONLY extends views *)
(* This is different from the cell extension that adds new messages *)
......@@ -738,7 +740,7 @@ Section Memory.
alloc_inv_max_dealloc : l, cell_dealloc_inv (M !!c l);
}.
Global Program Instance memory_state : StateFacts memory :=
Global Program Instance memory_state : StateFacts loc memory :=
{| state_dealloc := mem_deallocated; |}.
Next Obligation. intros. by apply mem_deallocated_sub. Defined.
......@@ -1247,7 +1249,7 @@ Section Memory.
Qed.
Section Allocation.
Context `{Shift loc} `{!Allocator loc memory}.
Context `{!Shift loc} `{!Allocator memory}.
(** Allocation *)
Inductive memory_alloc
(n : nat) l 𝑚s M1 M2 : Prop :=
......@@ -1467,7 +1469,7 @@ Section Memory.
(** Cell lists ------------------------------------------------------------ *)
Section cell_lists.
Context `{Shift loc}.
Context `{!Shift loc}.
Definition cell_cons l (n: nat) (M : memory) (Cl : list cell) : list cell :=
M !!c (l >> n) :: Cl.
......@@ -1586,7 +1588,7 @@ Section Memory.
by rewrite (lookup_seq_ge _ _ _ Ge) /=.
Qed.
Lemma memory_alloc_cell_list `{!Allocator loc memory} n l 𝑚s M1 M2
Lemma memory_alloc_cell_list `{!Allocator memory} n l 𝑚s M1 M2
(ALLOC: memory_alloc n l 𝑚s M1 M2):
(n': nat) C,
(cell_list l n M2) !! n' = Some C
......@@ -1613,7 +1615,7 @@ Section Memory.
by eexists.
Qed.
Lemma memory_alloc_cell_list_map `{!Allocator loc memory} n l 𝑚s M1 M2
Lemma memory_alloc_cell_list_map `{!Allocator memory} n l 𝑚s M1 M2
(ALLOC: memory_alloc n l 𝑚s M1 M2):
(cell_list l n M2) = fmap (λ 𝑚, {[𝑚.(mto) := 𝑚.(mbase)]}) 𝑚s.
Proof.
......@@ -1841,7 +1843,7 @@ Section Memory.
lookup_empty // in IN.
Qed.
Lemma mem_cut_memory_alloc `{!Shift loc} `{!Allocator loc memory} l n M1 M2 𝑚s 𝓝
Lemma mem_cut_memory_alloc `{!Shift loc} `{!Allocator memory} l n M1 M2 𝑚s 𝓝
(ALLOC: memory_alloc n l 𝑚s M1 M2) :
mem_cut M2 (alloc_new_na 𝓝 𝑚s) = alloc_new_mem (mem_cut M1 𝓝) 𝑚s.
Proof.
......@@ -1850,7 +1852,7 @@ Section Memory.
- by eapply memory_alloc_fresh_2.
Qed.
Lemma mem_cut_memory_dealloc `{!Shift loc} `{!Allocator loc memory} l n M1 M2 𝑚s 𝓝
Lemma mem_cut_memory_dealloc `{!Shift loc} `{!Allocator memory} l n M1 M2 𝑚s 𝓝
(DEALLOC: memory_dealloc n l 𝑚s M1 M2) :
mem_cut M2 (alloc_new_na 𝓝 𝑚s) = alloc_new_mem (mem_cut M1 𝓝) 𝑚s.
Proof.
......
......@@ -3,7 +3,7 @@ From orc11 Require Export thread.
Set Default Proof Using "Type".
Section Wellformedness.
Context `{LocFacts loc} `{CVAL: Countable VAL} `{Shift loc} `{!Allocator loc (memory loc VAL)}.
Context `{!LocFacts loc} `{CVAL: Countable VAL} `{!Shift loc} `{!Allocator (memory loc VAL)}.
Notation memory := (memory loc VAL).
Notation message := (message loc VAL).
......@@ -11,6 +11,8 @@ Section Wellformedness.
Notation global := (@global loc _ VAL).
Notation config := (@config loc _ VAL).
Notation val := (@val VAL).
Notation view := (view loc).
Notation threadView := (threadView loc).
Implicit Type (𝑚: message) (M: memory) (𝓝: view) (𝓥: threadView)
(l: loc) (G: global) (c: config).
......@@ -484,12 +486,13 @@ End Wellformedness.
Section AllocSteps.
Context `{LocFacts loc} `{CVAL: Countable VAL} `{Shift loc} `{!Allocator loc (memory loc VAL)}.
Context `{!LocFacts loc} `{CVAL: Countable VAL} `{!Shift loc} `{!Allocator (memory loc VAL)}.
Notation memory := (memory loc VAL).
Notation message := (message loc VAL).
Notation event := (event loc VAL).
Notation machine_step := (@machine_step _ _ VAL _ _).
Notation view := (@view loc _).
Implicit Type (𝑚: message) (M: memory) (𝓝: view).
......@@ -904,12 +907,14 @@ Section AllocSteps.
End AllocSteps.
Section Steps.
Context `{LocFacts loc} `{CVAL: Countable VAL} `{Shift loc} `{!Allocator loc (memory loc VAL)}.
Context `{!LocFacts loc} `{CVAL: Countable VAL} `{!Shift loc} `{!Allocator (memory loc VAL)}.
Notation memory := (memory loc VAL).
Notation message := (message loc VAL).
Notation event := (event loc VAL).
Notation machine_step := (@machine_step _ _ VAL _ _).
Notation view := (view loc).
Notation threadView := (threadView loc).
Implicit Types (M: memory) (𝑚: message).
......
......@@ -5,11 +5,13 @@ Set Default Proof Using "Type".
Section Thread.
Context `{!LocFacts loc} `{CVAL: Countable VAL} `{!Shift loc} `{!Allocator loc (memory loc VAL)}.
Context `{!LocFacts loc} `{CVAL: Countable VAL} `{!Shift loc} `{!Allocator (memory loc VAL)}.
Notation memory := (memory loc VAL).
Notation message := (message loc VAL).
Notation event := (event loc VAL).
Notation view := (view loc).
Notation threadView := (threadView loc).
Record global := mkGB {
sc: view;
......@@ -18,7 +20,8 @@ Section Thread.
}.
Record config := mkCFG { lc: threadView; gb : global; }.
Implicit Type (𝑚: message) (M: memory) (𝓝: view) (G: global) (c: config).
Implicit Type (𝑚: message) (M: memory) (𝓝: view) (G: global)
(c: config) (𝓥: threadView).
Definition dealloc_na_agree M 𝓝 :=
l t m, M !! (l, t) = Some m m.(mval) = DVal Some t 𝓝 !!w l.
......@@ -79,7 +82,7 @@ Section Thread.
(ALLOC: allocated 𝑚.(mloc) M1).
(* <𝓥,M> -{ W(l,v,o) }-> <𝓥',M'> *)
Inductive write_step 𝓥1 M1 𝑚 o V 𝓥2 M2: Prop :=
Inductive write_step 𝓥1 M1 𝑚 o V 𝓥2 M2: Prop :=
| WriteStep
(WRITE: memory_write M1 𝑚 M2)
(WVIEW : write_helper 𝓥1 o 𝑚.(mloc) 𝑚.(mto) V 𝑚.(mbase).(mrel) 𝓥2).
......
......@@ -4,9 +4,12 @@ From orc11 Require Export memory mem_order.
Set Default Proof Using "Type".
Section ThreadView.
Context `{LocFacts loc} `{CVAL: Countable VAL}.
Context `{!LocFacts loc} `{CVAL: Countable VAL}.
Notation view := (view loc).
Notation view_Lat := (view_Lat loc).
Implicit Types (V: view).
Global Instance all_gmap_sqsubseteq_decision (M : gmap loc view) (V: option view) :
Global Instance all_gmap_sqsubseteq_decision (M: gmap loc view) (V: option view) :
Decision ( l, M !! l V).
Proof.
assert (IFF : ( l, M !! l V) (Forall (λ lV', Some lV'.2 V) (map_to_list M))).
......@@ -18,7 +21,7 @@ Section ThreadView.
[left|right]; by rewrite IFF.
Qed.
Global Instance all_gmap_sqsubseteq_decision' (M : gmap loc view) (V:view) :
Global Instance all_gmap_sqsubseteq_decision' (M: gmap loc view) V :
Decision ( l V', M !! l = Some V' V V').
Proof.
assert (IFF : ( (l : loc) (V' : view), M !! l = Some V' V V')
......@@ -163,7 +166,7 @@ Section ThreadView.
Notation message := (message loc VAL).
Implicit Type (M: memory).
Record closed_tview' 𝓥 (M: memory) :=
Record closed_tview' 𝓥 M :=
{ closed_tview_rel: l, (𝓥.(rel) !! l) M;
closed_tview_frel: 𝓥.(frel) M;
closed_tview_cur: 𝓥.(cur) M;
......@@ -300,7 +303,7 @@ Section ThreadView.
(CLOSED: 𝓥 M) (CR: R M) (SOME: m, M !! (l, t) = Some m):
𝓥' M.
Proof.
inversion READ. clear H0.
inversion READ. subst.
have ?: {[l := [{ t,,,{[tr]} }] ]} M.
{ move => ??.
rewrite /view_lookup_write fmap_Some.
......@@ -527,3 +530,6 @@ Section ThreadView.
Qed.
End ThreadView.
Arguments threadView _ {_}.
Arguments tview_Lat _ {_}.
......@@ -72,11 +72,13 @@ Instance timeInfo_leibniz_eq : LeibnizEquiv timeInfo.
Proof. move => ?? //. Qed.
Section View.
Context `{LocFacts loc}.
Context `{!LocFacts loc}.
Definition view := gmap loc timeInfo.
Definition view_Lat := gmap_Lat loc timeInfo_Lat.
Implicit Types (V: view).
(* this is not canonical, as it overlaps [gmap_Lat]. This is to avoid TC divergence. *)
Canonical Structure view_Lat := gmap_Lat loc timeInfo_Lat.
Implicit Type (V: view).
Definition view_lookup_write: Lookup loc time view
:= fun l V => fmap twrite (V !! l).
......@@ -87,6 +89,9 @@ Section View.
Definition view_lookup_aread: Lookup loc time_ids view
:= fun l V => fmap taread (V !! l).
End View.
Arguments view _ {_}.
Arguments view_Lat _ {_}.
Notation "V !!w i" := (view_lookup_write i V) (at level 20) : stdpp_scope.
Notation "V !!aw i" := (view_lookup_awrite i V) (at level 20) : stdpp_scope.
......@@ -94,8 +99,8 @@ Notation "V !!ar i" := (view_lookup_aread i V) (at level 20) : stdpp_scope.
Notation "V !!nr i" := (view_lookup_nread i V) (at level 20) : stdpp_scope.
Section ViewLookup.
Context `{LocFacts loc}.
Implicit Types (V : view) (l : loc) (t: time).
Context `{!LocFacts loc}.
Implicit Types (V: view loc) (l : loc) (t: time).
Lemma view_lookup_w' V l o:
V !! l = o V !!w l = twrite <$> o.
......@@ -320,23 +325,22 @@ Tactic Notation "simplify_view":= repeat
cut g; first (rewrite (view_lookup_nr' V l o H); exact id)
end.
Section ViewLookup_more.
Context `{LocFacts loc}.
Lemma view_sqsubseteq (V1 V2 : view) (l : loc) :
V1 !! l V2 !! l
V1 !!w l V2 !!w l V1 !!aw l V2 !!aw l
V1 !!nr l V2 !!nr l V1 !!ar l V2 !!ar l.
Proof.
rewrite {1}/sqsubseteq /lat_sqsubseteq /= /option_sqsubseteq.
split.
- destruct (V1 !! l) as [[]|] eqn:Eq1;
destruct (V2 !! l) as [[]|] eqn:Eq2;
simplify_view; cbn; try done.
- destruct (V1 !! l) as [[]|] eqn:Eq1;
destruct (V2 !! l) as [[]|] eqn:Eq2;
simplify_view; cbn; try done. intuition.
Qed.
End ViewLookup_more.
Lemma view_sqsubseteq `{!LocFacts loc} (V1 V2 : view loc) (l : loc) :
V1 !! l V2 !! l
V1 !!w l V2 !!w l V1 !!aw l V2 !!aw l
V1 !!nr l V2 !!nr l V1 !!ar l V2 !!ar l.
Proof.
rewrite {1}/sqsubseteq /lat_sqsubseteq /= /option_sqsubseteq.
split.
- destruct (V1 !! l) as [[]|] eqn:Eq1;
destruct (V2 !! l) as [[]|] eqn:Eq2;
simplify_view; cbn; try done.
- destruct (V1 !! l) as [[]|] eqn:Eq1;
destruct (V2 !! l) as [[]|] eqn:Eq2;
simplify_view; cbn; try done. intuition.
Qed.
Instance twrite_sqsubseteq_proper: Proper (sqsubseteq ==> sqsubseteq) twrite.
Proof. solve_proper. Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment