Commit cb77b8a5 authored by Ralf Jung's avatar Ralf Jung
Browse files

Add some lemmas about mapsto to the atomic_heap interface; use IntoVal for alloc spec

parent df5c508e
From iris.heap_lang Require Export lifting notation. From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic. From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.bi.lib Require Import fractional.
Set Default Proof Using "Type". Set Default Proof Using "Type".
(** A general logically atomic interface for a heap. *) (** A general logically atomic interface for a heap. *)
...@@ -13,13 +13,16 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap { ...@@ -13,13 +13,16 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
store : val; store : val;
cas : val; cas : val;
(* -- predicates -- *) (* -- predicates -- *)
(* name is used to associate locked with is_lock *)
mapsto (l : loc) (q: Qp) (v : val) : iProp Σ; mapsto (l : loc) (q: Qp) (v : val) : iProp Σ;
(* -- general properties -- *) (* -- mapsto properties -- *)
mapsto_timeless l q v : Timeless (mapsto l q v); mapsto_timeless l q v :> Timeless (mapsto l q v);
mapsto_fractional l v :> Fractional (λ q, mapsto l q v);
mapsto_as_fractional l q v :>
AsFractional (mapsto l q v) (λ q, mapsto l q v) q;
mapsto_agree l q1 q2 v1 v2 :> mapsto l q1 v1 - mapsto l q2 v2 - v1 = v2;
(* -- operation specs -- *) (* -- operation specs -- *)
alloc_spec v : alloc_spec e v :
{{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}}; IntoVal e v {{{ True }}} alloc e {{{ l, RET #l; mapsto l 1 v }}};
load_spec (l : loc) : load_spec (l : loc) :
<<< (v : val) q, mapsto l q v >>> load #l @ <<< mapsto l q v, RET v >>>; <<< (v : val) q, mapsto l q v >>> load #l @ <<< mapsto l q v, RET v >>>;
store_spec (l : loc) (e : expr) (w : val) : store_spec (l : loc) (e : expr) (w : val) :
...@@ -69,10 +72,10 @@ Definition primitive_cas : val := ...@@ -69,10 +72,10 @@ Definition primitive_cas : val :=
Section proof. Section proof.
Context `{!heapG Σ}. Context `{!heapG Σ}.
Lemma primitive_alloc_spec v : Lemma primitive_alloc_spec e v :
{{{ True }}} primitive_alloc v {{{ l, RET #l; l v }}}. IntoVal e v {{{ True }}} primitive_alloc e {{{ l, RET #l; l v }}}.
Proof. Proof.
iIntros (Φ) "_ HΦ". wp_let. wp_alloc l. iApply "HΦ". done. iIntros (<- Φ) "_ HΦ". wp_let. wp_alloc l. iApply "HΦ". done.
Qed. Qed.
Lemma primitive_load_spec (l : loc) : Lemma primitive_load_spec (l : loc) :
...@@ -114,4 +117,5 @@ Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ := ...@@ -114,4 +117,5 @@ Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
{| alloc_spec := primitive_alloc_spec; {| alloc_spec := primitive_alloc_spec;
load_spec := primitive_load_spec; load_spec := primitive_load_spec;
store_spec := primitive_store_spec; store_spec := primitive_store_spec;
cas_spec := primitive_cas_spec |}. cas_spec := primitive_cas_spec;
mapsto_agree := gen_heap.mapsto_agree |}.
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