Commit 3ae7284d authored by Marianna Rapoport's avatar Marianna Rapoport

Adding support for prophecy resolution to heap_lang.CAS

parent fb2b152a
......@@ -116,7 +116,7 @@ Section tests.
Lemma wp_cas l v :
val_is_unboxed v
l v - WP CAS #l v v {{ _, True }}.
l v - WP cas: #l, v, v {{ _, True }}.
Proof.
iIntros (?) "?". wp_cas as ? | ?. done. done.
Qed.
......
......@@ -121,7 +121,7 @@ Definition newcounter : val := λ: <>, ref #0.
Definition incr : val :=
rec: "incr" "l" :=
let: "n" := !"l" in
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
if: cas: "l", "n", #1 + "n" then #() else "incr" "l".
Definition read : val := λ: "l", !"l".
(** The CMRA we need. *)
......@@ -222,7 +222,7 @@ Section counter_proof.
iDestruct 1 as (c) "[Hl Hγ]".
wp_load. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
wp_let. wp_op.
wp_bind (CAS _ _ _). iApply wp_inv_open; last iFrame "Hinv"; auto.
wp_bind (cas: _, _, _)%E. iApply wp_inv_open; last iFrame "Hinv"; auto.
iDestruct 1 as (c') ">[Hl Hγ]".
destruct (decide (c' = c)) as [->|].
- iCombine "Hγ" "Hγf" as "Hγ".
......
......@@ -8,7 +8,7 @@ Set Default Proof Using "Type".
Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in (
(* tryset *) (λ: "n",
CAS "x" NONE (SOME "n")),
cas: "x", NONE, SOME "n"),
(* check *) (λ: <>,
let: "y" := !"x" in λ: <>,
match: "y" with
......
......@@ -83,7 +83,7 @@ Inductive expr :=
| Alloc (e : expr)
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
| CAS (e0 : expr) (e1 : expr) (e2 : expr)
| CAS (e0 : expr) (e1 : expr) (e2 : expr) (e3 : expr) (e4 : expr)
| FAA (e1 : expr) (e2 : expr)
(* Prophecy *)
| NewProph
......@@ -190,8 +190,9 @@ Proof.
| Load e, Load e' => cast_if (decide (e = e'))
| Store e1 e2, Store e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| CAS e0 e1 e2, CAS e0' e1' e2' =>
cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
| CAS e0 e1 e2 e3 e4, CAS e0' e1' e2' e3' e4' =>
cast_if_and5 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
(decide (e3 = e3')) (decide (e4 = e4'))
| FAA e1 e2, FAA e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| NewProph, NewProph => left _
......@@ -251,7 +252,7 @@ Proof.
Qed.
Instance expr_countable : Countable expr.
Proof.
set (enc :=
set (enc :=
fix go e :=
match e with
| Val v => GenNode 0 [gov v]
......@@ -271,7 +272,7 @@ Proof.
| Alloc e => GenNode 13 [go e]
| Load e => GenNode 14 [go e]
| Store e1 e2 => GenNode 15 [go e1; go e2]
| CAS e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
| CAS e0 e1 e2 e3 e4 => GenNode 16 [go e0; go e1; go e2; go e3; go e4]
| FAA e1 e2 => GenNode 17 [go e1; go e2]
| NewProph => GenNode 18 []
| ResolveProph e1 e2 => GenNode 19 [go e1; go e2]
......@@ -306,7 +307,7 @@ Proof.
| GenNode 13 [e] => Alloc (go e)
| GenNode 14 [e] => Load (go e)
| GenNode 15 [e1; e2] => Store (go e1) (go e2)
| GenNode 16 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
| GenNode 16 [e0; e1; e2; e3; e4] => CAS (go e0) (go e1) (go e2) (go e3) (go e4)
| GenNode 17 [e1; e2] => FAA (go e1) (go e2)
| GenNode 18 [] => NewProph
| GenNode 19 [e1; e2] => ResolveProph (go e1) (go e2)
......@@ -359,9 +360,11 @@ Inductive ectx_item :=
| LoadCtx
| StoreLCtx (v2 : val)
| StoreRCtx (e1 : expr)
| CasLCtx (v1 : val) (v2 : val)
| CasMCtx (e0 : expr) (v2 : val)
| CasRCtx (e0 : expr) (e1 : expr)
| CasLCtx (v1 : val) (v2 : val) (v3 : val) (v4 : val)
| CasM1Ctx (e0 : expr) (v2 : val) (v3 : val) (v4 : val)
| CasM2Ctx (e0 : expr) (e1 : expr) (v3 : val) (v4 : val)
| CasM3Ctx (e0 : expr) (e1 : expr) (e2 : expr) (v4 : val)
| CasRCtx (e0 : expr) (e1 : expr) (e2 : expr) (e3 : expr)
| FaaLCtx (v2 : val)
| FaaRCtx (e1 : expr)
| ProphLCtx (v2 : val)
......@@ -386,9 +389,11 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
| LoadCtx => Load e
| StoreLCtx v2 => Store e (Val v2)
| StoreRCtx e1 => Store e1 e
| CasLCtx v1 v2 => CAS e (Val v1) (Val v2)
| CasMCtx e0 v2 => CAS e0 e (Val v2)
| CasRCtx e0 e1 => CAS e0 e1 e
| CasLCtx v1 v2 v3 v4 => CAS e (Val v1) (Val v2) (Val v3) (Val v4)
| CasM1Ctx e0 v2 v3 v4 => CAS e0 e (Val v2) (Val v3) (Val v4)
| CasM2Ctx e0 e1 v3 v4 => CAS e0 e1 e (Val v3) (Val v4)
| CasM3Ctx e0 e1 e2 v4 => CAS e0 e1 e2 e (Val v4)
| CasRCtx e0 e1 e2 e3 => CAS e0 e1 e2 e3 e
| FaaLCtx v2 => FAA e (Val v2)
| FaaRCtx e1 => FAA e1 e
| ProphLCtx v2 => ResolveProph e (of_val v2)
......@@ -416,7 +421,7 @@ Fixpoint subst (x : string) (v : val) (e : expr) : expr :=
| Alloc e => Alloc (subst x v e)
| Load e => Load (subst x v e)
| Store e1 e2 => Store (subst x v e1) (subst x v e2)
| CAS e0 e1 e2 => CAS (subst x v e0) (subst x v e1) (subst x v e2)
| CAS e0 e1 e2 e3 e4 => CAS (subst x v e0) (subst x v e1) (subst x v e2) (subst x v e3) (subst x v e4)
| FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
| NewProph => NewProph
| ResolveProph e1 e2 => ResolveProph (subst x v e1) (subst x v e2)
......@@ -485,6 +490,31 @@ Definition state_upd_used_proph_id (f: gset proph_id → gset proph_id) (σ: sta
{| heap := σ.(heap); used_proph_id := f σ.(used_proph_id) |}.
Arguments state_upd_used_proph_id _ !_ /.
(** We extend CAS to support atomic resolution of prophecy variables as follows:
[CAS p e1 e1 pv1 pv2]
where [pv1] and [pv2] are values of type [option (proph * val)].
If [CAS p e1 e2] succeeds, and if [pv1 = Some (p, v)], we atomically resolve the
prophecy variable [p] to [v]. If the [CAS] fails, we do the same of [pv2]:
[let b = CAS p e1 e2 ;;
match (if b then pv1 else pv2) with
| Some (p, v) => resolve p to v
| None => ()
end]
The following function takes a value and extracts its encoding
of an optional prophecy-value pair.
*)
Definition extract_proph_resolve (v : val) : option (option (proph_id * val)) :=
match v with
| InjLV (LitV LitUnit) =>
Some None
| InjRV (PairV (LitV (LitProphecy p)) v') =>
Some (Some (p, v'))
| _ =>
None
end.
Inductive head_step : expr state list observation expr state list (expr) Prop :=
| RecS f x e σ :
head_step (Rec f x e) σ [] (Val $ RecV f x e) σ []
......@@ -532,16 +562,22 @@ Inductive head_step : expr → state → list observation → expr → state →
[]
(Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
[]
| CasFailS l v1 v2 vl σ :
| CasFailS l v1 v2 v3 v4 pv pvs vl σ :
extract_proph_resolve v4 = Some pv
pvs = option_list pv
σ.(heap) !! l = Some vl vl v1
vals_cas_compare_safe vl v1
head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ []
(Val $ LitV $ LitBool false) σ []
| CasSucS l v1 v2 σ :
head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) (Val v3) (Val v4)) σ
pvs
(Val $ LitV $ LitBool false) σ
[]
| CasSucS l v1 v2 v3 v4 pv pvs σ :
extract_proph_resolve v3 = Some pv
pvs = option_list pv
σ.(heap) !! l = Some v1
vals_cas_compare_safe v1 v1
head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
[]
head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) (Val v3) (Val v4)) σ
pvs
(Val $ LitV $ LitBool true) (state_upd_heap <[l:=v2]> σ)
[]
| FaaS l i1 i2 σ :
......
......@@ -32,11 +32,23 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
*or* [v] to be unboxed. However, by writing it this way the [val_is_unboxed]
is outside the atomic triple, which makes it much easier to use -- and the
spec is still good enough for all our applications. *)
cas_spec (l : loc) (w1 w2 : val) :
cas_spec (l : loc) (w1 w2 w3 w4 : val) :
extract_proph_resolve w3 = Some None
extract_proph_resolve w4 = Some None
val_is_unboxed w1
<<< v, mapsto l 1 v >>> cas #l w1 w2 @
<<< v, mapsto l 1 v >>> cas #l w1 w2 w3 w4 @
<<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
RET #(if decide (v = w1) then true else false) >>>;
RET #(if decide (v = w1) then true else false) >>>;
cas_suc_proph_spec (l : loc) (w1 w2 w3 w4 w : val) v (p : proph_id) :
extract_proph_resolve w3 = Some (Some (p, w))
val_is_unboxed w1
<<< mapsto l 1 w1 proph p v >>> cas #l w1 w2 w3 w4 @
<<< mapsto l 1 w2 v = Some w, RET #true>>>;
cas_fail_proph_spec (l : loc) (w1 w2 w3 w4 w : val) v (p : proph_id) :
extract_proph_resolve w4 = Some (Some (p, w))
val_is_unboxed w1
<<< v', v' w1 mapsto l 1 v' proph p v >>> cas #l w1 w2 w3 w4 @
<<< mapsto l 1 v' v = Some w, RET #false>>>;
}.
Arguments atomic_heap _ {_}.
......@@ -54,7 +66,7 @@ Notation "'ref' e" := (alloc e) : expr_scope.
Notation "! e" := (load e) : expr_scope.
Notation "e1 <- e2" := (store e1 e2) : expr_scope.
Notation CAS e1 e2 e3 := (cas e1 e2 e3).
Notation CAS e1 e2 e3 e4 e5 := (cas e1 e2 e3 e4 e5).
End notation.
......@@ -66,7 +78,7 @@ Definition primitive_load : val :=
Definition primitive_store : val :=
λ: "l" "x", "l" <- "x".
Definition primitive_cas : val :=
λ: "l" "e1" "e2", CAS "l" "e1" "e2".
λ: "l" "e1" "e2" "e3" "e4", CAS "l" "e1" "e2" "e3" "e4".
Section proof.
Context `{!heapG Σ}.
......@@ -95,18 +107,46 @@ Section proof.
wp_store. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
Qed.
Lemma primitive_cas_spec (l : loc) (w1 w2 : val) :
Lemma primitive_cas_spec (l : loc) (w1 w2 w3 w4: val) :
extract_proph_resolve w3 = Some None
extract_proph_resolve w4 = Some None
val_is_unboxed w1
<<< (v : val), l v >>>
primitive_cas #l w1 w2 @
primitive_cas #l w1 w2 w3 w4 @
<<< if decide (v = w1) then l w2 else l v,
RET #(if decide (v = w1) then true else false) >>>.
Proof.
iIntros (? Q Φ) "? AU". wp_lam. wp_let. wp_let.
iIntros (??? Q Φ) "? AU". wp_lam. repeat wp_let.
iMod "AU" as (v) "[H↦ [_ Hclose]]".
destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
iMod ("Hclose" with "H↦") as "HΦ"; by iApply "HΦ".
Qed.
Lemma primitive_cas_suc_proph_spec (l : loc) (w1 w2 w3 w4 w : val) v (p : proph_id) :
extract_proph_resolve w3 = Some (Some (p, w))
val_is_unboxed w1
<<< l w1 proph p v >>>
primitive_cas #l w1 w2 w3 w4 @
<<< l w2 v = Some w, RET #true>>>.
Proof.
iIntros (?? Q Φ) "? AU". wp_lam. repeat wp_let.
iMod "AU" as "[[H↦ Hp] [_ Hclose]]".
wp_apply (wp_cas_suc_proph with "[H↦ Hp]"); eauto with iFrame; first by left.
iIntros "H". iMod ("Hclose" with "H") as "HΦ". by iApply "HΦ".
Qed.
Lemma primitive_cas_fail_proph_spec (l : loc) (w1 w2 w3 w4 w : val) v (p : proph_id) :
extract_proph_resolve w4 = Some (Some (p, w))
val_is_unboxed w1
<<< v', v' w1 l v' proph p v >>>
primitive_cas #l w1 w2 w3 w4 @
<<< l v' v = Some w, RET #false>>>.
Proof.
iIntros (? ? Q Φ) "? AU". wp_lam. repeat wp_let.
iMod "AU" as (v') "[(Hn & H↦ & Hp) [_ Hclose]]". iDestruct "Hn" as %Hn.
wp_apply (wp_cas_fail_proph with "[H↦ Hp]"); eauto with iFrame; first by right.
iIntros "H". iMod ("Hclose" with "H") as "HΦ". by iApply "HΦ".
Qed.
End proof.
(* NOT an instance because users should choose explicitly to use it
......@@ -116,4 +156,6 @@ Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
load_spec := primitive_load_spec;
store_spec := primitive_store_spec;
cas_spec := primitive_cas_spec;
mapsto_agree := gen_heap.mapsto_agree |}.
cas_suc_proph_spec := primitive_cas_suc_proph_spec;
cas_fail_proph_spec := primitive_cas_fail_proph_spec;
mapsto_agree := gen_heap.mapsto_agree |}.
This diff is collapsed.
......@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
Definition newcounter : val := λ: <>, ref #0.
Definition incr : val := rec: "incr" "l" :=
let: "n" := !"l" in
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
if: cas: "l", "n", #1 + "n" then #() else "incr" "l".
Definition read : val := λ: "l", !"l".
(** Monotone counter *)
......@@ -50,7 +50,7 @@ Section mono_proof.
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
wp_pures.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
wp_bind (CAS _ _ _ _ _). iInv N as (c') ">[Hγ Hl]".
destruct (decide (c' = c)) as [->|].
- iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_valid_discrete_2.
......@@ -127,7 +127,7 @@ Section contrib_spec.
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
wp_pures.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
wp_bind (CAS _ _ _ _ _). iInv N as (c') ">[Hγ Hl]".
destruct (decide (c' = c)) as [->|].
- iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. }
......
......@@ -16,7 +16,7 @@ Section increment.
Definition incr: val :=
rec: "incr" "l" :=
let: "oldv" := !"l" in
if: CAS "l" "oldv" ("oldv" + #1)
if: CAS "l" "oldv" ("oldv" + #1) NONEV NONEV
then "oldv" (* return old value if success *)
else "incr" "l".
......@@ -29,8 +29,8 @@ Section increment.
iAuIntro. iApply (aacc_aupd_abort with "AU"); first done.
iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
iIntros "$ !> AU !> _".
(* Now go on *)
wp_apply cas_spec; [done|iAccu|].
wp_let. wp_op. wp_bind (CAS _ _ _ _ _).
wp_apply cas_spec; [done|done|done|iAccu|].
(* Prove the atomic update for CAS *)
iAuIntro. iApply (aacc_aupd with "AU"); first done.
iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
......
......@@ -7,7 +7,7 @@ From iris.heap_lang.lib Require Import lock.
Set Default Proof Using "Type".
Definition newlock : val := λ: <>, ref #false.
Definition try_acquire : val := λ: "l", CAS "l" #false #true.
Definition try_acquire : val := λ: "l", cas: "l", #false, #true.
Definition acquire : val :=
rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false.
......
......@@ -20,7 +20,7 @@ Definition newlock : val :=
Definition acquire : val :=
rec: "acquire" "lk" :=
let: "n" := !(Snd "lk") in
if: CAS (Snd "lk") "n" ("n" + #1)
if: cas: Snd "lk", "n", "n" + #1
then wait_loop "n" "lk"
else "acquire" "lk".
......@@ -111,7 +111,7 @@ Section proof.
iInv N as (o n) "[Hlo [Hln Ha]]".
wp_load. iModIntro. iSplitL "Hlo Hln Ha".
{ iNext. iExists o, n. by iFrame. }
wp_pures. wp_bind (CAS _ _ _).
wp_pures. wp_bind (CAS _ _ _ _ _).
iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)".
destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
- iMod (own_update with "Hauth") as "[Hauth Hofull]".
......
......@@ -72,7 +72,7 @@ Instance load_atomic s v : Atomic s (Load (Val v)).
Proof. solve_atomic. Qed.
Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance cas_atomic s v0 v1 v2 : Atomic s (CAS (Val v0) (Val v1) (Val v2)).
Instance cas_atomic s v0 v1 v2 v3 v4 : Atomic s (CAS (Val v0) (Val v1) (Val v2) (Val v3) (Val v4)).
Proof. solve_atomic. Qed.
Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
......@@ -235,50 +235,105 @@ Proof.
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cas_fail s E l q v' v1 v2 :
Lemma wp_cas_fail s E l q v' v1 v2 v3 v4 :
v' v1 vals_cas_compare_safe v' v1
{{{ l {q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
extract_proph_resolve v4 = Some None
{{{ l {q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) (Val v3) (Val v4) @ s; E
{{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (??? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma twp_cas_fail s E l q v' v1 v2 :
Lemma twp_cas_fail s E l q v' v1 v2 v3 v4 :
v' v1 vals_cas_compare_safe v' v1
[[{ l {q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
extract_proph_resolve v4 = Some None
[[{ l {q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) (Val v3) (Val v4) @ s; E
[[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (??? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cas_suc s E l v1 v2 :
Lemma wp_cas_fail_proph s E l q v' v1 v2 v3 v4 p v w :
v' v1 vals_cas_compare_safe v' v1
extract_proph_resolve v4 = Some (Some (p, w))
{{{ (l {q} v' proph p v) }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) (Val v3) (Val v4) @ s; E
{{{ RET LitV (LitBool false); l {q} v' v = Some w}}}.
Proof.
iIntros (??? Φ) "[>Hl >Hp] HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iDestruct (@proph_map_valid with "HR Hp") as %Hlookup.
iSplit; first by eauto. simpl.
iNext; iIntros (v2' σ2 efs Hstep); inv_head_step. iApply fupd_frame_l.
iSplit=> //. iFrame.
iMod ((@proph_map_remove _ _ _ _ _ _ _ p) with "HR Hp") as "Hp". iModIntro.
iSplitR "HΦ Hl".
- iExists _. iFrame. iPureIntro. split. by eapply first_resolve_delete.
rewrite dom_delete. rewrite <- difference_empty_L. by eapply difference_mono.
- iApply "HΦ". iFrame. iPureIntro. by eapply first_resolve_eq.
Qed.
Lemma wp_cas_suc s E l v1 v2 v3 v4 :
vals_cas_compare_safe v1 v1
{{{ l v1 }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
extract_proph_resolve v3 = Some None
{{{ l v1 }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) (Val v3) (Val v4) @ s; E
{{{ RET LitV (LitBool true); l v2 }}}.
Proof.
iIntros (? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iSplit.
(* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
{ iPureIntro. repeat eexists. by econstructor. }
iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed.
Lemma twp_cas_suc s E l v1 v2 :
Lemma twp_cas_suc s E l v1 v2 v3 v4 :
vals_cas_compare_safe v1 v1
[[{ l v1 }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
extract_proph_resolve v3 = Some None
[[{ l v1 }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) (Val v3) (Val v4) @ s; E
[[{ RET LitV (LitBool true); l v2 }]].
Proof.
iIntros (? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iSplit.
(* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
{ iPureIntro. repeat eexists. by econstructor. }
iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cas_suc_proph s E l v1 v2 v3 v4 p v w :
vals_cas_compare_safe v1 v1
extract_proph_resolve v3 = Some (Some (p, w))
{{{ (l v1 proph p v) }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) (Val v3) (Val v4) @ s; E
{{{ RET LitV (LitBool true); l v2 v = Some w}}}.
Proof.
iIntros (?? Φ) "[>Hl >Hp] HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iDestruct (@proph_map_valid with "HR Hp") as %Hlookup.
iSplit.
{ iPureIntro. repeat eexists. by econstructor. }
iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iApply fupd_frame_l.
iSplit=> //. iFrame.
iMod ((@proph_map_remove _ _ _ _ _ _ _ p) with "HR Hp") as "Hp". iModIntro.
iSplitR "HΦ Hl".
- iExists _. iFrame. iPureIntro. split. by eapply first_resolve_delete.
rewrite dom_delete. rewrite <- difference_empty_L. by eapply difference_mono.
- iApply "HΦ". iFrame. iPureIntro. by eapply first_resolve_eq.
Qed.
Lemma wp_faa s E l i1 i2 :
{{{ l LitV (LitInt i1) }}} FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
{{{ RET LitV (LitInt i1); l LitV (LitInt (i1 + i2)) }}}.
......
......@@ -15,8 +15,11 @@ Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2
| ResolveProph e1 e2 =>
is_closed_expr X e1 && is_closed_expr X e2
| If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
| If e0 e1 e2 | Case e0 e1 e2 =>
is_closed_expr X e0 && is_closed_expr X e1 && is_closed_expr X e2
| CAS e0 e1 e2 e3 e4 =>
is_closed_expr X e0 && is_closed_expr X e1 && is_closed_expr X e2 &&
is_closed_expr X e3 && is_closed_expr X e4
| NewProph => true
end
with is_closed_val (v : val) : bool :=
......
......@@ -155,4 +155,8 @@ Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
(Match e0 BAnon e1 x%bind e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
Notation "'cas:' e1 ',' e2 ',' e3" := (CAS e1%E e2%E e3%E NONEV NONEV)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
Notation "'new' 'prophecy'" := NewProph (at level 100) : expr_scope.
Notation "'resolve_proph:' p 'to:' v" := (ResolveProph p v) (at level 100) : expr_scope.
......@@ -236,87 +236,95 @@ Proof.
rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v v1 v2 Φ :
Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v v1 v2 v3 v4 Φ :
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
vals_cas_compare_safe v v1
(v = v1 envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }}))
(v v1 envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }}))
envs_entails Δ (WP fill K (CAS (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
(v = v1
extract_proph_resolve v3 = Some None
envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }}))
(v v1
extract_proph_resolve v4 = Some None
envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }}))
envs_entails Δ (WP fill K (CAS (LitV l) (Val v1) (Val v2) (Val v3) (Val v4)) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ???? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
- rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
- rewrite -wp_bind. eapply wand_apply; first (apply wp_cas_suc; naive_solver).
rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; auto.
apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; naive_solver.
- rewrite -wp_bind. eapply wand_apply.
{ eapply wp_cas_fail; eauto. }
{ eapply wp_cas_fail; naive_solver. }
rewrite into_laterN_env_sound -later_sep /= {1}envs_lookup_split //; simpl.
apply later_mono, sep_mono_r. apply wand_mono; auto.
apply later_mono, sep_mono_r. apply wand_mono; naive_solver.
Qed.
Lemma tac_twp_cas Δ Δ' s E i K l v v1 v2 Φ :
Lemma tac_twp_cas Δ Δ' s E i K l v v1 v2 v3 v4 Φ :
envs_lookup i Δ = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ'
vals_cas_compare_safe v v1
(v = v1 envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }]))
(v v1 envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }]))
envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
(v = v1
extract_proph_resolve v3 = Some None
envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }]))
(v v1
extract_proph_resolve v4 = Some None
envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }]))
envs_entails Δ (WP fill K (CAS (LitV l) v1 v2 v3 v4) @ s; E [{ Φ }]).
Proof.
rewrite envs_entails_eq=> ??? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
- rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc.
- rewrite -twp_bind. eapply wand_apply; first (apply twp_cas_suc; naive_solver).
rewrite /= {1}envs_simple_replace_sound //; simpl.
apply sep_mono_r. rewrite right_id. apply wand_mono; auto.
apply sep_mono_r. rewrite right_id. apply wand_mono; naive_solver.
- rewrite -twp_bind. eapply wand_apply.
{ eapply twp_cas_fail; eauto. }
{ eapply twp_cas_fail; naive_solver. }
rewrite /= {1}envs_lookup_split //; simpl.
apply sep_mono_r. apply wand_mono; auto.
apply sep_mono_r. apply wand_mono; naive_solver.
Qed.