Commit f62249a1 authored by Dan Frumin's avatar Dan Frumin

Implement fractional locking heap

parent d6730f8e
......@@ -11,6 +11,7 @@ theories/c_translation/translation.v
theories/c_translation/derived.v
theories/heap_lang_vcgen/naive.v
theories/tests/test1.v
theories/tests/test2.v
theories/tests/fact.v
theories/tests/gcd.v
theories/tests/lists.v
......@@ -8,8 +8,8 @@ Section Derived.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Lemma a_load_ret (l: loc) (w: val) R Φ:
l U w (l U w - Φ w) -
Lemma a_load_ret (l: loc) (q : Qp) (w: val) R Φ:
l U{q} w (l U{q} w - Φ w) -
awp (a_load (a_ret (#l)%E)) R Φ.
Proof.
iIntros "H". iApply a_load_spec.
......
......@@ -160,8 +160,8 @@ Section proofs.
by iApply ("IH" with "Hi").
Qed.
Lemma a_load_spec R Φ e :
awp e R (λ v, (l : loc) (w : val), v = #l l U w (l U w - Φ w)) -
Lemma a_load_spec R Φ q e :
awp e R (λ v, (l : loc) (w : val), v = #l l U{q} w (l U{q} w - Φ w)) -
awp (a_load e) R Φ.
Proof.
iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
......@@ -284,6 +284,7 @@ Section proofs.
rewrite (bi.big_sepM_lookup_acc _ _ l ULvl); last done.
iDestruct "Hls" as "[Hl' Hls]".
iDestruct "Hl'" as (?) "Hl'".
rewrite Qp_mult_1_l.
iDestruct (mapsto_agree l (1/2) (1/2) with "Hl' Hv") as %->.
iCombine "Hv Hl'" as "Hv".
wp_store.
......
From iris.algebra Require Import cmra auth gmap excl.
From iris.algebra Require Import cmra auth gmap frac agree.
From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Export own.
From iris.heap_lang Require Import lang lifting.
From iris.proofmode Require Import tactics.
......@@ -10,9 +11,9 @@ Inductive level : Set :=
| ULvl : level.
Canonical Structure lvlC := leibnizC level.
(* Auth (Loc -> Ex (Level)) *)
(* Auth (Loc -> (Q * Agree Level)) *)
Definition locking_heapUR : ucmraT :=
gmapUR loc (exclR lvlC).
gmapUR loc (prodR fracR (agreeR lvlC)).
(** The CMRA we need. *)
Class locking_heapG (Σ : gFunctors) := LHeapG {
......@@ -33,7 +34,7 @@ Section definitions.
Context `{hG : locking_heapG Σ, !heapG Σ}.
Definition to_locking_heap (σ : gmap loc level) : locking_heapUR :=
fmap (λ x, Excl x) σ.
fmap (λ x, (1%Qp, to_agree x)) σ.
Definition is_lock_lvl (a : loc * level) : bool :=
match (snd a) with
......@@ -48,21 +49,27 @@ Section definitions.
Definition full_locking_heap (σ : gmap loc level) :=
own (@lheap_name _ hG) ( (to_locking_heap σ)).
Definition mapsto_def (l : loc) (b : level) (v: val) : iProp Σ :=
(l {1/2} v
own (@lheap_name _ hG) ( {[ l := Excl b ]}))%I.
Definition mapsto_def (l : loc) (b : level) (q : frac) (v: val) : iProp Σ :=
(l {q*(1/2)} v
own (@lheap_name _ hG) ( {[ l := (q, to_agree b) ]}))%I.
Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
Definition mapsto := unseal mapsto_aux.
Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux.
End definitions.
Notation "l ↦[ x ] v" := (mapsto l x v)
Notation "l ↦[ x & q ] v" := (mapsto l x q%Qp v%V)
(at level 20, q at level 50, format "l ↦[ x & q ] v") : uPred_scope.
Notation "l ↦[ x ] v" := (mapsto l x 1%Qp v%V)
(at level 20, x at level 50, format "l ↦[ x ] v") : bi_scope.
Notation "l ↦L v" := (l [LLvl] v)%I
(at level 20, format "l ↦L v") : bi_scope.
Notation "l ↦U v" := (l [ULvl] v)%I
(at level 20, format "l ↦U v") : bi_scope.
Notation "l ↦L{ q } v" := (mapsto l LLvl q%Qp v%V)%I
(at level 20, format "l ↦L{ q } v") : bi_scope.
Notation "l ↦U{ q } v" := (mapsto l ULvl q%Qp v%V)%I
(at level 20, format "l ↦U{ q } v") : bi_scope.
Notation "l ↦L -" := ( v, l L v)%I
(at level 20, format "l ↦L -") : bi_scope.
......@@ -86,17 +93,37 @@ Section properties.
Implicit Type x y : level.
Implicit Type l : loc.
Global Instance mapsto_timeless l x q v : Timeless (mapsto l x q v).
Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
Global Instance mapsto_fractional l x v : Fractional (λ q, mapsto l x q v)%I.
Proof.
intros p q. rewrite mapsto_eq /mapsto_def.
assert ((p + q) * (1 / 2) = (p * (1 / 2)) + (q * (1 / 2)))%Qp as ->.
{ apply Qp_mult_plus_distr_l. }
iSplit.
- iIntros "[Hl Ho]".
iDestruct "Hl" as "[$ $]".
rewrite -own_op -auth_frag_op op_singleton pair_op agree_idemp. done.
- iIntros "[[Hl1 Ho1] [Hl2 Ho2]]".
iCombine "Hl1 Hl2" as "Hl". iFrame.
iCombine "Ho1 Ho2" as "Ho".
rewrite op_singleton pair_op agree_idemp. done.
Qed.
Global Instance mapsto_as_fractional l q x v :
AsFractional (mapsto l x q v) (λ q, mapsto l x q v)%I q.
Proof. split. done. apply _. Qed.
Lemma to_locking_heap_insert σ l x :
to_locking_heap (<[l := x]> σ) = <[l := Excl x]>(to_locking_heap σ).
to_locking_heap (<[l := x]> σ) = <[l := (1%Qp, to_agree x)]>(to_locking_heap σ).
Proof. by rewrite /to_locking_heap fmap_insert. Qed.
Lemma to_locking_heap_lookup_Some σ l x :
σ !! l = Some x to_locking_heap σ !! l = Some (Excl x).
σ !! l = Some x to_locking_heap σ !! l = Some (1%Qp, to_agree x).
Proof. rewrite /to_locking_heap lookup_fmap => -> //. Qed.
Lemma to_locking_heap_lookup_None σ l :
σ !! l = None to_locking_heap σ !! l = None.
Proof. rewrite /to_locking_heap lookup_fmap => -> //. Qed.
Lemma locked_locs_lock σ l :
locked_locs (<[l := LLvl]>σ) = {[l]} locked_locs σ.
Proof.
......@@ -142,17 +169,16 @@ Section properties.
rewrite lookup_insert_ne; naive_solver.
Qed.
Lemma heap_singleton_included (σ : gmap loc level) l x :
{[l := Excl x]} (to_locking_heap σ) σ !! l = Some x.
Lemma heap_singleton_included (σ : gmap loc level) l x q :
{[l := (q, to_agree x)]} (to_locking_heap σ) σ !! l = Some x.
Proof.
rewrite singleton_included => -[y []]. fold_leibniz.
move=>Hl /Some_included_exclusive Hx. revert Hl.
rewrite /to_locking_heap lookup_fmap fmap_Some => -[z [-> Hz]].
simplify_eq/=. naive_solver.
rewrite singleton_included=> -[[q' av] []].
rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[v' [Hl [/= -> ->]]].
move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
Qed.
Lemma locked_locs_locked σ l v :
l L v - full_locking_heap σ - l locked_locs σ⌝.
Lemma locked_locs_locked σ l v q :
l L{q} v - full_locking_heap σ - l locked_locs σ⌝.
Proof.
rewrite mapsto_eq /mapsto_def /full_locking_heap.
iIntros "[Hl Hpart] Hfull".
......@@ -162,8 +188,8 @@ Section properties.
eapply elem_of_dom_2. apply map_filter_lookup_Some. eauto.
Qed.
Lemma locked_locs_unlocked σ l v :
l U v - full_locking_heap σ - l locked_locs σ⌝.
Lemma locked_locs_unlocked σ l v q :
l U{q} v - full_locking_heap σ - l locked_locs σ⌝.
Proof.
rewrite mapsto_eq /mapsto_def /full_locking_heap.
iIntros "[Hl Hpart] Hfull".
......@@ -183,7 +209,7 @@ Section properties.
iDestruct (own_valid_2 with "Hauth Hl")
as %[Hl%heap_singleton_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hauth Hl") as "Hauth".
{ apply (auth_update _ _ (to_locking_heap (<[l:=y]>σ)) {[l := Excl y]}).
{ apply (auth_update _ _ (to_locking_heap (<[l:=y]>σ)) {[l := (1%Qp, to_agree y)]}).
rewrite to_locking_heap_insert.
eapply singleton_local_update; first by eapply to_locking_heap_lookup_Some.
by apply exclusive_local_update. }
......@@ -194,9 +220,10 @@ Section properties.
σ !! l = None
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".
rewrite /full_locking_heap mapsto_eq /mapsto_def Qp_mult_1_l.
iIntros (?) "$ Hauth".
iMod (own_update with "Hauth") as "Hauth".
{ eapply (auth_update_alloc _ (to_locking_heap (<[l:=x]> σ)) {[l := Excl x]}).
{ eapply (auth_update_alloc _ (to_locking_heap (<[l:=x]> σ)) {[l := (1%Qp, to_agree x)]}).
rewrite to_locking_heap_insert.
apply alloc_singleton_local_update; last done.
by apply to_locking_heap_lookup_None. }
......
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.bi.lib Require Import fractional.
From iris.algebra Require Import frac auth.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import proofmode translation derived.
Section test.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Lemma test_fractional (x : loc) :
x U #1 -
awp (a_store (a_ret #x) (a_bin_op PlusOp (a_load (a_ret #x)) (a_load (a_ret #x))))%E True (λ _, x L #2).
Proof.
iIntros "[Hx Hx']".
iApply (a_store_spec _ _ (λ v, v = x) (λ v, v = #2 x U #1) with "[] [Hx Hx']")%I.
{ iApply awp_ret. wp_value_head. eauto. }
- iApply (a_bin_op_spec _ _ (λ v, v = #1 x U{1 / 2} #1)
(λ v, v = #1 x U{1 / 2} #1)
with "[Hx] [Hx']")%I.
awp_load_ret x.
awp_load_ret x.
iIntros (? ?) "[% Hx] [% Hx']"; simplify_eq/=.
iExists _; eauto. repeat iSplit; eauto.
iCombine "Hx Hx'" as "Hx". iFrame.
- iIntros (? ? ->) "[% Hx]"; simplify_eq/=.
iExists _; iFrame. eauto.
Qed.
End test.
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