atomic_sync.v 4.13 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.program_logic Require Export weakestpre hoare atomic.
Zhen Zhang's avatar
Zhen Zhang committed
2
From iris.heap_lang Require Export lang proofmode notation.
Zhen Zhang's avatar
Zhen Zhang committed
3
From iris.heap_lang.lib Require Import spin_lock.
4
From iris.algebra Require Import agree frac.
5
From iris_examples.logatom.flat_combiner Require Import sync misc.
Ralf Jung's avatar
Ralf Jung committed
6 7

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

9
Definition syncR := prodR fracR (agreeR valC). (* track the local knowledge of ghost state *)
Zhen Zhang's avatar
Zhen Zhang committed
10 11 12 13
Class syncG Σ := sync_tokG :> inG Σ syncR.
Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].

Instance subG_syncΣ {Σ} : subG syncΣ Σ  syncG Σ.
Ralf Jung's avatar
Ralf Jung committed
14
Proof. solve_inG. Qed.
Zhen Zhang's avatar
Zhen Zhang committed
15 16

Section atomic_sync.
17 18 19
  Context `{EqDecision A, !heapG Σ, !lockG Σ}.
  Canonical AC := leibnizC A.
  Context `{!inG Σ (prodR fracR (agreeR AC))}.
Zhen Zhang's avatar
Zhen Zhang committed
20

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

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

Ralf Jung's avatar
Ralf Jung committed
28 29 30
  (* 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
31
                       <<<  g, gHalf γ g   α g >>> f' x @  <<<  v,  g', gHalf γ g'  β g g' v, RET v >>>)%I.
Zhen Zhang's avatar
Zhen Zhang committed
32

Ralf Jung's avatar
Ralf Jung committed
33 34 35 36 37 38 39 40 41
  (* 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.
42

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

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

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