...
 
Commits (41)
......@@ -12,3 +12,5 @@ Makefile.coq
Makefile.coq.conf
.coq-native/
build-dep
_opam
.coqdeps.d
image: ralfjung/opam-ci:latest
image: ralfjung/opam-ci:opam2
stages:
- build
variables:
CPU_CORES: "9"
CPU_CORES: "10"
.template: &template
stage: build
tags:
- fp-timing
- fp
script:
# prepare
- . build/opam-ci.sh $OPAM_PINS
- env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
# build
- 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt'
- 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
- 'if test -n "$VALIDATE" && (( RANDOM % 10 == 0 )); then make validate; fi'
- git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
- ci/buildjob
cache:
key: "$CI_JOB_NAME"
paths:
......@@ -22,29 +20,22 @@ variables:
only:
- master
- /^ci/
build-coq8.7:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.dev coq-mathcomp-ssreflect version dev"
except:
- triggers
- schedules
## Build jobs
build-coq8.6.1:
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.6.1 coq-mathcomp-ssreflect version 1.6.1"
VALIDATE: "1"
artifacts:
paths:
- build-time.txt
- build-env.txt
except:
- triggers
OPAM_PINS: "coq version 8.8.2"
build-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.6.1 coq-mathcomp-ssreflect version 1.6.1 coq-iris.dev git https://gitlab.mpi-sws.org/FP/iris-coq.git#master"
OPAM_PINS: "coq version 8.8.2 coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/FP/iris-coq.git#$IRIS_REV"
except:
only:
- triggers
- schedules
[submodule "ci"]
path = ci
url = https://gitlab.mpi-sws.org/FP/iris-ci.git
All files in this development are distributed under the terms of the BSD
license, included below.
------------------------------------------------------------------------------
BSD LICENCE
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 <organization> 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 <COPYRIGHT HOLDER> 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.
......@@ -8,19 +8,17 @@ all: Makefile.coq
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
find theories $$(test -d tests && echo tests) \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
rm -f Makefile.coq
.PHONY: clean
# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
# filename, so we do some file gymnastics.
Makefile.coq: _CoqProject Makefile awk.Makefile
coq_makefile -f _CoqProject -o Makefile.coq
mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
# Create Coq Makefile.
Makefile.coq: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
# Install build-dependencies
build-dep/opam: opam Makefile
# Creating the build-dep package.
@echo "# Creating build-dep package."
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
......@@ -30,18 +28,19 @@ build-dep: build-dep/opam phony
@# 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.
@# Upgrading is needed in case the pin already exists, but the builddep package changed.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
echo "# Pinning build-dep package." && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
echo "# Updating build-dep package." && \
opam upgrade "$$BUILD_DEP_PACKAGE"
@# dependencies, but does not actually install anything itself.
@echo "# Pinning build-dep package." && \
if opam --version | grep "^1\." -q; then \
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
else \
opam install $(OPAMFLAGS) build-dep/; \
fi
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
awk.Makefile: ;
opam: ;
# Phony wildcard targets
......
uninstall::
@# This makes sure we also delete stale files in the destination directory
$(HIDE)df="$(COQLIBINSTALL)/`$(COQMKFILE) -destination-of "theories/base.v" $(COQLIBS)`" &&\
echo "RM in $$df" &&\
if [ -d "$$df" ]; then find "$$df" \( -name "*.vo" -o -name "*.v" -o -name "*.glob" -o \( -type d -empty \) \) -print -delete; fi
# Repository Archived
This repository is archived. For the current version of the Coq examples, see
[iris-examples](https://gitlab.mpi-sws.org/iris/examples/tree/master/theories/logatom).
# IRIS-ATOMIC
Atomicity related verification based on Iris logic.
......@@ -6,26 +12,23 @@ Atomicity related verification based on Iris logic.
This version is known to compile with:
- Coq 8.6.1
- Ssreflect 1.6.1
- Coq 8.8.2
- A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
The easiest way to install the correct versions of the dependencies is through
opam. Once you got opam set up, just run `make build-dep` to install the right
versions of the dependencies. When the dependencies change (e.g., a newer
version of Iris is needed), just run `make build-dep` again.
## Building from source
Alternatively, you can manually determine the required Iris commit by consulting
the `opam.pins` file.
When building from source, we recommend to use opam (1.2.2 or newer) for
installing the dependencies. This requires the following two repositories:
## Building Instructions
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
Run `make` to build the full development.
Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.
## For Developers: How to update the Iris dependency
Run `make -jN` to build the full development, where `N` is the number of your
CPU cores.
- Do the change in Iris, push it.
- In iris-atomic, change opam.pins to point to the new commit.
- Run "make build-dep" (in iris-atomic) to install the new version of Iris.
- You may have to do "make clean" as Coq will likely complain about .vo file
mismatches.
To update, do `git pull`. After an update, the development may fail to compile
because of outdated dependencies. To fix that, please run `opam update`
followed by `make build-dep`.
-Q theories iris_atomic
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/atomic.v
theories/sync.v
theories/atomic_incr.v
theories/simple_sync.v
theories/flat.v
theories/atomic_sync.v
......
# awk program that patches the Makefile generated by Coq.
# Detect the name this project will be installed under.
/\$\(COQLIBINSTALL\)\/.*\/\$\$i/ {
# Wow, POSIX awk is really broken. I mean, isn't it supposed to be a text processing language?
# And there is not even a way to access the matched groups of a regexp...?!? Lucky enough,
# we can just split the string at '/' here.
split($0, PIECES, /\//);
PROJECT=PIECES[2];
}
# Patch the uninstall target to work properly, and to also uninstall stale files.
# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
# This (and the section above) can be removed once we no longer support Coq 8.6.
/^uninstall: / {
print "uninstall:";
print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
getline;
next
}
# Add new target quick2vo to (a) run "make quick" with the same number of jobs, ensuring
# that the .vio files are up-to-date, and (b) only schedule vio2vo for those
# files where the .vo is *older* than the .vio.
/^vio2vo:/ {
print "quick2vo:";
print "\t@make -j $(J) quick"
print "\t@VIOFILES=$$(for vofile in $(VOFILES); do viofile=\"$$(echo \"$$vofile\" | sed \"s/\\.vo/.vio/\")\"; if [ \"$$vofile\" -ot \"$$viofile\" -o ! -e \"$$vofile\" ]; then echo -n \"$$viofile \"; fi; done); \\"
print "\t echo \"VIO2VO: $$VIOFILES\"; \\"
print "\t if [ -n \"$$VIOFILES\" ]; then $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
print ".PHONY: quick2vo"
}
# This forwards all unchanged lines
1
#!/bin/bash
set -e
## This script installs the build dependencies for CI builds.
function run_and_print() {
echo "$ $@"
"$@"
}
# Prepare OPAM configuration
export OPAMROOT="$(pwd)/opamroot"
export OPAMJOBS="$((2*$CPU_CORES))"
export OPAM_EDITOR="$(which false)"
# Make sure we got a good OPAM.
test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && run_and_print opam init --no-setup -y)
eval `opam conf env`
# Make sure the pin for the builddep package is not stale.
run_and_print make build-dep/opam
# Update repositories
if test $(find "$OPAMROOT/repo/package-index" -mtime +0); then
# last update was more than a day ago
run_and_print opam update
else
# only update iris-dev, and only if it already exists
if test -d "$OPAMROOT/repo/iris-dev"; then run_and_print opam update iris-dev; fi
fi
# Make sure we got the right set of repositories registered
if echo "$@" | fgrep "dev"; then
# We are compiling against a dev version of something. Get ourselves the dev repositories.
test -d "$OPAMROOT/repo/coq-extra-dev" || run_and_print opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 0
test -d "$OPAMROOT/repo/coq-core-dev" || run_and_print opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
else
# No dev version, make sure we do not have the dev repositories.
test -d "$OPAMROOT/repo/coq-extra-dev" && run_and_print opam repo remove coq-extra-dev
test -d "$OPAMROOT/repo/coq-core-dev" && run_and_print opam repo remove coq-core-dev
fi
test -d "$OPAMROOT/repo/coq-released" || run_and_print opam repo add coq-released https://coq.inria.fr/opam/released -p 10
test -d "$OPAMROOT/repo/iris-dev" || run_and_print opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
echo
# We really want to run all of the following in one opam transaction, but due to opam limitations,
# that is not currently possible.
# Install fixed versions of some dependencies.
echo
while (( "$#" )); do # while there are arguments left
PACKAGE="$1" ; shift
KIND="$1" ; shift
VERSION="$1" ; shift
# Check if the pin is already set
PIN=$(opam pin list | (egrep "^$PACKAGE[. ]" || true))
if [[ "$(echo "$PIN" | cut -d ' ' -f 2)" == "$KIND" && "$(echo "$PIN" | cut -d ' ' -f 3)" == "$VERSION" ]]; then
echo "[opam-ci] $PACKAGE already $KIND-pinned to $VERSION"
else
echo "[opam-ci] $KIND-pinning $PACKAGE to $VERSION"
run_and_print opam pin add -y -k "$KIND" "$PACKAGE" "$VERSION"
fi
done
# Upgrade cached things.
echo
echo "[opam-ci] Upgrading opam"
run_and_print opam upgrade -y
# Install build-dependencies.
echo
echo "[opam-ci] Installing build-dependencies"
make build-dep OPAMFLAGS=-y
# done
echo
coqc -v
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_atomic"]
depends: [
"coq-iris" { (= "dev.2017-09-27.1") | (= "dev") }
"coq-iris" { (= "dev.2018-10-31.4.4a1eb8a3") | (= "dev") }
]
(* Logically atomic triple *)
From iris.base_logic Require Export fancy_updates.
From iris.program_logic Require Export hoare weakestpre.
Import uPred.
Section atomic.
Context `{irisG Λ Σ} {A: Type}.
(* TODO RJ: IMHO it would make more sense to have the outer mask first, after all, that's what the shifts "starts" with. *)
(* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
Definition atomic_triple
(α: A iProp Σ) (* atomic pre-condition *)
(β: A val _ iProp Σ) (* atomic post-condition *)
(Ei Eo: coPset) (* inside/outside masks *)
(e: expr _) : iProp Σ :=
( P Q, (P ={Eo, Ei}=> x:A,
α x
((α x ={Ei, Eo}= P)
( v, β x v ={Ei, Eo}= Q v))
) - {{ P }} e @ {{ Q }})%I.
End atomic.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris_atomic Require Import atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang.lib Require Import par.
Section incr.
Context `{!heapG Σ} (N : namespace).
Definition incr: val :=
rec: "incr" "l" :=
let: "oldv" := !"l" in
if: CAS "l" "oldv" ("oldv" + #1)
then "oldv" (* return old value if success *)
else "incr" "l".
(* TODO: Can we have a more WP-style definition and avoid the equality? *)
Definition incr_triple (l: loc) :=
atomic_triple (fun (v: Z) => l #v)%I
(fun v ret => ret = #v l #(v + 1))%I
(incr #l).
Lemma incr_atomic_spec: (l: loc), incr_triple l.
Proof.
iIntros (l).
rewrite /incr_triple.
rewrite /atomic_triple.
iIntros (P Q) "#Hvs".
iLöb as "IH".
iIntros "!# HP".
wp_rec.
wp_bind (! _)%E.
iMod ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
wp_load.
iMod ("Hvs'" with "Hl") as "HP".
iModIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
iMod ("Hvs" with "HP") as (x') "[Hl Hvs']".
destruct (decide (x = x')).
- subst.
iDestruct "Hvs'" as "[_ Hvs']".
iSpecialize ("Hvs'" $! #x').
wp_cas_suc.
iMod ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
iModIntro. wp_if. done.
- iDestruct "Hvs'" as "[Hvs' _]".
wp_cas_fail.
iMod ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
iModIntro. wp_if. by iApply "IH".
Qed.
End incr.
Section user.
Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Definition incr_2 : val :=
λ: "x",
let: "l" := ref "x" in
incr "l" ||| incr "l";;
!"l".
(* prove that incr is safe w.r.t. data race. TODO: prove a stronger post-condition *)
Lemma incr_2_safe:
(x: Z), (WP incr_2 #x {{ _, True }})%I.
Proof.
iIntros (x).
rewrite /incr_2 /=.
wp_lam.
wp_alloc l as "Hl".
iMod (inv_alloc N _ (x':Z, l #x')%I with "[Hl]") as "#?"; first eauto.
wp_let.
wp_bind (_ ||| _)%E.
iAssert ( WP incr #l {{ _, True }})%I as "#?".
{ (* prove worker triple *)
iDestruct (incr_atomic_spec l) as "Hincr"=>//.
rewrite /incr_triple /atomic_triple.
iSpecialize ("Hincr" $! True%I (fun _ => True%I) with "[]").
- iIntros "!# _".
(* open the invariant *)
iInv N as (x') ">Hl'" "Hclose".
(* mask magic *)
iMod (fupd_intro_mask' _ ) as "Hvs"; first set_solver.
iModIntro. iExists x'. iFrame "Hl'". iSplit.
+ (* provide a way to rollback *)
iIntros "Hl'".
iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
+ (* provide a way to commit *)
iIntros (v) "[Heq Hl']".
iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
- iDestruct "Hincr" as "#HIncr". iAlways. by iApply "HIncr". }
iApply (wp_par (λ _, True%I) (λ _, True%I) with "[] []"); [done..|].
iIntros (v1 v2) "_ !>".
wp_seq. iInv N as (x') ">Hl" "Hclose".
wp_load. iApply "Hclose". eauto.
Qed.
End user.
From iris.program_logic Require Export weakestpre hoare.
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 atomic sync misc.
From iris_atomic Require Import sync misc.
(** The simple syncer spec in [sync.v] implies a logically atomic spec. *)
Definition syncR := prodR fracR (agreeR valC). (* track the local knowledge of ghost state *)
Class syncG Σ := sync_tokG :> inG Σ syncR.
......@@ -27,9 +29,7 @@ Section atomic_sync.
(* TODO: Provide better masks. as inner mask is pretty weak. *)
Definition atomic_synced (ϕ: A iProp Σ) γ (f f': val) :=
( α β (x: val), atomic_seq_spec ϕ α β f x
atomic_triple (fun g => gHalf γ g α g)%I
(fun g v => g', gHalf γ g' β g g' v)%I
(f' x))%I.
<<< g, gHalf γ g α g >>> f' x @ <<< v, g', gHalf γ g' β g g' v, RET v >>>)%I.
(* TODO: Use our usual style with a generic post-condition. *)
(* TODO: We could get rid of the x, and hard-code a unit. That would
......@@ -57,24 +57,23 @@ Section atomic_sync.
iSplitL "Hg2"; first done. iIntros "!#".
iIntros (f). iApply wp_wand_r. iSplitR; first by iApply "Hsyncer".
iIntros (f') "#Hsynced {Hsyncer}".
iAlways. iIntros (α β x) "#Hseq".
iIntros (P Q) "#Hvss !# HP".
iAlways. iIntros (α β x) "#Hseq". change (ofe_car AC) with A.
iApply wp_atomic_intro. iIntros (Φ') "?".
(* TODO: Why can't I iApply "Hsynced"? *)
iSpecialize ("Hsynced" $! P Q x).
iApply wp_wand_r. iSplitL "HP".
- iApply ("Hsynced" with "[]")=>//.
iSpecialize ("Hsynced" $! _ Φ' x).
iApply wp_wand_r. iSplitL.
- iApply ("Hsynced" with "[]")=>//; last iAccu.
iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ Hg1]".
(* we should view shift at this point *)
iDestruct ("Hvss" with "HP") as "Hvss'". iApply fupd_wp.
iMod "Hvss'". iDestruct "Hvss'" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
iDestruct (m_frag_agree with "[Hg1 Hg2]") as %Heq; first iFrame. subst.
iApply fupd_wp. iMod "HP" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
iDestruct (m_frag_agree with "Hg1 Hg2") as %Heq. subst.
iMod ("Hvs1" with "[Hg2]") as "HP"; first by iFrame.
iModIntro. iApply wp_fupd. iApply wp_wand_r. iSplitL "Hϕ".
{ iApply "Hseq". iFrame. done. }
iIntros (v) "H". iDestruct "H" as (g') "[Hϕ' Hβ]".
iMod ("Hvss" with "HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
iMod ("HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
iSpecialize ("Hvs2" $! v).
iDestruct (m_frag_agree' with "[Hg'' Hg1]") as "[Hg %]"; first iFrame. subst.
iDestruct (m_frag_agree' with "Hg'' Hg1") as "[Hg %]". subst.
rewrite Qp_div_2.
iAssert (|==> own γ (((1 / 2)%Qp, to_agree g') ((1 / 2)%Qp, to_agree g')))%I
with "[Hg]" as ">[Hg1 Hg2]".
......
......@@ -4,7 +4,7 @@ From iris.heap_lang Require Export lang.
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 big_op saved_prop.
From iris.base_logic Require Import saved_prop.
From iris_atomic Require Import misc peritem sync.
Definition doOp : val :=
......@@ -50,12 +50,12 @@ Definition reqR := prodR fracR (agreeR valC). (* request x should be kept same *
Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
Class flatG Σ := FlatG {
req_G :> inG Σ reqR;
sp_G :> savedPropG Σ (ofe_funCF val idCF)
sp_G :> savedPredG Σ val
}.
Definition flatΣ : gFunctors :=
#[ GFunctor (constRF reqR);
savedPropΣ (ofe_funCF val idCF) ].
savedPredΣ val ].
Instance subG_flatΣ {Σ} : subG flatΣ Σ flatG Σ.
Proof. intros [?%subG_inG [? _]%subG_inv]%subG_inv. split; apply _. Qed.
......@@ -70,7 +70,7 @@ Section proof.
let '(γx, γ1, _, γ4, γq) := ts in
( (P: val iProp Σ) Q,
own γx ((1/2)%Qp, to_agree x) P x ({{ R P x }} f x {{ v, R Q x v }})
saved_prop_own γq (Q x) own γ1 (Excl ()) own γ4 (Excl ()))%I.
saved_pred_own γq (Q x) own γ1 (Excl ()) own γ4 (Excl ()))%I.
Definition received_s (ts: toks) (x: val) γr :=
let '(γx, _, _, γ4, _) := ts in
......@@ -79,7 +79,7 @@ Section proof.
Definition finished_s (ts: toks) (x y: val) :=
let '(γx, γ1, _, γ4, γq) := ts in
( Q: val val iProp Σ,
own γx ((1/2)%Qp, to_agree x) saved_prop_own γq (Q x)
own γx ((1/2)%Qp, to_agree x) saved_pred_own γq (Q x)
Q x y own γ1 (Excl ()) own γ4 (Excl ()))%I.
Definition p_inv R (γm γr: gname) (ts: toks) (p : loc) :=
......@@ -99,7 +99,7 @@ Section proof.
Definition installed_recp (ts: toks) (x: val) (Q: val iProp Σ) :=
let '(γx, _, γ3, _, γq) := ts in
(own γ3 (Excl ()) own γx ((1/2)%Qp, to_agree x) saved_prop_own γq Q)%I.
(own γ3 (Excl ()) own γx ((1/2)%Qp, to_agree x) saved_pred_own γq Q)%I.
Lemma install_spec R P Q (f x: val) (γm γr: gname) (s: loc):
{{{ inv N (srv_bag R γm γr s) P ({{ R P }} f x {{ v, R Q v }}) }}}
......@@ -107,13 +107,13 @@ Section proof.
{{{ p ts, RET #p; installed_recp ts x Q inv N (p_inv R γm γr ts p) }}}.
Proof.
iIntros (Φ) "(#? & HP & Hf) HΦ".
wp_seq. wp_let. wp_let. wp_alloc p as "Hl".
wp_lam. wp_pures. wp_alloc p as "Hl".
iApply fupd_wp.
iMod (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
iMod (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
iMod (own_alloc (1%Qp, to_agree x)) as (γx) "Hx"; first done.
iMod (saved_prop_alloc (F:=(ofe_funCF val idCF)) Q) as (γq) "#?".
iMod (saved_pred_alloc Q) as (γq) "#?".
iDestruct (own_update with "Hx") as ">[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
iModIntro. wp_let. wp_bind (push _ _).
iMod (inv_alloc N _ (p_inv R γm γr (γx, γ1, γ3, γ4, γq) p)
......@@ -151,10 +151,10 @@ Section proof.
by apply pair_l_frac_op'. }
wp_load. iMod ("Hclose" with "[-Hf' Ho1 Hx2 HoQ HR HΦ Hpx]").
{ iNext. iFrame. iFrame "#". iRight. iRight. iLeft. iExists f, x. iFrame. }
iModIntro. wp_match. wp_proj. wp_proj.
iModIntro. wp_match. wp_pures.
wp_bind (f _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
{ iApply "Hf'". iFrame. }
iIntros (v) "[HR HQ]".
iIntros (v) "[HR HQ]". wp_pures.
iInv N as "Hx" "Hclose".
iDestruct "Hx" as "[Hp | [Hp | [Hp | Hp]]]"; subst.
* iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
......@@ -162,10 +162,10 @@ Section proof.
* iDestruct "Hp" as (? ?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
iApply excl_falso. iFrame.
* iDestruct "Hp" as (? x5) ">(Hp & Hx & Hor & Ho4)".
wp_store. iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
wp_store. iDestruct (m_frag_agree' with "Hx Hx2") as "[Hx %]".
subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ]").
{ iNext. iDestruct "Hp" as "[Hp1 Hp2]". iRight. iRight.
iRight. iExists x5, v. iFrame. iExists Q. iFrame. }
iRight. iExists _, v. iFrame. iExists Q. iFrame. }
iApply "HΦ". iFrame. done.
* iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
iApply excl_falso. iFrame.
......@@ -181,7 +181,7 @@ Section proof.
Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()).
Definition finished_recp (ts: toks) (x y: val) :=
let '(γx, _, _, _, γq) := ts in
( Q, own γx ((1 / 2)%Qp, to_agree x) saved_prop_own γq (Q x) Q x y)%I.
( Q, own γx ((1 / 2)%Qp, to_agree x) saved_pred_own γq (Q x) Q x y)%I.
Lemma loop_iter_doOp_spec R (γm γr: gname) xs:
(hd: loc),
......@@ -215,7 +215,7 @@ Section proof.
is_lock N γlk lk (own γr (Excl ()) R) Φ #()
WP try_srv lk #s {{ Φ }}.
Proof.
iIntros "(#? & #? & HΦ)". wp_seq. wp_let.
iIntros "(#? & #? & HΦ)". wp_lam. wp_pures.
wp_bind (try_acquire _). iApply (try_acquire_spec with "[]"); first done.
iNext. iIntros ([]); last by (iIntros; wp_if).
iIntros "[Hlocked [Ho2 HR]]".
......@@ -271,16 +271,16 @@ Section proof.
Proof.
iIntros (R Φ) "HR HΦ".
iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done.
wp_seq. wp_bind (newlock _).
wp_lam. wp_bind (newlock _).
iApply (newlock_spec _ (own γr (Excl ()) R)%I with "[$Ho2 $HR]")=>//.
iNext. iIntros (lk γlk) "#Hlk".
wp_let. wp_bind (new_stack _).
iApply (new_bag_spec N (p_inv' R γm γr))=>//.
iNext. iIntros (s) "#Hss".
wp_let. iApply "HΦ". rewrite /synced.
iAlways. iIntros (f). wp_let. iAlways.
wp_pures. iApply "HΦ". rewrite /synced.
iAlways. iIntros (f). wp_pures. iAlways.
iIntros (P Q x) "#Hf".
iIntros "!# Hp". wp_let. wp_bind (install _ _ _).
iIntros "!# Hp". wp_pures. wp_bind (install _ _ _).
iApply (install_spec R P Q f x γm γr s with "[-]")=>//.
{ iFrame. iFrame "#". }
iNext. iIntros (p [[[[γx γ1] γ3] γ4] γq]) "[(Ho3 & Hx & HoQ) #?]".
......@@ -290,9 +290,8 @@ Section proof.
iNext. iIntros (? ?) "Hs".
iDestruct "Hs" as (Q') "(Hx' & HoQ' & HQ')".
destruct (decide (x = a)) as [->|Hneq].
- iDestruct (saved_prop_agree with "[$HoQ] [HoQ']") as "Heq"; first by iFrame.
wp_let. iDestruct (uPred.ofe_funC_equivI with "Heq") as "Heq".
iSpecialize ("Heq" $! a0). by iRewrite -"Heq" in "HQ'".
- iDestruct (saved_pred_agree _ _ _ a0 with "[$HoQ] [HoQ']") as "Heq"; first by iFrame.
wp_let. by iRewrite -"Heq" in "HQ'".
- iExFalso. iCombine "Hx" "Hx'" as "Hx".
iDestruct (own_valid with "Hx") as %[_ H1].
rewrite //= in H1.
......
......@@ -3,7 +3,8 @@
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.algebra Require Import auth frac gmap agree.
From iris.base_logic Require Import big_op auth fractional.
From iris.bi Require Import fractional.
From iris.base_logic Require Import auth.
Import uPred.
......@@ -60,12 +61,12 @@ Section big_op_later.
End big_op_later.
Section pair.
Context {A : ofeT} `{EqDecision A, !Discrete A, !LeibnizEquiv A, !inG Σ (prodR fracR (agreeR A))}.
Context {A : ofeT} `{EqDecision A, !OfeDiscrete A, !LeibnizEquiv A, !inG Σ (prodR fracR (agreeR A))}.
Lemma m_frag_agree γm (q1 q2: Qp) (a1 a2: A):
own γm (q1, to_agree a1) own γm (q2, to_agree a2) a1 = a2.
own γm (q1, to_agree a1) - own γm (q2, to_agree a2) - a1 = a2.
Proof.
iIntros "[Ho Ho']".
iIntros "Ho Ho'".
destruct (decide (a1 = a2)) as [->|Hneq]=>//.
iCombine "Ho" "Ho'" as "Ho".
iDestruct (own_valid with "Ho") as %Hvalid.
......@@ -75,11 +76,11 @@ Section pair.
Qed.
Lemma m_frag_agree' γm (q1 q2: Qp) (a1 a2: A):
own γm (q1, to_agree a1) own γm (q2, to_agree a2)
own γm ((q1 + q2)%Qp, to_agree a1) a1 = a2.
own γm (q1, to_agree a1) - own γm (q2, to_agree a2)
- own γm ((q1 + q2)%Qp, to_agree a1) a1 = a2.
Proof.
iIntros "[Ho Ho']".
iDestruct (m_frag_agree with "[Ho Ho']") as %Heq; first iFrame.
iIntros "Ho Ho'".
iDestruct (m_frag_agree with "Ho Ho'") as %Heq.
subst. iCombine "Ho" "Ho'" as "Ho".
by iFrame.
Qed.
......
......@@ -3,9 +3,8 @@ 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.base_logic Require Import big_op.
From iris_atomic Require Export treiber misc.
From iris.base_logic.lib Require Import invariants namespaces.
From iris.base_logic.lib Require Import invariants.
Section defs.
Context `{heapG Σ} (N: namespace).
......@@ -48,7 +47,7 @@ Section proofs.
{{{ True }}} new_stack #() {{{ s, RET #s; bag_inv s }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply wp_fupd.
wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
wp_lam. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
wp_alloc s as "Hs".
iAssert (( xs, is_bag_R N R xs s))%I with "[-HΦ]" as "Hxs".
{ iFrame. iExists [], l.
......
......@@ -22,12 +22,12 @@ Section syncer.
Lemma mk_sync_spec: mk_syncer_spec mk_sync.
Proof.
iIntros (R Φ) "HR HΦ".
wp_seq. wp_bind (newlock _).
wp_lam. wp_bind (newlock _).
iApply (newlock_spec N R with "[HR]"); first done. iNext.
iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#".
iIntros (f). wp_let. iAlways.
iIntros (lk γ) "#Hl". wp_pures. iApply "HΦ". iIntros "!#".
iIntros (f). wp_pures. iAlways.
iIntros (P Q x) "#Hf !# HP".
wp_let. wp_bind (acquire _).
wp_pures. wp_bind (acquire _).
iApply (acquire_spec with "Hl"). iNext.
iIntros "[Hlocked R]". wp_seq. wp_bind (f _).
iSpecialize ("Hf" with "[R HP]"); first by iFrame.
......
......@@ -10,7 +10,7 @@ Section sync.
(* TODO: We could get rid of the x, and hard-code a unit. That would
be no loss in expressiveness, but probably more annoying to apply.
How much more annoying? And how much to we gain in terms of things
becomign easier to prove? *)
becoming easier to prove? *)
Definition synced R (f f': val) :=
( P Q (x: val), {{ R P }} f x {{ v, R Q v }}
{{ P }} f' x {{ Q }})%I.
......
From iris.program_logic Require Export weakestpre.
From stdpp Require Import namespaces.
From iris.program_logic Require Export weakestpre atomic.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import frac auth gmap csum.
From iris.base_logic Require Import big_op.
From iris_atomic Require Import atomic misc.
From iris_atomic Require Import misc.
Definition new_stack: val := λ: <>, ref (ref NONE).
......@@ -81,17 +81,17 @@ Section proof.
Definition is_stack (s: loc) xs: iProp Σ := ( hd: loc, s #hd is_list hd xs)%I.
Global Instance is_list_timeless xs hd: TimelessP (is_list hd xs).
Global Instance is_list_timeless xs hd: Timeless (is_list hd xs).
Proof. generalize hd. induction xs; apply _. Qed.
Global Instance is_stack_timeless xs hd: TimelessP (is_stack hd xs).
Global Instance is_stack_timeless xs hd: Timeless (is_stack hd xs).
Proof. generalize hd. induction xs; apply _. Qed.
Lemma new_stack_spec:
(Φ: val iProp Σ),
( s, is_stack s [] - Φ #s) WP new_stack #() {{ Φ }}.
Proof.
iIntros (Φ) "HΦ". wp_seq.
iIntros (Φ) "HΦ". wp_lam.
wp_bind (ref NONE)%E. wp_alloc l as "Hl".
wp_alloc l' as "Hl'".
iApply "HΦ". rewrite /is_stack. iExists l.
......@@ -99,32 +99,25 @@ Section proof.
Qed.
Definition push_triple (s: loc) (x: val) :=
atomic_triple (fun xs_hd: list val * loc =>
let '(xs, hd) := xs_hd in s #hd is_list hd xs)%I
(fun xs_hd ret =>
let '(xs, hd) := xs_hd in
hd': loc,
ret = #() s #hd' hd' SOMEV (x, #hd) is_list hd xs)%I
(push #s x).
<<< (xs : list val) (hd : loc), s #hd is_list hd xs >>>
push #s x @
<<< hd' : loc, s #hd' hd' SOMEV (x, #hd) is_list hd xs, RET #() >>>.
Lemma push_atomic_spec (s: loc) (x: val) :
push_triple s x.
Proof.
rewrite /push_triple /atomic_triple.
iIntros (P Q) "#Hvs".
iLöb as "IH". iIntros "!# HP". wp_rec.
rewrite /push_triple. iApply wp_atomic_intro.
iIntros (Φ) "HP". iLöb as "IH". wp_rec.
wp_let. wp_bind (! _)%E.
iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
iMod "HP" as (xs hd) "[[Hs Hhd] [Hvs' _]]".
wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame.
iModIntro. wp_let. wp_alloc l as "Hl". wp_let.
wp_bind (CAS _ _ _)%E.
iMod ("Hvs" with "HP") as ([xs' hd']) "[[Hs Hhd'] Hvs']".
iMod "HP" as (xs' hd') "[[Hs Hhd'] Hvs']".
destruct (decide (hd = hd')) as [->|Hneq].
* wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" $! #() with "[-]") as "HQ".
{ iExists l. iSplitR; first done. by iFrame. }
iMod ("Hvs'" with "[-]") as "HQ".
{ by iFrame. }
iModIntro. wp_if. eauto.
* wp_cas_fail.
iDestruct "Hvs'" as "[Hvs' _]".
......@@ -133,31 +126,25 @@ Section proof.
Qed.
Definition pop_triple (s: loc) :=
atomic_triple (fun xs_hd: list val * loc =>
let '(xs, hd) := xs_hd in s #hd is_list hd xs)%I
(fun xs_hd ret =>
let '(xs, hd) := xs_hd in
(ret = NONEV xs = [] s #hd is_list hd [])
( x q (hd': loc) xs', hd {q} SOMEV (x, #hd') ret = SOMEV x
xs = x :: xs'⌝ s #hd' is_list hd' xs'))%I
(pop #s).
<<< (xs : list val) (hd : loc), s #hd is_list hd xs >>>
pop #s @
<<< match xs with [] => s #hd is_list hd []
| x::xs' => q (hd': loc), hd {q} SOMEV (x, #hd') s #hd' is_list hd' xs' end,
RET match xs with [] => NONEV | x :: _ => SOMEV x end >>>.
Lemma pop_atomic_spec (s: loc):
pop_triple s.
Proof.
rewrite /pop_triple /atomic_triple.
iIntros (P Q) "#Hvs".
iLöb as "IH". iIntros "!# HP". wp_rec.
rewrite /pop_triple. iApply wp_atomic_intro.
iIntros (Φ) "HP". iLöb as "IH". wp_rec.
wp_bind (! _)%E.
iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] Hvs']".
iMod "HP" as (xs hd) "[[Hs Hhd] Hvs']".
destruct xs as [|y' xs'].
- simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']".
iDestruct "Hhd" as (q) "[Hhd Hhd']".
iMod ("Hvs'" $! NONEV with "[-Hhd]") as "HQ".
{ iLeft. iSplit=>//. iSplit=>//. iFrame. eauto. }
iModIntro. wp_let. wp_load. wp_match.
iMod ("Hvs'" with "[-Hhd]") as "HQ".
{ iFrame. eauto. }
iModIntro. wp_let. wp_load. wp_pures.
eauto.
- simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')".
iDestruct (dup_is_list with "[Hxs']") as "[Hxs1 Hxs2]"; first by iFrame.
......@@ -166,21 +153,20 @@ Section proof.
{ iFrame. iExists hd', (q / 2)%Qp. by iFrame. }
iModIntro. wp_let. wp_load. wp_match. wp_proj.
wp_bind (CAS _ _ _).
iMod ("Hvs" with "HP") as ([xs hd'']) "[[Hs Hhd''] Hvs']".
iMod "HP" as (xs hd'') "[[Hs Hhd''] Hvs']".
destruct (decide (hd = hd'')) as [->|Hneq].
+ wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" $! (SOMEV y') with "[-]") as "HQ".
{ iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
destruct xs as [|x' xs''].
- simpl. iDestruct "Hhd''" as (?) "H".
iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1] [$H]") as %?.
- simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
iDestruct (@mapsto_agree with "[$Hhd1] [$Hhd'']") as %[=].
subst.
iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
repeat (iSplitR "Hxs1 Hs"; first done).
iFrame. }
iModIntro. wp_if. wp_proj. eauto.
destruct xs as [|x' xs''].
{ simpl. iDestruct "Hhd''" as (?) "H".
iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1] [$H]") as %?. }
simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
iDestruct (@mapsto_agree with "[$Hhd1] [$Hhd'']") as %[=]. subst.
iMod ("Hvs'" with "[-]") as "HQ".
{ iExists (q / 2 / 2)%Qp, _.
iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
repeat (iSplitR "Hxs1 Hs"; first done).
iFrame. }
iModIntro. wp_if. wp_pures. eauto.
+ wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]".
iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
iModIntro. wp_if. by iApply "IH".
......