double.v 6.18 KB
Newer Older
Daniël Louwrink's avatar
Daniël Louwrink committed
1 2 3 4 5 6 7 8 9 10 11
(** This file contains a proof that the program

  λ c, (recv c ||| recv c)

can be assigned the semantic type

  chan (?int.?int.end) ⊸ (int * int)

This cannot be shown directly using the semantic typing rules, and therefore
manual proof is used to show that the program is semantically well-typed. This
demonstrates the extensibility of the type system. *)
12
From iris.algebra Require Import frac auth excl updates.
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14
From iris.heap_lang.lib Require Export par spin_lock.
From actris.channel Require Import proofmode.
Robbert Krebbers's avatar
Rename.  
Robbert Krebbers committed
15
From actris.logrel Require Export term_typing_judgment session_types.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
From actris.logrel Require Import environments.
17 18 19

Definition prog : val := λ: "c",
  let: "lock" := newlock #() in
20
  (
21 22 23 24 25 26 27 28 29
    acquire "lock";;
    let: "x1" := recv "c" in
    release "lock";;
    "x1"
  ) ||| (
    acquire "lock";;
    let: "x2" := recv "c" in
    release "lock";;
    "x2"
30
  ).
31

32
Section double.
33 34
  Context `{!heapG Σ, !chanG Σ, !spawnG Σ}.
  Context `{!inG Σ (exclR unitO), inG Σ (prodR fracR (agreeR (optionO valO)))}.
35

36 37
  Definition prog_prot (P : val  val  iProp Σ) : iProto Σ :=
    (<? (v1 : val)> MSG v1; <? (v2 : val)> MSG v2 {{ P v1 v2 }}; END)%proto.
38

39 40 41 42 43 44 45 46
  Definition chan_inv (γ γ1 γ2 : gname) (P : val  val  iProp Σ) (c : val) : iProp Σ :=
    (own γ (Excl ())  c  prog_prot P 
     ( b v1,
       own (if b : bool then γ1 else γ2) (3/4, to_agree (Some v1))%Qp 
       c  <? (v2 : val)> MSG v2 {{ P v1 v2 }}; END) 
     ( v1 v2,
       own γ1 (1/4, to_agree (Some v1))%Qp 
       own γ2 (1/4, to_agree (Some v2))%Qp))%I.
47

48 49
  Lemma wp_prog P c :
    {{{  c  prog_prot P }}}
50
      prog c
51
    {{{ v1 v2, RET (v1, v2); P v1 v2  P v2 v1 }}}.
52
  Proof.
53 54 55 56
    iIntros (Φ) "Hc HΦ". rewrite /prog.
    iMod (own_alloc (Excl ())) as (γ) "Hγ"; [done|].
    iMod (own_alloc (1, to_agree None)%Qp) as (γ1) "Hγ1"; [done|].
    iMod (own_alloc (1, to_agree None)%Qp) as (γ2) "Hγ2"; [done|].
57
    (* Create lock *)
58 59 60
    wp_apply (newlock_spec (chan_inv γ γ1 γ2 P c) with "[Hγ Hc]").
    { iLeft. by iFrame. }
    iIntros (lk γlk) "#Hlock". wp_pures.
61
    (* Fork into two threads *)
62 63 64 65 66 67 68
    wp_apply (wp_par
      (λ v1, own γ1 (1/4, to_agree (Some v1))%Qp  own γ (Excl ()) 
        ( v2, own γ1 (3/4, to_agree (Some v1))%Qp 
               own γ2 (1/2, to_agree (Some v2))%Qp  P v2 v1))%I
      (λ v2, own γ2 (1/4, to_agree (Some v2))%Qp  own γ (Excl ()) 
        ( v1, own γ2 (3/4, to_agree (Some v2))%Qp 
               own γ1 (1/2, to_agree (Some v1))%Qp  P v1 v2))%I with "[Hγ1] [Hγ2]").
