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

define logically atomic heap and instantiate it with physical heap

parent 75c98fae
...@@ -85,6 +85,7 @@ theories/heap_lang/lib/lock.v ...@@ -85,6 +85,7 @@ theories/heap_lang/lib/lock.v
theories/heap_lang/lib/spin_lock.v theories/heap_lang/lib/spin_lock.v
theories/heap_lang/lib/ticket_lock.v theories/heap_lang/lib/ticket_lock.v
theories/heap_lang/lib/counter.v theories/heap_lang/lib/counter.v
theories/heap_lang/lib/atomic_heap.v
theories/heap_lang/proofmode.v theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v theories/heap_lang/adequacy.v
theories/heap_lang/total_adequacy.v theories/heap_lang/total_adequacy.v
......
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.proofmode Require Import tactics.
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 {
(* -- operations -- *)
alloc : val;
load : val;
store : val;
(* -- predicates -- *)
(* name is used to associate locked with is_lock *)
mapsto (l : loc) (q: Qp) (v : val) : iProp Σ;
(* -- general properties -- *)
mapsto_timeless l q v : Timeless (mapsto l q v);
(* -- operation specs -- *)
alloc_spec v :
{{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
load_spec (l : loc) :
atomic_wp (load #l)%E
(λ '(v, q), mapsto l q v)
(λ '(v, q) (_:()), mapsto l q v)
(λ '(v, q) _, v);
store_spec (l : loc) (w : val) :
atomic_wp (store (#l, w))%E
(λ v, mapsto l 1 v)
(λ v (_:()), mapsto l 1 w)
(λ _ _, #()%V);
}.
(** Proof that the primitive physical operations of heap_lang satisfy said interface. *)
Definition primitive_alloc : val :=
λ: "v", ref "v".
Definition primitive_load : val :=
λ: "l", !"l".
Definition primitive_store : val :=
λ: "p", (Fst "p") <- (Snd "p").
Section proof.
Context `{!heapG Σ}.
Lemma primitive_alloc_spec v :
{{{ True }}} primitive_alloc v {{{ l, RET #l; l v }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_let. wp_alloc l. iApply "HΦ". done.
Qed.
Lemma primitive_load_spec (l : loc) :
atomic_wp (primitive_load #l)%E
(λ '(v, q), l {q} v)%I
(λ '(v, q) (_:()), l {q} v)%I
(λ '(v, q) _, v).
Proof.
iIntros (Φ) "Aupd". wp_let.
iMod (aupd_acc with "Aupd") as ((v, q)) "[H↦ [_ Hclose]]"; first solve_ndisj.
wp_load. iMod ("Hclose" $! () with "H↦"). done.
Qed.
Lemma primitive_store_spec (l : loc) (w : val) :
atomic_wp (primitive_store (#l, w))%E
(λ v, l v)%I
(λ v (_:()), l w)%I
(λ _ _, #()%V).
Proof.
iIntros (Φ) "Aupd". wp_let. wp_proj. wp_proj.
iMod (aupd_acc with "Aupd") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
wp_store. iMod ("Hclose" $! () with "H↦"). done.
Qed.
Definition primitive_atomic_heap : atomic_heap Σ :=
{| alloc_spec := primitive_alloc_spec;
load_spec := primitive_load_spec;
store_spec := primitive_store_spec |}.
End proof.
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics classes. From iris.proofmode Require Import tactics classes.
From iris.bi.lib Require Import atomic. From iris.bi.lib Require Export atomic.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Definition atomic_wp `{irisG Λ Σ} {A B : Type} Definition atomic_wp `{irisG Λ Σ} {A B : Type}
...@@ -13,4 +13,4 @@ Definition atomic_wp `{irisG Λ Σ} {A B : Type} ...@@ -13,4 +13,4 @@ Definition atomic_wp `{irisG Λ Σ} {A B : Type}
( Φ, atomic_update α β Eo Em (λ x y, Φ (f x y)) - ( Φ, atomic_update α β Eo Em (λ x y, Φ (f x y)) -
WP e {{ Φ }})%I. WP e {{ Φ }})%I.
(* Note: To add a private postcondition, use (* Note: To add a private postcondition, use
atomic_shift α β Eo Em (λ x y, POST x y -∗ Φ (f x y)) *) atomic_update α β Eo Em (λ x y, POST x y -∗ Φ (f x y)) *)
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