prepare for merge into gpfsl repo

.gitignore

-*.vo
-*.vio
-*.v.d
-*.coq.d
-*.vok
-*.vos
-*.glob
-*.cache
-*.aux
-\#*\#
-.\#*
-*~
-*.bak
-.coq-native/
-Makefile.coq
-Makefile.coq.conf
-builddep/
-*.crashcoqide
-.coqdeps.d
-_opam

.gitlab-ci.yml

-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"

LICENSE

-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.

Makefile

-# 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):: ;

README.md

-# 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

_CoqProject

--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