Commit df5c508e authored by Ralf Jung's avatar Ralf Jung

make atomic_heap a typeclass and add some notation for it

parent aae893bd
......@@ -6,7 +6,7 @@ From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
(** A general logically atomic interface for a heap. *)
Structure atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
(* -- operations -- *)
alloc : val;
load : val;
......@@ -38,6 +38,24 @@ Structure atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
}.
Arguments atomic_heap _ {_}.
(** Notation for heap primitives, in a module so you can import it separately. *)
Module notation.
Notation "l ↦{ q } v" := (mapsto l q v)
(at level 20, q at level 50, format "l ↦{ q } v") : bi_scope.
Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.
Notation "l ↦{ q } -" := ( v, l {q} v)%I
(at level 20, q at level 50, format "l ↦{ q } -") : bi_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.
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).
End notation.
(** Proof that the primitive physical operations of heap_lang satisfy said interface. *)
Definition primitive_alloc : val :=
λ: "v", ref "v".
......@@ -88,10 +106,12 @@ Section proof.
destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
iMod ("Hclose" with "H↦") as "HΦ"; by iApply "HΦ".
Qed.
Definition primitive_atomic_heap : atomic_heap Σ :=
{| alloc_spec := primitive_alloc_spec;
load_spec := primitive_load_spec;
store_spec := primitive_store_spec;
cas_spec := primitive_cas_spec |}.
End proof.
(* NOT an instance because users should choose explicitly to use it
(using [Explicit Instance]). *)
Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
{| alloc_spec := primitive_alloc_spec;
load_spec := primitive_load_spec;
store_spec := primitive_store_spec;
cas_spec := primitive_cas_spec |}.
......@@ -9,18 +9,19 @@ atomicity. *)
(* TODO: Move this to iris-examples once gen_proofmode is merged. *)
Section increment.
Context `{!heapG Σ} (aheap: atomic_heap Σ).
Context `{!heapG Σ} {aheap: atomic_heap Σ}.
Import atomic_heap.notation.
Definition incr: val :=
rec: "incr" "l" :=
let: "oldv" := aheap.(load) "l" in
if: aheap.(cas) ("l", "oldv", ("oldv" + #1))
let: "oldv" := !"l" in
if: CAS "l" "oldv" ("oldv" + #1)
then "oldv" (* return old value if success *)
else "incr" "l".
Lemma incr_spec (l: loc) :
<<< (v : Z), aheap.(mapsto) l 1 #v >>> incr #l @
<<< aheap.(mapsto) l 1 #(v + 1), RET #v >>>.
<<< (v : Z), l #v >>> incr #l @ <<< l #(v + 1), RET #v >>>.
Proof.
iIntros (Q Φ) "HQ AU". iLöb as "IH". wp_let.
wp_apply (load_spec with "[HQ]"); first by iAccu.
......@@ -32,7 +33,7 @@ Section increment.
{ iIntros "$ !> $ !> //". }
iIntros "$ !> AU !> HQ".
(* Now go on *)
wp_let. wp_op. wp_bind (aheap.(cas) _)%I.
wp_let. wp_op. wp_bind (CAS _ _ _)%I.
wp_apply (cas_spec with "[HQ]"); [done|iAccu|].
(* Prove the atomic shift for CAS *)
iAuIntro. iApply (aacc_aupd with "AU"); first done.
......@@ -55,10 +56,12 @@ End increment.
Section increment_client.
Context `{!heapG Σ, !spawnG Σ}.
Existing Instance primitive_atomic_heap.
Definition incr_client : val :=
λ: "x",
let: "l" := ref "x" in
incr primitive_atomic_heap "l" ||| incr primitive_atomic_heap "l".
incr "l" ||| incr "l".
Lemma incr_client_safe (x: Z):
WP incr_client #x {{ _, True }}%I.
......@@ -67,7 +70,7 @@ Section increment_client.
iMod (inv_alloc nroot _ (x':Z, l #x')%I with "[Hl]") as "#Hinv"; first eauto.
(* FIXME: I am only using persistent stuff, so I should be allowed
to move this to the persisten context even without the additional □. *)
iAssert ( WP incr primitive_atomic_heap #l {{ _, True }})%I as "#Aupd".
iAssert ( WP incr #l {{ _, True }})%I as "#Aupd".
{ iAlways. wp_apply (incr_spec with "[]"); first by iAccu. clear x.
iAuIntro. iInv nroot as (x) ">H↦".
(* FIXME: Oh wow this is bad. *)
......
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