Commit b254321f authored by Ralf Jung's avatar Ralf Jung

create logatom directory and move elimination stack into it

parent 3596240a
......@@ -23,5 +23,5 @@ logrel_heaplang: $(filter theories/logrel_heaplang/%,$(VOFILES))
hocap: $(filter theories/hocap/%,$(VOFILES))
.PHONY: hocap
logatom_stack: $(filter theories/logatom_stack/%,$(VOFILES))
.PHONY: logrel
logatom: $(filter theories/logatom/%,$(VOFILES))
.PHONY: logatom
......@@ -86,6 +86,6 @@ theories/hocap/lib/oneshot.v
theories/hocap/concurrent_runners.v
theories/hocap/parfib.v
theories/logatom_stack/stack.v
theories/logatom_stack/spec.v
theories/logatom_stack/hocap_spec.v
theories/logatom/elimination_stack/stack.v
theories/logatom/elimination_stack/spec.v
theories/logatom/elimination_stack/hocap_spec.v
......@@ -4,10 +4,10 @@ From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import proofmode atomic_heap.
From iris_examples.logatom_stack Require spec.
From iris_examples.logatom.elimination_stack Require spec.
Set Default Proof Using "Type".
Module logatom := logatom_stack.spec.
Module logatom := elimination_stack.spec.
(** A general HoCAP-style interface for a stack, modeled after the spec in
[hocap/abstract_bag.v]. There are two differences:
......
......@@ -4,7 +4,7 @@ From iris.program_logic Require Import atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode atomic_heap.
From iris.bi.lib Require Import fractional.
From iris_examples.logatom_stack Require Import spec.
From iris_examples.logatom.elimination_stack Require Import spec.
Set Default Proof Using "Type".
(** * Implement a concurrent stack with helping on top of an arbitrary atomic
......
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