atomic_pcas.v 3.04 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
4
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import dec_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
10
  Context `{!heapG Σ, !lockG Σ, !syncG Σ,
            !inG Σ (prodR fracR (dec_agreeR (val * val)))} (N : namespace).
Zhen Zhang's avatar
Zhen Zhang committed
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
  
  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.

  Definition α (x: val) : iProp Σ := ( a b: val, x = (a, b)%V)%I.
  
  Definition ϕ (ls: val) (xs: val) : iProp Σ :=
    ( (l1 l2: loc) (x1 x2: val),
       ls = (#l1, #l2)%V  xs = (x1, x2)%V  l1  x1  l2  x2)%I.

  Definition β (ab: val) (xs xs': val) (v: val) : iProp Σ :=
    (  a b x1 x2 x1' x2': val,
         ab = (a, b)%V  xs = (x1, x2)%V  xs' = (x1', x2')%V 
         ((v = #true   x1 = a  x2 = a  x1' = b  x2' = b) 
          (v = #false  (x1  a  x2  a)  xs = xs')))%I.

  Local Opaque β.
  
  Lemma pcas_seq_spec: seq_spec N pcas_seq ϕ α β .
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
38
    iIntros (_ l) "!# _". wp_seq. iVsIntro. iPureIntro.
39
    iIntros (x Φ g HN) "(#Hh & Hg & #Hα & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
40
41
42
43
44
45
46
47
48
49
50
    iDestruct "Hg" as (l1 l2 x1 x2) "(% & % & Hl1 & Hl2)".
    iDestruct "Hα" as (a b) "%".
    subst. simpl. wp_let. wp_proj. wp_load. wp_proj.
    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
51
52
53
        rewrite /β. iPureIntro.
        exists a, b, a, a, b, b.
        repeat (split; first done). left. eauto.
Zhen Zhang's avatar
Zhen Zhang committed
54
55
56
57
      + 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
58
59
60
        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
61
62
63
      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
64
65
66
      rewrite /β. iPureIntro.
      exists a, b, x1, x2, x1, x2.
      repeat (split; first done). right. eauto.
Zhen Zhang's avatar
Zhen Zhang committed
67
68
  Qed.

Zhen Zhang's avatar
Zhen Zhang committed
69
70
71
72
  Lemma pcas_atomic_spec (mk_syncer: val) (l1 l2: loc) (x1 x2: val) :
    heapN  N  mk_syncer_spec N mk_syncer 
    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
73
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
74
75
    iIntros (HN Hmk_syncer) "(#Hh & Hl1 & Hl2)".
    iDestruct (atomic_spec with "[Hl1 Hl2]") as "Hspec"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
76
    - apply pcas_seq_spec.
Zhen Zhang's avatar
Zhen Zhang committed
77
78
    - iFrame "Hh". iExists l1, l2, x1, x2. iFrame. eauto.
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
79
End atomic_pair.
Zhen Zhang's avatar
Zhen Zhang committed
80