simple_sync.v 1.23 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1 2
(* Coarse-grained syncer *)

Zhen Zhang's avatar
Zhen Zhang committed
3
From iris.program_logic Require Export weakestpre hoare.
Zhen Zhang's avatar
Zhen Zhang committed
4
From iris.heap_lang Require Export lang proofmode notation.
Zhen Zhang's avatar
Zhen Zhang committed
5
From iris.heap_lang.lib Require Import spin_lock.
Ralf Jung's avatar
Ralf Jung committed
6
From iris.algebra Require Import frac.
Zhen Zhang's avatar
Zhen Zhang committed
7
From iris_atomic Require Import sync.
Zhen Zhang's avatar
Zhen Zhang committed
8 9 10
Import uPred.

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

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