Commit 719be114 authored by Robbert Krebbers's avatar Robbert Krebbers

Start working on adding free.

parent 061dad60
......@@ -14,9 +14,35 @@ Definition a_alloc : val := λ: "x1" "x2",
"vv" ←ᶜ "x1" ||| "x2" ;;
let: "n" := Fst "vv" in
let: "v" := Snd "vv" in
a_atomic_env (λ: <>, (ref (lreplicate "n" "v"), #0)).
a_atomic_env (λ: <>, (ref (SOME (lreplicate "n" "v")), #0)).
Notation "'allocᶜ' ( e1 , e2 )" := (a_alloc e1%E e2%E) (at level 80) : expr_scope.
Definition a_free_check : val :=
rec: "go" "env" "l" "i" "n" :=
if: "i" < "n" then
assert: (mset_member ("l", "i") "env" = #false);;
"go" "env" "l" (#1 + "i") "n"
else #().
Definition a_free : val := λ: "x",
"v" ←ᶜ "x";;
a_atomic_env (λ: "env",
let: "l" := Fst "v" in
let: "i" := Snd "v" in
match: !"l" with
NONE => assert #false (* double free *)
| SOME "l" =>
(* We need to make sure `i = 0` and that all `0 ... length of block` are
unlocked. TODO: this means we need to change the spec of `alloc` back so
that we can actually establish we initially have the pointer to the first
element of the array. *)
assert ("i" = #0);;
let: "n" := llength "l" in
a_free_check "env" "l" #0 "n"
"l" <- NONE
end
).
Definition a_store : val := λ: "x1" "x2",
"vv" ←ᶜ "x1" ||| "x2" ;;
a_atomic_env (λ: "env",
......@@ -24,9 +50,10 @@ Definition a_store : val := λ: "x1" "x2",
let: "i" := Snd (Fst "vv") in
let: "v" := Snd "vv" in
mset_add ("l", "i") "env" ;;
let: "ll" := !"l" in
"l" <- linsert "i" "v" "ll" ;;
"v"
match: !"l" with
NONE => assert #false (* store after free *)
| SOME "ll" => "l" <- SOME (linsert "i" "v" "ll") ;; "v"
end
).
Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.
......@@ -36,8 +63,10 @@ Definition a_load : val := λ: "x",
let: "l" := Fst "v" in
let: "i" := Snd "v" in
assert: (mset_member ("l", "i") "env" = #false);;
let: "ll" := !"l" in
llookup "i" "ll"
match: !"l" with
NONE => assert #false (* load after free *)
| SOME "ll" => llookup "i" "ll"
end
).
Notation "∗ᶜ e" :=
(a_load e)%E (at level 9, right associativity) : expr_scope.
......@@ -168,7 +197,7 @@ Section proofs.
wp_let. do 2 wp_proj; wp_let. do 2 wp_proj; wp_let. wp_proj; wp_let.
wp_apply (mset_add_spec with "[$]"); first done.
iIntros "Hlocks /="; wp_seq.
wp_load; wp_let.
wp_load; wp_match.
wp_apply (linsert_spec with "[//]"); [eauto|]; iIntros (ll' Hl').
iApply wp_fupd. wp_store.
iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]".
......@@ -198,7 +227,7 @@ Section proofs.
wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=".
rewrite bool_decide_false //.
wp_op. iSplit; first done. iNext; wp_seq.
wp_load; wp_let. wp_apply (llookup_spec with "[//]"); [done|]; iIntros "_".
wp_load; wp_match. wp_apply (llookup_spec with "[//]"); [done|]; iIntros "_".
iDestruct ("Hclose" with "Hl") as "[Hσ Hl]".
iIntros "!> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
iExists X, _. by iFrame.
......
......@@ -106,7 +106,7 @@ Section definitions.
( τ : gmap loc (list (lvl * val)),
cl, σ !! cl = τ !! cl.1 = lookup (M:=list _) cl.2
own lheap_name ( (to_locking_heap σ))
[ map] llvvs τ, lv, l lv is_list lv (snd <$> lvvs) )%I.
[ map] llvvs τ, lv, l SOMEV lv is_list lv (snd <$> lvvs) )%I.
Definition mapsto_def (cl : cloc) (lv : lvl) (q : frac) (v: val) : iProp Σ :=
( lv',
......@@ -296,7 +296,7 @@ Section properties.
Lemma locking_heap_load cl lv q v σ :
full_locking_heap σ - cl C[lv]{q} v == ll vs,
is_list ll vs vs !! cl.2 = Some v
cl.1 ll (cl.1 ll - full_locking_heap σ cl C[lv]{q} v).
cl.1 SOMEV ll (cl.1 SOMEV ll - full_locking_heap σ cl C[lv]{q} v).
Proof.
iDestruct 1 as (τ Hτ) "[Hσ Hτ]".
rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ?) "Hl".
......@@ -315,8 +315,8 @@ Section properties.
Lemma locking_heap_store cl lv v σ :
full_locking_heap σ - cl C[lv] v == ll vs,
is_list ll vs vs !! cl.2 = Some v
cl.1 ll
( ll' lv' v', is_list ll' (<[cl.2:=v']>vs) - cl.1 ll' ==
cl.1 SOMEV ll
( ll' lv' v', is_list ll' (<[cl.2:=v']>vs) - cl.1 SOMEV ll' ==
full_locking_heap (<[cl:=(lv',v')]>σ) cl C[lv'] v').
Proof.
iDestruct 1 as (τ Hτ) "[Hσ Hτ]".
......@@ -392,7 +392,7 @@ Section properties.
Lemma locking_heap_alloc l ll vs σ :
is_list ll vs
full_locking_heap σ - l ll ==
full_locking_heap σ - l SOMEV ll ==
i, σ !! (l,i) = None
full_locking_heap (alloc_heap σ l vs O) (l,0) C vs.
Proof.
......
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