Commit 299978e2 authored by Dan Frumin's avatar Dan Frumin

Update the counter example

Thunk the FG/CG_increment functions at the point of initialization.
This allows us to avoid the use of lamsubst.
parent 45c61194
......@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris_logrel Require Export logrel.
From iris_logrel.examples Require Import lock.
Definition CG_increment : val := λ: "x" "l" <>,
Definition CG_increment : val := λ: "x" "l",
acquire "l";;
let: "n" := !"x" in
"x" <- #1 + "n";;
......@@ -14,17 +14,17 @@ Definition counter_read : val := λ: "x" <>, !"x".
Definition CG_counter : val := λ: <>,
let: "l" := newlock #() in
let: "x" := ref #0 in
(CG_increment "x" "l", counter_read "x").
((λ: <>, CG_increment "x" "l"), counter_read "x").
Definition FG_increment : val := λ: "v", rec: "inc" <> :=
Definition FG_increment : val := rec: "inc" "v" :=
let: "c" := !"v" in
if: CAS "v" "c" (#1 + "c")
then "c"
else "inc" #().
else "inc" "v".
Definition FG_counter : val := λ: <>,
let: "x" := ref #0 in
(FG_increment "x", counter_read "x").
((λ: <>, FG_increment "x"), counter_read "x").
Section CG_Counter.
Context `{logrelG Σ}.
......@@ -32,7 +32,7 @@ Section CG_Counter.
(* Coarse-grained increment *)
Lemma CG_increment_type Γ :
typed Γ CG_increment (TArrow (Tref TNat) (TArrow LockType (TArrow TUnit TNat))).
typed Γ CG_increment (TArrow (Tref TNat) (TArrow LockType TNat)).
Proof. solve_typed. Qed.
Hint Resolve CG_increment_type : typeable.
......@@ -42,11 +42,11 @@ Section CG_Counter.
(x ↦ₛ # n - l ↦ₛ #false -
(x ↦ₛ # (S n) - l ↦ₛ #false -
({E1,E2;Δ;Γ} t log fill K #n : τ)) -
{E1,E2;Δ;Γ} t log fill K ((CG_increment $/ (LitV (Loc x)) $/ LitV (Loc l)) #()) : τ)%I.
{E1,E2;Δ;Γ} t log fill K (CG_increment #x #l) : τ)%I.
Proof.
iIntros (?) "Hx Hl Hlog".
unfold CG_increment. unlock. simpl_subst/=.
rel_seq_r.
repeat rel_rec_r.
rel_apply_r (bin_log_related_acquire_r with "Hl"); eauto.
iIntros "Hl".
rel_rec_r.
......@@ -87,7 +87,7 @@ Section CG_Counter.
(* Fine-grained increment *)
Lemma FG_increment_type Γ :
typed Γ FG_increment (TArrow (Tref TNat) (TArrow TUnit TNat)).
typed Γ FG_increment (TArrow (Tref TNat) TNat).
Proof. solve_typed. Qed.
Hint Resolve FG_increment_type : typeable.
......@@ -97,7 +97,7 @@ Section CG_Counter.
(x ↦ₛ # n -
(x ↦ₛ #(S n) -
{E1,E2;Δ;Γ} t log fill K #n : τ) -
{E1,E2;Δ;Γ} t log fill K ((FG_increment $/ (LitV (Loc x))) #()) : τ)%I.
{E1,E2;Δ;Γ} t log fill K (FG_increment #x) : τ)%I.
Proof.
iIntros (?) "Hx Hlog".
unlock FG_increment. simpl_subst/=.
......@@ -129,7 +129,7 @@ Section CG_Counter.
(( n : nat, x ↦ᵢ #n R n) ={E2,E1}= True)
( m, x ↦ᵢ # (S m) R m - P -
{E2,E1;Δ;Γ} fill K #m log t : τ))
- ({E1;Δ;Γ} fill K ((FG_increment $/ LitV (Loc x)) #()) log t : τ).
- ({E1;Δ;Γ} fill K (FG_increment #x) log t : τ).
Proof.
iIntros "HP #H".
iLöb as "IH".
......@@ -187,22 +187,9 @@ Section CG_Counter.
Lemma FG_CG_increment_refinement l cnt cnt' Γ :
inv counterN (counter_inv l cnt cnt') -
{Δ;Γ} FG_increment #cnt log CG_increment #cnt' #l : TArrow TUnit TNat.
{Δ;Γ} FG_increment #cnt log CG_increment #cnt' #l : TNat.
Proof.
iIntros "#Hinv".
rel_rec_l.
unlock CG_increment.
do 2 rel_rec_r.
replace (λ: <>, acquire #l;; let: "n" := ! #cnt' in #cnt' <- #1 + "n";; release #l;; "n")%E
with (CG_increment $/ LitV (Loc cnt') $/ LitV (Loc l))%E; last first.
{ unlock CG_increment. by simpl_subst/=. }
iApply bin_log_related_arrow_val.
{ unfold FG_increment. unlock; simpl_subst. reflexivity. }
{ unfold CG_increment. unlock; simpl_subst. reflexivity. }
{ unfold FG_increment. unlock; simpl_subst/=. solve_closed. (* TODO: add a clause to the reflection mechanism that reifies a [lambdasubst] expression as a closed one *) }
{ unfold CG_increment. unlock; simpl_subst/=. solve_closed. }
iAlways. iIntros (v v') "[% %]"; simplify_eq/=.
rel_apply_l
(bin_log_FG_increment_logatomic
(fun n => (l ↦ₛ #false) cnt' ↦ₛ #n)%I
......@@ -279,7 +266,9 @@ Section CG_Counter.
iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.
iApply bin_log_related_pair.
- iApply (FG_CG_increment_refinement with "Hinv").
- iApply bin_log_related_arrow; eauto.
iAlways. iIntros (??) "_". rel_seq_l; rel_seq_r.
iApply (FG_CG_increment_refinement with "Hinv").
- iApply (counter_read_refinement with "Hinv").
Qed.
End CG_Counter.
......
......@@ -16,7 +16,7 @@ Definition nameGen1 : val :=
Definition nameGen2 : expr :=
let: "x" := ref #0 in
Pack (λ: <>, FG_increment "x" #();; !"x"
Pack (λ: <>, FG_increment "x";; !"x"
,λ: "y" "z", "y" = "z").
Lemma nameGen1_typed Γ :
......@@ -39,7 +39,6 @@ Proof.
econstructor. cbn.
econstructor. cbn. solve_typed.
econstructor; eauto; solve_typed.
econstructor; eauto; solve_typed.
Qed.
Hint Resolve nameGen2_typed : typeable.
......@@ -83,7 +82,6 @@ Section namegen_refinement.
rel_alloc_l_atomic.
iInv N as (n L) "(HB & Hc & HL)" "Hcl".
iModIntro. iNext. iIntros (l') "Hl'".
rel_rec_r.
rel_apply_r (bin_log_related_FG_increment_r with "Hc").
{ solve_ndisj. }
iIntros "Hc".
......
......@@ -13,7 +13,7 @@ Definition newlock : val :=
λ: <>, ((* owner *) ref #0, (* next *) ref #0).
Definition acquire : val := λ: "lk",
let: "n" := FG_increment (Snd "lk") #() in
let: "n" := FG_increment (Snd "lk") in
wait_loop "n" "lk".
Definition wkincr : val := λ: "l",
......@@ -35,7 +35,6 @@ Proof.
econstructor; cbn; solve_typed.
econstructor; cbn; solve_typed.
econstructor; cbn; solve_typed.
econstructor; cbn; solve_typed.
Qed.
Hint Resolve acquire_type : typeable.
......@@ -314,8 +313,6 @@ Section refinement.
iIntros "HP #H".
rewrite /acquire. unlock. simpl.
rel_rec_l. rel_proj_l.
rel_bind_l ((FG_increment #ln) #())%E.
rel_rec_l.
rel_apply_l (bin_log_FG_increment_logatomic _ (fun n : nat => o : nat, lo ↦ᵢ #o issuedTickets γ n R o)%I P%I with "HP").
iAlways.
iPoseProof "H" as "H2".
......@@ -410,8 +407,6 @@ Section refinement.
iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq.
rel_let_l. repeat rel_proj_l.
(* rel_rec_l. (* TODO: cannot find the reduct *) *)
rel_bind_l (FG_increment _ #()).
rel_rec_l.
rel_apply_l (bin_log_FG_increment_logatomic _ (issuedTickets γ)%I True%I); first done.
iAlways.
openI N.
......
......@@ -360,7 +360,7 @@ Section refinement.
Definition τg := TArrow TUnit TUnit.
Definition τf := TArrow τg TUnit.
Definition p : val := λ: "g", let: "c" := ref #0 in
(λ: <>, FG_increment "c" #();; "g" #(), λ: <>, !"c").
(λ: <>, FG_increment "c";; "g" #(), λ: <>, !"c").
(** The idea for the invariant is that we have to states:
a) c1 = n, c2 = n
b) c1 = n+1, c2 = n
......@@ -378,16 +378,15 @@ Section refinement.
inv shootN (i6 c1 c2 γ γ') -
τg Δ (g1, g2) -
{Δ;Γ}
(FG_increment #c1 #() ;; g1 #())
(FG_increment #c1;; g1 #())
log
(FG_increment #c2 #() ;; g2 #()) : TUnit.
(FG_increment #c2;; g2 #()) : TUnit.
Proof.
iIntros "#Hinv #Hg".
iApply (bin_log_related_seq _ TRV _ _ _ _ _ _ (TVar 0)); auto; last first.
{ iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit).
iApply bin_log_related_val; eauto using to_of_val.
iApply bin_log_related_unit. }
rel_rec_l.
rel_apply_l (bin_log_FG_increment_logatomic _
(fun (n : nat) => (c2 ↦ₛ #n pending γ) (c2 ↦ₛ #(n-1) shot γ own γ' (Excl ()) 1 n))%I True%I); first done.
iAlways.
......@@ -404,7 +403,6 @@ Section refinement.
iFrame. }
{ iIntros (m) "[Hc1 Hc] _".
iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]";
rel_rec_r;
(rel_apply_r (bin_log_related_FG_increment_r with "Hc2"); first solve_ndisj);
iIntros "Hc2".
- iMod ("Hcl" with "[-]") as "_".
......@@ -428,7 +426,6 @@ Section refinement.
iFrame. }
{ iIntros (m) "[Hc1 Hc] _".
iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]";
rel_rec_r;
(rel_apply_r (bin_log_related_FG_increment_r with "Hc2"); first solve_ndisj);
iIntros "Hc2".
- iMod ("Hcl" with "[-]") as "_".
......@@ -445,9 +442,9 @@ Section refinement.
inv shootN (i6 c1 c2 γ γ') -
τg Δ (g1, g2) -
{Δ;Γ}
(λ: <>, FG_increment #c1 #() ;; g1 #())
(λ: <>, FG_increment #c1;; g1 #())
log
(λ: <>, FG_increment #c2 #() ;; g2 #()) : τg.
(λ: <>, FG_increment #c2;; g2 #()) : τg.
Proof.
iIntros "#Hinv #Hg".
iApply bin_log_related_arrow_val; auto.
......@@ -478,10 +475,10 @@ Section refinement.
c2 ↦ₛ #(m - 1) shot γ own γ' (Excl ()) 1 m) -
own γ' (Excl ()) -
{ shootN,;Δ;Γ}
(g1 #() ;; f'1 (λ: <>, (FG_increment #c1) #() ;; g1 #()) ;; #() ;; ! #c1)
(g1 #() ;; f'1 (λ: <>, (FG_increment #c1);; g1 #()) ;; #() ;; ! #c1)
log
(g2 #() ;;
f'2 (λ: <>, (FG_increment #c2) #() ;; g2 #()) ;; (#() ;; ! #c2) + #1) : TNat.
f'2 (λ: <>, (FG_increment #c2);; g2 #()) ;; (#() ;; ! #c2) + #1) : TNat.
Proof.
iIntros "#Hinv #Hg #Hf Hcl Hc1 Hc2 Ht".
iDestruct "Hc2" as "[(Hc2 & Hp) | (Hc2 & Hs & Ht'2 & %)]"; last first.
......@@ -555,7 +552,6 @@ Section refinement.
iApply bin_log_related_val; eauto using to_of_val.
by iApply profiled_g'. }
rel_seq_l.
rel_bind_l (FG_increment _). rel_rec_l.
rel_apply_l (bin_log_FG_increment_logatomic _
(fun (n : nat) => (c2 ↦ₛ #n pending γ) (c2 ↦ₛ #(n-1) shot γ own γ' (Excl ()) 1 n))%I with "Ht'").
iAlways.
......
......@@ -54,7 +54,7 @@ Section liftings.
(fun (n : nat) => x ↦ᵢ #n)%I
(fun (n : nat) (v : val) => v = #n x ↦ᵢ #(S n))%I
E2 E1
((FG_increment $/ LitV (Loc x)) #())
(FG_increment #x)
Δ Γ.
Proof.
iIntros (K t τ R2 R1) "[HR2 #Hlog]".
......@@ -107,51 +107,4 @@ Section liftings.
iApply "Hm". by iFrame.
Qed.
(* Lemma LA_hoare {A : Type} α (e : expr) β E1 E2 Δ Γ : *)
(* atomic_logrel α β E2 E1 e Δ Γ - *)
(* ( (x : A), lhs_ht (α x) e (β x) E1 Δ Γ). *)
(* Proof. *)
(* rewrite /atomic_logrel /lhs_ht. *)
(* iIntros "#HLA" (x K t τ). *)
(* iSpecialize ("HLA" $! K t τ True%I (fun _ => True)%I). *)
(* iAlways. iIntros "Hα Hv". *)
(* iApply "HLA". *)
(* iSplitR; [done | iAlways]. *)
(* Increment refinement using the log atomic triple *)
Lemma FG_CG_increment_refinement2 l cnt cnt' Γ Δ :
inv counterN (counter_inv l cnt cnt') -
{Δ;Γ} FG_increment $/ LitV (Loc cnt) log CG_increment $/ LitV (Loc cnt') $/ LitV (Loc l) : TArrow TUnit TNat.
Proof.
iIntros "#Hinv".
iApply bin_log_related_arrow_val.
{ unfold FG_increment. unlock; simpl_subst. reflexivity. }
{ unfold CG_increment. unlock; simpl_subst. reflexivity. }
{ unfold FG_increment. unlock; simpl_subst/=. solve_closed. (* TODO: add a clause to the reflection mechanism that reifies a [lambdasubst] expression as a closed one *) }
{ unfold CG_increment. unlock; simpl_subst/=. solve_closed. }
iAlways. iIntros (v v') "[% %]"; simplify_eq/=.
pose (F := (fun (n : nat) => (l ↦ₛ #false) cnt' ↦ₛ #n)%I).
iPoseProof (counter_atomic cnt ( counterN) Δ Γ
$! [] _ _ True%I F)
as "Hrule /=".
iApply "Hrule". iSplitR; first done. iAlways.
iInv counterN as ">Hcnt" "Hcl". iModIntro.
iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]".
iExists n. iFrame. clear n.
iSplit; cbv[F].
- iDestruct 1 as (n) "[Hcnt [Hl Hcnt']]".
iMod ("Hcl" with "[-]").
{ iNext. iExists _. iFrame. }
done.
- iIntros (m ?) "([% Hcnt] & [Hl Hcnt'] & _)"; simplify_eq/=.
iApply (bin_log_related_CG_increment_r _ _ [] with "[Hcnt'] [Hl]"); auto.
{ solve_ndisj. }
iIntros "Hcnt' Hl".
iMod ("Hcl" with "[-]").
{ iNext. iExists _. iFrame. }
simpl.
by iApply bin_log_related_nat.
Qed.
End liftings.
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