Commit 31eb5eb3 authored by Ralf Jung's avatar Ralf Jung
Browse files

integrate the iris-atomic files and make them build

parent 4beb6889
...@@ -86,6 +86,13 @@ theories/hocap/lib/oneshot.v ...@@ -86,6 +86,13 @@ theories/hocap/lib/oneshot.v
theories/hocap/concurrent_runners.v theories/hocap/concurrent_runners.v
theories/hocap/parfib.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/stack.v
theories/logatom/elimination_stack/spec.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
From iris.program_logic Require Export weakestpre hoare atomic. From iris.program_logic Require Export weakestpre hoare atomic.
From iris.heap_lang Require Export lang proofmode notation. From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Import spin_lock. From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import agree frac. 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. *) (** The simple syncer spec in [sync.v] implies a logically atomic spec. *)
......
...@@ -5,7 +5,7 @@ From iris.heap_lang Require Import proofmode notation. ...@@ -5,7 +5,7 @@ From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock. From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import auth frac agree excl agree gset gmap. From iris.algebra Require Import auth frac agree excl agree gset gmap.
From iris.base_logic Require Import saved_prop. 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 := Definition doOp : val :=
λ: "p", λ: "p",
......
...@@ -3,9 +3,12 @@ From iris.heap_lang Require Export lang. ...@@ -3,9 +3,12 @@ From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap csum. 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. 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. Section defs.
Context `{heapG Σ} (N: namespace). Context `{heapG Σ} (N: namespace).
Context (R: val iProp Σ) `{ x, TimelessP (R x)}. Context (R: val iProp Σ) `{ x, TimelessP (R x)}.
......
...@@ -4,7 +4,7 @@ From iris.program_logic Require Export weakestpre hoare. ...@@ -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 Require Export lang proofmode notation.
From iris.heap_lang.lib Require Import spin_lock. From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import frac. From iris.algebra Require Import frac.
From iris_atomic Require Import sync. From iris_examples.logatom.flat_combiner Require Import sync.
Import uPred. Import uPred.
Definition mk_sync: val := Definition mk_sync: val :=
......
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