Commit 851f05c2 authored by Marianna Rapoport's avatar Marianna Rapoport

Adding support for prophecy resolution to heap_lang.CAS

parent ad2ce8bb
......@@ -118,7 +118,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
......
......@@ -64,7 +64,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
......@@ -81,8 +81,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
is_closed X e
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | ResolveProph e1 e2 =>
is_closed X e1 && is_closed X e2
| If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
| If e0 e1 e2 | Case e0 e1 e2 =>
is_closed X e0 && is_closed X e1 && is_closed X e2
| CAS e0 e1 e2 e3 e4 =>
is_closed X e0 && is_closed X e1 && is_closed X e2 && is_closed X e3 && is_closed X e4
end.
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
......@@ -239,7 +241,7 @@ Proof.
| Alloc e => GenNode 12 [go e]
| Load e => GenNode 13 [go e]
| Store e1 e2 => GenNode 14 [go e1; go e2]
| CAS e0 e1 e2 => GenNode 15 [go e0; go e1; go e2]
| CAS e0 e1 e2 e3 e4 => GenNode 15 [go e0; go e1; go e2; go e3; go e4]
| FAA e1 e2 => GenNode 16 [go e1; go e2]
| NewProph => GenLeaf None
| ResolveProph e1 e2 => GenNode 17 [go e1; go e2]
......@@ -263,7 +265,7 @@ Proof.
| GenNode 12 [e] => Alloc (go e)
| GenNode 13 [e] => Load (go e)
| GenNode 14 [e1; e2] => Store (go e1) (go e2)
| GenNode 15 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
| GenNode 15 [e0; e1; e2; e3; e4] => CAS (go e0) (go e1) (go e2) (go e3) (go e4)
| GenNode 16 [e1; e2] => FAA (go e1) (go e2)
| GenLeaf None => NewProph
| GenNode 17 [e1; e2] => ResolveProph (go e1) (go e2)
......@@ -300,9 +302,11 @@ Inductive ectx_item :=
| LoadCtx
| StoreLCtx (e2 : expr)
| StoreRCtx (v1 : val)
| CasLCtx (e1 : expr) (e2 : expr)
| CasMCtx (v0 : val) (e2 : expr)
| CasRCtx (v0 : val) (v1 : val)
| CasLCtx (e1 : expr) (e2 : expr) (e3 : expr) (e4 : expr)
| CasM1Ctx (v0 : val) (e2 : expr) (e3 : expr) (e4 : expr)
| CasM2Ctx (v0 : val) (v1 : val) (e3 : expr) (e4 : expr)
| CasM3Ctx (v0 : val) (v1 : val) (v2 : val) (e4 : expr)
| CasRCtx (v0 : val) (v1 : val) (v2 : val) (v3 : val)
| FaaLCtx (e2 : expr)
| FaaRCtx (v1 : val)
| ProphLCtx (e2 : expr)
......@@ -327,9 +331,11 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
| LoadCtx => Load e
| StoreLCtx e2 => Store e e2
| StoreRCtx v1 => Store (of_val v1) e
| CasLCtx e1 e2 => CAS e e1 e2
| CasMCtx v0 e2 => CAS (of_val v0) e e2
| CasRCtx v0 v1 => CAS (of_val v0) (of_val v1) e
| CasLCtx e1 e2 e3 e4 => CAS e e1 e2 e3 e4
| CasM1Ctx v0 e2 e3 e4 => CAS (of_val v0) e e2 e3 e4
| CasM2Ctx v0 v1 e3 e4 => CAS (of_val v0) (of_val v1) e e3 e4
| CasM3Ctx v0 v1 v2 e4 => CAS (of_val v0) (of_val v1) (of_val v2) e e4
| CasRCtx v0 v1 v2 v3 => CAS (of_val v0) (of_val v1) (of_val v2) (of_val v3) e
| FaaLCtx e2 => FAA e e2
| FaaRCtx v1 => FAA (of_val v1) e
| ProphLCtx e2 => ResolveProph e e2
......@@ -357,7 +363,7 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
| Alloc e => Alloc (subst x es e)
| Load e => Load (subst x es e)
| Store e1 e2 => Store (subst x es e1) (subst x es e2)
| CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
| CAS e0 e1 e2 e3 e4 => CAS (subst x es e0) (subst x es e1) (subst x es e2) (subst x es e3) (subst x es e4)
| FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
| NewProph => NewProph
| ResolveProph e1 e2 => ResolveProph (subst x es e1) (subst x es e2)
......@@ -419,6 +425,31 @@ Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
val_is_unboxed vl val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
(** 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]:
Please register or sign in to reply
[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.
  • It's worth saying why there are two levels of option: None means this is not a valid encoding, Some None means that it's a valid encoding of no pair.

Please register or sign in to reply
*)
Definition extract_proph_resolve (v : val) : option (option (proph * val)) :=
match v with
| InjLV (LitV LitUnit) =>
Some None
| InjRV (PairV (LitV (LitProphecy p)) v') =>
Some (Some (p, v'))
| _ =>
None
end.
  • Uh, okay, I expected something slightly different where the option is on the Coq level. But I guess this works as well, and it might even be better.

    Please use NoneV and SomeV though, to make this more readable. (You may have to move them over from notation.v, I do not remember where they are defined currently.)

  • done (I didn't move NONEV and SOMEV, but copied them as a Local Notation instead)

Please register or sign in to reply
Inductive head_step : expr state option observation -> expr state list (expr) Prop :=
| BetaS f x e1 e2 v2 e' σ :
to_val e2 = Some v2
......@@ -460,16 +491,20 @@ Inductive head_step : expr → state → option observation -> expr → state
| StoreS l e v σ :
to_val e = Some v is_Some (σ.1 !! l)
head_step (Store (Lit $ LitLoc l) e) σ None (Lit LitUnit) (<[l:=v]>σ.1, σ.2) []
| CasFailS l e1 v1 e2 v2 vl σ :
| CasFailS l e1 v1 e2 v2 e3 v3 e4 v4 pv vl σ :
to_val e1 = Some v1 to_val e2 = Some v2
to_val e3 = Some v3 to_val e4 = Some v4
extract_proph_resolve v4 = Some pv
  • Please give better names that v1 through v4. The old v1 v2 made sense because it was CAS'ing from 1 to 2. But the other two values are of a completely different nature.

    Also, I think you should have is_some (extract_proph_resolve v3), to make sure the CAS is stuck if that is not a valid prophecy resolution. We want it to always be of that shape.

    Same below for the success case.

Please register or sign in to reply
σ.1 !! l = Some vl vl v1
vals_cas_compare_safe vl v1
head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool false) σ []
| CasSucS l e1 v1 e2 v2 σ :
head_step (CAS (Lit $ LitLoc l) e1 e2 e3 e4) σ pv (Lit $ LitBool false) σ []
| CasSucS l e1 v1 e2 v2 e3 v3 e4 v4 pv σ :
to_val e1 = Some v1 to_val e2 = Some v2
to_val e3 = Some v3 to_val e4 = Some v4
extract_proph_resolve v3 = Some pv
σ.1 !! l = Some v1
vals_cas_compare_safe v1 v1
head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool true) (<[l:=v2]>σ.1, σ.2) []
head_step (CAS (Lit $ LitLoc l) e1 e2 e3 e4) σ pv (Lit $ LitBool true) (<[l:=v2]>σ.1, σ.2) []
| FaaS l i1 e2 i2 σ :
to_val e2 = Some (LitV (LitInt i2))
σ.1 !! l = Some (LitV (LitInt i1))
......
......@@ -33,11 +33,30 @@ 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) (e1 e2 : expr) (w1 w2 : val) :
IntoVal e1 w1 IntoVal e2 w2 val_is_unboxed w1
<<< v, mapsto l 1 v >>> cas (#l, e1, e2) @
(* TODO (MR) this spec is weaker than the non-atomic spec for CAS in heap_lang
because it requires both prophecy-value pairs to be None, rather than only
the pair that will be relevant depending on what the CAS evaluates to.
Does this matter? *)
cas_spec (l : loc) (e1 e2 e3 e4 : expr) (w1 w2 w3 w4 : val) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 w3 IntoVal e4 w4
extract_proph_resolve w3 = Some None
extract_proph_resolve w4 = Some None
val_is_unboxed w1
<<< v, mapsto l 1 v >>> cas (#l, e1, e2, e3, e4) @
<<< 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) (e1 e2 e3 e4 : expr) (w1 w2 w3 w4 w : val) v (p : proph) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 w3 IntoVal e4 w4
extract_proph_resolve w3 = Some (Some (p, w))
val_is_unboxed w1
<<< mapsto l 1 w1 p v >>> cas (#l, e1, e2, e3, e4) @
<<< mapsto l 1 w2 v = Some w, RET #true>>>;
cas_fail_proph_spec (l : loc) (e1 e2 e3 e4 : expr) (w1 w2 w3 w4 w : val) v (p : proph) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 w3 IntoVal e4 w4
extract_proph_resolve w4 = Some (Some (p, w))
val_is_unboxed w1
<<< v', v' w1 mapsto l 1 v' p v >>> cas (#l, e1, e2, e3, e4) @
<<< mapsto l 1 v' v = Some w, RET #false>>>;
  • Why are there three CAS specs now? There should be only one.

    You can have derived specs but they should not be in the interface, but derived from it.

  • I have multiple specs for the same reason that I have multiple CAS specs in lifting.v (see the other comment). This spec in particular, which tries to combine the succeeding and failing case into one, would become big and complicated. Why would this be necessary?

    Edited by Marianna Rapoport
Please register or sign in to reply
}.
Arguments atomic_heap _ {_}.
......@@ -55,7 +74,7 @@ Notation "'ref' e" := (alloc e) : expr_scope.
Notation "! e" := (load e) : expr_scope.
Notation "e1 <- e2" := (store (e1, e2)%E) : expr_scope.
Notation CAS e1 e2 e3 := (cas (e1, e2, e3)%E).
Notation CAS e1 e2 e3 e4 e5 := (cas (e1, e2, e3, e4, e5)%E).
Please register or sign in to reply
End notation.
......@@ -67,7 +86,11 @@ Definition primitive_load : val :=
Definition primitive_store : val :=
λ: "p", (Fst "p") <- (Snd "p").
Definition primitive_cas : val :=
λ: "p", CAS (Fst (Fst "p")) (Snd (Fst "p")) (Snd "p").
λ: "p", CAS (Fst $ Fst $ Fst $ Fst "p")
(Snd $ Fst $ Fst $ Fst "p")
(Snd $ Fst $ Fst "p")
(Snd $ Fst "p")
(Snd "p").
Section proof.
Context `{!heapG Σ}.
......@@ -97,18 +120,51 @@ Section proof.
wp_store. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
Qed.
Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) :
IntoVal e1 w1 IntoVal e2 w2 val_is_unboxed w1
Lemma primitive_cas_spec (l : loc) e1 e2 e3 e4 (w1 w2 w3 w4 : val) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 w3 IntoVal e4 w4
extract_proph_resolve w3 = Some None
extract_proph_resolve w4 = Some None
val_is_unboxed w1
<<< (v : val), l v >>>
primitive_cas (#l, e1, e2) @
primitive_cas (#l, e1, e2, e3, e4) @
<<< if decide (v = w1) then l w2 else l v,
RET #(if decide (v = w1) then true else false) >>>.
Proof.
iIntros (<- <- ? Q Φ) "? AU". wp_let. repeat wp_proj.
iIntros (<- <- <- <- ? ? ? Q Φ) "? AU". wp_let. repeat wp_proj.
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) (e1 e2 e3 e4 : expr) (w1 w2 w3 w4 w : val) v (p : proph) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 w3 IntoVal e4 w4
extract_proph_resolve w3 = Some (Some (p, w))
val_is_unboxed w1
<<< l w1 p v >>>
primitive_cas (#l, e1, e2, e3, e4) @
<<< l w2 v = Some w, RET #true>>>.
Proof.
iIntros (<- <- <- <- ? ? Q Φ) "? AU". wp_let. repeat wp_proj.
iMod "AU" as "[[H↦ Hp] [_ Hclose]]".
wp_apply (wp_cas_suc_proph with "[H↦ Hp]"); eauto with iFrame.
{ by left. }
iIntros "H". iMod ("Hclose" with "H") as "HΦ". by iApply "HΦ".
Qed.
Lemma primitive_cas_fail_proph_spec (l : loc) (e1 e2 e3 e4 : expr) (w1 w2 w3 w4 w : val) v (p : proph) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 w3 IntoVal e4 w4
extract_proph_resolve w4 = Some (Some (p, w))
val_is_unboxed w1
<<< v', v' w1 l v' p v >>>
primitive_cas (#l, e1, e2, e3, e4) @
<<< l v' v = Some w, RET #false>>>.
Proof.
iIntros (<- <- <- <- ? ? Q Φ) "? AU". wp_let. repeat wp_proj.
iMod "AU" as (v') "[(Hn & H↦ & Hp) [_ Hclose]]". iDestruct "Hn" as %Hn.
wp_apply (wp_cas_fail_proph with "[H↦ Hp]"); eauto with iFrame.
{ 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
......@@ -118,4 +174,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 |}.
......@@ -64,7 +64,7 @@ Section atomic_snapshot.
let: "xp1" := !"xp" in
let: "v" := Snd (!"xp1") in
let: "xp2" := ref ("x", "v" + #1) in
if: CAS "xp" "xp1" "xp2"
if: cas: "xp", "xp1", "xp2"
then #()
else "writeX" "args".
......@@ -280,7 +280,7 @@ Section atomic_snapshot.
wp_load. wp_proj. wp_let. wp_op. wp_alloc l1'new as "Hl1'new".
wp_let.
(* CAS *)
wp_bind (CAS _ _ _)%E.
wp_bind (cas: _, _, _)%E.
(* open invariant *)
iInv N as (q' l1'' T x') ">Hinvp".
iDestruct "Hinvp" as (y' v'') "[Hl1 [Hl1'' [Hl2 [Hp⚫ [Ht● Ht]]]]]".
......
......@@ -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_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
wp_bind (cas: _, _, _)%E. 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_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
wp_bind (cas: _, _, _)%E. 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".
......@@ -30,8 +30,8 @@ Section increment.
iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
iIntros "$ !> AU !> _".
(* Now go on *)
wp_let. wp_op. wp_bind (CAS _ _ _)%I.
wp_apply cas_spec; [done|iAccu|].
wp_let. wp_op. wp_bind (CAS _ _ _ _ _)%I.
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_let. wp_proj. wp_op. wp_bind (CAS _ _ _).
wp_let. wp_proj. wp_op. wp_bind (cas: _, _, _)%E.
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]".
......
......@@ -202,35 +202,64 @@ Proof.
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cas_fail s E l q v' e1 v1 e2 :
IntoVal e1 v1 AsVal e2 v' v1 vals_cas_compare_safe v' v1
{{{ l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
Lemma wp_cas_fail s E l q v' e1 v1 e2 e3 v3 e4 v4 :
IntoVal e1 v1 IntoVal e3 v3 IntoVal e4 v4
extract_proph_resolve v4 = Some None
AsVal e2 v' v1 vals_cas_compare_safe v' v1
{{{ l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 e3 e4 @ s; E
{{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
iIntros (<- [v2 <-] ?? Φ) ">Hl HΦ".
iIntros (<- <- <- ? [v2 <-] ?? Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma twp_cas_fail s E l q v' e1 v1 e2 :
IntoVal e1 v1 AsVal e2 v' v1 vals_cas_compare_safe v' v1
[[{ l {q} v' }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
Lemma twp_cas_fail s E l q v' e1 v1 e2 e3 v3 e4 v4 :
IntoVal e1 v1 IntoVal e3 v3 IntoVal e4 v4
extract_proph_resolve v4 = Some None
AsVal e2 v' v1 vals_cas_compare_safe v' v1
[[{ l {q} v' }]] CAS (Lit (LitLoc l)) e1 e2 e3 e4 @ s; E
[[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
iIntros (<- [v2 <-] ?? Φ) "Hl HΦ".
iIntros (<- <- <- ? [v2 <-] ?? Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[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 e1 v1 e2 v2 :
IntoVal e1 v1 IntoVal e2 v2 vals_cas_compare_safe v1 v1
{{{ l v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
Lemma wp_cas_fail_proph s E l q v' e1 v1 e2 e3 v3 e4 v4 p v w :
IntoVal e1 v1 IntoVal e3 v3 IntoVal e4 v4
extract_proph_resolve v4 = Some (Some (p, w))
AsVal e2 v' v1 vals_cas_compare_safe v' v1
{{{ (l {q} v' p v) }}} CAS (Lit (LitLoc l)) e1 e2 e3 e4 @ s; E
{{{ RET LitV (LitBool false); l {q} v' v = Some w}}}.
Proof.
iIntros (<- <- <- ? [v2 <-] ?? Φ) "[>Hl >Hp] HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[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. unfold cons_obs. simpl.
iNext; iIntros (κ κs' 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; first 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.
  • It seems excessive to have separate lemmas for the proph and non-proph cases. Why is that?

  • Just as there are two CAS specs for the succeeding and failing case, I think it makes sense to distinguish the specs depending on whether we want to resolve a prophecy variable. If we combine the specs into one, it will get pretty ugly and inconvenient to use in my opinion:

     {{{ ▷ (l ↦{q} v' ∗
             ((⌜extract_proph_resolve p2 = Some (Some (p, pv))⌝ ∗ p2 ⥱ w) ∨
               ⌜extract_proph_resolve p2 = Some None⌝)) }}}
        CAS (Lit (LitLoc l)) e1 e2 e3 e4 @ s; E
      {{{ RET LitV (LitBool false); l ↦{q} v' ∗
             ((⌜extract_proph_resolve p2 = Some (Some (p, pv)) ∧ w = Some v⌝) ∨
               ⌜extract_proph_resolve p2 = Some None⌝) }}}.
    Edited by Marianna Rapoport
Please register or sign in to reply
Lemma wp_cas_suc s E l e1 v1 e2 v2 e3 v3 e4 v4 :
IntoVal e1 v1 IntoVal e2 v2 IntoVal e3 v3 IntoVal e4 v4
vals_cas_compare_safe v1 v1
extract_proph_resolve v3 = Some None
{{{ l v1 }}} CAS (Lit (LitLoc l)) e1 e2 e3 e4 @ s; E
{{{ RET LitV (LitBool true); l v2 }}}.
Proof.
iIntros (<- <- ? Φ) ">Hl HΦ".
iIntros (<- <- <- <- ? ? Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit.
......@@ -240,12 +269,14 @@ Proof.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed.
Lemma twp_cas_suc s E l e1 v1 e2 v2 :
IntoVal e1 v1 IntoVal e2 v2 vals_cas_compare_safe v1 v1
[[{ l v1 }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
Lemma twp_cas_suc s E l e1 v1 e2 v2 e3 v3 e4 v4 :
IntoVal e1 v1 IntoVal e2 v2 IntoVal e3 v3 IntoVal e4 v4
vals_cas_compare_safe v1 v1
extract_proph_resolve v3 = Some None
[[{ l v1 }]] CAS (Lit (LitLoc l)) e1 e2 e3 e4 @ s; E
[[{ RET LitV (LitBool true); l v2 }]].
Proof.
iIntros (<- <- ? Φ) "Hl HΦ".
iIntros (<- <- <- <- ? ? Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit.
......@@ -256,6 +287,32 @@ Proof.
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cas_suc_proph s E l e1 v1 e2 v2 e3 v3 e4 v4 p v w :
IntoVal e1 v1 IntoVal e2 v2 IntoVal e3 v3 IntoVal e4 v4
vals_cas_compare_safe v1 v1
extract_proph_resolve v3 = Some (Some (p, w))
{{{ (l v1 p v) }}} CAS (Lit (LitLoc l)) e1 e2 e3 e4 @ 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) "[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.
(* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
{ iPureIntro. repeat eexists. by econstructor. }
unfold cons_obs. simpl.
iNext; iIntros (κ κs' 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; first 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 e2 i2 :
IntoVal e2 (LitV (LitInt i2))
{{{ l LitV (LitInt i1) }}} FAA (Lit (LitLoc l)) e2 @ s; E
......@@ -310,9 +367,9 @@ Qed.
Lemma wp_resolve_proph e1 e2 p v w:
IntoVal e1 (LitV (LitProphecy p))
IntoVal e2 w
{{{ p v }}} ResolveProph e1 e2 {{{ RET (LitV LitUnit); v = Some w }}}.
{{{ p v }}} ResolveProph e1 e2 {{{ RET (LitV LitUnit); v = Some w }}}.
Proof.
iIntros (<- <- Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (<- <- Φ) ">Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iDestruct (@proph_map_valid with "HR Hp") as %Hlookup. iSplit.
(* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
......
......@@ -158,5 +158,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' p 'to' v" := (ResolveProph p v) (at level 100) : expr_scope.
This diff is collapsed.
......@@ -34,7 +34,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)
| NewProph
| ResolveProph (e1 : expr) (e2 : expr).
......@@ -60,7 +60,7 @@ Fixpoint to_expr (e : expr) : heap_lang.expr :=
| Alloc e => heap_lang.Alloc (to_expr e)
| Load e => heap_lang.Load (to_expr e)
| Store e1 e2 => heap_lang.Store (to_expr e1) (to_expr e2)
| CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
| CAS e0 e1 e2 e3 e4 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2) (to_expr e3) (to_expr e4)
| FAA e1 e2 => heap_lang.FAA (to_expr e1) (to_expr e2)
| NewProph => heap_lang.NewProph
| ResolveProph e1 e2 => heap_lang.ResolveProph (to_expr e1) (to_expr e2)
......@@ -93,9 +93,10 @@ Ltac of_expr e :=
| heap_lang.Load ?e => let e := of_expr e in constr:(Load e)
| heap_lang.Store ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Store e1 e2)
| heap_lang.CAS ?e0 ?e1 ?e2 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(CAS e0 e1 e2)
| heap_lang.CAS ?e0 ?e1 ?e2 ?e3 ?e4 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
let e3 := of_expr e3 in let e4 := of_expr e4 in
constr:(CAS e0 e1 e2 e3 e4)
| heap_lang.FAA ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
| heap_lang.NewProph =>
......@@ -121,8 +122,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=