atomic_sync.v 4.14 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1

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

(** The simple syncer spec in [sync.v] implies a logically atomic spec. *)
Zhen Zhang's avatar
Zhen Zhang committed
9

10
Definition syncR := prodR fracR (agreeR valC). (* track the local knowledge of ghost state *)
Zhen Zhang's avatar
Zhen Zhang committed
11 12 13 14 15 16 17
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.
18 19 20
  Context `{EqDecision A, !heapG Σ, !lockG Σ}.
  Canonical AC := leibnizC A.
  Context `{!inG Σ (prodR fracR (agreeR AC))}.
Zhen Zhang's avatar
Zhen Zhang committed
21

Ralf Jung's avatar
Ralf Jung committed
22 23
  (* TODO: Rename and make opaque; the fact that this is a half should not be visible
           to the user. *)
24
  Definition gHalf (γ: gname) g : iProp Σ := own γ ((1/2)%Qp, to_agree g).
Zhen Zhang's avatar
Zhen Zhang committed
25

Ralf Jung's avatar
Ralf Jung committed
26
  Definition atomic_seq_spec (ϕ: A  iProp Σ) α β (f x: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
27
    ( g, {{ ϕ g  α g }} f x {{ v,  g', ϕ g'  β g g' v }})%I.
28

Ralf Jung's avatar
Ralf Jung committed
29 30 31
  (* TODO: Provide better masks. ∅ as inner mask is pretty weak. *)
  Definition atomic_synced (ϕ: A  iProp Σ) γ (f f': val) :=
    (  α β (x: val), atomic_seq_spec ϕ α β f x 
Ralf Jung's avatar
Ralf Jung committed
32
                       <<<  g, gHalf γ g   α g >>> f' x @  <<<  v,  g', gHalf γ g'  β g g' v, RET v >>>)%I.
Zhen Zhang's avatar
Zhen Zhang committed
33

Ralf Jung's avatar
Ralf Jung committed
34 35 36 37 38 39 40 41 42
  (* TODO: Use our usual style with a generic post-condition. *)
  (* TODO: We could get rid of the x, and hard-code a unit. That would
     be no loss in expressiveness, but probably more annoying to apply.
     How much more annoying? And how much to we gain in terms of things
     becomign easier to prove? *)
  (* This is really the core of the spec: It says that executing `s` on `f`
     turns the sequential spec with f, α, β into the concurrent triple with f', α, β. *)
  Definition is_atomic_syncer (ϕ: A  iProp Σ) γ (s: val) := 
    (  (f: val), WP s f {{ f', atomic_synced ϕ γ f f' }})%I.
43

Ralf Jung's avatar
Ralf Jung committed
44 45
  Definition atomic_syncer_spec (mk_syncer: val) :=
     (g0: A) (ϕ: A  iProp Σ),
46
      {{{ ϕ g0 }}} mk_syncer #() {{{ γ s, RET s; gHalf γ g0  is_atomic_syncer ϕ γ s }}}.
Ralf Jung's avatar
Ralf Jung committed
47 48

  Lemma atomic_spec (mk_syncer: val):
49
      mk_syncer_spec mk_syncer  atomic_syncer_spec mk_syncer.
Zhen Zhang's avatar
Zhen Zhang committed
50
  Proof.
51
    iIntros (Hsync g0 ϕ ret) "Hϕ Hret".
52 53
    iMod (own_alloc (((1 / 2)%Qp, to_agree g0)  ((1 / 2)%Qp, to_agree g0))) as (γ) "[Hg1 Hg2]".
    { by rewrite pair_op agree_idemp. }
54
    iApply (Hsync ( g: A, ϕ g  gHalf γ g)%I with "[Hg1 Hϕ]")=>//.
Zhen Zhang's avatar
Zhen Zhang committed
55
    { iExists g0. by iFrame. }
Ralf Jung's avatar
Ralf Jung committed
56 57 58 59
    iNext. iIntros (s) "#Hsyncer". iApply "Hret".
    iSplitL "Hg2"; first done. iIntros "!#".
    iIntros (f). iApply wp_wand_r. iSplitR; first by iApply "Hsyncer".
    iIntros (f') "#Hsynced {Hsyncer}".
Ralf Jung's avatar
Ralf Jung committed
60 61
    iAlways. iIntros (α β x) "#Hseq". change (ofe_car AC) with A.
    iApply wp_atomic_intro. iIntros (Φ') "?".
Ralf Jung's avatar
Ralf Jung committed
62
    (* TODO: Why can't I iApply "Hsynced"? *)
Ralf Jung's avatar
Ralf Jung committed
63 64 65
    iSpecialize ("Hsynced" $! _ Φ' x).
    iApply wp_wand_r. iSplitL.
    - iApply ("Hsynced" with "[]")=>//; last iAccu.
66
      iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ Hg1]".
67
      (* we should view shift at this point *)
Ralf Jung's avatar
Ralf Jung committed
68
      iApply fupd_wp. iMod "HP" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
Ralf Jung's avatar
Ralf Jung committed
69
      iDestruct (m_frag_agree with "Hg1 Hg2") as %Heq. subst.
Ralf Jung's avatar
Ralf Jung committed
70
      iMod ("Hvs1" with "[Hg2]") as "HP"; first by iFrame.
Ralf Jung's avatar
Ralf Jung committed
71 72 73
      iModIntro. iApply wp_fupd. iApply wp_wand_r. iSplitL "Hϕ".
      { iApply "Hseq". iFrame. done. }
      iIntros (v) "H". iDestruct "H" as (g') "[Hϕ' Hβ]".
Ralf Jung's avatar
Ralf Jung committed
74
      iMod ("HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
Ralf Jung's avatar
Ralf Jung committed
75
      iSpecialize ("Hvs2" $! v).
Ralf Jung's avatar
Ralf Jung committed
76
      iDestruct (m_frag_agree' with "Hg'' Hg1") as "[Hg %]". subst.
77
      rewrite Qp_div_2.
78
      iAssert (|==> own γ (((1 / 2)%Qp, to_agree g')  ((1 / 2)%Qp, to_agree g')))%I
Ralf Jung's avatar
Ralf Jung committed
79
              with "[Hg]" as ">[Hg1 Hg2]".
80
      { iApply own_update; last by iAssumption.
81
        apply cmra_update_exclusive. by rewrite pair_op agree_idemp. }
Ralf Jung's avatar
Ralf Jung committed
82
      iMod ("Hvs2" with "[Hg1 Hβ]").
83
      { iExists g'. iFrame. }
84
      iModIntro. iSplitL "Hg2 Hϕ'"; last done.
Zhen Zhang's avatar
Zhen Zhang committed
85
      iExists g'. by iFrame.
Ralf Jung's avatar
Ralf Jung committed
86
    - iIntros (?) "?". done.
Zhen Zhang's avatar
Zhen Zhang committed
87
  Qed.
88

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