atomic_pcas.v 3.14 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
From iris.program_logic Require Export weakestpre hoare.
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.
Ralf Jung's avatar
Ralf Jung committed
4
From iris.algebra Require Import agree frac.
Zhen Zhang's avatar
Zhen Zhang committed
5
From iris_atomic Require Import sync atomic_sync.
Zhen Zhang's avatar
Zhen Zhang committed
6 7 8
Import uPred.

Section atomic_pair.
Zhen Zhang's avatar
Zhen Zhang committed
9
  Context `{!heapG Σ, !lockG Σ, !syncG Σ,
Ralf Jung's avatar
Ralf Jung committed
10
            !inG Σ (prodR fracR (agreeR (prodC valC valC)))} (N : namespace).
Zhen Zhang's avatar
Zhen Zhang committed
11 12 13 14 15 16 17 18 19 20 21
  
  Definition pcas_seq : val :=
    λ: "ls" "ab",
       if: !(Fst "ls") = Fst "ab"
         then if: !(Snd "ls") = Fst "ab"
                then Fst "ls" <- Snd "ab";; Snd "ls" <- Snd "ab";; #true
                else #false
         else #false.

  Local Opaque pcas_seq.

22
  Definition α (x: val) (_: val) : iProp Σ := ( a b: val, x = (a, b)%V)%I.
Zhen Zhang's avatar
Zhen Zhang committed
23 24 25
  
  Definition ϕ (ls: val) (xs: val) : iProp Σ :=
    ( (l1 l2: loc) (x1 x2: val),
26
       ls = (#l1, #l2)%V  xs = (x1, x2)%V  l1  x1  l2  x2)%I.
Zhen Zhang's avatar
Zhen Zhang committed
27 28

  Definition β (ab: val) (xs xs': val) (v: val) : iProp Σ :=
29
     a b x1 x2 x1' x2': val,
Zhen Zhang's avatar
Zhen Zhang committed
30 31
         ab = (a, b)%V  xs = (x1, x2)%V  xs' = (x1', x2')%V 
         ((v = #true   x1 = a  x2 = a  x1' = b  x2' = b) 
32
          (v = #false  (x1  a  x2  a)  xs = xs'))%I.
Zhen Zhang's avatar
Zhen Zhang committed
33 34 35

  Local Opaque β.
  
Ralf Jung's avatar
Ralf Jung committed
36 37
  (* TODO: This needs updating for the new atomic_syncer.
  Lemma pcas_seq_spec x: atomic_seq_spec ϕ α β ⊤ pcas_seq x.
Zhen Zhang's avatar
Zhen Zhang committed
38
  Proof.
39
    iIntros (_ l) "!# _". wp_seq. iPureIntro.
40
    iIntros (x Φ g HN) "(#Hh & Hg & #Hα & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
41 42
    iDestruct "Hg" as (l1 l2 x1 x2) "(% & % & Hl1 & Hl2)".
    iDestruct "Hα" as (a b) "%".
43
    subst. simpl. iApply wp_fupd. wp_let. wp_proj. wp_load. wp_proj.
Zhen Zhang's avatar
Zhen Zhang committed
44 45 46 47 48 49 50 51
    wp_op=>[?|Hx1na].
    - subst.
      wp_if. wp_proj. wp_load. wp_proj.
      wp_op=>[?|Hx2na]. subst.
      + wp_if. wp_proj. wp_proj. wp_store. wp_proj. wp_proj. wp_store.
        iDestruct ("HΦ" $! #true (b, b)%V) as "HΦ".
        iApply ("HΦ" with "[Hl1 Hl2]").
        { iExists l1, l2, b, b. iFrame. eauto. }
Zhen Zhang's avatar
Zhen Zhang committed
52 53 54
        rewrite /β. iPureIntro.
        exists a, b, a, a, b, b.
        repeat (split; first done). left. eauto.
Zhen Zhang's avatar
Zhen Zhang committed
55 56 57 58
      + wp_if.
        iDestruct ("HΦ" $! #false (a, x2)%V) as "H".
        iApply ("H" with "[Hl1 Hl2]").
        { iExists l1, l2, a, x2. iFrame. eauto. }
Zhen Zhang's avatar
Zhen Zhang committed
59 60 61
        rewrite /β. iPureIntro.
        exists a, b, a, x2, a, x2. repeat (split; first done). right. eauto.
    - subst. wp_if.
Zhen Zhang's avatar
Zhen Zhang committed
62 63 64
      iDestruct ("HΦ" $! #false (x1, x2)%V) as "H".
      iApply ("H" with "[Hl1 Hl2]").
      { iExists l1, l2, x1, x2. iFrame. eauto. }
Zhen Zhang's avatar
Zhen Zhang committed
65 66 67
      rewrite /β. iPureIntro.
      exists a, b, x1, x2, x1, x2.
      repeat (split; first done). right. eauto.
Zhen Zhang's avatar
Zhen Zhang committed
68 69
  Qed.

Zhen Zhang's avatar
Zhen Zhang committed
70 71
  Lemma pcas_atomic_spec (mk_syncer: val) (l1 l2: loc) (x1 x2: val) :
    heapN ⊥ N → mk_syncer_spec N mk_syncer →
Zhen Zhang's avatar
Zhen Zhang committed
72 73
    heap_ctx ∗ l1 ↦ x1 ∗ l2 ↦ x2
    ⊢ WP sync mk_syncer pcas_seq (LitV l1, LitV l2)%V {{ f, ∃ γ, gHalf γ (x1, x2)%V ∗ ∀ x, □ atomic_triple' α β ⊤ ⊤ f x γ  }}.
Zhen Zhang's avatar
Zhen Zhang committed
74
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
75 76
    iIntros (HN Hmk_syncer) "(#Hh & Hl1 & Hl2)".
    iDestruct (atomic_spec with "[Hl1 Hl2]") as "Hspec"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
77
    - apply pcas_seq_spec.
Zhen Zhang's avatar
Zhen Zhang committed
78
    - iFrame "Hh". iExists l1, l2, x1, x2. iFrame. eauto.
Ralf Jung's avatar
Ralf Jung committed
79
  Qed.*)
Zhen Zhang's avatar
Zhen Zhang committed
80
End atomic_pair.
Zhen Zhang's avatar
Zhen Zhang committed
81