69 70 71
    - (* Acquire lock *)
      wp_apply (acquire_spec with "Hlock").
      iIntros "[Hlocked Hc]". wp_pures.
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
      iDestruct "Hc" as "[[Hγ Hc]|[Hc|Hc]]".
      + wp_recv (v) as "_". wp_pures.
        iMod (own_update _ _ ((3/4  1/4), to_agree (Some v))%Qp with "Hγ1")
          as "[Hγ1a Hγ1b]"; [by apply cmra_update_exclusive|].
        wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hc]").
        { iRight. iLeft. iExists true, v. iFrame. }
        iIntros "_". wp_pures. iLeft. iFrame.
      + iDestruct "Hc" as ([] v) "[Hγ2 Hc]".
        { by iDestruct (own_valid_2 with "Hγ1 Hγ2") as %[]. }
        wp_recv (v') as "HP". wp_pures.
        iMod (own_update _ _ ((1/4  3/4), to_agree (Some v'))%Qp with "Hγ1")
          as "[Hγ1a Hγ1b]"; [by apply cmra_update_exclusive|].
        rewrite {1}(_ : 3/4 = 1/4 + 1/2)%Qp; last (by apply: bool_decide_unpack).
        iDestruct "Hγ2" as "[Hγ2a Hγ2b]".
        wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hγ2a Hc]").
        { do 2 iRight. iExists v', v. iFrame. }
        iIntros "_". wp_pures. iRight. iExists v. iFrame.
      + iDestruct "Hc" as (v v') "[Hγ1' _]".
        by iDestruct (own_valid_2 with "Hγ1 Hγ1'") as %[].
91 92 93
    - (* Acquire lock *)
      wp_apply (acquire_spec with "Hlock").
      iIntros "[Hlocked Hc]". wp_pures.
94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122
      iDestruct "Hc" as "[[Hγ Hc]|[Hc|Hc]]".
      + wp_recv (v) as "_". wp_pures.
        iMod (own_update _ _ ((3/4  1/4), to_agree (Some v))%Qp with "Hγ2")
          as "[Hγ2a Hγ2b]"; [by apply cmra_update_exclusive|].
        wp_apply (release_spec with "[$Hlock $Hlocked Hγ2a Hc]").
        { iRight. iLeft. iExists false, v. iFrame. }
        iIntros "_". wp_pures. iLeft. iFrame.
      + iDestruct "Hc" as ([] v) "[Hγ1 Hc]"; last first.
        { by iDestruct (own_valid_2 with "Hγ1 Hγ2") as %[]. }
        wp_recv (v') as "HP". wp_pures.
        iMod (own_update _ _ ((1/4  3/4), to_agree (Some v'))%Qp with "Hγ2")
          as "[Hγ2a Hγ2b]"; [by apply cmra_update_exclusive|].
        rewrite {1}(_ : 3/4 = 1/4 + 1/2)%Qp; last (by apply: bool_decide_unpack).
        iDestruct "Hγ1" as "[Hγ1a Hγ1b]".
        wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hγ2a Hc]").
        { do 2 iRight. iExists v, v'. iFrame. }
        iIntros "_". wp_pures. iRight. iExists v. iFrame.
      + iDestruct "Hc" as (v v') "(_ & Hγ2' & _)".
        by iDestruct (own_valid_2 with "Hγ2 Hγ2'") as %[].
    - iIntros (v1 v2) "[[[H1 Hγ]|H1] [[H2 Hγ']|H2]] !>".
      + by iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
      + iDestruct "H2" as (v2') "(_&H1'&HP)".
        iDestruct (own_valid_2 with "H1 H1'") as %[_ [=->]%agree_op_invL'].
        iApply "HΦ"; auto.
      + iDestruct "H1" as (v1') "(_&H2'&HP)".
        iDestruct (own_valid_2 with "H2 H2'") as %[_ [=->]%agree_op_invL'].
        iApply "HΦ"; auto.
      + iDestruct "H1" as (v1') "[H1 _]"; iDestruct "H2" as (v2') "(_&H2&_)".
        by iDestruct (own_valid_2 with "H1 H2") as %[].
123 124 125
  Qed.

  Lemma prog_typed :
126
       prog : chan (<??> TY lty_int; <??> TY lty_int; END)  lty_int * lty_int.
127 128 129
  Proof.
    iIntros (vs) "!> HΓ /=".
    iApply wp_value.
130
    iSplitL; last by iApply env_ltyped_empty.
131
    iIntros (c) "Hc".
132
    iApply (wp_prog (λ v1 v2, ltty_car lty_int v1  ltty_car lty_int v2)%I with "[Hc]").
133
    { iApply (iProto_mapsto_le _ (lsty_car (<??> TY lty_int; <??> TY lty_int; END)) with "Hc").
134 135 136 137 138
      iIntros "!> !>" (v1). iMod 1 as %[x1 ->]. iExists #x1.
      iIntros "!>" (v2). iMod 1 as %[x2 ->]. iExists #x2. iSplitL; last done.
      rewrite /ltty_car /=. auto. }
    iIntros "!>" (v1 v2 [[[k1 ->] [k2 ->]]|[[k1 ->] [k2 ->]]]);
      iExists _, _; iSplit; by eauto.
139
  Qed.
140
End double.