Commit b115ff3f authored by Ralf Jung's avatar Ralf Jung

use lock-based opaqueness for everything in heap_lang

parent 659b1a56
Pipeline #3234 passed with stage
in 10 minutes and 53 seconds
......@@ -4,15 +4,13 @@ From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
locked (λ: "v", if: "v" #() then #() else #0 #0)%V. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, v = #true Φ #() }} WP assert: e @ E {{ Φ }}.
Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iIntros "HΦ". rewrite /assert -lock. wp_let. wp_seq.
iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
Global Opaque assert.
From iris.heap_lang Require Export notation.
Definition newbarrier : val := λ: <>, ref #false.
Definition signal : val := λ: "x", "x" <- #true.
Definition newbarrier : val := locked (λ: <>, ref #false)%V.
Definition signal : val := locked (λ: "x", "x" <- #true)%V.
Definition wait : val :=
rec: "wait" "x" := if: !"x" then #() else "wait" "x".
Global Opaque newbarrier signal wait.
locked (rec: "wait" "x" := if: !"x" then #() else "wait" "x")%V.
......@@ -22,8 +22,6 @@ Section proof.
Context `{!heapG Σ, !barrierG Σ} (N : namespace).
Implicit Types I : gset gname.
Local Transparent newbarrier signal wait.
Definition ress (P : iProp Σ) (I : gset gname) : iProp Σ :=
( Ψ : gname iProp Σ,
(P - [ set] i I, Ψ i) [ set] i I, saved_prop_own i (Ψ i))%I.
......@@ -97,7 +95,7 @@ Lemma newbarrier_spec (P : iProp Σ) :
{{{ heap_ctx }}} newbarrier #() {{{ l, RET #l; recv l P send l P }}}.
Proof.
iIntros (HN Φ) "#? HΦ".
rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
rewrite -wp_fupd /newbarrier -lock /=. wp_seq. wp_alloc l as "Hl".
iApply ("HΦ" with ">[-]").
iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
......@@ -121,7 +119,7 @@ Qed.
Lemma signal_spec l P :
{{{ send l P P }}} signal #l {{{ RET #(); True }}}.
Proof.
rewrite /signal /send /barrier_ctx /=.
rewrite /signal /send /barrier_ctx -lock /=.
iIntros (Φ) "(Hs&HP) HΦ"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
......
......@@ -5,11 +5,11 @@ Import uPred.
Definition parN : namespace := nroot .@ "par".
Definition par : val :=
λ: "fs",
locked (λ: "fs",
let: "handle" := spawn (Fst "fs") in
let: "v2" := Snd "fs" #() in
let: "v1" := join "handle" in
("v1", "v2").
("v1", "v2"))%V.
Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
Section proof.
......@@ -26,7 +26,7 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp
WP par e {{ Φ }}.
Proof.
iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
rewrite /par. wp_value. wp_let. wp_proj.
rewrite /par -lock. wp_value. wp_let. wp_proj.
wp_apply (spawn_spec parN with "[$Hh $Hf1]"); try wp_done; try solve_ndisj.
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
......
......@@ -5,15 +5,15 @@ From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
Definition spawn : val :=
λ: "f",
locked (λ: "f",
let: "c" := ref NONE in
Fork ("c" <- SOME ("f" #())) ;; "c".
Fork ("c" <- SOME ("f" #())) ;; "c")%V.
Definition join : val :=
rec: "join" "c" :=
locked (rec: "join" "c" :=
match: !"c" with
SOME "x" => "x"
| NONE => "join" "c"
end.
end)%V.
(** The CMRA & functor we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
......@@ -50,7 +50,7 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
heapN N
{{{ heap_ctx WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
Proof.
iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn /=.
iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn -lock /=.
wp_let. wp_alloc l as "Hl". wp_let.
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
......@@ -78,4 +78,3 @@ Qed.
End proof.
Typeclasses Opaque join_handle.
Global Opaque spawn join.
......@@ -5,11 +5,11 @@ From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
From iris.heap_lang.lib Require Import lock.
Definition newlock : val := λ: <>, ref #false.
Definition try_acquire : val := λ: "l", CAS "l" #false #true.
Definition newlock : val := ssreflect.locked (λ: <>, ref #false)%V.
Definition try_acquire : val := ssreflect.locked (λ: "l", CAS "l" #false #true)%V.
Definition acquire : val :=
rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false.
ssreflect.locked (rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l")%V.
Definition release : val := ssreflect.locked (λ: "l", "l" <- #false)%V.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
......@@ -48,7 +48,7 @@ Section proof.
heapN N
{{{ heap_ctx R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock /=.
iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock. unlock.
wp_seq. wp_alloc l as "Hl".
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
......@@ -83,13 +83,12 @@ Section proof.
Proof.
iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
rewrite /release. unlock. wp_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed.
End proof.
Typeclasses Opaque is_lock locked.
Global Opaque newlock try_acquire acquire release.
Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
......
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