diff --git a/theories/concurrent_stacks/concurrent_stack1.v b/theories/concurrent_stacks/concurrent_stack1.v index f00b2fc60ccef50a492c5fdcdbd374fe13e2f3d4..ffe481c550f1f6d415db732b2b4335753ee12521 100644 --- a/theories/concurrent_stacks/concurrent_stack1.v +++ b/theories/concurrent_stacks/concurrent_stack1.v @@ -5,6 +5,9 @@ From iris.program_logic Require Export weakestpre hoare. From iris.heap_lang Require Export lang. From iris.algebra Require Import agree list. From iris.heap_lang Require Import assert proofmode notation. + +From iris_examples.concurrent_stacks Require Import spec. + Set Default Proof Using "Type". (** Stack 1: No helping, bag spec. *) @@ -14,10 +17,10 @@ Definition mk_stack : val := let: "r" := ref NONEV in (rec: "pop" "n" := match: !"r" with - NONE => #-1 + NONE => NONE | SOME "hd" => if: CAS "r" (SOME "hd") (Snd !"hd") - then Fst !"hd" + then SOME (Fst !"hd") else "pop" "n" end, rec: "push" "n" := @@ -81,8 +84,8 @@ Section stacks. (* Per-element invariant (i.e., bag spec). *) Theorem stack_works P Φ : - (∀ (f₁ f₂ : val), - (∀ (v : val), □ WP f₁ #() {{ v, P v ∨ v ≡ #-1 }}) + ▷ (∀ (f₁ f₂ : val), + (□ WP f₁ #() {{ v, (∃ v', v ≡ SOMEV v' ∗ P v') ∨ v ≡ NONEV }}) -∗ (∀ (v : val), □ (P v -∗ WP f₂ v {{ v, True }})) -∗ Φ (f₁, f₂)%V)%I -∗ WP mk_stack #() {{ Φ }}. @@ -98,7 +101,7 @@ Section stacks. wp_let. iModIntro. iApply "HΦ". - - iIntros (v) "!#". + - iIntros "!#". iLöb as "IH". wp_rec. wp_bind (! #l)%E. @@ -129,7 +132,7 @@ Section stacks. wp_if. wp_load. wp_proj. - iLeft; auto. + eauto. * simpl in Hne. wp_cas_fail. iMod ("Hclose" with "[Hl'' Hstack]"). { iExists v''; iFrame; auto. } @@ -172,3 +175,10 @@ Section stacks. done. Qed. End stacks. + +Program Definition is_concurrent_bag `{!heapG Σ} : concurrent_bag Σ := + {| spec.mk_bag := mk_stack |}. +Next Obligation. + iIntros (??? P Φ) "_ HΦ". iApply stack_works. + iNext. iIntros (f₁ f₂) "Hpop Hpush". iApply "HΦ". iFrame. +Qed. diff --git a/theories/concurrent_stacks/concurrent_stack2.v b/theories/concurrent_stacks/concurrent_stack2.v index 59ebf9a7373fffb267cc0f3d0066f557d31ffb2c..d7023b9bfe2708be884f2f1afa8a733d61b20175 100644 --- a/theories/concurrent_stacks/concurrent_stack2.v +++ b/theories/concurrent_stacks/concurrent_stack2.v @@ -3,6 +3,9 @@ stricter CAS requirements yet. *) 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. + Set Default Proof Using "Type". (** Stack 2: With helping, bag spec. *) @@ -268,7 +271,7 @@ Section stack_works. (* Per-element invariant (i.e., bag spec). *) Theorem stack_works {channelG0 : channelG Σ} P Φ : - (∀ (f₁ f₂ : val), + ▷ (∀ (f₁ f₂ : val), (□ WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ P v') ∨ v ≡ NONEV }}) -∗ (∀ (v : val), □ (P v -∗ WP f₂ v {{ v, True }})) -∗ Φ (f₁, f₂)%V)%I @@ -405,3 +408,10 @@ Section stack_works. done. Qed. End stack_works. + +Program Definition is_concurrent_bag `{!heapG Σ, !channelG Σ} : concurrent_bag Σ := + {| spec.mk_bag := mk_stack |}. +Next Obligation. + iIntros (???? P Φ) "_ HΦ". iApply stack_works. + iNext. iIntros (f₁ f₂) "Hpop Hpush". iApply "HΦ". iFrame. +Qed. diff --git a/theories/concurrent_stacks/concurrent_stack3.v b/theories/concurrent_stacks/concurrent_stack3.v index 10792a953fb9067bbc1a4c015b53c716df2cbf14..0876be16db26b06fff9445c9bf282b0643423d6f 100644 --- a/theories/concurrent_stacks/concurrent_stack3.v +++ b/theories/concurrent_stacks/concurrent_stack3.v @@ -1,10 +1,11 @@ From iris.program_logic Require Export weakestpre hoare. 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. +Set Default Proof Using "Type". + (** Stack 3: No helping, view-shift spec. *) Definition mk_stack : val := @@ -213,11 +214,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"). - iNext. iIntros (f₁ f₂) "Hpop Hpush". iApply "HΦ". iFrame. - Qed. End stack_works. + +Program Definition is_concurrent_stack `{!heapG Σ} : concurrent_stack Σ := + {| spec.mk_stack := mk_stack |}. +Next Obligation. + iIntros (??????? Φ) "HP HΦ". iApply (stack_works with "[HΦ] HP"). + iNext. iIntros (f₁ f₂) "Hpop Hpush". iApply "HΦ". iFrame. +Qed. diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v index e07cd22a506dd3287b03ca576a4f5b6406fc01cf..e3565fafb82a59ce0c5257d41288de80451dbeea 100644 --- a/theories/concurrent_stacks/concurrent_stack4.v +++ b/theories/concurrent_stacks/concurrent_stack4.v @@ -6,6 +6,8 @@ From iris.algebra Require Import excl. From iris_examples.concurrent_stacks Require Import spec. +Set Default Proof Using "Type". + (** Stack 3: Helping, view-shift spec. *) Definition mk_offer : val := @@ -620,11 +622,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"). - iNext. iIntros (f₁ f₂) "#[Hpop Hpush]". iApply "HΦ". iFrame "#". - Qed. End stack_works. + +Program Definition is_concurrent_stack `{!heapG Σ, !channelG Σ} : concurrent_stack Σ := + {| spec.mk_stack := mk_stack |}. +Next Obligation. + iIntros (???????? Φ) "HP HΦ". iApply (stack_works with "[HΦ] HP"). + iNext. iIntros (f₁ f₂) "#[Hpop Hpush]". iApply "HΦ". iFrame "#". +Qed. diff --git a/theories/concurrent_stacks/spec.v b/theories/concurrent_stacks/spec.v index b8b61fc675230105a35ba4b6b156cbcbc9e1f7a6..d88aac3a2611ddd571b2d1c3cc2d71c524b09372 100644 --- a/theories/concurrent_stacks/spec.v +++ b/theories/concurrent_stacks/spec.v @@ -2,6 +2,19 @@ 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 bag ("per-elemt spec") *) +Record concurrent_bag {Σ} `{!heapG Σ} := ConcurrentBag { + mk_bag : val; + mk_bag_spec (N : namespace) (P : val → iProp Σ) : + {{{ True }}} + mk_bag #() + {{{ (f₁ f₂ : val), RET (f₁, f₂); + (□ WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ P v') ∨ v ≡ NONEV }}) + ∗ (∀ (v : val), □ (P v -∗ WP f₂ v {{ v, True }})) + }}} +}. +Arguments concurrent_bag _ {_}. + (** General (HoCAP-style) spec for a concurrent stack *) Record concurrent_stack {Σ} `{!heapG Σ} := ConcurrentStack {