atomic_sync.v 4.48 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 atomic misc.
Zhen Zhang's avatar
Zhen Zhang committed
7 8 9 10 11 12 13 14 15

Definition syncR := prodR fracR (dec_agreeR val).
Class syncG Σ := sync_tokG :> inG Σ syncR.
Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].

Instance subG_syncΣ {Σ} : subG syncΣ Σ  syncG Σ.
Proof. by intros ?%subG_inG. Qed.

Section atomic_sync.
16
  Context `{EqDecision A, !heapG Σ, !lockG Σ, !inG Σ (prodR fracR (dec_agreeR A))} (N : namespace).
Zhen Zhang's avatar
Zhen Zhang committed
17 18 19 20 21 22 23 24

  Definition gHalf (γ: gname) g : iProp Σ := own γ ((1/2)%Qp, DecAgree g).

  Definition atomic_triple'
             (α: val  iProp Σ)
             (β: val  A  A  val  iProp Σ)
             (Ei Eo: coPset)
             (f x: val) γ : iProp Σ :=
25 26 27 28 29 30
    ( P Q, atomic_triple_base A (fun g => gHalf γ g   α x)
                                 (fun g v =>  g':A, gHalf γ g'  β x g g' v)
                                 Ei Eo
                                (f x) (P x) (fun _ => Q x))%I.
       
  Definition sync (mk_syncer: val) : val :=
Zhen Zhang's avatar
Zhen Zhang committed
31
    λ: "f_cons" "f_seq" "l",
32 33
       let: "s" := mk_syncer #() in
       "s" ("f_seq" "l").
Zhen Zhang's avatar
Zhen Zhang committed
34 35 36 37 38 39 40 41 42 43

  Definition seq_spec (f: val) (ϕ: val  A  iProp Σ) α β (E: coPset) :=
       (Φ: val  iProp Σ) (l: val),
         {{ True }} f l {{ f',  ( (x: val) (Φ: val  iProp Σ) (g: A),
                               heapN  N 
                               heap_ctx  ϕ l g   α x 
                               ( (v: val) (g': A), ϕ l g' - β x g g' v - |={E}=> Φ v)
                                WP f' x @ E {{ Φ }} )}}.

  Definition synced R (f' f: val) :=
44 45 46 47
    (  P Q (x: val), ({{ R  P x }} f x {{ v, R  Q x v }})  ({{ P x }} f' x {{ v, Q x v }}))%I.

  Definition is_syncer (R: iProp Σ) (s: val) :=
    ( (f : val), WP s f {{ f', synced R f' f }})%I.
Zhen Zhang's avatar
Zhen Zhang committed
48

49 50 51 52
  Definition mk_syncer_spec (mk_syncer: val) :=
     (R: iProp Σ) (Φ: val -> iProp Σ),
      heapN  N 
      heap_ctx  R  ( s,  (is_syncer R s) - Φ s)  WP mk_syncer #() {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
53
  
Zhen Zhang's avatar
Zhen Zhang committed
54
  Lemma atomic_spec (mk_syncer f_cons f_seq l: val) (ϕ: val  A  iProp Σ) α β Ei:
Zhen Zhang's avatar
Zhen Zhang committed
55
       (g0: A),
Zhen Zhang's avatar
Zhen Zhang committed
56
        heapN  N  seq_spec f_seq ϕ α β  
57
        mk_syncer_spec mk_syncer 
Zhen Zhang's avatar
Zhen Zhang committed
58 59
        heap_ctx  ϕ l g0
         WP (sync mk_syncer) f_cons f_seq l {{ f,  γ, gHalf γ g0   x,  atomic_triple' α β Ei  f x γ  }}.
Zhen Zhang's avatar
Zhen Zhang committed
60
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
61 62 63 64
    iIntros (g0 HN Hseq Hsync) "[#Hh Hϕ]".
    iVs (own_alloc (((1 / 2)%Qp, DecAgree g0)  ((1 / 2)%Qp, DecAgree g0))) as (γ) "[Hg1 Hg2]".
    { by rewrite pair_op dec_agree_idemp. }
    repeat wp_let. wp_bind (mk_syncer _).
65
    iApply (Hsync ( g: A, ϕ l g  gHalf γ g)%I)=>//. iFrame "Hh".
Zhen Zhang's avatar
Zhen Zhang committed
66
    iSplitL "Hg1 Hϕ".
Zhen Zhang's avatar
Zhen Zhang committed
67
    { iExists g0. by iFrame. }
68 69 70 71 72 73 74
    iIntros (s) "#Hsyncer".
    wp_let. wp_bind (f_seq _). iApply wp_wand_r.
    iSplitR; first by iApply (Hseq with "[]")=>//.
    iIntros (f) "%".
    iApply wp_wand_r.
    iSplitR; first iApply "Hsyncer".
    iIntros (f') "#Hsynced".
Zhen Zhang's avatar
Zhen Zhang committed
75 76 77 78 79
    iExists γ. iFrame.
    iIntros (x). iAlways.
    rewrite /atomic_triple'.
    iIntros (P Q) "#Hvss".
    rewrite /synced.
80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
    iSpecialize ("Hsynced" $! P Q x). 
    iIntros "!# HP". iApply wp_wand_r. iSplitL "HP".
    - iApply ("Hsynced" with "[]")=>//.
      iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ Hg1]".
      (* we should view shift at this point *) 
      iDestruct ("Hvss" with "HP") as "Hvss'". iApply pvs_wp.
      iVs "Hvss'". iDestruct "Hvss'" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
      iVs ("Hvs1" with "[Hg2]") as "HP"; first by iFrame.
      iVsIntro. iApply H=>//.
      iFrame "Hh Hϕ". iSplitR; first done. iIntros (ret g') "Hϕ' Hβ".
      iVs ("Hvss" with "HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
      iSpecialize ("Hvs2" $! ret).
      iDestruct (m_frag_agree' with "[Hg'' Hg1]") as "[Hg %]"; first iFrame. subst.
      rewrite Qp_div_2.
      iAssert (|=r=> own γ (((1 / 2)%Qp, DecAgree g')  ((1 / 2)%Qp, DecAgree g')))%I
              with "[Hg]" as "==>[Hg1 Hg2]".
      { iApply own_update; last by iAssumption.
Zhen Zhang's avatar
Zhen Zhang committed
97
        apply cmra_update_exclusive. by rewrite pair_op dec_agree_idemp. }
98 99 100 101 102 103
      iVs ("Hvs2" with "[Hg1 Hβ]").
      { iExists g'. iFrame. }
      iVsIntro. iSplitL "Hg2 Hϕ'".
      * iExists g'. by iFrame.
      * done.
    - iIntros (?) "?". by iExists g0.
Zhen Zhang's avatar
Zhen Zhang committed
104
  Qed.
105

Zhen Zhang's avatar
Zhen Zhang committed
106
End atomic_sync.