From 31eb5eb385952d4e7d56ff906c1419089f723d8d Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Fri, 25 Jan 2019 11:15:30 +0100 Subject: [PATCH] integrate the iris-atomic files and make them build --- _CoqProject | 9 ++++++++- theories/logatom/flat_combiner/atomic_sync.v | 3 +-- theories/logatom/flat_combiner/flat.v | 2 +- theories/logatom/flat_combiner/peritem.v | 5 ++++- theories/logatom/flat_combiner/simple_sync.v | 2 +- 5 files changed, 15 insertions(+), 6 deletions(-) diff --git a/_CoqProject b/_CoqProject index 557a55e..8d49f2e 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 08cfa3d..a001f5c 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 c6b0b31..257689f 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 5590e2b..2ddcb83 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 b601b31..661f672 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 := -- GitLab