Commit cc57fef5 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Add slides for the talks.

parent 236ffeda
From iris.heap_lang Require Import proofmode notation.
(* PART 1: Basic setup *)
Lemma sep_exist {Σ} A (P R: iProp Σ) (Ψ: A iProp Σ) :
P ( a, Ψ a) R - a, Ψ a P.
Proof.
iIntros "[HP [HΨ HR]]". iDestruct "HΨ" as (a) "HΨ".
iExists a. iSplitL "HΨ". done. done.
Qed.
Lemma sep_logic_misc Σ (P Q: iProp Σ) (Ψ : Z iProp Σ) :
( x, P (True - True) - Q - Ψ x) -
(P Q) -
Ψ 0.
Proof.
iIntros "H [HP HQ]". iApply ("H" with "[HP] HQ"). auto.
Qed.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import par.
(* PART 2: Texan triples *)
Definition strange_inc : val := λ: "p",
let: "q" := ref #() in
"p" <- #1 + !"p" ;; !"q".
Lemma strange_inc_spec1 `{heapG Σ} l (x : Z) :
l #x - WP strange_inc #l {{ v, v = #() l #(1 + x) }}.
Proof.
iIntros "?". wp_let. wp_alloc k. wp_let.
wp_load. wp_op. wp_store. wp_load. auto.
Qed.
Definition strange_inc_twice : val := λ: "p",
strange_inc "p";;
strange_inc "p".
Lemma strange_inc_twice_spec1 `{heapG Σ} l (x : Z) :
l #x -
WP strange_inc_twice #l {{ v, v = #() l #(2 + x) }}.
Proof.
iIntros "Hl". wp_let. wp_bind (strange_inc _).
(* now what? *)
Abort.
Lemma strange_inc_spec2 `{heapG Σ} Φ l (x : Z) :
l #x -
(l #(1 + x) - Φ #()) -
WP strange_inc #l {{ Φ }}.
Proof.
iIntros "Hl Post". wp_let. wp_alloc k. wp_let.
wp_load. wp_op. wp_store. wp_load. by iApply "Post".
Qed.
Lemma strange_inc_spec `{heapG Σ} l (x : Z) :
{{{ l #x }}} strange_inc #l {{{ RET #(); l #(1 + x) }}}.
Proof.
iIntros (Φ) "? Post". wp_let. wp_alloc k. wp_let.
wp_load. wp_op. wp_store. wp_load. by iApply "Post".
Qed.
Lemma strange_inc_twice_spec2 `{heapG Σ} l (x : Z) :
l #x -
WP strange_inc_twice #l {{ v, v = #() l #(2 + x) }}.
Proof.
iIntros "Hl". wp_let.
wp_apply (strange_inc_spec with "Hl"); iIntros "Hl"; wp_seq.
wp_apply (strange_inc_spec with "Hl"); iIntros "Hl".
rewrite (_ : 2 + x = 1 + (1 + x)); last lia. auto.
Qed.
Lemma strange_inc_twice_spec `{heapG Σ} l (x : Z) :
{{{ l #x }}} strange_inc_twice #l {{{ RET #(); l #(2 + x) }}}.
Proof.
iIntros (Φ) "Hl Post". wp_let.
wp_apply (strange_inc_spec with "Hl"); iIntros "Hl"; wp_seq.
wp_apply (strange_inc_spec with "Hl"); iIntros "Hl".
iApply "Post". rewrite (_ : 2 + x = 1 + (1 + x)); last lia. done.
Qed.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import par.
Local Definition N := nroot .@ "example".
(* PART 3: Basic concurrency *)
Definition coin_flip : val := λ: <>,
let: "l" := ref #0 in
(("l" <- #0) ||| ("l" <- #1));;
!"l".
Lemma test2_spec `{heapG Σ, spawnG Σ} :
{{{ True }}} coin_flip #() {{{ n, RET #n; n = 0 n = 1 }}}.
Proof.
iIntros (Φ) "_ Post". wp_let. wp_alloc l as "Hl". wp_let.
iMod (inv_alloc N _
( x : Z, l #x x = 0 x = 1 )%I with "[Hl]") as "#?".
{ eauto 10. }
wp_apply (wp_par (λ _, True)%I (λ _, True)%I).
- iInv N as (n) ">[Hl _]" "Hclose".
wp_store. iMod ("Hclose" with "[Hl]"); eauto 10.
- iInv N as (n) ">[Hl _]" "Hclose".
wp_store. iMod ("Hclose" with "[Hl]"); eauto 10.
- iIntros (v1 v2) "_ !> /=". wp_seq.
iInv N as (n) ">[Hl %]" "Hclose".
wp_load. iMod ("Hclose" with "[Hl]") as "_"; first eauto 10.
iApply "Post"; auto.
Qed.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import par.
From iris.algebra Require Import frac_auth.
Local Definition N := nroot .@ "example".
(* PART 4: Parellel increment (from JH's talk) *)
Definition par_inc : val := λ: <>,
let: "l" := ref #0 in
(FAA "l" #2 ||| FAA "l" #2);;
!"l".
Section proof1.
Context `{heapG Σ, spawnG Σ}.
Lemma Zeven_2 : Zeven 2.
Proof. done. Qed.
Hint Resolve Zeven_2 Zeven_plus_Zeven.
Lemma par_inc_even_spec :
{{{ True }}} par_inc #() {{{ n, RET #n; Zeven n }}}.
Proof.
iIntros (Φ) "_ Post". wp_lam. wp_alloc l as "Hl". wp_let.
iMod (inv_alloc N _ ( n : Z, l #n Zeven n )%I with "[Hl]") as "#?".
{ iExists 0. auto. }
wp_bind (_ ||| _)%E.
wp_apply (wp_par (λ _, True)%I (λ _, True)%I).
- iInv N as (n) ">[Hl %]" "Hclose".
wp_faa. iMod ("Hclose" with "[Hl]"); first eauto 10.
auto.
- iInv N as (n) ">[Hl %]" "Hclose".
wp_faa. iMod ("Hclose" with "[Hl]"); first eauto 10.
auto.
- iIntros (v1 v2) "_". iNext. wp_seq.
iInv N as (n) ">[Hl %]" "Hclose".
wp_load. iMod ("Hclose" with "[Hl]"); first eauto 10.
iApply "Post"; auto.
Qed.
End proof1.
(* PART 5: Better parellel increment *)
Definition par_incN_helper : val :=
rec: "helper" "n" "l" :=
if: "n" = #0 then #()
else (FAA "l" #2 ||| "helper" ("n" - #1) "l").
Definition par_incN : val := λ: "n",
let: "l" := ref #0 in
par_incN_helper "n" "l";;
!"l".
Section proof2.
Context `{heapG Σ, spawnG Σ, inG Σ (frac_authR natR)}.
Implicit Types n : nat.
(* Rules for fractional ghost variables
(proved from generic principles) *)
Lemma frac_auth_alloc n :
(|==> γ, own γ (! n) own γ (!{1} n))%I.
Proof.
by iMod (own_alloc (! n ! n))
as (γ) "[??]"; eauto with iFrame.
Qed.
Lemma frac_auth_update n n1 n2 q γ :
own γ (! n1) -
own γ (!{q} n2) - |==>
own γ (! (n1 + n)%nat) own γ (!{q} (n2 + n)%nat).
Proof.
iIntros "H H'". iMod (own_update_2 with "H H'") as "[$ $]"; last done.
apply frac_auth_update, nat_local_update. lia.
Qed.
Lemma frac_auth_agree n n' γ :
own γ (! n) - own γ (!{1} n') - n = n'.
Proof.
iIntros "H H'".
by iDestruct (own_valid_2 with "H H'") as %->%frac_auth_agreeL.
Qed.
(* The invariant that we use *)
Definition proof2_inv (γ : gname) (l : loc) : iProp Σ :=
( n : nat, own γ (! n) l #n)%I.
(* Proof of the threads *)
Lemma par_inc_FAA_spec n n' γ l q :
{{{ inv N (proof2_inv γ l) own γ (!{q} n) }}}
FAA #l #n'
{{{ m, RET #m; own γ (!{q} (n + n'))%nat }}}.
Proof.
iIntros (Φ) "[#Hinv Hγ] Post". iInv N as (m) ">[Hauth Hl]" "Hclose".
wp_faa.
iMod (frac_auth_update n' with "Hauth Hγ") as "[Hauth Hγ]".
iMod ("Hclose" with "[Hauth Hl]") as "_".
{ iNext; iExists (m + n')%nat. rewrite Nat2Z.inj_add. iFrame. }
by iApply "Post".
Qed.
(* Proof of the whole program *)
Lemma par_inc_spec :
{{{ True }}} par_inc #() {{{ RET #4%nat; True }}}.
Proof.
iIntros (Φ) "_ Post". wp_lam. wp_alloc l as "Hl". wp_let.
iMod (frac_auth_alloc 0) as (γ) "[Hauth Hγ]".
iDestruct "Hγ" as "[Hγ1 Hγ2]".
iMod (inv_alloc _ _ (proof2_inv γ l) with "[Hl Hauth]") as "#Hinv".
{ iNext. iExists 0%nat. iFrame. }
wp_apply (wp_par (λ _, own γ (!{1/2} 2%nat))
(λ _, own γ (!{1/2} 2%nat)) with "[Hγ1] [Hγ2]").
- iApply (par_inc_FAA_spec 0 2 with "[$]"); auto.
- iApply (par_inc_FAA_spec 0 2 with "[$]"); auto.
- iIntros (v1 v2) "[Hγ1 Hγ2] !>". iCombine "Hγ1 Hγ2" as "Hγ". simpl.
wp_seq. iInv N as (m) ">[Hauth Hx]" "Hclose".
iDestruct (frac_auth_agree with "Hauth Hγ") as %->.
wp_load.
iMod ("Hclose" with "[Hauth Hx]") as "_".
{ iNext. iExists 4%nat. iFrame. }
by iApply "Post".
Qed.
Lemma par_incN_helper_spec n γ l q :
{{{ inv N (proof2_inv γ l) own γ (!{q} 0%nat) }}}
par_incN_helper #n #l
{{{ v, RET v; own γ (!{q} (n * 2))%nat }}}.
Proof.
iIntros (Φ) "[#? Hγ] Post /=".
iInduction n as [|n] "IH" forall (q Φ).
{ do 2 wp_let. wp_op. wp_if. by iApply "Post". }
rewrite Nat2Z.inj_succ. do 2 wp_let.
wp_op. case_bool_decide; first lia. wp_if.
iDestruct "Hγ" as "[Hγ1 Hγ2]".
wp_apply (wp_par (λ _, own γ (!{q/2} 2%nat))
(λ _, own γ (!{q/2} (n * 2)%nat)) with "[Hγ1] [Hγ2]").
- iApply (par_inc_FAA_spec 0 2 with "[$]"); auto.
- wp_op. rewrite (_ : Z.succ n - 1 = n); last lia.
iApply ("IH" with "Hγ2"); auto.
- iIntros (v1 v2) "[Hγ1 Hγ2] !>". iCombine "Hγ1 Hγ2" as "Hγ".
by iApply "Post".
Qed.
Lemma par_incN_spec n :
{{{ True }}} par_incN #n {{{ RET #(n * 2)%nat; True }}}.
Proof.
iIntros (Φ) "_ Post". wp_lam. wp_alloc l as "Hl". wp_let.
iMod (frac_auth_alloc 0) as (γ) "[Hauth Hγ]".
iMod (inv_alloc _ _ (proof2_inv γ l) with "[Hl Hauth]") as "#Hinv".
{ iNext. iExists 0%nat. iFrame. }
wp_apply (par_incN_helper_spec with "[$]").
iIntros (v) "Hγ". wp_seq.
iInv N as (m) ">[Hauth Hx]" "Hclose".
iDestruct (frac_auth_agree with "Hauth Hγ") as %->.
wp_load.
iMod ("Hclose" with "[Hauth Hx]") as "_".
{ iNext. iExists (n * 2)%nat. iFrame. }
by iApply "Post".
Qed.
End proof2.
File added
File added
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment