From 59a2fc1ad5d380c32c59bc8b87283ada0db44466 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Aug 2022 16:01:37 -0400
Subject: [PATCH] prepare for merge into gpfsl repo
---
.gitignore | 20 ------------
.gitlab-ci.yml | 51 ------------------------------
LICENSE | 28 -----------------
Makefile | 55 --------------------------------
README.md | 56 ---------------------------------
_CoqProject | 17 ----------
{theories => orc11}/base.v | 0
{theories => orc11}/event.v | 0
{theories => orc11}/location.v | 0
{theories => orc11}/mem_order.v | 0
{theories => orc11}/memory.v | 0
{theories => orc11}/progress.v | 0
{theories => orc11}/thread.v | 0
{theories => orc11}/tview.v | 0
{theories => orc11}/value.v | 0
{theories => orc11}/view.v | 0
16 files changed, 227 deletions(-)
delete mode 100644 .gitignore
delete mode 100644 .gitlab-ci.yml
delete mode 100644 LICENSE
delete mode 100644 Makefile
delete mode 100644 README.md
delete mode 100644 _CoqProject
rename {theories => orc11}/base.v (100%)
rename {theories => orc11}/event.v (100%)
rename {theories => orc11}/location.v (100%)
rename {theories => orc11}/mem_order.v (100%)
rename {theories => orc11}/memory.v (100%)
rename {theories => orc11}/progress.v (100%)
rename {theories => orc11}/thread.v (100%)
rename {theories => orc11}/tview.v (100%)
rename {theories => orc11}/value.v (100%)
rename {theories => orc11}/view.v (100%)
diff --git a/.gitignore b/.gitignore
deleted file mode 100644
index bb243f15..00000000
--- a/.gitignore
+++ /dev/null
@@ -1,20 +0,0 @@
-*.vo
-*.vio
-*.v.d
-*.coq.d
-*.vok
-*.vos
-*.glob
-*.cache
-*.aux
-\#*\#
-.\#*
-*~
-*.bak
-.coq-native/
-Makefile.coq
-Makefile.coq.conf
-builddep/
-*.crashcoqide
-.coqdeps.d
-_opam
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
deleted file mode 100644
index 95b41442..00000000
--- a/.gitlab-ci.yml
+++ /dev/null
@@ -1,51 +0,0 @@
-image: ralfjung/opam-ci:opam2
-
-stages:
- - build
-
-variables:
- CPU_CORES: "10"
- OCAML: "ocaml-base-compiler.4.14.0"
-
-.template: &template
- stage: build
- tags:
- - fp
- script:
- - git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
- - ci/buildjob
- cache:
- key: "$CI_JOB_NAME"
- paths:
- - _opam/
- only:
- - master@iris/orc11
- - /^ci/@iris/orc11
- except:
- - triggers
- - schedules
- - api
-
-## Build jobs
-
-build-coq.8.15.1:
- <<: *template
- variables:
- OPAM_PINS: "coq version 8.15.1"
- DENY_WARNINGS: "1"
- OPAM_PKG: "1"
- CI_COQCHK: "1"
- tags:
- - fp-timing
-
-build-coq.8.14.1:
- <<: *template
- variables:
- OPAM_PINS: "coq version 8.14.1"
- DENY_WARNINGS: "1"
-
-build-coq.8.13.2:
- <<: *template
- variables:
- OPAM_PINS: "coq version 8.13.2"
- DENY_WARNINGS: "1"
diff --git a/LICENSE b/LICENSE
deleted file mode 100644
index dc298ab5..00000000
--- a/LICENSE
+++ /dev/null
@@ -1,28 +0,0 @@
-All files in this development are distributed under the terms of the BSD
-license, included below.
-
-Copyright: orc11 developers and contributors
-
-------------------------------------------------------------------------------
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are met:
- * Redistributions of source code must retain the above copyright
- notice, this list of conditions and the following disclaimer.
- * Redistributions in binary form must reproduce the above copyright
- notice, this list of conditions and the following disclaimer in the
- documentation and/or other materials provided with the distribution.
- * Neither the name of the copyright holder nor the names of its contributors
- may be used to endorse or promote products derived from this software
- without specific prior written permission.
-
-THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
-ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
-WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
-ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
-(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
-LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
-ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Makefile b/Makefile
deleted file mode 100644
index ac8dba01..00000000
--- a/Makefile
+++ /dev/null
@@ -1,55 +0,0 @@
-# Default target
-all: Makefile.coq
- +@$(MAKE) -f Makefile.coq all
-.PHONY: all
-
-# Permit local customization
--include Makefile.local
-
-# Forward most targets to Coq makefile (with some trick to make this phony)
-%: Makefile.coq phony
- @#echo "Forwarding $@"
- +@$(MAKE) -f Makefile.coq $@
-phony: ;
-.PHONY: phony
-
-clean: Makefile.coq
- +@$(MAKE) -f Makefile.coq clean
- @# Make sure not to enter the `_opam` folder.
- find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
- rm -f Makefile.coq .lia.cache builddep/*
-.PHONY: clean
-
-# Create Coq Makefile.
-Makefile.coq: _CoqProject Makefile
- "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
-
-# Install build-dependencies
-OPAMFILES=$(wildcard *.opam)
-BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
-
-builddep/%-builddep.opam: %.opam Makefile
- @echo "# Creating builddep package for $<."
- @mkdir -p builddep
- @sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
-
-builddep-opamfiles: $(BUILDDEPFILES)
-.PHONY: builddep-opamfiles
-
-builddep: builddep-opamfiles
- @# We want opam to not just install the build-deps now, but to also keep satisfying these
- @# constraints. Otherwise, `opam upgrade` may well update some packages to versions
- @# that are incompatible with our build requirements.
- @# To achieve this, we create a fake opam package that has our build-dependencies as
- @# dependencies, but does not actually install anything itself.
- @echo "# Installing builddep packages."
- @opam install $(OPAMFLAGS) $(BUILDDEPFILES)
-.PHONY: builddep
-
-# Backwards compatibility target
-build-dep: builddep
-.PHONY: build-dep
-
-# Some files that do *not* need to be forwarded to Makefile.coq.
-# ("::" lets Makefile.local overwrite this.)
-Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
diff --git a/README.md b/README.md
deleted file mode 100644
index ea9e5526..00000000
--- a/README.md
+++ /dev/null
@@ -1,56 +0,0 @@
-# ORC11 (Operational Repaired C11) COQ DEVELOPMENT
-
-ORC11 provides an operational version of [RC11] without SC accesses and SC fences,
-and with a race detector for non-atomics.
-
-In [thread.v](theories/thread.v), the definition of the semantics
-is decomposed into 3 relations `lbl_machine_step`, `drf_pre`, and `drf_post`.
-`lbl_machine_step` concerns the main semantics of views, while `drf_pre` and
-`drf_post` implement the race detector (Section 5.1 of the RBrlx paper).
-
-## Race detector simplified
-
-The race detector is summarized as follows (NA: non-atomic / AT : atomic):
-* An NA write must have seen all other operations
-* An NA read must have seen all writes (NA & AT)
-* An AT write must have seen all NA operations (read & writes)
-* An AT read must have seen all NA writes
-
-| Must have seen | NA write | NA read | AT write | AT read |
-| -----------------| --------:| --------:| --------:| -------:|
-| NA write | + | + | + | + |
-| NA read | + | | + | |
-| AT write | + | + | | |
-| AT read | + | | | |
-
-
-## Prerequisites
-
-This version is known to compile with:
-
- - Coq 8.13.2 / 8.14.1 / 8.15.1
- - A development version of [stdpp]. See the [opam](opam) file for the exact
- version.
-
-The easiest way to install the correct versions of the dependencies is through
-opam (2.0.0 or newer). You will need the Coq and Iris opam repositories:
-
- opam repo add coq-released https://coq.inria.fr/opam/released
- opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
-
-Once you got opam set up, run `make build-dep` to install the right versions
-of the dependencies.
-
-## Updating
-
-After doing `git pull`, the development may fail to compile because of outdated
-dependencies. To fix that, please run `opam update` followed by
-`make build-dep`.
-
-## Building Instructions
-
-Run `make -jN` to build the full development, where `N` is the number of your
-CPU cores.
-
-[RC11]: http://plv.mpi-sws.org/scfix/
-[stdpp]: https://gitlab.mpi-sws.org/iris/stdpp
diff --git a/_CoqProject b/_CoqProject
deleted file mode 100644
index 329d13de..00000000
--- a/_CoqProject
+++ /dev/null
@@ -1,17 +0,0 @@
--Q theories orc11
-# We sometimes want to locally override notation, and there is no good way to do that with scopes.
--arg -w -arg -notation-overridden
-# Cannot use non-canonical projections as it causes massive unification failures
-# (https://github.com/coq/coq/issues/6294).
--arg -w -arg -redundant-canonical-projection
-
-theories/base.v
-theories/value.v
-theories/mem_order.v
-theories/event.v
-theories/location.v
-theories/view.v
-theories/memory.v
-theories/tview.v
-theories/thread.v
-theories/progress.v
diff --git a/theories/base.v b/orc11/base.v
similarity index 100%
rename from theories/base.v
rename to orc11/base.v
diff --git a/theories/event.v b/orc11/event.v
similarity index 100%
rename from theories/event.v
rename to orc11/event.v
diff --git a/theories/location.v b/orc11/location.v
similarity index 100%
rename from theories/location.v
rename to orc11/location.v
diff --git a/theories/mem_order.v b/orc11/mem_order.v
similarity index 100%
rename from theories/mem_order.v
rename to orc11/mem_order.v
diff --git a/theories/memory.v b/orc11/memory.v
similarity index 100%
rename from theories/memory.v
rename to orc11/memory.v
diff --git a/theories/progress.v b/orc11/progress.v
similarity index 100%
rename from theories/progress.v
rename to orc11/progress.v
diff --git a/theories/thread.v b/orc11/thread.v
similarity index 100%
rename from theories/thread.v
rename to orc11/thread.v
diff --git a/theories/tview.v b/orc11/tview.v
similarity index 100%
rename from theories/tview.v
rename to orc11/tview.v
diff --git a/theories/value.v b/orc11/value.v
similarity index 100%
rename from theories/value.v
rename to orc11/value.v
diff --git a/theories/view.v b/orc11/view.v
similarity index 100%
rename from theories/view.v
rename to orc11/view.v
--
GitLab