Commit 702df1a2 by Robbert Krebbers

Bump Iris (make use of `excl_auth`).

parent 4a9d8f2f
Pipeline #22769 passed with stage
in 14 minutes and 52 seconds
 ... ... @@ -3,7 +3,7 @@ In this exercise we use the spin-lock from the previous exercise to implement the running example during the lecture of the tutorial: proving that when two threads increase a reference that's initially zero by two, the result is four. *) From iris.algebra Require Import auth frac_auth excl. From iris.algebra Require Import excl_auth frac_auth. From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import lib.par proofmode notation. From exercises Require Import ex_03_spinlock. ... ... @@ -58,43 +58,41 @@ Whereas we previously abstracted over an arbitrary "ghost state" [Σ] in the proofs, we now need to make sure that we can use integer ghost variables. For this, we add the type class constraint: inG Σ (authR (optionUR (exclR ZO))) inG Σ (excl_authR ZO) *) Section proof2. Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR ZO)))}. Context `{!heapG Σ, !spawnG Σ, !inG Σ (excl_authR ZO)}. Definition parallel_add_inv_2 (r : loc) (γ1 γ2 : gname) : iProp Σ := (∃ n1 n2 : Z, r ↦ #(n1 + n2) ∗ own γ1 (● (Excl' n1)) ∗ own γ2 (● (Excl' n2)))%I. ∗ own γ1 (●E n1) ∗ own γ2 (●E n2))%I. (** Some helping lemmas for ghost state that we need in the proof. In actual proofs we tend to inline simple lemmas like these, but they are here to make things easier to understand. *) Lemma ghost_var_alloc n : (|==> ∃ γ, own γ (● (Excl' n)) ∗ own γ (◯ (Excl' n)))%I. (|==> ∃ γ, own γ (●E n) ∗ own γ (◯E n))%I. Proof. iMod (own_alloc (● (Excl' n) ⋅ ◯ (Excl' n))) as (γ) "[??]". - by apply auth_both_valid. iMod (own_alloc (●E n ⋅ ◯E n)) as (γ) "[??]". - by apply excl_auth_valid. - by eauto with iFrame. Qed. Lemma ghost_var_agree γ n m : own γ (● (Excl' n)) -∗ own γ (◯ (Excl' m)) -∗ ⌜ n = m ⌝. own γ (●E n) -∗ own γ (◯E m) -∗ ⌜ n = m ⌝. Proof. iIntros "Hγ● Hγ◯". by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid. by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %?%excl_auth_agreeL. Qed. Lemma ghost_var_update γ n' n m : own γ (● (Excl' n)) -∗ own γ (◯ (Excl' m)) ==∗ own γ (● (Excl' n')) ∗ own γ (◯ (Excl' n')). own γ (●E n) -∗ own γ (◯E m) ==∗ own γ (●E n') ∗ own γ (◯E n'). Proof. iIntros "Hγ● Hγ◯". iMod (own_update_2 _ _ _ (● Excl' n' ⋅ ◯ Excl' n') with "Hγ● Hγ◯") as "[\$\$]". { by apply auth_update, option_local_update, exclusive_local_update. } iMod (own_update_2 _ _ _ (●E n' ⋅ ◯E n') with "Hγ● Hγ◯") as "[\$\$]". { by apply excl_auth_update. } done. Qed. ... ... @@ -110,7 +108,7 @@ Section proof2. { (* exercise *) admit. } iIntros (l) "#Hl". wp_let. wp_apply (wp_par (λ _, own γ1 (◯ Excl' 2)) (λ _, own γ2 (◯ Excl' 2)) wp_apply (wp_par (λ _, own γ1 (◯E 2)) (λ _, own γ2 (◯E 2)) with "[Hγ1◯] [Hγ2◯]"). - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & Hγ1● & Hγ2●)". wp_seq. wp_load. wp_op. wp_store. ... ...
 ... ... @@ -8,7 +8,7 @@ first, the outcome is either 2 or 4. Contrary to the earlier exercises, this exercise is nearly entirely open. *) From iris.algebra Require Import auth frac_auth excl. From iris.algebra Require Import excl_auth frac_auth. From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import proofmode notation lib.par. From exercises Require Import ex_03_spinlock. ... ... @@ -26,33 +26,31 @@ Definition parallel_add_mul : expr := (** In this proof we will make use of Boolean ghost variables. *) Section proof. Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR boolO)))}. Context `{!heapG Σ, !spawnG Σ, !inG Σ (excl_authR boolO)}. (** The same helping lemmas for ghost variables that we have already seen in the previous exercise. *) Lemma ghost_var_alloc b : (|==> ∃ γ, own γ (● (Excl' b)) ∗ own γ (◯ (Excl' b)))%I. (|==> ∃ γ, own γ (●E b) ∗ own γ (◯E b))%I. Proof. iMod (own_alloc (● (Excl' b) ⋅ ◯ (Excl' b))) as (γ) "[??]". - by apply auth_both_valid. iMod (own_alloc (●E b ⋅ ◯E b)) as (γ) "[??]". - by apply excl_auth_valid. - by eauto with iFrame. Qed. Lemma ghost_var_agree γ b c : own γ (● (Excl' b)) -∗ own γ (◯ (Excl' c)) -∗ ⌜ b = c ⌝. own γ (●E b) -∗ own γ (◯E c) -∗ ⌜ b = c ⌝. Proof. iIntros "Hγ● Hγ◯". by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid. by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %<-%excl_auth_agreeL. Qed. Lemma ghost_var_update γ b' b c : own γ (● (Excl' b)) -∗ own γ (◯ (Excl' c)) ==∗ own γ (● (Excl' b')) ∗ own γ (◯ (Excl' b')). own γ (●E b) -∗ own γ (◯E c) ==∗ own γ (●E b') ∗ own γ (◯E b'). Proof. iIntros "Hγ● Hγ◯". iMod (own_update_2 _ _ _ (● Excl' b' ⋅ ◯ Excl' b') with "Hγ● Hγ◯") as "[\$\$]". { by apply auth_update, option_local_update, exclusive_local_update. } iMod (own_update_2 _ _ _ (●E b' ⋅ ◯E b') with "Hγ● Hγ◯") as "[\$\$]". { by apply excl_auth_update. } done. Qed. ... ...
 ... ... @@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] install: [] # This repo does not install remove: [] depends: [ "coq-iris" { (= "dev.2019-07-01.1.6e79f000") | (= "dev") } "coq-iris" { (= "dev.2019-11-21.4.d1787db2") | (= "dev") } ]
 ... ... @@ -3,7 +3,7 @@ In this exercise we use the spin-lock from the previous exercise to implement the running example during the lecture of the tutorial: proving that when two threads increase a reference that's initially zero by two, the result is four. *) From iris.algebra Require Import auth frac_auth excl. From iris.algebra Require Import excl_auth frac_auth. From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import lib.par proofmode notation. From solutions Require Import ex_03_spinlock. ... ... @@ -67,38 +67,36 @@ this, we add the type class constraint: *) Section proof2. Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR ZO)))}. Context `{!heapG Σ, !spawnG Σ, !inG Σ (excl_authR ZO)}. Definition parallel_add_inv_2 (r : loc) (γ1 γ2 : gname) : iProp Σ := (∃ n1 n2 : Z, r ↦ #(n1 + n2) ∗ own γ1 (● (Excl' n1)) ∗ own γ2 (● (Excl' n2)))%I. ∗ own γ1 (●E n1) ∗ own γ2 (●E n2))%I. (** Some helping lemmas for ghost state that we need in the proof. In actual proofs we tend to inline simple lemmas like these, but they are here to make things easier to understand. *) Lemma ghost_var_alloc n : (|==> ∃ γ, own γ (● (Excl' n)) ∗ own γ (◯ (Excl' n)))%I. (|==> ∃ γ, own γ (●E n) ∗ own γ (◯E n))%I. Proof. iMod (own_alloc (● (Excl' n) ⋅ ◯ (Excl' n))) as (γ) "[??]". - by apply auth_both_valid. iMod (own_alloc (●E n ⋅ ◯E n)) as (γ) "[??]". - by apply excl_auth_valid. - by eauto with iFrame. Qed. Lemma ghost_var_agree γ n m : own γ (● (Excl' n)) -∗ own γ (◯ (Excl' m)) -∗ ⌜ n = m ⌝. own γ (●E n) -∗ own γ (◯E m) -∗ ⌜ n = m ⌝. Proof. iIntros "Hγ● Hγ◯". by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid. by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %?%excl_auth_agreeL. Qed. Lemma ghost_var_update γ n' n m : own γ (● (Excl' n)) -∗ own γ (◯ (Excl' m)) ==∗ own γ (● (Excl' n')) ∗ own γ (◯ (Excl' n')). own γ (●E n) -∗ own γ (◯E m) ==∗ own γ (●E n') ∗ own γ (◯E n'). Proof. iIntros "Hγ● Hγ◯". iMod (own_update_2 _ _ _ (● Excl' n' ⋅ ◯ Excl' n') with "Hγ● Hγ◯") as "[\$\$]". { by apply auth_update, option_local_update, exclusive_local_update. } iMod (own_update_2 _ _ _ (●E n' ⋅ ◯E n') with "Hγ● Hγ◯") as "[\$\$]". { by apply excl_auth_update. } done. Qed. ... ... @@ -113,7 +111,7 @@ Section proof2. wp_apply (newlock_spec (parallel_add_inv_2 r γ1 γ2) with "[Hr Hγ1● Hγ2●]"). { (* exercise *) iExists 0, 0. iFrame. } iIntros (l) "#Hl". wp_let. wp_apply (wp_par (λ _, own γ1 (◯ Excl' 2)) (λ _, own γ2 (◯ Excl' 2)) wp_apply (wp_par (λ _, own γ1 (◯E 2)) (λ _, own γ2 (◯E 2)) with "[Hγ1◯] [Hγ2◯]"). - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & Hγ1● & Hγ2●)". wp_seq. wp_load. wp_op. wp_store. ... ...
 ... ... @@ -8,7 +8,7 @@ first, the outcome is either 2 or 4. Contrary to the earlier exercises, this exercise is nearly entirely open. *) From iris.algebra Require Import auth frac_auth excl. From iris.algebra Require Import excl_auth frac_auth. From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import proofmode notation lib.par. From solutions Require Import ex_03_spinlock. ... ... @@ -26,33 +26,31 @@ Definition parallel_add_mul : expr := (** In this proof we will make use of Boolean ghost variables. *) Section proof. Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR boolO)))}. Context `{!heapG Σ, !spawnG Σ, !inG Σ (excl_authR boolO)}. (** The same helping lemmas for ghost variables that we have already seen in the previous exercise. *) Lemma ghost_var_alloc b : (|==> ∃ γ, own γ (● (Excl' b)) ∗ own γ (◯ (Excl' b)))%I. (|==> ∃ γ, own γ (●E b) ∗ own γ (◯E b))%I. Proof. iMod (own_alloc (● (Excl' b) ⋅ ◯ (Excl' b))) as (γ) "[??]". - by apply auth_both_valid. iMod (own_alloc (●E b ⋅ ◯E b)) as (γ) "[??]". - by apply excl_auth_valid. - by eauto with iFrame. Qed. Lemma ghost_var_agree γ b c : own γ (● (Excl' b)) -∗ own γ (◯ (Excl' c)) -∗ ⌜ b = c ⌝. own γ (●E b) -∗ own γ (◯E c) -∗ ⌜ b = c ⌝. Proof. iIntros "Hγ● Hγ◯". by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid. by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %<-%excl_auth_agreeL. Qed. Lemma ghost_var_update γ b' b c : own γ (● (Excl' b)) -∗ own γ (◯ (Excl' c)) ==∗ own γ (● (Excl' b')) ∗ own γ (◯ (Excl' b')). own γ (●E b) -∗ own γ (◯E c) ==∗ own γ (●E b') ∗ own γ (◯E b'). Proof. iIntros "Hγ● Hγ◯". iMod (own_update_2 _ _ _ (● Excl' b' ⋅ ◯ Excl' b') with "Hγ● Hγ◯") as "[\$\$]". { by apply auth_update, option_local_update, exclusive_local_update. } iMod (own_update_2 _ _ _ (●E b' ⋅ ◯E b') with "Hγ● Hγ◯") as "[\$\$]". { by apply excl_auth_update. } done. Qed. ... ... @@ -62,7 +60,7 @@ Section proof. Boolean ghost variables. *) Definition parallel_add_mul_inv (r : loc) (γ1 γ2 : gname) : iProp Σ := (∃ (b1 b2 : bool) (z : Z), own γ1 (● Excl' b1) ∗ own γ2 (● Excl' b2) ∗ r ↦ #z ∗ own γ1 (●E b1) ∗ own γ2 (●E b2) ∗ r ↦ #z ∗ ⌜match b1, b2 with | true, true => z = 2 ∨ z = 4 | true, false => z = 2 ... ... @@ -79,7 +77,7 @@ Section proof. wp_apply (newlock_spec (parallel_add_mul_inv r γ1 γ2) with "[Hr Hγ1● Hγ2●]"). { iExists false, false, 0. iFrame. done. } iIntros (l) "#Hl". wp_let. wp_apply (wp_par (λ _, own γ1 (◯ Excl' true)) (λ _, own γ2 (◯ Excl' true)) wp_apply (wp_par (λ _, own γ1 (◯E true)) (λ _, own γ2 (◯E true)) with "[Hγ1◯] [Hγ2◯]"). - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (b1 b2 z) "(Hγ1● & Hγ2● & Hr & %)". ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!