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

Zhen Zhang's avatar
Zhen Zhang committed
2
From iris.program_logic Require Export weakestpre hoare.
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
5
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 sync misc.
Zhen Zhang's avatar
Zhen Zhang committed
7

Zhen Zhang's avatar
Zhen Zhang committed
8
Definition syncR := prodR fracR (dec_agreeR val). (* track the local knowledge of ghost state *)
Zhen Zhang's avatar
Zhen Zhang committed
9
10
11
12
13
14
15
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

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

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

Ralf Jung's avatar
Ralf Jung committed
25
26
27
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 
                       atomic_triple (fun g => gHalf γ g   α g)%I
                                     (fun g v =>  g', gHalf γ g'  β g g' v)%I
                                       (f' x))%I.
Zhen Zhang's avatar
Zhen Zhang committed
31

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

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

  Lemma atomic_spec (mk_syncer: val):
      mk_syncer_spec N mk_syncer  atomic_syncer_spec mk_syncer.
Zhen Zhang's avatar
Zhen Zhang committed
49
  Proof.
Ralf Jung's avatar
Ralf Jung committed
50
    iIntros (Hsync g0 ϕ HN ret) "[#Hh Hϕ] Hret".
Ralf Jung's avatar
Ralf Jung committed
51
    iMod (own_alloc (((1 / 2)%Qp, DecAgree g0)  ((1 / 2)%Qp, DecAgree g0))) as (γ) "[Hg1 Hg2]".
Zhen Zhang's avatar
Zhen Zhang committed
52
    { by rewrite pair_op dec_agree_idemp. }
Ralf Jung's avatar
Ralf Jung committed
53
    iApply (Hsync ( g: A, ϕ g  gHalf γ g)%I with "[$Hh 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
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}".
    iAlways. iIntros (α β x) "#Hseq".
60
    iIntros (P Q) "#Hvss !# HP".
Ralf Jung's avatar
Ralf Jung committed
61
    (* TODO: Why can't I iApply "Hsynced"? *)
62
    iSpecialize ("Hsynced" $! P Q x).
Ralf Jung's avatar
Ralf Jung committed
63
    iApply wp_wand_r. iSplitL "HP".
64
65
    - iApply ("Hsynced" with "[]")=>//.
      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
68
      iDestruct ("Hvss" with "HP") as "Hvss'". iApply fupd_wp.
      iMod "Hvss'". iDestruct "Hvss'" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
Zhen Zhang's avatar
Zhen Zhang committed
69
      iDestruct (m_frag_agree with "[Hg1 Hg2]") as %Heq; first iFrame. 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 ("Hvss" with "HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
Ralf Jung's avatar
Ralf Jung committed
75
      iSpecialize ("Hvs2" $! v).
76
77
      iDestruct (m_frag_agree' with "[Hg'' Hg1]") as "[Hg %]"; first iFrame. subst.
      rewrite Qp_div_2.
Ralf Jung's avatar
Ralf Jung committed
78
79
      iAssert (|==> own γ (((1 / 2)%Qp, DecAgree g')  ((1 / 2)%Qp, DecAgree g')))%I
              with "[Hg]" as ">[Hg1 Hg2]".
80
      { iApply own_update; last by iAssumption.
Zhen Zhang's avatar
Zhen Zhang committed
81
        apply cmra_update_exclusive. by rewrite pair_op dec_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.