From 2649cb67bc5e68832d09d3488be4d5f27190a467 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 14 Jun 2018 18:14:13 +0200 Subject: [PATCH] concurrent stacks: add an interface that both stack3 and stack4 implement Had to slightly tweak (strengthen) stack3's spec for that --- _CoqProject | 1 + .../concurrent_stacks/concurrent_stack3.v | 23 ++++++++++++++----- .../concurrent_stacks/concurrent_stack4.v | 11 ++++++++- theories/concurrent_stacks/spec.v | 21 +++++++++++++++++ 4 files changed, 49 insertions(+), 7 deletions(-) create mode 100644 theories/concurrent_stacks/spec.v diff --git a/_CoqProject b/_CoqProject index 0a83e13..d061939 100644 --- a/_CoqProject +++ b/_CoqProject @@ -27,6 +27,7 @@ theories/concurrent_stacks/concurrent_stack1.v theories/concurrent_stacks/concurrent_stack2.v theories/concurrent_stacks/concurrent_stack3.v theories/concurrent_stacks/concurrent_stack4.v +theories/concurrent_stacks/spec.v theories/logrel/prelude/base.v theories/logrel/stlc/lang.v diff --git a/theories/concurrent_stacks/concurrent_stack3.v b/theories/concurrent_stacks/concurrent_stack3.v index 9ec1daa..d246581 100644 --- a/theories/concurrent_stacks/concurrent_stack3.v +++ b/theories/concurrent_stacks/concurrent_stack3.v @@ -3,6 +3,8 @@ From iris.heap_lang Require Export lang proofmode notation. From iris.algebra Require Import excl. Set Default Proof Using "Type". +From iris_examples.concurrent_stacks Require Import spec. + (** Stack 3: No helping, view-shift spec. *) Definition mk_stack : val := @@ -89,9 +91,9 @@ Section stack_works. - The resources for the successful and failing pop must be disjoint. Instead, there should be a normal conjunction between them. Open question: How does this relate to a logically atomic spec? *) - Theorem stack_works P Q Q' Q'' Φ : - (∀ (f₁ f₂ : val) ι, - (□((∀ v vs, P (v :: vs) ={⊤∖↑ι}=∗ Q v ∗ P vs) -∗ (* pop *) + Theorem stack_works ι P Q Q' Q'' Φ : + ▷ (∀ (f₁ f₂ : val), + (□((∀ v vs, P (v :: vs) ={⊤∖↑ι}=∗ Q v ∗ P vs) ∧ (* pop *) (P [] ={⊤∖↑ι}=∗ Q' ∗ P []) -∗ WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ Q v') ∨ (v ≡ NONEV ∗ Q')}})) -∗ (∀ (v : val), (* push *) @@ -102,14 +104,14 @@ Section stack_works. -∗ WP mk_stack #() {{ Φ }}. Proof. iIntros "HΦ HP". - pose proof (nroot .@ "N") as N. + rename ι into N. wp_let. wp_alloc l as "Hl". iMod (inv_alloc N _ (stack_inv P #l) with "[Hl HP]") as "#Istack". { iNext; iExists l, (InjLV #()), []; iSplit; iFrame; auto. } wp_let. iApply "HΦ". - - iIntros "!# Hsucc Hfail". + - iIntros "!# Hcont". iLöb as "IH". wp_rec. wp_bind (! _)%E. @@ -122,6 +124,7 @@ Section stack_works. * subst. iDestruct (is_stack_empty with "Hstack") as "%". subst. + iDestruct "Hcont" as "[_ Hfail]". iMod ("Hfail" with "HP") as "[HQ' HP]". iMod ("Hclose" with "[Hl' Hstack HP]"). { iExists l', (InjLV #()), []; iSplit; iFrame; auto. } @@ -152,6 +155,7 @@ Section stack_works. iDestruct "H" as (ys') "%"; subst. iDestruct "Hstack" as (t') "[% Hstack]". injection H3; intros; subst. + iDestruct "Hcont" as "[Hsucc _]". iDestruct ("Hsucc" with "[HP]") as "> [HQ HP]"; auto. iMod ("Hclose" with "[Hl'' Hstack HP]"). { iExists l'', t', ys'; iSplit; iFrame; auto. } @@ -164,7 +168,7 @@ Section stack_works. { iExists l'', v', ys; iSplit; iFrame; auto. } iModIntro. wp_if. - iApply ("IH" with "Hsucc Hfail"). + iApply ("IH" with "Hcont"). - iIntros (v) "!# Hpush". iLöb as "IH". wp_rec. @@ -199,4 +203,11 @@ Section stack_works. wp_if. iApply ("IH" with "Hpush"). Qed. + + Program Definition is_concurrent_stack : concurrent_stack Σ := + {| spec.mk_stack := mk_stack |}. + Next Obligation. + iIntros (????? Φ) "HP HΦ". iApply (stack_works with "[HΦ] HP"). + iIntros "!>" (f₁ f₂) "Hpop Hpush". iApply "HΦ". iFrame. + Qed. End stack_works. diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v index 544aae0..ed94b8f 100644 --- a/theories/concurrent_stacks/concurrent_stack4.v +++ b/theories/concurrent_stacks/concurrent_stack4.v @@ -2,6 +2,8 @@ From iris.program_logic Require Export weakestpre hoare. From iris.heap_lang Require Export lang proofmode notation. From iris.algebra Require Import excl. +From iris_examples.concurrent_stacks Require Import spec. + (** Stack 3: Helping, view-shift spec. *) Definition mk_offer : val := @@ -143,7 +145,7 @@ Section stack_works. (* Whole-stack invariant (P). *) Theorem stack_works {channelG0 : channelG Σ} N P Q Q' Q'' Φ : - (∀ (f₁ f₂ : val), + ▷ (∀ (f₁ f₂ : val), (□(((∀ v vs, P (v :: vs) ={⊤ ∖ ↑ N}=∗ Q v ∗ P vs) ∧ (P [] ={⊤ ∖ ↑ N}=∗ Q' ∗ P []) -∗ WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ Q v') ∨ (v ≡ NONEV ∗ Q')}})) @@ -618,4 +620,11 @@ Section stack_works. wp_cas_fail. by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. Qed. + + Program Definition is_concurrent_stack `{!channelG Σ} : concurrent_stack Σ := + {| spec.mk_stack := mk_stack |}. + Next Obligation. + iIntros (?????? Φ) "HP HΦ". iApply (stack_works with "[HΦ] HP"). + iIntros "!>" (f₁ f₂) "#[Hpop Hpush]". iApply "HΦ". iFrame "#". + Qed. End stack_works. diff --git a/theories/concurrent_stacks/spec.v b/theories/concurrent_stacks/spec.v new file mode 100644 index 0000000..b8b61fc --- /dev/null +++ b/theories/concurrent_stacks/spec.v @@ -0,0 +1,21 @@ +From stdpp Require Import namespaces. +From iris.program_logic Require Export weakestpre. +From iris.heap_lang Require Export proofmode notation. + +(** General (HoCAP-style) spec for a concurrent stack *) + +Record concurrent_stack {Σ} `{!heapG Σ} := ConcurrentStack { + mk_stack : val; + mk_stack_spec (N : namespace) (P : list val → iProp Σ) + (Q : val → iProp Σ) (Q' Q'' : iProp Σ) : + {{{ P [] }}} + mk_stack #() + {{{ (f₁ f₂ : val), RET (f₁, f₂); + (□ ( (∀ v vs, P (v :: vs) ={⊤ ∖ ↑ N}=∗ Q v ∗ P vs) + ∧ (P [] ={⊤ ∖ ↑ N}=∗ Q' ∗ P []) -∗ + WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ Q v') ∨ (v ≡ NONEV ∗ Q')}})) + ∗ (∀ (v : val), + □ ((∀ vs, P vs ={⊤ ∖ ↑ N}=∗ P (v :: vs) ∗ Q'') -∗ WP f₂ v {{ v, Q'' }})) + }}} +}. +Arguments concurrent_stack _ {_}. -- GitLab