diff --git a/_CoqProject b/_CoqProject index 557a55edcf3f344a7f67e3990758166ac12cfb63..8d49f2e0d21510b54ca036b56f76e4ed5bf985cc 100644 --- a/_CoqProject +++ b/_CoqProject @@ -86,6 +86,13 @@ theories/hocap/lib/oneshot.v theories/hocap/concurrent_runners.v theories/hocap/parfib.v +theories/logatom/treiber.v +theories/logatom/elimination_stack/hocap_spec.v theories/logatom/elimination_stack/stack.v theories/logatom/elimination_stack/spec.v -theories/logatom/elimination_stack/hocap_spec.v +theories/logatom/flat_combiner/flat.v +theories/logatom/flat_combiner/simple_sync.v +theories/logatom/flat_combiner/sync.v +theories/logatom/flat_combiner/peritem.v +theories/logatom/flat_combiner/atomic_sync.v +theories/logatom/flat_combiner/misc.v diff --git a/theories/logatom/flat_combiner/atomic_sync.v b/theories/logatom/flat_combiner/atomic_sync.v index 08cfa3d3b442c1ac01e8d726a1248ace7e7d7100..a001f5c378963ef79f0c7c558f47dfaa1f70738f 100644 --- a/theories/logatom/flat_combiner/atomic_sync.v +++ b/theories/logatom/flat_combiner/atomic_sync.v @@ -1,9 +1,8 @@ - From iris.program_logic Require Export weakestpre hoare atomic. From iris.heap_lang Require Export lang proofmode notation. From iris.heap_lang.lib Require Import spin_lock. From iris.algebra Require Import agree frac. -From iris_atomic Require Import sync misc. +From iris_examples.logatom.flat_combiner Require Import sync misc. (** The simple syncer spec in [sync.v] implies a logically atomic spec. *) diff --git a/theories/logatom/flat_combiner/flat.v b/theories/logatom/flat_combiner/flat.v index c6b0b316d26e9aa3a4a4181b88871619d16e356e..257689f910f106d7556868a420f9df310f5230d1 100644 --- a/theories/logatom/flat_combiner/flat.v +++ b/theories/logatom/flat_combiner/flat.v @@ -5,7 +5,7 @@ From iris.heap_lang Require Import proofmode notation. From iris.heap_lang.lib Require Import spin_lock. From iris.algebra Require Import auth frac agree excl agree gset gmap. From iris.base_logic Require Import saved_prop. -From iris_atomic Require Import misc peritem sync. +From iris_examples.logatom.flat_combiner Require Import misc peritem sync. Definition doOp : val := λ: "p", diff --git a/theories/logatom/flat_combiner/peritem.v b/theories/logatom/flat_combiner/peritem.v index 5590e2b98c3eab25f3a0f61294551879fab23922..2ddcb838cf2eb8a50cc26b9b891c1adc2361127f 100644 --- a/theories/logatom/flat_combiner/peritem.v +++ b/theories/logatom/flat_combiner/peritem.v @@ -3,9 +3,12 @@ From iris.heap_lang Require Export lang. From iris.heap_lang Require Import proofmode notation. From iris.proofmode Require Import tactics. From iris.algebra Require Import frac auth gmap csum. -From iris_atomic Require Export treiber misc. +From iris_examples.logatom Require Export treiber. From iris.base_logic.lib Require Import invariants. +(** The flat combiner uses a bag, this is where we prove the spec for that. + We re-use the code but not the spec of the treiber stack. *) + Section defs. Context `{heapG Σ} (N: namespace). Context (R: val → iProp Σ) `{∀ x, TimelessP (R x)}. diff --git a/theories/logatom/flat_combiner/simple_sync.v b/theories/logatom/flat_combiner/simple_sync.v index b601b31d1211e449dfcdc25146216b67f4e518cc..661f6727ad92aba7c2d6df5ab1b0cd7d9d681792 100644 --- a/theories/logatom/flat_combiner/simple_sync.v +++ b/theories/logatom/flat_combiner/simple_sync.v @@ -4,7 +4,7 @@ From iris.program_logic Require Export weakestpre hoare. From iris.heap_lang Require Export lang proofmode notation. From iris.heap_lang.lib Require Import spin_lock. From iris.algebra Require Import frac. -From iris_atomic Require Import sync. +From iris_examples.logatom.flat_combiner Require Import sync. Import uPred. Definition mk_sync: val :=