Commit 51418462 authored by Ralf Jung's avatar Ralf Jung

we can use wp_par again now

parent b69f5182
Pipeline #14710 passed with stage
in 7 minutes and 41 seconds
......@@ -39,7 +39,7 @@ Section proof1.
{ (* exercise *)
admit. }
iIntros (l) "#Hl". wp_let.
wp_apply (par_spec (λ _, True%I) (λ _, True%I)).
wp_apply (wp_par (λ _, True%I) (λ _, True%I)).
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]".
wp_seq. wp_load. wp_op. wp_store.
wp_apply (release_spec with "[Hr $Hl]"); [|done].
......@@ -108,7 +108,7 @@ Section proof2.
{ (* exercise *)
admit. }
iIntros (l) "#Hl". wp_let.
wp_apply (par_spec (λ _, own γ1 ( Excl' 2)) (λ _, own γ2 ( Excl' 2))
wp_apply (wp_par (λ _, own γ1 ( Excl' 2)) (λ _, own γ2 ( Excl' 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.
......@@ -142,7 +142,7 @@ Section proof3.
{ (* exercise *)
admit. }
iIntros (l) "#Hl". wp_let.
wp_apply (par_spec (λ _, own γ (!{1/2} 2%nat)) (λ _, own γ (!{1/2} 2%nat))
wp_apply (wp_par (λ _, own γ (!{1/2} 2%nat)) (λ _, own γ (!{1/2} 2%nat))
with "[Hγ1◯] [Hγ2◯]").
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]".
wp_seq. wp_load. wp_op. wp_store.
......
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [] # This repo does not install
remove: []
depends: [
"coq-iris" { (= "dev.2019-01-22.0.b85a3cfc") | (= "dev") }
"coq-iris" { (= "dev.2019-02-18.1.a1cf5cb9") | (= "dev") }
]
......@@ -38,7 +38,7 @@ Section proof1.
wp_apply (newlock_spec (parallel_add_inv_1 r) with "[Hr]").
{ (* exercise *) iExists 0. iFrame. }
iIntros (l) "#Hl". wp_let.
wp_apply (par_spec (λ _, True%I) (λ _, True%I)).
wp_apply (wp_par (λ _, True%I) (λ _, True%I)).
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]".
wp_seq. wp_load. wp_op. wp_store.
wp_apply (release_spec with "[Hr $Hl]"); [|done].
......@@ -111,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 (par_spec (λ _, own γ1 ( Excl' 2)) (λ _, own γ2 ( Excl' 2))
wp_apply (wp_par (λ _, own γ1 ( Excl' 2)) (λ _, own γ2 ( Excl' 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.
......@@ -154,7 +154,7 @@ Section proof3.
wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]").
{ (* exercise *) iExists 0%nat. iFrame. }
iIntros (l) "#Hl". wp_let.
wp_apply (par_spec (λ _, own γ (!{1/2} 2%nat)) (λ _, own γ (!{1/2} 2%nat))
wp_apply (wp_par (λ _, own γ (!{1/2} 2%nat)) (λ _, own γ (!{1/2} 2%nat))
with "[Hγ1◯] [Hγ2◯]").
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]".
wp_seq. wp_load. wp_op. wp_store.
......
......@@ -77,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 (par_spec (λ _, own γ1 ( Excl' true)) (λ _, own γ2 ( Excl' true))
wp_apply (wp_par (λ _, own γ1 ( Excl' true)) (λ _, own γ2 ( Excl' 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!
Please register or to comment