Commit 6017b1af authored by Dan Frumin's avatar Dan Frumin

Add some translation proofs

parent 91d112e1
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.heap_lang Require Import adequacy spin_lock assert par.
From iris.algebra Require Import frac.
From iris.base_logic.lib Require Import fractional.
From iris_c.lib Require Import mset flock.
From iris_c.lib Require Import mset flock locking_heap.
(* M A := ref (list loc) → Mutex → A *)
......@@ -42,10 +42,18 @@ Definition a_par : val := λ: "x" "y" "env" "l",
Definition amonadN := nroot .@ "amonad".
Section a_wp.
Context `{heapG Σ, flockG Σ, spawnG Σ}.
Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapG Σ}.
Definition env_inv `{heapG Σ} (env : val) : iProp Σ :=
( X, is_set_mut env X)%I.
(* X ⊆ σ^{-1}(L) *)
Definition correct_locks (X : gset val) (preσ : gset loc) : Prop :=
set_Forall (fun x => l : loc, x = #l l preσ) X.
Definition env_inv (env : val) : iProp Σ :=
( (X : gset val) (σ : gmap loc level),
is_set_mut env X
full_locking_heap σ
([ map] l _ σ, v', l {1/2} v')
correct_locks X (locked_locs σ))%I.
Definition awp (e : expr)
(R : iProp Σ) (Φ : val iProp Σ) : iProp Σ :=
......@@ -76,23 +84,6 @@ Section a_wp.
iIntros (w) "[Hwp Hunfl]". wp_let. by iApply "Hwp".
Qed.
Lemma awp_run (v : val) R Φ `{Timeless _ R} :
R - awp v R (λ w, R - Φ w) -
WP a_run v {{ Φ }}.
Proof.
iIntros "HR Hwp". rewrite /a_run /=. wp_let.
wp_bind (mset_create #()). iApply mset_create_spec; first done.
iNext. iIntros (env) "H". wp_let.
wp_apply (newlock_cancel_spec amonadN (env_inv env R)%I with "[H HR]");
first by iFrame; iExists .
iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd.
iApply (wp_wand with "[Hwp Hunfl]").
unfold awp. by iApply ("Hwp" with "Hlock").
iIntros (w) "[HΦ Hunfl]".
iApply "HΦ".
iMod (cancel_lock with "Hlock Hunfl") as "[HEnv HR]". done.
Qed.
Lemma awp_atomic (v : val) R Φ `{Timeless _ R} :
(R - R', Timeless R' R' awp v R' (λ w, R' - R Φ w)) -
awp (a_atomic v) R Φ.
......@@ -145,3 +136,43 @@ Section a_wp.
iApply ("HΦ" with "[$] [$]").
Qed.
End a_wp.
Section a_wp_run.
Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapPreG Σ}.
Lemma awp_run (v : val) R Φ `{Timeless _ R} :
R - ( `{locking_heapG Σ}, awp v R (λ w, R - Φ w)) -
WP a_run v {{ Φ }}.
Proof.
iIntros "HR Hwp". rewrite /a_run /=. wp_let.
wp_bind (mset_create #()). iApply mset_create_spec; first done.
iNext. iIntros (env) "Henv". wp_let.
iMod (locking_heap_init ) as (?) "Hσ".
wp_apply (newlock_cancel_spec amonadN (env_inv env R)%I with "[Henv Hσ $HR]").
{ iExists , . iFrame. eauto. }
iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd.
iApply (wp_wand with "[Hwp Hunfl]").
unfold awp. by iApply ("Hwp" with "Hlock").
iIntros (w) "[HΦ Hunfl]".
iApply "HΦ".
iMod (cancel_lock with "Hlock Hunfl") as "[HEnv HR]". done.
Qed.
End a_wp_run.
(* Definition locking_heapΣ : gFunctors := *)
(* #[heapΣ; GFunctor (auth.authR locking_heapUR)]. *)
(* Instance subG_locking_heapG {Σ} : subG locking_heapΣ Σ → locking_heapPreG Σ. *)
(* Proof. solve_inG. Qed. *)
(* Definition awp_adequacy Σ R s v σ φ : *)
(* (R -∗ (∀ `{locking_heapG Σ}, awp (of_val v) R (λ w, R -∗ ⌜φ w⌝)))%I → *)
(* adequate MaybeStuck (a_run v) σ φ. *)
(* (∀ `{heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}%I) → *)
(* Proof. *)
(* intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "". *)
(* iMod (gen_heap_init σ) as (?) "Hh". *)
(* iModIntro. iExists gen_heap_ctx. iFrame "Hh". *)
(* iApply (Hwp (HeapG _ _ _)). *)
(* Qed. *)
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac.
From iris.algebra Require Import frac auth.
From iris.base_logic.lib Require Import fractional.
From iris_c.lib Require Import mset flock.
From iris_c.lib Require Import locking_heap mset flock.
From iris_c.c_translation Require Import monad.
Definition a_alloc : val := λ: "x",
a_bind (λ: "v", a_atomic_env (λ: <>, ref "v")) "x".
Definition a_store : val := λ: "x1" "x2",
a_bind (λ: "vv",
......@@ -18,7 +20,7 @@ Definition a_store : val := λ: "x1" "x2",
Definition a_load : val := λ: "x",
a_bind (λ: "v",
a_atomic_env (λ: "env",
assert (mset_member "v" "env" = #false);;
assert: (mset_member "v" "env" = #false);;
!"v"
)
) "x".
......@@ -35,3 +37,84 @@ Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
(* The eta expansion is used to turn it into a value *)
Definition a_seq : val := λ: "env",
a_atomic_env (λ: "env", mset_clear "env") "env".
Notation "l ↦[ x ] v" := (mapsto l x v)
(at level 20, x at level 50, format "l ↦[ x ] v") : uPred_scope.
Notation "l ↦L v" := (l [LLvl] v)%I
(at level 20, format "l ↦L v") : uPred_scope.
Notation "l ↦U v" := (l [ULvl] v)%I
(at level 20, format "l ↦U v") : uPred_scope.
Notation "l ↦L -" := ( v, l L v)%I
(at level 20, format "l ↦L -") : uPred_scope.
Notation "l ↦U -" := ( v, l U v)%I
(at level 20, format "l ↦U -") : uPred_scope.
Section proofs.
Context `{locking_heapG Σ, heapG Σ, flockG Σ}.
Lemma a_load_spec R `{Timeless _ R} (l : loc) (v : val) Φ :
l U v -
(l U v - Φ v) -
awp (a_load (a_ret #l)) R Φ.
Proof.
unfold a_load. iIntros "Hv HΦ".
rewrite /awp /a_ret.
iIntros (γ π env lk) "#Hfl Hunfl".
Opaque acquire release.
repeat wp_rec.
wp_apply (acquire_cancel_spec with "[$]").
iIntros "(Hlkd & Henv & HR)".
wp_seq.
rewrite {2}/env_inv.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
iDestruct "Hlocks" as %Hlocks.
iDestruct (locked_locs_unlocked with "Hv Hσ") as %Hl.
assert (#l X).
{ unfold correct_locks in *. intros Hx. apply Hl.
destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
wp_let.
wp_apply wp_assert.
wp_apply (mset_member_spec #l env with "HX").
iIntros (w) "[Henv [[% %]|[% %]]]"; simplify_eq/=; first done.
wp_op. iSplit; eauto. iNext. wp_seq.
rewrite mapsto_eq /mapsto_def. iDestruct "Hv" as "[Hv Hl]". wp_load.
iCombine "Hv Hl" as "Hv".
wp_seq.
wp_apply (release_cancel_spec with "[$Hfl $Hlkd $HR Hσ Hls Henv]").
{ iExists X,σ. by iFrame. }
iIntros "Hunfl". wp_seq. iFrame. by iApply "HΦ".
Qed.
Lemma a_alloc_spec R `{Timeless _ R} (v : val) Φ :
( l, l U v - Φ #l) -
awp (a_alloc (a_ret v)) R Φ.
Proof.
unfold a_alloc. iIntros "HΦ".
rewrite /awp.
iIntros (γ π env lk) "#Hfl Hunfl".
Opaque acquire release.
repeat wp_rec.
wp_apply (acquire_cancel_spec with "[$]").
iIntros "(Hlkd & Henv & HR)".
wp_seq.
rewrite {2}/env_inv.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". iDestruct "Hlocks" as %Hlocks.
wp_let. wp_alloc l as "Hl". wp_let.
iAssert (⌜σ !! l = None)%I with "[Hl Hls]" as %Hl.
{ remember (σ !! l) as σl. destruct σl; simplify_eq; eauto.
iExFalso. rewrite (big_sepM_lookup _ σ l _); last eauto.
iDestruct "Hls" as (v') "Hl'". admit.
(* iDestruct (mapsto_valid_2 with "[Hl] [Hl']") as "Hfoo". *) }
iDestruct "Hl" as "[Hl Hl']".
iMod (locking_heap_alloc σ l ULvl v with "Hl' Hσ") as "[Hσ Hl']"; eauto.
wp_apply (release_cancel_spec with "[$Hfl $Hlkd $HR Hσ Hls Hl HX]").
{ iExists X,(<[l:=ULvl]>σ). iFrame. iSplit.
- rewrite big_sepM_insert; eauto. iFrame. eauto.
- iPureIntro. admit. (* TODO: need a lemma for corrrect locks *)
}
iIntros "Hunfl". wp_seq. iFrame. by iApply "HΦ".
Admitted.
End proofs.
......@@ -10,6 +10,7 @@ Inductive level : Set :=
| ULvl : level.
Canonical Structure lvlC := leibnizC level.
(* Auth (Loc -> Ex (Level)) *)
Definition locking_heapUR : ucmraT :=
gmapUR loc (exclR lvlC).
......@@ -40,6 +41,7 @@ Section definitions.
| ULvl => false
end.
(* σ^{-1}(L) *)
Definition locked_locs (σ : gmap loc level) : gset loc :=
dom (gset loc) (filter is_lock_lvl σ).
......@@ -47,7 +49,7 @@ Section definitions.
own (@lheap_name _ hG) ( (to_locking_heap σ)).
Definition mapsto_def (l : loc) (b : level) (v: val) : iProp Σ :=
(l v
(l {1/2} v
own (@lheap_name _ hG) ( {[ l := Excl b ]}))%I.
Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
......@@ -166,7 +168,7 @@ Section properties.
Lemma locking_heap_alloc σ l x v :
σ !! l = None
l v - full_locking_heap σ == full_locking_heap (<[l:=x]>σ) l [ x ] v.
l {1/2} v - full_locking_heap σ == full_locking_heap (<[l:=x]>σ) l [ x ] v.
Proof.
rewrite /full_locking_heap mapsto_eq /mapsto_def. iIntros (?) "$ Hauth".
iMod (own_update with "Hauth") as "Hauth".
......@@ -177,3 +179,4 @@ Section properties.
by iDestruct "Hauth" as "[$ $]".
Qed.
End properties.
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