parfib.v 4.27 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
(** Concurrent Runner example from
    "Modular Reasoning about Separation of Concurrent Data Structures"
    <http://www.kasv.dk/articles/hocap-ext.pdf>

Fibonaci divide-and-conquer computation
*)
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import cmra agree frac csum excl.
From iris.heap_lang.lib Require Import lock spin_lock.
From iris_examples.hocap Require Import abstract_bag shared_bag concurrent_runners.

Section contents.
  Context `{heapG Σ, !oneshotG Σ, !saG Σ}.
  Variable b : bag Σ.
  Variable N : namespace.

  Fixpoint fib (a : nat) : nat :=
    match a with
    | O => 1
    | S n =>
      match n with
      | O => 1
      | S n' => fib n + fib n'
      end
    end.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
  Arguments fib !_ / : simpl nomatch.
30 31 32 33 34 35 36 37 38 39 40 41

  Definition seqFib : val := rec: "fib" "a" :=
    if: "a" = #0
    then #1
    else if: "a" = #1
         then #1
         else ("fib" ("a"-#1)) + ("fib" ("a"-#2)).

  Lemma seqFib_spec (n : nat) :
    {{{ True }}} seqFib #n {{{ (m : nat), RET #m; fib n = m }}}.
  Proof.
    iIntros (Φ) "_ HΦ".
42
    iLöb as "IH" forall (n Φ).
Robbert Krebbers's avatar
Robbert Krebbers committed
43
    wp_rec. simpl. wp_op. case_bool_decide; simplify_eq; wp_if.
44
    { assert (n = O) as -> by lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
      by iApply ("HΦ" $! 1%nat). }
46
    wp_op. case_bool_decide; simplify_eq; wp_if.
Robbert Krebbers's avatar
Robbert Krebbers committed
47 48 49 50 51 52 53 54 55 56
    { assert (n = 1%nat) as -> by lia.
      by iApply ("HΦ" $! 1%nat). }
    wp_op. destruct n as [|[|n]]=> //.
    rewrite !Nat2Z.inj_succ.
    replace (Z.succ (Z.succ n) - 2) with (Z.of_nat n) by lia.
    wp_apply "IH". iIntros (? <-).
    wp_op.
    replace (Z.succ (Z.succ n) - 1) with (Z.of_nat (S n)) by lia.
    wp_apply "IH". iIntros (? <-). wp_op.
    rewrite -Nat2Z.inj_add. by iApply "HΦ".
57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
  Qed.

  Definition parFib : val := λ: "r" "a",
    if: "a" < #25 then seqFib "a"
    else let: "a1" := "a" - #1 in
         let: "a2" := "a" - #2 in
         let: "t1" := runner_Fork b "r" "a1" in
         let: "t2" := runner_Fork b "r" "a2" in
         (task_Join "t1") + (task_Join "t2").

  Definition fibRunner : val := λ: "n" "a",
    let: "r" := newRunner b parFib "n" in
    task_Join (runner_Fork b "r" "a").

  Definition P (v: val) : iProp Σ := ( n: nat, v = #n)%I.
  Definition Q (a v: val) : iProp Σ := ( n: nat, a = #n  v = #(fib n))%I.
  Lemma parFib_spec r γb a :
Dan Frumin's avatar
Dan Frumin committed
74
    {{{ runner b N γb P Q r  P a }}}
75 76 77 78 79
      parFib r a
    {{{ v, RET v; Q a v }}}.
  Proof.
    iIntros (Φ) "[#Hrunner HP] HΦ".
    iDestruct "HP" as (n) "%"; simplify_eq.
80
    wp_lam. wp_let. wp_op. case_bool_decide; wp_if.
81 82 83 84
    - iApply seqFib_spec; eauto.
      iNext. iIntros (? <-). iApply "HΦ".
      iExists n; done.
    - do 2 (wp_op; wp_let).
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86 87 88 89 90 91 92
      destruct n as [|[|n]]=> //.
      rewrite !Nat2Z.inj_succ.
      replace (Z.succ (Z.succ n) - 2) with (Z.of_nat n) by lia.
      replace (Z.succ (Z.succ n) - 1) with (Z.succ n) by lia.
      wp_apply (runner_Fork_spec).
      { iFrame "Hrunner". iExists (S n). by rewrite Nat2Z.inj_succ. }
      iIntros (γ1 γ1' t1) "Ht1". wp_let.
      wp_apply (runner_Fork_spec).
93
      { iFrame "Hrunner". eauto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
94 95 96
      iIntros (γ2 γ2' t2) "Ht2". wp_let.
      wp_apply (task_Join_spec with "[$Ht2]"); try done.
      iIntros (v2) "HQ"; simplify_eq.
97
      iDestruct "HQ" as (m2' m2) "%". simplify_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
98 99 100 101 102 103
      wp_apply (task_Join_spec with "[$Ht1]"); try done.
      iIntros (v1) "HQ"; simplify_eq.
      iDestruct "HQ" as (m1' m1) "%". simplify_eq.
      wp_op. iApply "HΦ". iExists (S (S m2')).
      rewrite !Nat2Z.inj_succ -Nat2Z.inj_add.
      by replace m1' with (S m2') by lia.
104 105 106 107 108 109
  Qed.

  Lemma fibRunner_spec (n a : nat) :
    {{{ True }}} fibRunner #n #a {{{ (m : nat), RET #m; fib a = m }}}.
  Proof.
    iIntros (Φ) "_ HΦ".
110
    unfold fibRunner. wp_lam. wp_let. wp_bind (newRunner _ _ _).
111 112 113 114 115 116 117 118 119 120 121 122
    iApply (newRunner_spec b N P Q).
    - iIntros (γb r). iAlways. iIntros (a') "[#Hrunner HP]".
      iApply (parFib_spec with "[$HP]"); eauto.
    - iNext. iIntros (γb r) "#Hrunner".
      wp_let. wp_bind (runner_Fork b r #a).
      iApply (runner_Fork_spec); eauto.
      iNext. iIntros (γ γ' t) "Ht".
      iApply (task_Join_spec with "[$Ht]"); eauto.
      iNext. iIntros (res). iDestruct 1 as (?) "[% %]"; simplify_eq/=.
      by iApply "HΦ".
  Qed.
End contents.