simple_sync.v 1.32 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1 2 3 4 5
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import dec_agree frac.
Zhen Zhang's avatar
Zhen Zhang committed
6
From iris_atomic Require Import sync.
Zhen Zhang's avatar
Zhen Zhang committed
7 8 9
Import uPred.

Definition mk_sync: val :=
10
  λ: <>,
Zhen Zhang's avatar
Zhen Zhang committed
11
       let: "l" := newlock #() in
12
       λ: "f" "x",
Zhen Zhang's avatar
Zhen Zhang committed
13 14 15 16 17 18 19 20 21 22
          acquire "l";;
          let: "ret" := "f" "x" in
          release "l";;
          "ret".

Global Opaque mk_sync.

Section syncer.
  Context `{!heapG Σ, !lockG Σ} (N: namespace).
  
23
  Lemma mk_sync_spec: mk_syncer_spec N mk_sync.
Zhen Zhang's avatar
Zhen Zhang committed
24
  Proof.
25
    iIntros (R Φ HN) "(#Hh & HR & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
26 27 28 29 30
    wp_seq. wp_bind (newlock _).
    iApply newlock_spec; first done.
    iSplitR "HR HΦ"; first done.
    iFrame "HR".
    iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#".
31 32
    iIntros (f). wp_let. iVsIntro. iAlways.
    iIntros (P Q x) "#Hf !# HP".
Zhen Zhang's avatar
Zhen Zhang committed
33 34 35 36 37 38 39 40 41 42
    wp_let. wp_bind (acquire _).
    iApply acquire_spec. iSplit; first done.
    iIntros "Hlocked R". wp_seq. wp_bind (f _).
    iDestruct ("Hf" with "[R HP]") as "Hf'"; first by iFrame.
    iApply wp_wand_r.  iSplitL "Hf'"; first done.
    iIntros (v') "[HR HQv]". wp_let. wp_bind (release _).
    iApply release_spec. iFrame "HR". iSplitR; first done.
    iFrame. by wp_seq.
  Qed.
End syncer.