Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • snyke7/reloc
  • iris/reloc
  • simonfv/reloc
  • jtassaro/reloc
  • lgaeher/reloc
  • NiklasM/reloc
  • Blaisorblade/reloc
  • arthuraa/reloc
8 results
Show changes
Commits on Source (55)
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 2479 additions and 131 deletions
.gitignore
View file @ 37a694fd
...@@ -14,7 +14,7 @@ ...@@ -14,7 +14,7 @@
.coqdeps.d .coqdeps.d
.coq-native/ .coq-native/
_opam _opam
build-dep/ builddep/
Makefile.coq Makefile.coq
Makefile.coq.conf Makefile.coq.conf
.Makefile.coq.d .Makefile.coq.d
......
.gitlab-ci.yml
View file @ 37a694fd
...@@ -5,6 +5,7 @@ stages: ...@@ -5,6 +5,7 @@ stages:
variables: variables:
CPU_CORES: "10" CPU_CORES: "10"
OCAML: "ocaml-base-compiler.4.14.0"
.template: &template .template: &template
stage: build stage: build
...@@ -27,11 +28,10 @@ variables: ...@@ -27,11 +28,10 @@ variables:
## Build jobs ## Build jobs
build-coq.8.13.0: build-coq.8.20.0:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.13.0" OPAM_PINS: "coq version 8.20.0"
DENY_WARNINGS: "1"
tags: tags:
- fp-timing - fp-timing
...@@ -40,7 +40,7 @@ trigger-iris.dev: ...@@ -40,7 +40,7 @@ trigger-iris.dev:
variables: variables:
STDPP_REPO: "iris/stdpp" STDPP_REPO: "iris/stdpp"
IRIS_REPO: "iris/iris" IRIS_REPO: "iris/iris"
OPAM_PINS: "coq version 8.13.dev git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV" OPAM_PINS: "coq version $NIGHTLY_COQ git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
except: except:
only: only:
- triggers - triggers
......
Makefile
View file @ 37a694fd
# Forward most targets to Coq makefile (with some trick to make this phony) # Default target
%: Makefile.coq phony
+@make -f Makefile.coq $@
all: Makefile.coq all: Makefile.coq
+@make -f Makefile.coq all +@$(MAKE) -f Makefile.coq all
.PHONY: 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 clean: Makefile.coq
+@make -f Makefile.coq clean +@$(MAKE) -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true @# Make sure not to enter the `_opam` folder.
rm -f Makefile.coq .lia.cache 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 .PHONY: clean
# Create Coq Makefile. # Create Coq Makefile.
Makefile.coq: _CoqProject Makefile Makefile.coq: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
# Install build-dependencies # Install build-dependencies
build-dep/opam: opam Makefile OPAMFILES=$(wildcard *.opam)
@echo "# Creating build-dep package." BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam builddep/%-builddep.opam: %.opam Makefile
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check @echo "# Creating builddep package for $<."
@mkdir -p builddep
build-dep: build-dep/opam phony @sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
@# We want opam to not just instal the build-deps now, but to also keep satisfying these
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 @# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements. @# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as @# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything itself. @# dependencies, but does not actually install anything itself.
@echo "# Installing build-dep package." @echo "# Installing builddep packages."
@opam install $(OPAMFLAGS) build-dep/ @opam install $(OPAMFLAGS) $(BUILDDEPFILES)
.PHONY: builddep
# Some files that do *not* need to be forwarded to Makefile.coq # Backwards compatibility target
Makefile: ; build-dep: builddep
_CoqProject: ; .PHONY: build-dep
opam: ;
# Phony wildcard targets # Some files that do *not* need to be forwarded to Makefile.coq.
phony: ; # ("::" lets Makefile.local overwrite this.)
.PHONY: phony Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
README.md
View file @ 37a694fd
...@@ -10,7 +10,7 @@ See the small ReLoC [docs/guide.md](docs/guide.md) and the Iris [ProofGuide.md]( ...@@ -10,7 +10,7 @@ See the small ReLoC [docs/guide.md](docs/guide.md) and the Iris [ProofGuide.md](
## Building ## Building
This project has been tested with Coq 8.13.0. This project has been tested with Coq 8.20.0.
### OPAM ### OPAM
...@@ -43,13 +43,14 @@ they can illustrate the usage of the logic. ...@@ -43,13 +43,14 @@ they can illustrate the usage of the logic.
+ `bit.v` - "representation independence example" for a simple bit interface + `bit.v` - "representation independence example" for a simple bit interface
+ `or.v` - expressing non-determinism with concurrency + `or.v` - expressing non-determinism with concurrency
+ `symbol.v` and `namegen.v` - generative ADTs for symbol and name generation + `symbol.v` and `namegen.v` - generative ADTs for symbol and name generation
+ `stack/refinement.v` - Treiber stack refines sequential stack + `stack` - Treiber stack refines sequential stack
+ `cell.v` - higher-order cell objects + `cell.v` - higher-order cell objects
+ `ticket_lock.v` - ticket lock refines spin lock + `ticket_lock.v` - ticket lock refines spin lock
+ `various.v` - lots of examples with higher-order functions with local state, in the style of "The effects of higher-order state and control on local relational reasoning" paper + `various.v` - lots of examples with higher-order functions with local state, in the style of "The effects of higher-order state and control on local relational reasoning" paper
+ `coinflip.v` and `lateearlychoice.v` - examples with prophecy variable + `coinflip.v` and `lateearlychoice.v` - examples with prophecy variable
+ `stack_helping` - linearizability of stack with helping, see [this technical appendix](https://cs.ru.nl/~dfrumin/reloc/tech-appendix.pdf) for a detailed description
+ `folly_queue` - linearizability of the MPMC queue from the Folly library
- `experimental` more "experimental" stuff - `experimental` more "experimental" stuff
+ `helping/helping_stack.v` - linearizability of stack with helping, see [this technical appendix](https://cs.ru.nl/~dfrumin/reloc/tech-appendix.pdf) for a detailed description
+ `hocap/` - hocap style specifications for a concurrent counter and a refinement proof for a ticket lock + `hocap/` - hocap style specifications for a concurrent counter and a refinement proof for a ticket lock
+ `cka.v` - some axioms from the CKA equational theory + `cka.v` - some axioms from the CKA equational theory
......
_CoqProject
View file @ 37a694fd
...@@ -10,6 +10,7 @@ theories/prelude/properness.v ...@@ -10,6 +10,7 @@ theories/prelude/properness.v
theories/prelude/asubst.v theories/prelude/asubst.v
theories/prelude/bijections.v theories/prelude/bijections.v
theories/prelude/lang_facts.v theories/prelude/lang_facts.v
theories/prelude/arith.v
theories/logic/spec_ra.v theories/logic/spec_ra.v
theories/logic/spec_rules.v theories/logic/spec_rules.v
...@@ -53,13 +54,23 @@ theories/examples/stack/refinement.v ...@@ -53,13 +54,23 @@ theories/examples/stack/refinement.v
theories/examples/various.v theories/examples/various.v
theories/examples/lateearlychoice.v theories/examples/lateearlychoice.v
theories/examples/coinflip.v theories/examples/coinflip.v
theories/examples/red_blue_flag.v
theories/examples/par.v theories/examples/folly_queue/set.v
theories/examples/folly_queue/CG_queue.v
theories/examples/folly_queue/turnSequencer.v
theories/examples/folly_queue/singleElementQueue.v
theories/examples/folly_queue/mpmcqueue.v
theories/examples/folly_queue/refinement.v
theories/examples/folly_queue/ticketLock.v
theories/examples/stack_helping/offers.v
theories/examples/stack_helping/stack.v
theories/examples/stack_helping/helping_wrapper.v
theories/experimental/cka.v
theories/experimental/helping/offers.v theories/examples/par.v
theories/experimental/helping/helping_stack.v theories/experimental/cka.v
theories/experimental/hocap/counter.v theories/experimental/hocap/counter.v
theories/experimental/hocap/ticket_lock.v theories/experimental/hocap/ticket_lock.v
......
opam → coq-reloc.opam
View file @ 37a694fd
opam-version: "1.2" opam-version: "2.0"
name: "coq-reloc"
maintainer: "Ralf Jung <jung@mpi-sws.org>" maintainer: "Ralf Jung <jung@mpi-sws.org>"
authors: "Dan Frumin, Robbert Krebbers" authors: "Dan Frumin, Robbert Krebbers"
homepage: "http://iris-project.org/" homepage: "http://iris-project.org/"
bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues" bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
dev-repo: "https://gitlab.mpi-sws.org/dfrumin/reloc.git" dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
depends: [ depends: [
"coq-iris-heap-lang" { (= "dev.2021-06-18.0.366d607e") | (= "dev") } "coq-iris-heap-lang" { (= "dev.2025-03-28.0.fa344cbe") | (= "dev") }
"coq-autosubst" { = "dev" } "coq-autosubst" { = "dev" }
] ]
build: [make "-j%{jobs}%"]
install: [make "install"]
theories/examples/bit.v
View file @ 37a694fd
(* ReLoC -- Relational logic for fine-grained concurrency *) (* ReLoC -- Relational logic for fine-grained concurrency *)
(** A simple bit module *) (** A simple bit module *)
From iris.proofmode Require Import tactics. From iris.proofmode Require Import proofmode.
From reloc Require Import reloc. From reloc Require Import reloc.
Set Default Proof Using "Type". Set Default Proof Using "Type".
......
theories/examples/coinflip.v
View file @ 37a694fd
...@@ -103,13 +103,11 @@ Section proofs. ...@@ -103,13 +103,11 @@ Section proofs.
rel_store_l; repeat rel_pure_l. rel_store_l; repeat rel_pure_l.
+ rel_apply_r (refines_rand_r (extract_bool vs)). + rel_apply_r (refines_rand_r (extract_bool vs)).
rel_store_r. rel_store_r.
rel_apply_l (refines_release_l with "Hlk Hlocked [-]"). rel_apply_l (refines_release_l with "Hlk Hlocked [$]").
{ iExists vs. iFrame. iLeft. iFrame. }
iNext. rel_values. iNext. rel_values.
+ rel_apply_r (refines_rand_r (extract_bool vs)). + rel_apply_r (refines_rand_r (extract_bool vs)).
rel_store_r. rel_store_r.
rel_apply_l (refines_release_l with "Hlk Hlocked [-]"). rel_apply_l (refines_release_l with "Hlk Hlocked [$]").
{ iExists vs. iFrame. iLeft. iFrame. }
iNext. rel_values. iNext. rel_values.
Qed. Qed.
...@@ -130,13 +128,12 @@ Section proofs. ...@@ -130,13 +128,12 @@ Section proofs.
(∃ (b : bool), is_locked_r lk false (∃ (b : bool), is_locked_r lk false
∗ ce ↦ #b ∗ ce ↦ #b
∗ (cl ↦ₛ NONEV ∨ cl ↦ₛ SOMEV #b))%I ∗ (cl ↦ₛ NONEV ∨ cl ↦ₛ SOMEV #b))%I
with "[-]") as "#Hinv". with "[$]") as "#Hinv".
{ iNext. iExists false. iFrame. }
iApply refines_pair. iApply refines_pair.
- rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _". - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l. rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
rel_load_l_atomic. iInv coinN as (b) "(Hlk & Hce & H)" "Hclose". rel_load_l_atomic. iInv coinN as (b) "(Hlk & Hce & H)" "Hclose".
iModIntro. iExists _. iFrame. iNext. iIntros "Hce". repeat rel_pure_r. iModIntro. iFrame. iNext. iIntros "Hce". repeat rel_pure_r.
rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk". rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
repeat rel_pure_r. repeat rel_pure_r.
iDestruct "H" as "[Hcl|Hcl]"; rel_load_r; repeat rel_pure_r. iDestruct "H" as "[Hcl|Hcl]"; rel_load_r; repeat rel_pure_r.
...@@ -144,28 +141,24 @@ Section proofs. ...@@ -144,28 +141,24 @@ Section proofs.
rel_store_r. repeat rel_pure_r. rel_store_r. repeat rel_pure_r.
rel_resolveproph_r. repeat rel_pure_r. rel_resolveproph_r. repeat rel_pure_r.
rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk". rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_". repeat rel_pure_r. iMod ("Hclose" with "[$]") as "_".
{ eauto with iFrame. }
rel_values. rel_values.
+ rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk". + rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_". repeat rel_pure_r. iMod ("Hclose" with "[$]") as "_".
{ eauto with iFrame. }
rel_values. rel_values.
- rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _". - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l. rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
rel_apply_l refines_rand_l. iNext. iIntros (b). rel_apply_l refines_rand_l. iNext. iIntros (b).
rel_store_l_atomic. iInv coinN as (b') "(Hlk & Hce & H)" "Hclose". rel_store_l_atomic. iInv coinN as (b') "(Hlk & Hce & H)" "Hclose".
iModIntro. iExists _. iFrame. iNext. iIntros "Hce". repeat rel_pure_r. iModIntro. iFrame. iNext. iIntros "Hce". repeat rel_pure_r.
rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk". rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
repeat rel_pure_r. repeat rel_pure_r.
iDestruct "H" as "[Hcl|Hcl]"; rel_store_r; repeat rel_pure_r. iDestruct "H" as "[Hcl|Hcl]"; rel_store_r; repeat rel_pure_r.
+ rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk". + rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_". repeat rel_pure_r. iMod ("Hclose" with "[$]") as "_".
{ eauto with iFrame. }
rel_values. rel_values.
+ rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk". + rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_". repeat rel_pure_r. iMod ("Hclose" with "[$]") as "_".
{ eauto with iFrame. }
rel_values. rel_values.
Qed. Qed.
...@@ -205,11 +198,11 @@ Section proofs. ...@@ -205,11 +198,11 @@ Section proofs.
rel_apply_r (refines_rand_r b). repeat rel_pure_r. rel_apply_r (refines_rand_r b). repeat rel_pure_r.
rel_cmpxchg_suc_r. repeat rel_pure_r. rel_cmpxchg_suc_r. repeat rel_pure_r.
rel_apply_l (refines_release_l with "Hlk Hlocked [-]"). rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
{ iExists vs'. iFrame. iRight. iExists b. iFrame. } { iExists vs'. iFrame. iRight. iFrame. }
iNext. repeat rel_pure_l; rel_values. iNext. repeat rel_pure_l; rel_values.
+ repeat rel_pure_r. + repeat rel_pure_r.
rel_apply_l (refines_release_l with "Hlk Hlocked [-]"). rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
{ iExists vs. iFrame. iRight. iExists x. iFrame. } { iExists vs. iFrame. iRight. iFrame. }
iNext. repeat rel_pure_l; rel_values. iNext. repeat rel_pure_l; rel_values.
- rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _". - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l. rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
...@@ -244,7 +237,7 @@ Section proofs. ...@@ -244,7 +237,7 @@ Section proofs.
∗ (c' ↦ₛ NONEV ∗ c ↦ NONEV ∗ (c' ↦ₛ NONEV ∗ c ↦ NONEV
∨ ∃ (b : bool), c' ↦ₛ SOMEV #b ∗ c ↦ SOMEV #b))%I ∨ ∃ (b : bool), c' ↦ₛ SOMEV #b ∗ c ↦ SOMEV #b))%I
with "[-]") as "#Hinv". with "[-]") as "#Hinv".
{ iNext. iFrame. iRight. iExists false. iFrame. } { iNext. iFrame. iRight. iFrame. }
do 2 rel_pure_r. do 2 rel_pure_r.
iApply refines_pair. iApply refines_pair.
...@@ -275,7 +268,7 @@ Section proofs. ...@@ -275,7 +268,7 @@ Section proofs.
{ eauto with iFrame. } { eauto with iFrame. }
rel_values. rel_values.
* iDestruct "H" as (x) "[Hc' Hc]". * iDestruct "H" as (x) "[Hc' Hc]".
iModIntro; iExists _. iFrame. iSplit; last first. iModIntro; iFrame. iSplit; last first.
{ iIntros (?); simplify_eq/=. } { iIntros (?); simplify_eq/=. }
iIntros (_). iNext. iIntros "Hc". iIntros (_). iNext. iIntros "Hc".
rel_pures_l. rel_pures_l.
...@@ -283,7 +276,7 @@ Section proofs. ...@@ -283,7 +276,7 @@ Section proofs.
{ eauto with iFrame. } { eauto with iFrame. }
iApply "IH". iApply "IH".
+ iClear "IH". + iClear "IH".
iDestruct "H" as (b) "[Hc' Hc]". iExists _. iFrame. iNext. iIntros "Hc". iDestruct "H" as (b) "[Hc' Hc]". iFrame. iNext. iIntros "Hc".
repeat rel_pure_l. repeat rel_pure_l.
rel_apply_r (refines_acquire_r with "Hlk"). rel_apply_r (refines_acquire_r with "Hlk").
iIntros "Hlk". repeat rel_pure_r. rel_load_r. iIntros "Hlk". repeat rel_pure_r. rel_load_r.
...@@ -297,7 +290,7 @@ Section proofs. ...@@ -297,7 +290,7 @@ Section proofs.
repeat rel_rec_l. repeat rel_rec_r. repeat rel_pure_l. repeat rel_pure_r. repeat rel_rec_l. repeat rel_rec_r. repeat rel_pure_l. repeat rel_pure_r.
rel_store_l_atomic. iInv coinN as "(Hlk & [[Hc' Hc]|H])" "Hclose"; rel_store_l_atomic. iInv coinN as "(Hlk & [[Hc' Hc]|H])" "Hclose";
iModIntro. iModIntro.
+ iExists _. iFrame. iNext. iIntros "Hc". + iFrame. iNext. iIntros "Hc".
rel_apply_r (refines_acquire_r with "Hlk"). rel_apply_r (refines_acquire_r with "Hlk").
iIntros "Hlk". repeat rel_pure_r. rel_store_r. iIntros "Hlk". repeat rel_pure_r. rel_store_r.
repeat rel_pure_r. rel_apply_r (refines_release_r with "Hlk"). repeat rel_pure_r. rel_apply_r (refines_release_r with "Hlk").
...@@ -306,7 +299,7 @@ Section proofs. ...@@ -306,7 +299,7 @@ Section proofs.
{ eauto with iFrame. } { eauto with iFrame. }
rel_values. rel_values.
+ iDestruct "H" as (x) "[Hc' Hc]". + iDestruct "H" as (x) "[Hc' Hc]".
iExists _. iFrame. iNext. iIntros "Hc". iFrame. iNext. iIntros "Hc".
rel_apply_r (refines_acquire_r with "Hlk"). rel_apply_r (refines_acquire_r with "Hlk").
iIntros "Hlk". repeat rel_pure_r. rel_store_r. iIntros "Hlk". repeat rel_pure_r. rel_store_r.
repeat rel_pure_r. rel_apply_r (refines_release_r with "Hlk"). repeat rel_pure_r. rel_apply_r (refines_release_r with "Hlk").
......
theories/examples/folly_queue/CG_queue.v 0 → 100644
View file @ 37a694fd
From reloc Require Import reloc lib.lock lib.list.
(* The course-grained queue is implemented as a linked list guarded by a
lock. *)
Definition CG_dequeue_go : val := λ: "head",
match: !"head" with
NONE => #() #() (* Stuck. *)
| SOME "p" => "head" <- (Snd "p");; Fst "p"
end.
Definition CG_dequeue : val := λ: "lock" "head" <>,
acquire "lock" ;;
let: "v" := CG_dequeue_go "head" in
release "lock" ;;
"v".
Definition CG_enqueue_go : val := rec: "enqueue" "x" "head" :=
match: "head" with
NONE => CONS "x" NIL
| SOME "p" => CONS (Fst "p") ("enqueue" "x" (Snd "p"))
end.
Definition CG_enqueue : val := λ: "lock" "head" "x",
acquire "lock" ;;
"head" <- CG_enqueue_go "x" (! "head") ;;
release "lock".
Definition CG_queue : val := Λ:
let: "head" := ref NIL in
let: "lock" := newlock #() in
((λ: "x", CG_enqueue "lock" "head" "x"),
(λ: "x", CG_dequeue "lock" "head" "x")).
Section CG_queue.
Context `{relocG Σ}.
(* Representation predicate for the course grained queue. *)
Fixpoint isCGQueue_go (xs : list val) : val :=
match xs with
| nil => NILV
| x :: xs' => (CONSV x (isCGQueue_go xs'))
end.
Definition cgQueueInv (ℓ : loc) lk (xs : list val) : iProp Σ :=
ℓ ↦ₛ (isCGQueue_go xs) ∗ is_locked_r lk false.
Lemma refines_CG_enqueue_body_r E t (K : Datatypes.list (ectxi_language.ectx_item heap_ectxi_lang)) A x xs :
nclose relocN ⊆ E →
(REL t << fill K (isCGQueue_go (xs ++ [x])) @ E : A) -∗
(REL t << fill K (CG_enqueue_go x (isCGQueue_go xs)) @ E : A).
Proof.
iIntros (HNE) "H".
iInduction xs as [|x' xs'] "IH" forall (K). simpl.
- rel_rec_r. rel_pures_r. rel_pures_r.
iApply "H".
- simpl.
rel_rec_r. rel_pures_r. rel_pures_r. rel_apply_r ("IH").
rel_pures_r. done.
Qed.
Lemma refines_CG_enqueue_r list lk E t A x xs :
nclose relocN ⊆ E →
cgQueueInv list lk xs -∗
(cgQueueInv list lk (xs ++ [x]) -∗ REL t << #() @ E : A) -∗
REL t << (CG_enqueue lk #list x) @ E : A.
Proof.
iIntros (HNE) "[pts lofal] H".
rewrite /CG_enqueue.
rel_pures_r.
rel_apply_r (refines_acquire_r with "lofal"). iIntros "lotru".
rel_pures_r.
rel_load_r.
rel_apply_r (refines_CG_enqueue_body_r).
rel_pures_r.
rel_store_r.
rel_pures_r.
rel_apply_r (refines_release_r with "lotru"). iIntros "lofal".
iApply "H".
iFrame.
Qed.
Lemma refines_right_CG_dequeue E k lk list x xs :
nclose relocN ⊆ E →
cgQueueInv list lk (x :: xs) -∗
refines_right k (CG_dequeue lk #list #()) ={E}=∗
cgQueueInv list lk (xs) ∗ refines_right k (of_val x).
Proof.
iIntros (HNE) "[pts lofal] H". simpl.
rewrite /CG_dequeue /CG_dequeue_go /is_locked_r.
iDestruct "lofal" as (ℓk ->) "Hlk".
tp_pures k.
tp_rec k.
tp_cmpxchg_suc k.
tp_pures k.
tp_load k.
tp_pures k.
tp_store k.
tp_pures k.
tp_rec k.
tp_store k.
tp_pures k.
iModIntro. iFrame "H". rewrite /cgQueueInv. iFrame "pts".
iExists _. by iFrame.
Qed.
Lemma refines_CG_dequeue_cons_r E t A lk list x xs :
nclose relocN ⊆ E →
cgQueueInv list lk (x :: xs) -∗
(cgQueueInv list lk xs -∗ REL t << x @ E : A) -∗
REL t << (CG_dequeue lk #list #()) @ E : A.
Proof.
iIntros (HNE) "H1 H2".
iApply refines_split. iIntros (k) "Hk".
iMod (refines_right_CG_dequeue with "H1 Hk") as "[H1 Hk]"; first done.
iSpecialize ("H2" with "H1").
iApply (refines_combine with "H2 Hk").
Qed.
End CG_queue.
theories/examples/folly_queue/README.md 0 → 100644
View file @ 37a694fd
# MPMC queue from the Folly library
In this case study we prove linearizability of the MPMC queue algorithm from the Folly library:
- https://github.com/facebook/folly/blob/master/folly/MPMCQueue.h
theories/examples/folly_queue/mpmcqueue.v 0 → 100644
View file @ 37a694fd
From iris.heap_lang.lib Require Export array.
From reloc Require Export reloc.
From reloc.examples.folly_queue Require Export singleElementQueue.
Definition enqueue : val := λ: "slots" "cap" "ticket_" "v",
let: "ticket" := FAA "ticket_" #1 in
let: "turn" := "ticket" `quot` "cap" in
let: "idx" := "ticket" `rem` "cap" in
enqueueWithTicket (!("slots" +ₗ "idx")) "turn" "v".
Definition dequeue : val := λ: "slots" "cap" "ticket_",
let: "ticket" := FAA "ticket_" #1 in
let: "turn" := "ticket" `quot` "cap" in
let: "idx" := "ticket" `rem` "cap" in
dequeueWithTicket (!("slots" +ₗ "idx")) "turn".
Definition newSQueue : val := λ: <>,
let: "r" := ref NONE in
let: "t" := newTS #() in
("t", "r").
Definition newQueue : val := λ: "q", Λ:
let: "slots" := array_init "q" newSQueue in
let: "pushTicket" := ref #0 in
let: "popTicket" := ref #0 in
(λ: "v", enqueue "slots" "q" "pushTicket" "v",
λ: <>, dequeue "slots" "q" "popTicket").
theories/examples/folly_queue/refinement.v 0 → 100644
View file @ 37a694fd
This diff is collapsed.
theories/examples/folly_queue/set.v 0 → 100644
View file @ 37a694fd
From stdpp Require Import base decidable.
From iris.algebra Require Import numbers cmra excl stepindex_finite.
From reloc.prelude Require Import arith.
(* A camera of, potentially, infinite sets. Most of the lemmas are about sets of
natural numbers. *)
Definition setUR (A : Type) := discrete_funUR (λ (a : A), optionUR (exclR unitO)).
(* Sets of natural numbers. *)
(* Create a set from a characteristic function. *)
Definition set_cf {A : Type} (f : A → bool) : setUR A :=
λ a, if f a then Some (Excl ()) else None.
Definition set_of (A : Type) := @set_cf A (const true).
Definition set_singleton `{!EqDecision A} (a : A) :=
set_cf (λ a', if decide (a = a') then true else false).
Definition set_nat := set_of nat.
Definition set_even := set_cf Nat.even.
Definition set_odd := set_cf Nat.odd.
Lemma split_even_odd : set_nat ≡ set_even ⋅ set_odd.
Proof.
intros n. rewrite /set_even /set_odd /set_cf. simpl.
rewrite discrete_fun_lookup_op.
destruct (even_odd_spec n) as [[-> ->]|[-> ->]]; done.
Qed.
(* Set of nats including and above n. *)
Definition set_above n := set_cf (λ n', n <=? n').
Definition set_upto n := set_cf (λ n', n' <? n).
Lemma set_above_lookup n m : n ≤ m → set_above n m = Excl' ().
Proof. rewrite /set_above /set_cf. by intros ->%Nat.leb_le. Qed.
Lemma set_above_lookup_none n m : m < n → (set_above n) m = None.
Proof. rewrite /set_above /set_cf. by intros ->%Nat.leb_gt. Qed.
Lemma set_upto_lookup n m : m < n → (set_upto n) m = Excl' ().
Proof. rewrite /set_upto /set_cf. by intros ->%Nat.ltb_lt. Qed.
Lemma set_upto_lookup_none n m : n ≤ m → (set_upto n) m = None.
Proof. rewrite /set_upto /set_cf. by intros ->%Nat.ltb_ge. Qed.
Lemma set_above_zero : set_above 0 ≡ set_nat.
Proof. intros n. rewrite set_above_lookup; [done | lia]. Qed.
Lemma set_upto_zero : set_upto 0 ≡ ε.
Proof.
intros n. rewrite /set_upto /set_cf.
assert (n <? 0 = false) as ->; last done.
apply leb_correct_conv. lia.
Qed.
Lemma discrete_fun_valid' (s : setUR nat) (n : nat) : ✓ s → ✓ (s n).
Proof. done. Qed.
Lemma set_singleton_lookup (n : nat) : set_singleton n n = Excl' ().
Proof. rewrite /set_singleton /set_cf. rewrite decide_True; done. Qed.
Lemma set_singleton_lookup_none (n m : nat) : n ≠ m → set_singleton n m = None.
Proof.
intros H. rewrite /set_singleton /set_cf. rewrite decide_False; done.
Qed.
Lemma set_singleton_invalid (n : nat) : ¬ ✓ (set_singleton n ⋅ set_singleton n).
Proof.
rewrite /set_singleton /set_cf.
intros Hv.
pose proof (Hv n) as Hv.
rewrite discrete_fun_lookup_op in Hv.
rewrite decide_True in Hv; done.
Qed.
Lemma set_singletons_valid (n m : nat) : ✓ (set_singleton n ⋅ set_singleton m) → n ≠ m.
Proof.
intros Hv ->.
by apply set_singleton_invalid in Hv.
Qed.
(* Rewrite n <? m when true *)
Global Hint Rewrite ltb_lt_1 using lia : natb.
Global Hint Rewrite leb_correct_conv using lia : natb.
Global Hint Rewrite leb_correct using lia : natb.
Global Hint Rewrite set_above_lookup using lia : natb.
Global Hint Rewrite @decide_False using lia : natb.
Global Hint Rewrite @decide_True using lia : natb.
Global Hint Rewrite set_above_lookup_none using lia : natb.
Global Hint Rewrite set_upto_lookup_none using lia : natb.
Global Hint Rewrite set_upto_lookup using lia : natb.
Global Hint Rewrite set_singleton_lookup_none using lia : natb.
Global Hint Rewrite set_singleton_lookup using lia : natb.
Global Hint Rewrite div_mod' : natb.
Global Hint Rewrite mod0 : natb.
Global Hint Rewrite div0 : natb.
Global Hint Rewrite Nat.add_0_r : natb.
Global Hint Rewrite Nat.add_0_l : natb.
Global Hint Rewrite Nat.ltb_irrefl : natb.
Global Hint Rewrite Nat.max_0_r : natb.
Global Hint Rewrite Nat.max_0_l : natb.
Lemma set_upto_singleton_valid n m : ✓ (set_upto n ⋅ set_singleton m) → n ≤ m.
Proof.
destruct (le_gt_dec n m); first done.
intros Hv.
pose proof (Hv m).
rewrite discrete_fun_lookup_op in H.
rewrite /set_singleton /set_cf in H.
autorewrite with natb in H.
done.
Qed.
Lemma take_first n : set_above n ≡ set_singleton n ⋅ set_above (n + 1).
Proof.
intros n'.
rewrite /set_singleton. rewrite /set_cf.
rewrite discrete_fun_lookup_op.
destruct (le_lt_dec n n').
- case_decide; subst; by autorewrite with natb.
- autorewrite with natb. done.
Qed.
Lemma set_upto_singleton n : set_singleton n ⋅ set_upto n ≡ set_upto (n + 1).
Proof.
intros m.
rewrite discrete_fun_lookup_op.
destruct (le_gt_dec m n).
- rewrite (set_upto_lookup (n + 1)); last lia.
assert (m < n ∨ m = n) as [] by lia.
* autorewrite with natb. done.
* subst. autorewrite with natb. done.
- autorewrite with natb. done.
Qed.
(* Create a set from a decidable predicate. *)
Definition set_prop {A : Type} (f : A → Prop) `{!∀ a, Decision (f a)} : setUR A :=
λ a, if decide (f a) then Some (Excl ()) else None.
(* All even numbers except for the first n. *)
Definition set_even_drop n := set_cf (λ n', (Nat.even n') && (2 * n <=? n')).
(* All odd numbers except for the first n. *)
Definition set_odd_drop n := set_cf (λ n', (Nat.odd n') && (2 * n + 1 <=? n')).
Lemma set_even_drop_lookup n m : Nat.Even m → 2 * n ≤ m → set_even_drop n m = Excl' ().
Proof.
intros He Hle.
rewrite /set_even_drop /set_cf.
assert (Nat.even m = true) as -> by by apply Nat.even_spec.
rewrite leb_correct; last done.
done.
Qed.
Lemma set_even_drop_zero : set_even_drop 0 ≡ set_even.
Proof.
intros n.
rewrite /set_even_drop /set_even /set_cf.
destruct (Nat.even n); done.
Qed.
Lemma set_odd_drop_zero : set_odd_drop 0 ≡ set_odd.
Proof.
intros n.
rewrite /set_odd_drop /set_odd /set_cf.
destruct n; first done.
destruct (Nat.odd (S n)); done.
Qed.
Lemma set_even_drop_singleton n : set_even_drop n ≡ set_even_drop (n + 1) ⋅ set_singleton (2 * n).
Proof.
intros m.
rewrite /set_even_drop /set_singleton /set_cf /=.
autorewrite with natb.
rewrite discrete_fun_lookup_op.
destruct (Nat.Even_or_Odd m) as [[a b]|[a b]].
- replace (Nat.even m) with true.
+ destruct (gt_eq_gt_dec m (n + n)) as [[He|He]|He]; autorewrite with natb; eauto.
+ symmetry. apply Nat.even_spec. by econstructor.
- replace (Nat.even m) with false.
+ by autorewrite with natb.
+ rewrite -Nat.negb_odd.
cut (Nat.odd m = true); first by intros ->.
eapply Nat.odd_spec. by econstructor.
Qed.
Lemma set_odd_drop_singleton n : set_odd_drop n ≡ set_odd_drop (n + 1) ⋅ set_singleton (2 * n + 1).
Proof.
intros m.
rewrite /set_odd_drop /set_singleton /set_cf /=.
autorewrite with natb.
rewrite discrete_fun_lookup_op.
destruct (Nat.Even_or_Odd m) as [[a b]|[a b]].
- replace (Nat.odd m) with false.
+ destruct (gt_eq_gt_dec m (n + n)) as [[He|He]|He]; autorewrite with natb; eauto.
+ rewrite -Nat.negb_even.
cut (Nat.even m = true); first by intros ->.
eapply Nat.even_spec. by econstructor.
- replace (Nat.odd m) with true.
+ destruct (gt_eq_gt_dec m (n + n)) as [[He|He]|He];
autorewrite with natb; try lia; eauto.
destruct (gt_eq_gt_dec m ((n+1) + (n+1))) as [[He1|He1]|He1];
autorewrite with natb; try lia; eauto.
+ symmetry. apply Nat.odd_spec. by econstructor.
Qed.
theories/examples/folly_queue/singleElementQueue.v 0 → 100644
View file @ 37a694fd
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl auth gset.
From reloc Require Import reloc.
From reloc.prelude Require Export arith.
From reloc.examples.folly_queue Require Export set turnSequencer.
Definition enqueueWithTicket : val := λ: "this" "ticket" "v",
let: "t" := Fst "this" in
let: "r" := Snd "this" in
let: "turn" := "ticket" * #2 in
waitForTurn "t" "turn";;
"r" <- SOME "v";;
completeTurn "t" "turn".
Definition getSome : val := λ: "r",
match: !"r" with
NONE => errorE (* Error *)
| SOME "x" => "r" <- NONE;; "x"
end.
Definition dequeueWithTicket : val := λ: "this" "ticket",
let: "t" := Fst "this" in
let: "r" := Snd "this" in
let: "turn" := ("ticket" * #2) + #1 in
waitForTurn "t" "turn";;
let: "v" := getSome "r" in
completeTurn "t" "turn";;
"v".
(* The single-element queue used by the MPMC queue. *)
Definition newSEQ : val := λ: <>,
let: "r" := ref NONE in
let: "t" := newTS #() in
("t", "r").
(* Code for a single element queue that manages tickets itself. *)
Definition enqueue : val := rec: "enqueue" "t" "r" "ticket_" "v" :=
let: "ticket" := FAA "ticket_" #1 in
enqueueWithTicket ("t", "r") "ticket" "v".
Definition dequeue : val := rec: "dequeue" "t" "r" "ticket_" <> :=
let: "ticket" := FAA "ticket_" #1 in
dequeueWithTicket ("t","r") "ticket".
Definition newQueue : val := λ: <>,
let: "popTicket" := ref #0 in
let: "pushTicket" := ref #0 in
let: "r" := ref NONE in
let: "t" := newTS #() in
(λ: "v", enqueue "t" "r" "pushTicket" "v", λ: <>, dequeue "t" "r" "popTicket" #()).
(* Alternative spec for the TS. *)
Section spec.
Context `{!relocG Σ, !TSG Σ}.
Definition Nseq : namespace := nroot .@ "SEQ".
(* R is the resource that the single element queue protects. The i'th dequeue
is sure to get a value, v, that satisfies R i v. *)
Implicit Type R : nat → val → iProp Σ.
(* The resource for the turn sequencer. *)
Definition TSR R (ℓ : loc) (n : nat) : iProp Σ :=
(if Nat.even n
then ℓ ↦ NONEV
else ∃ v, ℓ ↦ SOMEV v ∗ R ((n - 1) / 2) v)%I.
Definition isSEQ (γ : gname) R (v : val) : iProp Σ :=
∃ ts (ℓ : loc), ⌜v = (ts, #ℓ)%V⌝ ∗ isTS γ (TSR R ℓ) ts.
Definition enqueue_turns γ n := own γ (set_even_drop n).
Definition dequeue_turns γ n := own γ (set_odd_drop n).
Definition enqueue_turn γ n := own γ (set_singleton (2 * n)).
Definition dequeue_turn γ n := own γ (set_singleton (2 * n + 1)).
Lemma enqueue_turns_take γ n :
enqueue_turns γ n ⊣⊢ enqueue_turns γ (n + 1) ∗ enqueue_turn γ n.
Proof. by rewrite -own_op -set_even_drop_singleton. Qed.
Lemma dequeue_turns_take γ n :
dequeue_turns γ n ⊣⊢ dequeue_turns γ (n + 1) ∗ dequeue_turn γ n.
Proof. by rewrite -own_op -set_odd_drop_singleton. Qed.
Lemma newSEQ_spec (v : val) R :
{{{ True }}} newSEQ v {{{ γ v, RET v; isSEQ γ R v ∗ enqueue_turns γ 0 ∗ dequeue_turns γ 0 }}}.
Proof.
iIntros (Φ) "_ HΦ".
wp_rec.
wp_alloc ℓ as "pts". wp_pures.
wp_apply (ts_mk_spec (TSR R ℓ) with "pts").
iIntros (γ ts) "[Hts turns]".
wp_pures.
iApply ("HΦ" $! γ).
iSplitL "Hts". { iExists _, _. iFrame. done. }
rewrite /turns_from /enqueue_turns /dequeue_turns.
rewrite set_above_zero.
rewrite split_even_odd.
rewrite set_even_drop_zero.
rewrite set_odd_drop_zero.
rewrite own_op.
by iFrame.
Qed.
(* For the [lia] tactic. *)
(* To support Z.div, Z.modulo, Z.quot, and Z.rem: *)
Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
Lemma enqueueWithTicket_spec' γ R v x n :
{{{ isSEQ γ R v ∗ enqueue_turn γ n ∗ R n x }}}
enqueueWithTicket v #n x
{{{ RET #(); True }}}.
Proof.
iIntros (Φ) "(isSEQ & Hturn & HR) HΦ".
iDestruct "isSEQ" as (ts ℓ) "[-> #Hts]".
wp_rec.
wp_pures.
assert ((n * 2)%Z = (2 * n)%nat) as ->. { lia. }
wp_apply (wait_spec with "[$Hts Hturn]"); first done.
iIntros "[Htsr Hclose]".
iEval (rewrite /TSR) in "Htsr".
wp_pures.
assert (Nat.even (2 * n) = true) as ->.
{ apply Nat.even_spec, Even_mul2. }
wp_store.
wp_apply (complete_spec with "[Hclose HR Htsr]").
{ simpl. iFrame "#∗".
rewrite /TSR.
assert (Nat.even (n + (n + 0) + 1) = false) as ->.
{ replace (n + (n + 0) + 1) with (S (2 * n)) by lia.
rewrite Nat.even_succ. rewrite -Nat.negb_even.
assert (Nat.even (2 * n) = true) as ->; last done.
apply Nat.even_spec. apply Even_mul2. }
iExists _. iFrame.
replace (n + (n + 0) + 1 - 1) with (n * 2) by lia.
rewrite Nat.div_mul; last done.
done. }
iAssumption.
Qed.
Lemma dequeueWithTicket_spec' γ R v n :
{{{ isSEQ γ R v ∗ dequeue_turn γ n }}}
dequeueWithTicket v #n
{{{ v, RET v; R n v }}}.
Proof.
iIntros (Φ) "(isSEQ & Hturn) HΦ".
iDestruct "isSEQ" as (ts ℓ) "[-> #Hts]".
wp_rec. wp_pures.
assert ((n * 2 + 1)%Z = (2 * n + 1)%nat) as -> by lia.
wp_apply (wait_spec with "[$Hts Hturn]"); first done.
iIntros "[Htsr Hclose]".
rewrite /getSome. wp_pures.
iEval (rewrite /TSR) in "Htsr".
rewrite Nat.add_0_r.
assert (Nat.even (2 * n + 1) = false) as ->.
{ replace (2 * n + 1) with (S (2 * n)) by lia.
rewrite Nat.even_succ. rewrite -Nat.negb_even.
assert (Nat.even (2 * n) = true) as ->; last done.
apply Nat.even_spec. apply Even_mul2. }
iDestruct "Htsr" as (v) "[pts HR]".
wp_load.
wp_store. wp_pures.
wp_apply (complete_spec with "[Hclose pts]").
{ iFrame "#∗".
replace (n + n + 1 + 1) with (2 * (n + 1)) by lia.
replace (n + n + 1) with (2 * n + 1) by lia.
rewrite /TSR.
assert (Nat.even _ = true) as ->.
{ apply Nat.even_spec. apply Even_mul2. }
by iFrame. }
iIntros "_".
wp_pures.
iApply "HΦ".
replace (2 * n + 1 - 1) with (n * 2) by lia.
rewrite Nat.div_mul; last done.
by iFrame.
Qed.
Lemma dequeueWithTicket_spec2 (γ : gname) R (v : val) (n : nat) (Φ : val → iPropI Σ) :
isSEQ γ R v ∗ dequeue_turn γ n
-∗ ▷ (∀ v0 : val, R n v0 ={⊤}=∗ ▷ Φ v0 )
-∗ WP dequeueWithTicket v #n {{ v, Φ v }}.
Proof.
iIntros "(isSEQ & Hturn) HΦ".
iDestruct "isSEQ" as (ts ℓ) "[-> #Hts]".
wp_rec. wp_pures.
assert ((n * 2 + 1)%Z = (2 * n + 1)%nat) as -> by lia.
wp_apply (wait_spec with "[$Hts Hturn]"); first done.
iIntros "[Htsr Hclose]".
rewrite /getSome. wp_pures.
iEval (rewrite /TSR) in "Htsr".
rewrite Nat.add_0_r.
assert (Nat.even (2 * n + 1) = false) as ->.
{ replace (2 * n + 1) with (S (2 * n)) by lia.
rewrite Nat.even_succ. rewrite -Nat.negb_even.
assert (Nat.even (2 * n) = true) as ->; last done.
apply Nat.even_spec. apply Even_mul2. }
iDestruct "Htsr" as (v) "[pts HR]".
wp_load.
wp_store. wp_pures.
wp_apply (complete_spec with "[Hclose pts]").
{ iFrame "#∗".
replace (n + n + 1 + 1) with (2 * (n + 1)) by lia.
replace (n + n + 1) with (2 * n + 1) by lia.
rewrite /TSR.
assert (Nat.even _ = true) as ->.
{ apply Nat.even_spec. apply Even_mul2. }
by iFrame. }
iIntros "_".
replace (2 * n + 1 - 1) with (n * 2) by lia.
rewrite Nat.div_mul; last done.
iMod ("HΦ" $! v with "HR") as "HI".
wp_pures.
by iFrame.
Qed.
End spec.
theories/examples/folly_queue/ticketLock.v 0 → 100644
View file @ 37a694fd
(* A ticket lock using a turn sequencer *)
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth excl cmra agree frac gset.
From reloc Require Import reloc.
From reloc.examples.folly_queue Require Import set turnSequencer.
Definition newlock : val := λ: <>,
let: "turn" := ref #0 in
let: "t" := newTS #() in
("t", "turn").
Definition acquire : val := rec: "acquire" "l" :=
let: "t" := Fst "l" in
let: "turn" := Snd "l" in
let: "ct" := !"turn" in
if: CAS "turn" "ct" ("ct" + #1)
then waitForTurn "t" "ct";; "ct"
else "acquire" "l".
Definition release : val := λ: "l" "ct",
let: "t" := Fst "l" in
completeTurn "t" "ct".
Section contents.
Context `{!relocG Σ, !TSG Σ}.
Context (N' : namespace).
Context (R : iProp Σ).
Definition N := N'.@"N".
Definition LN := N'.@"ticketLock".
Definition lock_inv_body (γTS : gname) turn : iProp Σ :=
(∃ (n : nat), turn ↦ #n ∗ turns_from γTS n)%I.
Definition lock_inv (γTS : gname) (ts : val) (turn : loc) : iProp Σ :=
(isTS γTS (fun _ => R) ts ∗
inv LN (lock_inv_body γTS turn))%I.
Definition locked ts n := complete ts n.
Lemma newlock_spec :
{{{ R }}}
newlock #()
{{{ ts turn γTS, RET (ts, #turn); lock_inv γTS ts turn }}}.
Proof.
iIntros (Φ) "HR HΦ".
unlock newlock. wp_rec.
wp_alloc turn as "Hturn". wp_let.
(* iMod (own_alloc ((● Excl' 0) ⋅ (◯ Excl' 0))) as (γ) "[Hγ HP]". *)
(* { by apply auth_both_valid_discrete. } *)
wp_bind (newTS #()).
iApply (ts_mk_spec (fun _ => R)%I with "HR").
iNext. iIntros (γTS ts) "[#Hts Hturns]".
iMod (inv_alloc LN _ (lock_inv_body γTS turn) with "[Hturn Hturns]") as "#Hinv".
{ iNext. iExists 0. by iFrame. }
wp_pures.
iApply "HΦ". rewrite /lock_inv. by iFrame "Hts Hinv".
Qed.
Lemma turns_take γ m : turns_from γ m ⊢ turns_from γ (m + 1) ∗ turn γ m.
Proof. by rewrite /turns_from /turn -own_op comm -take_first. Qed.
Lemma acquire_spec γTS ts (turn : loc) :
{{{ lock_inv γTS ts turn }}}
acquire (ts, #turn)
{{{ n, RET #n; locked ts n ∗ R }}}.
Proof.
iIntros (Φ) "#[Hts Hlinv] HΦ".
wp_pures. iLöb as "IH". wp_rec. wp_pures.
wp_bind (! #turn)%E.
iInv LN as (n) "(Hturn & Htickets)" "Hcl".
wp_load.
iMod ("Hcl" with "[Hturn Htickets]") as "_".
{ iNext. iExists _; iFrame. }
iModIntro. wp_pures.
wp_bind (CmpXchg _ _ _).
iInv LN as (n') "(Hturn & Htickets)" "Hcl".
destruct (decide (n = n')); subst.
- wp_cmpxchg_suc.
rewrite turns_take. iDestruct "Htickets" as "[Htickets Hticket]".
iMod ("Hcl" with "[Hturn Htickets]") as "_".
{ iNext. iExists _.
rewrite -(Nat2Z.inj_add n' 1).
assert (n' + 1 = S n') as -> by lia.
by iFrame. }
iModIntro. wp_pures.
wp_apply (wait_spec with "[$Hts $Hticket]").
iIntros "[HR Hcompl]". wp_pures. iApply "HΦ".
by iFrame.
- wp_cmpxchg_fail. naive_solver.
iMod ("Hcl" with "[-HΦ]") as "_".
{ iNext. iExists _. by iFrame. }
iModIntro. wp_pures.
by iApply "IH".
Qed.
Lemma release_spec γTS ts (turn : loc) n :
{{{ lock_inv γTS ts turn ∗ locked ts n ∗ R }}}
release (ts, #turn) #n
{{{ RET #(); True }}}.
Proof.
iIntros (Φ) "[#[Hts Hlinv] [Hlk HR]] HΦ".
wp_pures. wp_rec. wp_pures.
by iApply (complete_spec with "[$Hts $Hlk $HR]").
Qed.
End contents.
theories/examples/folly_queue/turnSequencer.v 0 → 100644
View file @ 37a694fd
From iris.algebra Require Import auth excl cmra agree frac gset.
From reloc Require Import reloc.
From reloc.lib Require Import lock.
From reloc.examples.folly_queue Require Import set.
(** * Implementation *)
Notation errorE := (#0 #1). (* This gets stuck *)
(* Turn Sequencer with simple spinning. Ignoring arithmetic, shifter turns and use of futex. *)
Definition newTS : val := λ: <>, ref #0.
Definition completeTurn : val :=
rec: "complete" "state_" "turn" :=
let: "state" := !"state_" in
if: ("state" ≠ "turn")
then errorE
else "state_" <- ("turn" + #1).
Definition waitForTurn : val :=
rec: "wait" "state_" "turn" :=
let: "state" := !"state_" in
if: ("state" = "turn") then #()
else if: ("turn" < "state") then errorE
else "wait" "state_" "turn".
Definition turnSequencer : val :=
(newTS, completeTurn, waitForTurn).
Class TSG Σ := { TSG_tickets :: inG Σ (setUR nat) }.
(* Alternative spec for the TS. *)
Section spec.
Context `{!relocG Σ, !TSG Σ}.
Implicit Types R : nat → iProp Σ.
Definition N : namespace := nroot .@ "TS".
Definition turn γ n := own γ (set_singleton n).
Definition turns_from γ n := own γ (set_above n).
Definition turns γ n := own γ (set_upto n).
Lemma turns_add γ m : turns γ m -∗ turn γ m -∗ turns γ (m + 1).
Proof.
iIntros "T S". iCombine "S T" as "T". by rewrite set_upto_singleton.
Qed.
Definition complete v (n : nat) : iProp Σ :=
(∃ ℓ : loc, ⌜v = #ℓ⌝ ∗ ℓ ↦{#1/2} #n)%I.
Definition TS_inv γ R ℓ : iProp Σ :=
∃ (n : nat), ℓ ↦{#1/2} #n ∗ turns γ n ∗ (R n ∗ complete #ℓ n ∨ turn γ n).
Definition isTS (γ : gname) R v := (∃ ℓ : loc, ⌜v = #ℓ⌝ ∗ inv N (TS_inv γ R ℓ))%I.
Lemma ts_mk_spec R :
{{{ R 0 }}} newTS #() {{{ γ v, RET v; isTS γ R v ∗ turns_from γ 0 }}}.
Proof.
iIntros (ϕ) "Hr Hϕ".
wp_rec.
iApply wp_fupd.
wp_alloc ℓ as "[ℓPts ℓPts']".
iMod (own_alloc (set_above 0)) as (γ) "Hturns"; first done.
iMod (own_unit (setUR nat)) as "H".
iMod (inv_alloc N _ (TS_inv γ R ℓ)%I with "[-Hϕ Hturns] ") as "HI".
{ iNext. iExists 0. unfold turns.
rewrite -set_upto_zero.
iFrame "ℓPts H". iLeft. iFrame "Hr". iExists _; eauto with iFrame. }
iApply "Hϕ".
iModIntro. iFrame "Hturns". iExists _. iSplit; eauto with iFrame.
Qed.
Lemma wait_spec γ R v n :
{{{ isTS γ R v ∗ turn γ n }}} waitForTurn v #n {{{ RET #(); R n ∗ complete v n }}}.
Proof.
iLöb as "IH".
iIntros (ϕ) "[#Hts Ht] Hϕ".
iDestruct "Hts" as (ℓ ->) "#Hinv".
wp_rec.
wp_pures.
wp_bind (! _)%E.
iInv N as (m) "(>ℓPts & Hturns & Hdisj)" "Hcl".
wp_load.
destruct (lt_eq_lt_dec n m) as [[Hle|<-]|Hho].
- iCombine "Hturns Ht" gives %HI%set_upto_singleton_valid.
exfalso. lia.
- iDestruct "Hdisj" as "[[Hr ℓPts'] | Ht']"; last first.
{ by iCombine "Ht Ht'" gives %?%set_singleton_invalid. }
iMod ("Hcl" with "[Ht ℓPts Hturns]") as "_".
{ iNext. iExists _. iFrame. }
iModIntro. wp_pures.
rewrite bool_decide_true //. wp_pures.
iApply "Hϕ". by iFrame.
- iMod ("Hcl" with "[-Hϕ Ht]") as "_".
{ iNext. iExists _. iFrame. }
iModIntro. wp_pures.
case_bool_decide; simplify_eq; first lia.
wp_pures.
rewrite bool_decide_false; last lia.
wp_pures.
iApply ("IH" with "[$Ht]"); last done.
{ iExists _. eauto with iFrame. }
Qed.
Lemma complete_spec γ R v n :
{{{ isTS γ R v ∗ R (n + 1) ∗ complete v n }}} completeTurn v #n {{{ RET #(); True }}}.
Proof.
iIntros (ϕ) "(#Hts & Hr & Hc) Hϕ".
wp_rec.
wp_pures.
wp_bind (! _)%E.
iDestruct "Hts" as (ℓ ->) "#Hinv".
iDestruct "Hc" as (ℓ1 ?) "Hc".
simplify_eq/=.
iInv N as (m) "(>ℓPts & >Hturns & [(_ & >Hc')|Ht])" "Hcl".
{ rewrite /complete.
iDestruct "Hc'" as (ℓ1' ?) "Hc'".
simplify_eq/=.
iCombine "ℓPts Hc'" as "ℓPts".
iCombine "ℓPts Hc" gives %[?%Qp.not_add_le_l _].
done. }
wp_load.
iDestruct (pointsto_agree with "ℓPts Hc") as %[= Heq].
iMod ("Hcl" with "[Ht ℓPts Hturns]") as "_".
{ iNext. iExists m. iFrame. }
iModIntro. wp_pures. simplify_eq/=.
rewrite bool_decide_true //.
wp_pures.
iInv N as (m) "(>ℓPts & >Hturns & [(_ & >Hc')|>Ht])" "Hcl".
{ rewrite /complete.
iDestruct "Hc'" as (ℓ1' ?) "Hc'".
simplify_eq/=.
iCombine "ℓPts Hc'" as "ℓPts".
iCombine "ℓPts Hc" gives %[?%Qp.not_add_le_l _].
done. }
iDestruct (pointsto_combine with "ℓPts Hc") as "[ℓPts %Heq]".
simplify_eq/=.
rewrite dfrac_op_own Qp.half_half.
wp_store.
assert ((n + 1)%Z = (n + 1)%nat) as ->. { lia. }
iDestruct "ℓPts" as "[ℓPts ℓPts']".
iDestruct (turns_add with "Hturns Ht") as "Hturns".
iMod ("Hcl" with "[-Hϕ]") as "_".
{ iNext. iExists (n + 1). eauto with iFrame. }
iModIntro. by iApply "Hϕ".
Qed.
End spec.
theories/examples/namegen.v
View file @ 37a694fd
...@@ -64,7 +64,7 @@ Section namegen_refinement. ...@@ -64,7 +64,7 @@ Section namegen_refinement.
{ iIntros (Hy). destruct Hy as [y Hy]. { iIntros (Hy). destruct Hy as [y Hy].
rewrite (big_sepS_elem_of _ L (l',y) Hy). rewrite (big_sepS_elem_of _ L (l',y) Hy).
iDestruct "HL" as "[Hl _]". iDestruct "HL" as "[Hl _]".
iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %[Hfoo _]. iCombine "Hl Hl'" gives %[Hfoo _].
compute in Hfoo. eauto. } compute in Hfoo. eauto. }
iAssert (⌜(∃ x, (x, S n) ∈ L) → False⌝)%I with "[HL]" as %Hc. iAssert (⌜(∃ x, (x, S n) ∈ L) → False⌝)%I with "[HL]" as %Hc.
{ iIntros (Hx). destruct Hx as [x Hy]. { iIntros (Hx). destruct Hx as [x Hy].
......
theories/examples/or.v
View file @ 37a694fd
...@@ -30,7 +30,8 @@ Notation "e1 ⊕ e2" := (or (λ: <>, e1)%V (λ: <>, e2)%V) ...@@ -30,7 +30,8 @@ Notation "e1 ⊕ e2" := (or (λ: <>, e1)%V (λ: <>, e2)%V)
(at level 60) : val_scope. (at level 60) : val_scope.
Section rules. Section rules.
Context `{relocG Σ}. Context `{!relocG Σ}.
Implicit Types e : expr.
(** Symbolic execution rule for the LHS *) (** Symbolic execution rule for the LHS *)
Definition or_inv x : iProp Σ := Definition or_inv x : iProp Σ :=
...@@ -260,9 +261,9 @@ Section rules. ...@@ -260,9 +261,9 @@ Section rules.
end. end.
Lemma seq_or_2' (f g h f' g' h' : expr) A : Lemma seq_or_2' (f g h f' g' h' : expr) A :
is_closed_expr [] f → is_closed_expr ∅ f →
is_closed_expr [] g → is_closed_expr ∅ g →
is_closed_expr [] h → is_closed_expr ∅ h →
(REL f << f' : A) -∗ (REL f << f' : A) -∗
(REL g << g' : A) -∗ (REL g << g' : A) -∗
(REL h << h' : A) -∗ (REL h << h' : A) -∗
...@@ -274,7 +275,7 @@ Section rules. ...@@ -274,7 +275,7 @@ Section rules.
Proof. Proof.
iIntros (???) "Hf Hg Hh". rel_pures_r. iIntros (???) "Hf Hg Hh". rel_pures_r.
rel_newproph_l vs p as "Hp". repeat rel_pure_l. rel_newproph_l vs p as "Hp". repeat rel_pure_l.
(rewrite !(subst_is_closed []) //; try by set_solver); []. (rewrite !(subst_is_closed ∅) //; try by set_solver); [].
rel_apply_r or_refines_r. rel_apply_r or_refines_r.
destruct (to_choice vs) as [|] eqn:Hchoice. destruct (to_choice vs) as [|] eqn:Hchoice.
- iLeft. iApply (refines_seq with "Hf"). - iLeft. iApply (refines_seq with "Hf").
...@@ -297,9 +298,9 @@ Section rules. ...@@ -297,9 +298,9 @@ Section rules.
(** We then prove that the non-instrumented program refines the original one *) (** We then prove that the non-instrumented program refines the original one *)
Lemma seq_or_2_instrument (f g h f' g' h' : expr) A : Lemma seq_or_2_instrument (f g h f' g' h' : expr) A :
is_closed_expr [] f' → is_closed_expr ∅ f' →
is_closed_expr [] g' → is_closed_expr ∅ g' →
is_closed_expr [] h' → is_closed_expr ∅ h' →
(REL f << f' : A) -∗ (REL f << f' : A) -∗
(REL g << g' : A) -∗ (REL g << g' : A) -∗
(REL h << h' : A) -∗ (REL h << h' : A) -∗
...@@ -311,7 +312,7 @@ Section rules. ...@@ -311,7 +312,7 @@ Section rules.
Proof. Proof.
iIntros (???) "Hf Hg Hh". iIntros (???) "Hf Hg Hh".
rel_newproph_r p. repeat rel_pure_r. rel_newproph_r p. repeat rel_pure_r.
(rewrite !(subst_is_closed []) //; try by set_solver); []. (rewrite !(subst_is_closed ∅) //; try by set_solver); [].
iApply (refines_seq with "Hf"). iApply (refines_seq with "Hf").
rel_pures_l. rel_pures_r. rel_pures_l. rel_pures_r.
iApply (or_compatible with "[Hg] [Hh]"). iApply (or_compatible with "[Hg] [Hh]").
......
theories/examples/par.v
View file @ 37a694fd
...@@ -24,6 +24,7 @@ Notation "e1 ∥ e2" := (((e1;; #()) ||| (e2;; #()));; #())%E ...@@ -24,6 +24,7 @@ Notation "e1 ∥ e2" := (((e1;; #()) ||| (e2;; #()));; #())%E
Section rules. Section rules.
Context `{!relocG Σ, !spawnG Σ}. Context `{!relocG Σ, !spawnG Σ}.
Implicit Type e t : expr.
Lemma par_l_2 e1 e2 t : Lemma par_l_2 e1 e2 t :
(WP e1 {{ _, True }}) -∗ (WP e1 {{ _, True }}) -∗
...@@ -85,22 +86,35 @@ Section rules. ...@@ -85,22 +86,35 @@ Section rules.
rel_pures_l. rel_rec_l. rel_pures_l. rel_rec_l.
rel_pures_l. rel_pures_l.
pose (N:=nroot.@"par"). pose (N:=nroot.@"par").
rewrite refines_eq /refines_def. iIntros (j K) "#Hspec Hj". iApply refines_split. iIntros (k) "Hk".
iModIntro. wp_bind (spawn _). rel_bind_l (spawn _). iApply refines_wp_l.
iApply (spawn_spec N (λ _, j ⤇ fill K #())%I with "[He1 Hj]"). iApply (spawn_spec N (λ _, refines_right k #())%I with "[He1 Hk]").
- wp_pures. wp_bind e1. - wp_pures. wp_bind e1.
iMod ("He1" with "Hspec Hj") as "He1". rewrite refines_eq /refines_def /=.
iMod ("He1" with "Hk") as "He1".
iApply (wp_wand with "He1"). iApply (wp_wand with "He1").
iIntros (?) "P". wp_pures. iIntros (?) "P". wp_pures.
by iDestruct "P" as (v') "[Hj [-> ->]]". by iDestruct "P" as (v') "[? [-> ->]]".
- iNext. iIntros (l) "hndl". iSimpl. - iNext. iIntros (l) "hndl". iSimpl.
wp_pures. wp_bind e2. rel_pures_l. rel_bind_l e2.
iApply refines_wp_l.
iApply (wp_wand with "He2"). iIntros (?) "_". iApply (wp_wand with "He2"). iIntros (?) "_".
wp_pures. simpl. rel_pures_l. rel_bind_l (spawn.join _).
wp_apply (join_spec with "hndl"). iApply refines_wp_l.
iIntros (?) "Hj". wp_pures. iExists #(). eauto with iFrame. iApply (join_spec with "hndl"). iNext.
iIntros (?) "Hk". simpl. rel_pures_l. iApply (refines_combine with "[] Hk").
rel_values.
Qed. Qed.
Lemma refines_right_cons k' Ki K e :
refines_right (RefId k' (Ki::K)) e =
refines_right (RefId k' K) (fill_item Ki e).
Proof. rewrite /refines_right /= //. Qed.
Lemma refines_right_fill k K e :
refines_right k (fill K e) =
refines_right (RefId (tp_id k) (K ++ tp_ctx k)) e.
Proof. rewrite /refines_right fill_app //. Qed.
Lemma par_l_1' Q K e1 e2 t : Lemma par_l_1' Q K e1 e2 t :
(REL e1 << t : ()) -∗ (REL e1 << t : ()) -∗
(WP e2 {{ _, Q }}) -∗ (WP e2 {{ _, Q }}) -∗
...@@ -111,27 +125,27 @@ Section rules. ...@@ -111,27 +125,27 @@ Section rules.
rel_pures_l. rel_rec_l. rel_pures_l. rel_rec_l.
rel_pures_l. rel_pures_l.
pose (N:=nroot.@"par"). pose (N:=nroot.@"par").
rewrite {1 3}refines_eq /refines_def. iIntros (j K') "#Hspec Hj". iApply refines_split. iIntros (k) "Hk".
iModIntro. wp_bind (spawn _). rel_bind_l (spawn _). iApply refines_wp_l.
iApply (spawn_spec N (λ _, j ⤇ fill (K++K') #())%I with "[He1 Hj]"). rewrite refines_right_bind.
iApply (spawn_spec N (λ _, refines_right k (fill K #()))%I with "[He1 Hk]").
- wp_pures. wp_bind e1. - wp_pures. wp_bind e1.
rewrite -fill_app. rewrite refines_eq /refines_def.
iMod ("He1" with "Hspec Hj") as "He1". iMod ("He1" with "Hk") as "He1".
iApply (wp_wand with "He1"). iApply (wp_wand with "He1").
iIntros (?) "P". wp_pures. iIntros (?) "P". wp_pures.
by iDestruct "P" as (v') "[Hj [-> ->]]". iDestruct "P" as (v') "[Hj [-> ->]]".
- iNext. iIntros (l) "hndl". iSimpl. by rewrite refines_right_fill.
wp_pures. wp_bind e2. - iNext. iIntros (l) "Hl". simpl.
rel_pures_l. rel_bind_l e2.
iApply refines_wp_l.
iApply (wp_wand with "He2"). iIntros (?) "HQ". iApply (wp_wand with "He2"). iIntros (?) "HQ".
wp_pures. simpl. rel_pures_l. rel_bind_l (spawn.join _).
wp_apply (join_spec with "hndl"). iApply refines_wp_l.
iIntros (?) "Hj". wp_apply (join_spec with "Hl").
iSpecialize ("Ht" with "HQ"). iIntros (?) "Hk".
rewrite refines_eq /refines_def. iSpecialize ("Ht" with "HQ"). simpl.
rewrite fill_app. rel_pures_l. iApply (refines_combine with "Ht Hk").
iMod ("Ht" with "Hspec Hj") as "Ht".
rewrite wp_value_fupd. iMod "Ht" as (?) "[Ht [_ ->]]".
wp_pures. iExists #(). eauto with iFrame.
Qed. Qed.
(* Lemma par_r_1 e1 e2 t (A : lrel Σ) E : *) (* Lemma par_r_1 e1 e2 t (A : lrel Σ) E : *)
...@@ -188,8 +202,8 @@ Section rules. ...@@ -188,8 +202,8 @@ Section rules.
(* This proof is now simpler but it still requires unfolding the REL judgement *) (* This proof is now simpler but it still requires unfolding the REL judgement *)
Lemma par_comm e1 e2 : Lemma par_comm e1 e2 :
is_closed_expr [] e1 → is_closed_expr ∅ e1 →
is_closed_expr [] e2 → is_closed_expr ∅ e2 →
(REL e1 << e1 : ()) -∗ (REL e1 << e1 : ()) -∗
(REL e2 << e2 : ()) -∗ (REL e2 << e2 : ()) -∗
REL (e2 ∥ e1) << (e1 ∥ e2) : (). REL (e2 ∥ e1) << (e1 ∥ e2) : ().
...@@ -202,14 +216,17 @@ Section rules. ...@@ -202,14 +216,17 @@ Section rules.
tp_pure i (App _ _). simpl. tp_pure i (App _ _). simpl.
rel_pures_r. rel_pures_r.
rel_bind_r e2. rel_bind_r e2.
iApply refines_spec_ctx. iIntros "#Hs". iApply (par_l_1' (refines_right i (#c2 <- InjR (#();; #())))%I
iApply (par_l_1' (i ⤇ (#c2 <- InjR (#();; #())))%I
with "He2 [He1 Hi]"). with "He2 [He1 Hi]").
{ rewrite refines_eq /refines_def. { rewrite refines_eq /refines_def.
tp_bind i e1. tp_bind i e1.
iMod ("He1" with "Hs Hi") as "He1". simpl. rewrite refines_right_bind.
iAssert (spec_ctx) with "[Hi]" as "#Hs".
{ iDestruct "Hi" as "[$ _]". }
iMod ("He1" with "Hi") as "He1". simpl.
iApply (wp_wand with "He1"). iIntros (?). iApply (wp_wand with "He1"). iIntros (?).
iDestruct 1 as (?) "[Hi [-> ->]]". done. } iDestruct 1 as (?) "[Hi [-> ->]]".
rewrite /refines_right. by iFrame. }
iIntros "Hi". simpl. rel_pures_r. iIntros "Hi". simpl. rel_pures_r.
tp_pures i. tp_store i. tp_pures i. tp_store i.
rel_rec_r. rel_load_r. rel_pures_r. rel_values. rel_rec_r. rel_load_r. rel_pures_r. rel_values.
...@@ -229,8 +246,8 @@ Section rules. ...@@ -229,8 +246,8 @@ Section rules.
Qed. Qed.
Lemma seq_par e1 e2 (A B : lrel Σ) : Lemma seq_par e1 e2 (A B : lrel Σ) :
is_closed_expr [] e1 → is_closed_expr ∅ e1 →
is_closed_expr [] e2 → is_closed_expr ∅ e2 →
(REL e1 << e1 : A) -∗ (REL e1 << e1 : A) -∗
(REL e2 << e2 : B) -∗ (REL e2 << e2 : B) -∗
REL e1 ;; e2 << (e1 ||| e2)%V : lrel_true. REL e1 ;; e2 << (e1 ||| e2)%V : lrel_true.
...@@ -242,35 +259,40 @@ Section rules. ...@@ -242,35 +259,40 @@ Section rules.
{ simpl. eauto. } { simpl. eauto. }
repeat rel_pure_r. repeat rel_pure_r.
tp_rec i. simpl. tp_rec i. simpl.
rewrite {3}refines_eq /refines_def. rewrite {3}refines_eq /refines_def /=.
iIntros (j K) "#Hs Hj". iModIntro. iIntros (j) "Hj". iModIntro.
tp_bind j e2. tp_bind i e1. tp_bind j e2. tp_bind i e1.
(* execute e1 *) (* execute e1 *)
wp_bind e1. tp_bind i e1. wp_bind e1. tp_bind i e1.
rewrite {1}refines_eq /refines_def. rewrite !refines_right_fill.
iMod ("He1" with "Hs Hi") as "He1". rewrite {1}refines_eq /refines_def /=.
iMod ("He1" with "Hi") as "He1".
iApply (wp_wand with "He1"). iIntros (v1). iApply (wp_wand with "He1"). iIntros (v1).
iDestruct 1 as (v2) "[Hi Hv]". wp_pures. iDestruct 1 as (v2) "[Hi Hv]". wp_pures.
(* execute e2 *) (* execute e2 *)
rewrite refines_eq /refines_def. rewrite refines_eq /refines_def.
iMod ("He2" with "Hs Hj") as "He2". iMod ("He2" with "Hj") as "He2".
iApply wp_fupd. iApply wp_fupd.
iApply (wp_wand with "He2"). iIntros (w1). iApply (wp_wand with "He2"). iIntros (w1).
iDestruct 1 as (w2) "[Hj Hw]". iDestruct 1 as (w2) "[Hj Hw]".
iSimpl in "Hi". iSimpl in "Hj". iSimpl in "Hi". iSimpl in "Hj".
rewrite !refines_right_cons /=.
change (RefId (tp_id i) (tp_ctx i)) with i.
change (RefId (tp_id j) (tp_ctx j)) with j.
tp_pure i _. tp_pure i _.
tp_store i. tp_store i.
tp_pures j. tp_rec j. tp_pures j. tp_rec j.
tp_load j. tp_load j.
tp_pures j. tp_pures j.
iModIntro. iExists _. iFrame. iModIntro. iExists _.
by iFrame.
Qed. Qed.
Lemma interchange a b c d (A B C D : lrel Σ) : Lemma interchange a b c d (A B C D : lrel Σ) :
is_closed_expr [] a → is_closed_expr ∅ a →
is_closed_expr [] b → is_closed_expr ∅ b →
is_closed_expr [] c → is_closed_expr ∅ c →
is_closed_expr [] d → is_closed_expr ∅ d →
(REL a << a : A) -∗ (REL a << a : A) -∗
(REL b << b : B) -∗ (REL b << b : B) -∗
(REL c << c : C) -∗ (REL c << c : C) -∗
...@@ -286,45 +308,58 @@ Section rules. ...@@ -286,45 +308,58 @@ Section rules.
tp_rec i. simpl. tp_rec i. simpl.
rel_rec_l. repeat rel_pure_l. rel_rec_l. repeat rel_pure_l.
rewrite {5}refines_eq /refines_def. rewrite {5}refines_eq /refines_def.
iIntros (j K) "#Hs Hj". iModIntro. iIntros (j) "Hj". iModIntro.
pose (N:=nroot.@"par"). pose (N:=nroot.@"par").
wp_bind (spawn _). wp_bind (spawn _).
iApply (spawn_spec N with "[Ha Hj]"). iApply (spawn_spec N with "[Ha Hj]").
- wp_lam. rewrite refines_eq /refines_def. - wp_lam. rewrite refines_eq /refines_def.
tp_bind j a. tp_bind j a.
iMod ("Ha" with "Hs Hj") as "Ha". rewrite refines_right_fill.
iMod ("Ha" with "Hj") as "Ha".
iExact "Ha". iExact "Ha".
- iNext. iIntros (h) "Hdl". wp_pures. - iNext. iIntros (h) "Hdl". wp_pures.
wp_bind b. wp_bind b.
rewrite {1}refines_eq /refines_def. rewrite {1}refines_eq /refines_def.
tp_bind i b. tp_bind i b.
iMod ("Hb" with "Hs Hi") as "Hb". rewrite refines_right_fill.
iMod ("Hb" with "Hi") as "Hb".
iApply (wp_wand with "Hb"). iApply (wp_wand with "Hb").
iIntros (bv). iDestruct 1 as (bv') "[Hi HB]". simpl. iIntros (bv). iDestruct 1 as (bv') "[Hi HB]". simpl.
wp_pures. wp_bind (spawn.join _). wp_pures. wp_bind (spawn.join _).
iApply (join_spec with "Hdl"). iApply (join_spec with "Hdl").
iNext. iIntros (av). iDestruct 1 as (av') "[Hj HA]". iNext. iIntros (av). iDestruct 1 as (av') "[Hj HA]".
wp_pures. tp_pures j. tp_pures i. wp_pures.
rewrite !refines_right_cons /=.
change (RefId (tp_id i) (tp_ctx i)) with i.
change (RefId (tp_id j) (tp_ctx j)) with j.
tp_pures j. tp_pures i.
wp_rec. wp_pures. wp_rec. wp_pures.
wp_apply (spawn_spec N with "[Hc Hi]"). wp_apply (spawn_spec N with "[Hc Hi]").
{ wp_pures. { wp_pures.
rewrite refines_eq /refines_def. rewrite refines_eq /refines_def /=.
tp_bind i c. tp_bind i c.
iMod ("Hc" with "Hs Hi") as "Hc". iExact "Hc". } rewrite refines_right_fill.
iMod ("Hc" with "Hi") as "Hc".
iExact "Hc". }
clear h. iIntros (h) "Hdl". wp_pures. clear h. iIntros (h) "Hdl". wp_pures.
wp_bind d. wp_bind d.
rewrite refines_eq /refines_def. rewrite refines_eq /refines_def.
tp_bind j d. tp_bind j d.
iMod ("Hd" with "Hs Hj") as "Hd". rewrite refines_right_fill.
iMod ("Hd" with "Hj") as "Hd".
iApply (wp_wand with "Hd"). iIntros (dv). iApply (wp_wand with "Hd"). iIntros (dv).
iDestruct 1 as (dv') "[Hj HD]". iDestruct 1 as (dv') "[Hj HD]".
wp_pures. wp_apply (join_spec with "Hdl"). wp_pures. wp_apply (join_spec with "Hdl").
iIntros (cv). iDestruct 1 as (cv') "[Hi HC]". iIntros (cv). iDestruct 1 as (cv') "[Hi HC]".
iApply wp_fupd. iApply wp_fupd.
wp_pures. iExists (cv', dv')%V. simpl. wp_pures. iExists (cv', dv')%V. simpl.
rewrite !refines_right_cons /=.
change (RefId (tp_id i) (tp_ctx i)) with i.
change (RefId (tp_id j) (tp_ctx j)) with j.
tp_pures i. tp_store i. tp_pures i. tp_store i.
tp_pures j. tp_pures j.
rewrite /spawn.join. tp_pures j. rewrite /spawn.join. tp_pures j.
tp_load j. tp_pures j. eauto with iFrame. tp_load j. tp_pures j.
iModIntro; iSplit; eauto with iFrame.
Qed. Qed.
End rules. End rules.
theories/examples/red_blue_flag.v 0 → 100644
View file @ 37a694fd
(* This example considers two implementations of a concurrent flag. That is, a
single "bit" with a flip operation and a read operation.
The example demonstrates how to handle an _external_ linearization points in
ReLoC.
The specification uses a lock to guard the critical section in flip.
This example is from "Logical Relations for Fine-Grained Concurrency". *)
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth excl cmra agree frac gset csum.
From reloc Require Import reloc lib.lock.
(* blueFlag - the specification *)
Definition blueFlip : val := λ: "flag" "lock",
acquire "lock" ;;
"flag" <- ~ !"flag" ;;
release "lock".
Definition blueRead : val := λ: "flag", !"flag".
Definition blueFlag : val := λ: <>,
let: "flag" := ref #true in
let: "lock" := newlock #() in
(λ: <>, blueRead "flag",
λ: <>, blueFlip "flag" "lock").
(* redFlag - the implementation *)
(* The value of the side channel represents:
0 - No one is using the side channel.
1 - An offer is made on the side channel.
2 - An offer was accepted. *)
Definition redFlip : val := λ: "flag" "chan",
rec: "try" <> :=
if: CAS "chan" #1 #2 then #() else (* Take an offer. *)
if: CAS "flag" #true #false then #() else (* LP if this succeeds. *)
if: CAS "flag" #false #true then #() else (* LP if this succeeds. *)
if: CAS "chan" #0 #1 (* Make an offer. This is _not_ LP but when someone takes the offer our LP is during the execution of "someone". *)
then (if: CAS "chan" #1 #0 then "try" #() else "chan" <- #0;; #()) (* Did someone take our offer? *)
else "try" #().
Definition redRead : val :=
λ: "flag" <>, ! "flag".
Definition redFlag : val := λ: <>,
let: "flag" := ref #true in
let: "chan" := ref #0 in
(redRead "flag", redFlip "flag" "chan").
Definition offer : Type := Qp * gname * (list ectx_item).
Definition offerR :=
csumR (exclR unitR)
(prodR fracR (agreeR ref_idO)).
Class offerPreG Σ := OfferPreG {
offer_inG :: inG Σ offerR;
offer_token_inG :: inG Σ fracR;
}.
Section offer_theory.
Context `{!relocG Σ, !lockG Σ, !offerPreG Σ}.
Definition no_offer γ := own γ (Cinl (Excl ())).
Definition offer_elm (q : Qp) k : offerR := Cinr (q, to_agree k).
Definition own_offer γ q k := own γ (offer_elm q k).
Definition half_offer γ k := own_offer γ (1/2) k.
Definition quarter_offer γ k := own_offer γ (1/4) k.
(* Global Instance no_offer_exclusive' : Exclusive (Cinl (Excl ()) : offerR).
Proof. apply _. Qed. *)
Lemma no_offer_alloc : ⊢ |==> ∃ γ, no_offer γ.
Proof. by iApply own_alloc. Qed.
Lemma own_offer_valid γ q k : (own_offer γ q k -∗ ⌜(q ≤ 1)%Qp⌝).
Proof.
iIntros "Hown".
rewrite /own_offer /offer_elm.
iDestruct (own_valid with "Hown") as %[Hown _].
done.
Qed.
Lemma no_offer_exclusive γ q k : no_offer γ -∗ own_offer γ q k -∗ False.
Proof. iIntros "O P". by iCombine "O P" gives %?. Qed.
Lemma no_offer_to_offer γ k : no_offer γ ==∗ own_offer γ 1 k.
Proof.
iIntros "O".
iMod (own_update with "O") as "$"; last done.
by apply cmra_update_exclusive.
Qed.
Lemma offer_to_no_offer γ k : own_offer γ 1 k ==∗ no_offer γ.
Proof.
iIntros "O".
iMod (own_update with "O") as "$"; last done.
by apply cmra_update_exclusive.
Qed.
Lemma offer_agree γ q q' k k' :
own_offer γ q k -∗ own_offer γ q' k' -∗ ⌜k = k'⌝.
Proof.
iIntros "O P".
iCombine "O P" gives %[_ ?%to_agree_op_inv]%pair_valid.
by unfold_leibniz.
Qed.
(** TODO: Implement Fractional and AsFractional instances *)
Lemma offer_split γ q q' k :
own_offer γ (q + q') k ⊣⊢ own_offer γ q k ∗ own_offer γ q' k.
Proof.
rewrite -own_op /own_offer.
rewrite /offer_elm.
rewrite -Cinr_op -pair_op.
rewrite frac_op.
by rewrite agree_idemp.
Qed.
Lemma offer_combine γ q q' k k' :
own_offer γ q k -∗ own_offer γ q' k' -∗ ⌜k = k'⌝ ∗ own_offer γ (q + q') k.
Proof.
iIntros "O P".
iDestruct (offer_agree with "O P") as %<-.
repeat iSplit; first done.
iCombine "O P" as "O".
rewrite -Cinr_op -pair_op frac_op.
by rewrite agree_idemp.
Qed.
Lemma half_offer_combine γ k k' :
half_offer γ k -∗ half_offer γ k' ==∗ ⌜k = k'⌝ ∗ no_offer γ.
Proof.
iIntros "O P".
iDestruct (offer_agree with "O P") as %<-.
iMod (own_update_2 _ _ _ (Cinl (Excl ())) with "O P") as "O".
{ rewrite -Cinr_op -pair_op frac_op Qp.half_half.
apply cmra_update_exclusive. done. }
iModIntro. iFrame. done.
Qed.
Lemma no_offer_to_offers γ k : no_offer γ ==∗ own_offer γ (3/4) k ∗ quarter_offer γ k.
Proof.
iIntros "O".
iMod (no_offer_to_offer with "O") as "O".
rewrite -{1}Qp.three_quarter_quarter.
iDestruct (offer_split with "O") as "[Hhalf Hhalf']".
iModIntro. iFrame.
Qed.
End offer_theory.
Section proofs.
Context `{!relocG Σ, !lockG Σ, !offerPreG Σ}.
Definition offer_token γ q := own γ (q : frac).
Lemma offer_token_split γ : own γ 1%Qp ⊣⊢ own γ (1/2)%Qp ∗ own γ (1/2)%Qp.
Proof. rewrite -{1}Qp.half_half. rewrite -own_op. done. Qed.
(* The specification thread `k` is about to run a flip. *)
Definition tp_flip k bf lk := (refines_right k (blueFlip #bf lk))%I.
(* The specification thread `k` is done flipping. *)
Definition tp_flip_done k := (refines_right k (of_val #()))%I.
(** The offer invariant *)
Definition I_offer γ γ' (l : loc) bf lk : iProp Σ := ∃ (n : nat),
l ↦ #n ∗
(⌜n = 0⌝ ∗ offer_token γ' 1 ∗ no_offer γ (* No offer, everyone is free to make one. *)
∨ (∃ k, (* The side channel is being used. *)
⌜n = 1⌝ ∗ own_offer γ (1/2) k ∗ (refines_right k (blueFlip #bf lk)) (* An offer is made. *)
∨ ⌜n = 2⌝ ∗ (own_offer γ (1/2) k ∗ (refines_right k #()) ∨ offer_token γ' (1/2)))). (* An offer is accepted. *)
Definition I γ γ' (rf bf chan : loc) lk : iProp Σ :=
∃ (b : bool),
is_locked_r lk false ∗
rf ↦ #b ∗ bf ↦ₛ #b ∗
I_offer γ γ' chan bf lk.
Definition iN := nroot .@ "invariant".
(* When you take an offer you have to step whoever made the offer's
specification thread forward. *)
Lemma take_offer_l γ γ' l bf lk E t A K :
(|={⊤, E}=> ▷ I_offer γ γ' l bf lk ∗
▷ ((I_offer γ γ' l bf lk -∗ REL fill K (of_val #false) << t @ E : A)
∧ (∀ k, tp_flip k bf lk -∗ (tp_flip_done k -∗ I_offer γ γ' l bf lk) -∗
REL fill K (of_val #true) << t @ E : A))) -∗
REL fill K (CAS #l #1 #2) << t : A.
Proof.
iIntros "Hlog".
rel_cmpxchg_l_atomic.
iMod "Hlog" as "(Hoff & Hcont)".
iDestruct "Hoff" as (n) "[lPts Hdisj]".
iModIntro. iExists _. iFrame "lPts". iSplit.
- iIntros (Hneq).
iNext. iIntros "lPts".
rel_pures_l.
iDestruct "Hcont" as "[Hcont _]".
iApply "Hcont".
iExists _. iFrame.
- iIntros ([= Heq]).
iNext. iIntros "lPts".
iDestruct "Hdisj" as "[[% _] | Hdisj]"; first by subst.
iDestruct "Hdisj" as (k) "[(_ & Hoff & Hs) | [% _]]"; last by subst.
iDestruct "Hcont" as "[_ Hcont]".
rel_pures_l.
iApply ("Hcont" with "Hs").
iIntros "HI". iExists 2. iFrame "lPts".
iRight. iExists _. iRight. iFrame. iSplit; first done. iLeft. iFrame.
Qed.
Lemma blue_refines_red :
⊢ REL redFlag << blueFlag : () → (() → lrel_bool) * (() → ()).
Proof.
rewrite /redFlag /blueFlag.
rel_arrow_val. iIntros (?? [-> ->]).
rel_pures_l.
rel_pures_r.
(* Implementation initialization. *)
rel_alloc_l rf as "rfPts".
rel_alloc_l chan as "chanPts".
rel_pures_l.
(* Specification initialization. *)
rel_alloc_r bf as "bfPts".
rel_pures_r.
rel_apply_r refines_newlock_r. iIntros (lk) "Hlk".
do 2 rel_pure_r.
(* Allocate the invariant. *)
iMod no_offer_alloc as (γ) "Hno".
iMod (own_alloc (1%Qp)) as (γ') "Htok"; first done.
iMod (inv_alloc iN _ (I γ γ' rf bf chan lk) with "[-]") as "#Hinv".
{ iNext. iFrame. iExists 0. iFrame. iLeft. iFrame. done. }
iApply refines_pair.
(* Refines read. *)
- rel_rec_l.
rel_arrow_val. iIntros (?? [-> ->]).
rel_pures_l.
rel_pures_r.
rel_load_l_atomic.
iInv iN as (?) "(>Hlk & rfPts & bfPts & chanPts)" "Hclose".
iExists _. iFrame "rfPts". iModIntro. iNext. iIntros "rfPts".
rel_rec_r.
rel_load_r.
iMod ("Hclose" with "[-]") as "_".
{ iNext. iExists _. iFrame. }
rel_values.
(* Refines flip. *)
- rel_rec_l.
rel_pures_l.
rel_pures_r.
rel_arrow_val. iIntros (?? [-> ->]).
fold blueFlip.
rel_pures_r.
iLöb as "IH".
rel_pures_l.
(* The first CAS. *)
rel_apply_l take_offer_l.
iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
iModIntro. iFrame "Hchan". iNext. iSplit.
(* Taking the offer succeeded. *)
2: {
iIntros (j) "Hj Hrest".
(* Step our specification forward for our LP. *)
rewrite /blueFlip.
rel_pures_r.
rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
rel_load_r.
rel_store_r.
rel_pures_r.
rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
(* Step the other thread's spec forward for their LP. *)
rewrite /tp_flip /tp_flip_done.
tp_rec j. tp_pures j.
(* Handle the acquire. *)
tp_rec j.
rewrite /is_locked_r. iDestruct "Hlk" as (lk' ->) "Hl".
tp_cmpxchg_suc j.
tp_pures j.
tp_load j.
tp_pures j.
tp_store j.
tp_pures j.
tp_rec j. tp_store j.
rewrite negb_involutive.
iDestruct ("Hrest" with "Hj") as "Hoff".
iMod ("Hclose" with "[-]") as "_".
{ by iFrame. }
rel_pures_l.
rel_values. }
iIntros "Hoff".
iMod ("Hclose" with "[$]") as "_".
rel_pures_l.
(* The second CAS. *)
rel_cmpxchg_l_atomic.
iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
iFrame "rfPts". iModIntro. iSplit.
2: {
iIntros ([= ->]). iNext. iIntros "rfPts".
rel_pures_l.
rel_rec_r.
rel_pures_r.
rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
rel_load_r.
rel_store_r.
rel_pures_r.
rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
rel_values. }
iIntros (_). iNext. iIntros "rfPts".
iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
rel_pures_l.
(* The third CAS. *)
rel_cmpxchg_l_atomic.
iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
iExists _. iFrame "rfPts". iModIntro. iSplit.
2: {
iIntros ([= ->]). iNext. iIntros "rfPts".
rel_pures_l.
rel_rec_r.
rel_pures_r.
rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
rel_load_r.
rel_store_r.
rel_pures_r.
rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
rel_values. }
iIntros (_). iNext. iIntros "rfPts".
iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
rel_pures_l.
(* ALTERNATIVE fourth CAS. *)
iApply refines_split.
iIntros (k) "Hk".
rel_cmpxchg_l_atomic.
iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
iDestruct "Hchan" as (n) "[>chanPts Hdisj]".
iModIntro. iExists _. iFrame. iSplit.
{ (* If the CAS fails we didn't succeed in making and offer, we recurse
and use the IH. *)
iIntros (Heq). simplify_eq/=.
iNext. iIntros "Hchan".
iMod ("Hclose" with "[$]") as "_".
iApply (refines_combine with "[] Hk").
do 2 rel_pure_l _.
iApply "IH". }
iIntros (Heq). simplify_eq/=.
assert (n = 0) as -> by lia.
iNext. iIntros "Hchan".
iDestruct "Hdisj" as "[(_ & Htok & Hoff) | Hdisj]".
2: { iDestruct "Hdisj" as (?) "[[% _]|[% _]]"; by subst. }
iMod (no_offer_to_offer _ k with "Hoff") as "Hoff".
iEval (rewrite -Qp.half_half) in "Hoff".
iDestruct (offer_split with "Hoff") as "[Hoff Hoff']".
iMod ("Hclose" with "[-IH Hoff Htok]") as "_".
{ iNext. iExists _. iFrame. iExists 1. iFrame. iRight. iExists k. iLeft. by iFrame. }
rel_pures_l.
rel_cmpxchg_l_atomic.
iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
iDestruct "Hchan" as (n) "[>chanPts Hdisj]".
iModIntro. iExists _. iFrame "chanPts". iSplit.
2: { (* Revoking the offer succeeded. *)
iIntros (?) "!> Hchan". simplify_eq/=.
assert (n = 1) as -> by lia.
iDestruct "Hdisj" as "[[% _] | Hdisj]"; first by subst.
iDestruct "Hdisj" as (?) "[(% & Hoff' & Hj) | [% _]]"; last by subst.
iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
rewrite Qp.half_half.
iMod (offer_to_no_offer with "Hoff") as "Hoff".
iMod ("Hclose" with "[-IH Hj]") as "_".
{ iNext. iExists _. iFrame. iExists 0. iFrame. iLeft. by iFrame. }
do 2 rel_pure_l _.
iApply (refines_combine with "[] Hj").
iApply "IH". }
iIntros (Heq2) "!> Hchan".
iDestruct "Hdisj" as "[(% & _ & Hoff') | Hdisj]".
{ iDestruct (no_offer_exclusive with "Hoff' Hoff") as %?. done. }
iDestruct "Hdisj" as (?) "[[% _] | (% & Hdisj)]"; first by subst.
iDestruct "Hdisj" as "[[Hoff' Hj] | Hoff']".
2: {
iCombine "Htok Hoff'" gives %Hv.
by apply Qp.not_add_le_l in Hv. }
iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
iDestruct (offer_token_split with "Htok") as "[Htok Htok']".
iMod ("Hclose" with "[-IH Hj Hoff Htok]") as "_".
{ iNext. iExists _. iFrame. iRight.
iExists k. iRight. by iFrame. }
rel_pures_l.
(* Clean up the offer. *)
rel_store_l_atomic.
iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
iDestruct "Hchan" as (m) "[>chanPts Hdisj]".
iModIntro. iExists _. iFrame "chanPts". iNext.
iIntros "chanPts".
iDestruct "Hdisj" as "[(_ & _ & Hoff') | Hdisj]".
{ iDestruct (no_offer_exclusive with "Hoff' Hoff") as %?. done. }
iDestruct "Hdisj" as (?) "[(_ & Hoff' & _) | (% & Hdisj)]".
{ iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
rewrite Qp.half_half.
iDestruct (own_offer_valid with "Hoff") as %Hle.
by apply Qp.not_add_le_l in Hle. }
iDestruct "Hdisj" as "[[Hoff' _] | Htok']".
{ iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
rewrite Qp.half_half.
iDestruct (own_offer_valid with "Hoff") as %Hle.
by apply Qp.not_add_le_l in Hle. }
iCombine "Htok Htok'" as "Htok".
iEval (rewrite Qp.half_half) in "Hoff".
iMod (offer_to_no_offer with "Hoff") as "Hoff".
iMod ("Hclose" with "[-IH Hj]") as "_".
{ iNext. iExists _. iFrame. iExists 0. iFrame. iLeft. iFrame. done. }
iApply (refines_combine with "[] Hj"). rel_pures_l. rel_values.
Qed.
End proofs.