From e2681e43cc7849d66425d5bc93565e9e177d229a Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Wed, 24 Jun 2026 19:29:28 +0200 Subject: Initial commit --- .envrc | 1 + .gitignore | 17 + Makefile | 55 +++ _CoqProject | 12 + flake.lock | 61 +++ flake.nix | 44 ++ theories/basic_queue_proof.v | 652 ++++++++++++++++++++++++++ theories/basic_queue_spec.v | 30 ++ theories/example.v | 723 +++++++++++++++++++++++++++++ theories/fin_queue_proof.v | 932 ++++++++++++++++++++++++++++++++++++++ theories/fin_queue_spec.v | 67 +++ theories/lmpmc_blocking_dequeue.v | 40 ++ theories/lmpmc_queue_proof.v | 362 +++++++++++++++ theories/lmpmc_queue_spec.v | 49 ++ theories/upstream.v | 60 +++ theories/util.v | 12 + 16 files changed, 3117 insertions(+) create mode 100644 .envrc create mode 100644 .gitignore create mode 100644 Makefile create mode 100644 _CoqProject create mode 100644 flake.lock create mode 100644 flake.nix create mode 100644 theories/basic_queue_proof.v create mode 100644 theories/basic_queue_spec.v create mode 100644 theories/example.v create mode 100644 theories/fin_queue_proof.v create mode 100644 theories/fin_queue_spec.v create mode 100644 theories/lmpmc_blocking_dequeue.v create mode 100644 theories/lmpmc_queue_proof.v create mode 100644 theories/lmpmc_queue_spec.v create mode 100644 theories/upstream.v create mode 100644 theories/util.v diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..3550a30 --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +use flake diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..56fa1a1 --- /dev/null +++ b/.gitignore @@ -0,0 +1,17 @@ +*.aux +*.glob +*.vio +*.vo +*.vok +*.vos +.CoqMakefile.d +.Makefile.coq.d +.direnv +.lia.cache +Makefile.coq +Makefile.coq.conf +*#*.v# +*#*.vok# +*~ +.#* +\#*# diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..ac8dba0 --- /dev/null +++ b/Makefile @@ -0,0 +1,55 @@ +# Default target +all: Makefile.coq + +@$(MAKE) -f Makefile.coq all +.PHONY: all + +# Permit local customization +-include Makefile.local + +# Forward most targets to Coq makefile (with some trick to make this phony) +%: Makefile.coq phony + @#echo "Forwarding $@" + +@$(MAKE) -f Makefile.coq $@ +phony: ; +.PHONY: phony + +clean: Makefile.coq + +@$(MAKE) -f Makefile.coq clean + @# Make sure not to enter the `_opam` folder. + find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true + rm -f Makefile.coq .lia.cache builddep/* +.PHONY: clean + +# Create Coq Makefile. +Makefile.coq: _CoqProject Makefile + "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES) + +# Install build-dependencies +OPAMFILES=$(wildcard *.opam) +BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES)))) + +builddep/%-builddep.opam: %.opam Makefile + @echo "# Creating builddep package for $<." + @mkdir -p builddep + @sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@ + +builddep-opamfiles: $(BUILDDEPFILES) +.PHONY: builddep-opamfiles + +builddep: builddep-opamfiles + @# We want opam to not just install the build-deps now, but to also keep satisfying these + @# constraints. Otherwise, `opam upgrade` may well update some packages to versions + @# that are incompatible with our build requirements. + @# To achieve this, we create a fake opam package that has our build-dependencies as + @# dependencies, but does not actually install anything itself. + @echo "# Installing builddep packages." + @opam install $(OPAMFLAGS) $(BUILDDEPFILES) +.PHONY: builddep + +# Backwards compatibility target +build-dep: builddep +.PHONY: build-dep + +# Some files that do *not* need to be forwarded to Makefile.coq. +# ("::" lets Makefile.local overwrite this.) +Makefile Makefile.local _CoqProject $(OPAMFILES):: ; diff --git a/_CoqProject b/_CoqProject new file mode 100644 index 0000000..a3d9642 --- /dev/null +++ b/_CoqProject @@ -0,0 +1,12 @@ +-Q theories lmpmc + +theories/util.v +theories/upstream.v +theories/basic_queue_spec.v +theories/fin_queue_spec.v +theories/lmpmc_queue_spec.v +theories/basic_queue_proof.v +theories/fin_queue_proof.v +theories/lmpmc_queue_proof.v +theories/lmpmc_blocking_dequeue.v +theories/example.v diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..f4a7de9 --- /dev/null +++ b/flake.lock @@ -0,0 +1,61 @@ +{ + "nodes": { + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1777077449, + "narHash": "sha256-AIiMJiqvGrN4HyLEbKAoCSRRYn0rnlW5VbKNIMIYqm4=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "a4bf06618f0b5ee50f14ed8f0da77d34ecc19160", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-25.11", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..4fcc282 --- /dev/null +++ b/flake.nix @@ -0,0 +1,44 @@ +{ + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.11"; + flake-utils.url = "github:numtide/flake-utils"; + }; + + outputs = { self, nixpkgs, flake-utils, ... }: + flake-utils.lib.eachDefaultSystem (system: + let + pkgs = import nixpkgs { inherit system; }; + + # From 22-04-2026 + stdpp = with pkgs; coqPackages.lib.overrideCoqDerivation { + version = "dev"; + release."dev".sha256 = "hN+sEZcIaFoFF2+4dStTc0TRz5A03US6csEk5q0r/z8="; + release."dev".rev = "d3c67aa46ed22b1e593457cd34fc711f1a53b8be"; + } coqPackages.stdpp; + + # From 04-05-2026 + iris = with pkgs; coqPackages.lib.overrideCoqDerivation { + version = "dev"; + release."dev".sha256 = "P2cELkPl8RcHE1PzoswhMjXS5l8RBInW9q7Es0wtkus="; + release."dev".rev = "306c37bfc12b0d459d302dabad9de5ab09d6a6d4"; + propagatedBuildInputs = [ stdpp ]; + } coqPackages.iris; + + # From 11-03-2026 + iris-named-props = with pkgs; coqPackages.mkCoqDerivation rec { + pname = "iris-named-props"; + owner = "tchajed"; + version = "dev"; + release."dev".sha256 = "1YHAItQ9XsCy+0M/pG2ib/GeaLTFJOrGJwF8noViwKg="; + release."dev".rev = "ca663d2709888a789a03edc861b7bde86ddd56e5"; + propagatedBuildInputs = [ iris ]; + }; + in + { + devShells.default = with pkgs; mkShell { + buildInputs = [ coq iris iris-named-props ]; + }; + + formatter = pkgs.nixpkgs-fmt; + }); +} diff --git a/theories/basic_queue_proof.v b/theories/basic_queue_proof.v new file mode 100644 index 0000000..f169878 --- /dev/null +++ b/theories/basic_queue_proof.v @@ -0,0 +1,652 @@ +From iris.program_logic Require Import atomic. +From iris.heap_lang Require Import notation proofmode. +From iris.algebra.lib Require Import excl_auth. +From iris.base_logic.lib Require Import invariants. +From iris.base_logic.lib Require Import invariants mono_nat mono_list. +From iris_named_props Require Import custom_syntax. + +From lmpmc Require Import basic_queue_spec upstream util. + +Definition new_node : val := λ: "data", + let: "ℓ_node" := AllocN #2 #() in + "ℓ_node" <- "data";; + "ℓ_node" +ₗ #1 <- NONE;; + "ℓ_node". + +Definition new : val := λ: <>, + let: "ℓ_node" := new_node #() in + AllocN #2 "ℓ_node". + +Definition set_tail : val := rec: "go" "ℓ_q" "ℓ_node" := + let: "ℓ_tail" := !("ℓ_q" +ₗ #1) in + match: !("ℓ_tail" +ₗ #1) with + NONE => + if: CAS ("ℓ_tail" +ₗ #1) NONE (SOME "ℓ_node") then + #() + else + "go" "ℓ_q" "ℓ_node" + | SOME "ℓ_next" => + CAS ("ℓ_q" +ₗ #1) "ℓ_tail" "ℓ_next";; + "go" "ℓ_q" "ℓ_node" + end. + +Definition enqueue : val := λ: "ℓ_q" "data", + set_tail "ℓ_q" (new_node "data"). + +Definition try_dequeue : val := rec: "go" "ℓ_q" := + let: "ℓ_head" := !"ℓ_q" in + match: !("ℓ_head" +ₗ #1) with + NONE => NONE + | SOME "ℓ_next" => + let: "v" := !"ℓ_next" in + if: CAS "ℓ_q" "ℓ_head" "ℓ_next" then + SOME "v" + else + "go" "ℓ_q" + end. + +Class basic_queueG Σ := BasicQueueG + { basic_queue_mono_natG :: mono_natG Σ; + basic_queue_mono_listG :: mono_listG (prodO locO valO) Σ; }. + +Definition basic_queueΣ : gFunctors := + #[ mono_natΣ; mono_listΣ (prodO locO valO) ]. + +#[global] Instance subG_basic_queueΣ {Σ} : subG basic_queueΣ Σ → basic_queueG Σ. +Proof. solve_inG. Qed. + +Section basic_queue. + Context `{!heapGS Σ, !basic_queueG Σ}. + + Record gstate := + { γ_hist : gname; + γ_hpos : gname; }. + Definition gstate_to_pair (γ : gstate) := + (γ.(γ_hist), γ.(γ_hpos)). + Definition gstate_of_pair '(γ_hist, γ_hpos) := + {| γ_hist := γ_hist; γ_hpos := γ_hpos |}. + Instance gstate_eq_dec : EqDecision gstate := ltac:(solve_decision). + Instance gstate_countable : Countable gstate. + Proof. + refine {| encode := encode ∘ gstate_to_pair; + decode := fmap gstate_of_pair ∘ decode; |}. + intros []. by rewrite /= decode_encode. + Qed. + + Definition node_repr (ℓ : loc) (data : val) (mℓ_next : option loc) : iProp Σ := + ("Hndata" ∷ ℓ ↦□ data) ∗ + ("Hnnext" ∷ (ℓ +ₗ 1) ↦ loc_opt_hl mℓ_next). + + Definition loc_at (hist : list (loc * val)) i := + hist.*1 !! i. + Definition val_at (hist : list (loc * val)) i := + hist.*2 !! i. + + Lemma loc_at_prefix xs xs' i ℓ : + loc_at xs i = Some ℓ → xs `prefix_of` xs' → loc_at xs' i = Some ℓ. + Proof. + unfold loc_at. intros Hxs Hpre. + eapply prefix_lookup_Some; first exact Hxs. + by apply prefix_of_fmap. + Qed. + + Lemma val_at_prefix xs xs' i ℓ : + val_at xs i = Some ℓ → xs `prefix_of` xs' → val_at xs' i = Some ℓ. + Proof. + unfold val_at. intros Hxs Hpre. + eapply prefix_lookup_Some; first exact Hxs. + by apply prefix_of_fmap. + Qed. + + Lemma loc_at_val_at_Some xs i ℓ : + loc_at xs i = Some ℓ → ∃ v, val_at xs i = Some v. + Proof. + unfold loc_at, val_at. rewrite [xs.*2 !! i]list_lookup_fmap. + intros [[ℓ' v] [-> ->]]%list_lookup_fmap_Some_1. by exists v. + Qed. + + Lemma loc_at_val_at_combine {hist i ℓ v} : + loc_at hist i = Some ℓ → + val_at hist i = Some v → + hist !! i = Some (ℓ, v). + Proof. + unfold loc_at, val_at. intros Hloc Hval. + rewrite list_lookup_fmap in Hloc. + rewrite list_lookup_fmap in Hval. + destruct (hist !! i) as [[ℓ' v']|]; last done. + simpl in *. congruence. + Qed. + + Lemma loc_at_Some_length hist i ℓ : + loc_at hist i = Some ℓ → i < length hist. + Proof. + intros Hloc%lookup_lt_Some. + by rewrite length_fmap in Hloc. + Qed. + + Lemma loc_at_drop hist n i ℓ : + loc_at hist (n + i) = Some ℓ → + loc_at (drop n hist) i = Some ℓ. + Proof. + unfold loc_at. intros Hloc. + by rewrite list_lookup_fmap lookup_drop -list_lookup_fmap. + Qed. + + Lemma loc_at_drop_2 hist n i : + loc_at (drop n hist) i = loc_at hist (n + i). + Proof. by rewrite /loc_at list_lookup_fmap lookup_drop -list_lookup_fmap. Qed. + + Lemma val_at_drop hist n i ℓ : + val_at hist (n + i) = Some ℓ → + val_at (drop n hist) i = Some ℓ. + Proof. + unfold val_at. intros Hval. + by rewrite list_lookup_fmap lookup_drop -list_lookup_fmap. + Qed. + + Definition hist_repr (hist : list (loc * val)) : iProp Σ := + [∗ list] i ↦ '(ℓ, data) ∈ hist, node_repr ℓ data (loc_at hist (S i)). + + Lemma hist_repr_peek_1 hist i ℓ data : + loc_at hist i = Some ℓ → + val_at hist i = Some data → + hist_repr hist -∗ + node_repr ℓ data (loc_at hist (S i)) ∗ + (node_repr ℓ data (loc_at hist (S i)) -∗ hist_repr hist). + Proof. + iIntros "%Hloc %Hval Hrepr". + pose proof (loc_at_val_at_combine Hloc Hval) as Hi. + iPoseProof (big_sepL_lookup_acc with "Hrepr") as "[Hnode Hclose]". + { apply Hi. } + iFrame. + Qed. + + Lemma hist_repr_peek_2 hist i ℓ : + loc_at hist i = Some ℓ → + hist_repr hist -∗ + ∃ data, node_repr ℓ data (loc_at hist (S i)) ∗ + (node_repr ℓ data (loc_at hist (S i)) -∗ hist_repr hist). + Proof. + iIntros "%Hloc Hrepr". + assert (∃ v, val_at hist i = Some v) as [v Hval]. + { by apply loc_at_val_at_Some in Hloc. } + iExists v. by iApply hist_repr_peek_1. + Qed. + + Lemma hist_repr_peek_3 hist i ℓ : + loc_at hist i = Some ℓ → + hist_repr hist -∗ + (ℓ +ₗ 1) ↦ loc_opt_hl (loc_at hist (S i)) ∗ + ((ℓ +ₗ 1) ↦ loc_opt_hl (loc_at hist (S i)) -∗ hist_repr hist). + Proof. + iIntros "%Hloc Hrepr". + iDestruct (hist_repr_peek_2 with "[$]") as "(%v & @ & Hclose)"; first done. + iFrame. iIntros "Hnnext". iApply "Hclose". iFrame. + Qed. + + Lemma loc_at_None hist pos : + loc_at hist pos = None → hist !! pos = None. + Proof. + rewrite /loc_at list_lookup_fmap. + by destruct (hist !! pos). + Qed. + + Lemma loc_at_length hist pos : + loc_at hist pos = None → length hist ≤ pos. + Proof. + intros H%loc_at_None. + by apply lookup_ge_None. + Qed. + + Lemma hist_repr_proj hist i ℓ : + loc_at hist i = Some ℓ → + hist_repr hist -∗ + (∃ v, (ℓ +ₗ 1) ↦ v) ∗ hist_repr (drop (S i) hist). + Proof. + iIntros "%Hℓi Hrepr". + iDestruct (big_sepL_take_drop _ _ (S i) with "Hrepr") as "[Hrepr1 Hrepr2]". + + rewrite /loc_at list_lookup_fmap in Hℓi. + destruct (hist !! i) as [[ℓ' v]|] eqn:Hi; last done. + simpl in *. injection Hℓi as ->. + + iDestruct (big_sepL_lookup_acc with "Hrepr1") as "[Hrepr Hclose]". + { rewrite lookup_take_lt //. lia. } + iSimplifyEq. iDestruct "Hrepr" as "@". iFrame. + iClear "Hndata Hclose". + + iAssert (hist_repr (drop (S i) hist)) with "[Hrepr2]" as "Hrepr2". + { unfold hist_repr. iApply (big_sepL_mono with "Hrepr2"). + iIntros (k [ℓ' v'] Hk) "Hrepr". + by rewrite loc_at_drop_2 Nat.add_succ_l Nat.add_succ_r. } + done. + Qed. + + Lemma loc_at_inj_aux hist i j ℓ : + i < j → + loc_at hist i = Some ℓ → + loc_at hist j = Some ℓ → + hist_repr hist -∗ + False. + Proof. + iIntros "%ij %Hloci %Hlocj Hrepr". + assert (i < length hist). { by eapply loc_at_Some_length. } + assert (j < length hist). { by eapply loc_at_Some_length. } + assert (∃ n, j = S i + n) as [n ->]. + { exists (j - i - 1). lia. } + iPoseProof (hist_repr_proj hist i ℓ Hloci with "Hrepr") as "[[%ni Hℓi] Hrepr']". + + assert (Hlocj' : loc_at (drop (S i) hist) n = Some ℓ). + { by apply loc_at_drop. } + + iPoseProof (hist_repr_proj _ n ℓ Hlocj' with "Hrepr'") as "[[%nj Hℓj] _]". + by iCombine "Hℓi Hℓj" gives %[? _]. + Qed. + + Lemma loc_at_inj {hist i j ℓ} : + loc_at hist i = Some ℓ → + loc_at hist j = Some ℓ → + hist_repr hist -∗ + ⌜i = j⌝. + Proof. + iIntros "%Hloci %Hlocj Hrepr". + destruct (loc_at_val_at_Some hist i ℓ Hloci) as [vi Hvali]. + destruct (loc_at_val_at_Some hist j ℓ Hlocj) as [vj Hvalj]. + destruct (decide (i < j)) as [Hij|Hij]. + - (* i < j *) + by iPoseProof (loc_at_inj_aux with "Hrepr") as "H". + - (* i ≥ j *) + destruct (decide (j < i)) as [Hji|Hji]. + + (* j < i *) + by iPoseProof (loc_at_inj_aux with "Hrepr") as "H". + + (* i = j *) + iPureIntro. lia. + Qed. + + Definition queue_repr_1 (γs : gstate) ℓ_q (vs : list val) : iProp Σ := + ∃ (hist : list (loc * val)) (ℓ_head ℓ_tail : loc) (hpos tpos : nat), + ("Hhead" ∷ ℓ_q ↦ #ℓ_head) ∗ + ("Htail" ∷ (ℓ_q +ₗ 1) ↦ #ℓ_tail) ∗ + ("Hrepr" ∷ hist_repr hist) ∗ + ("Hhist●" ∷ γs.(γ_hist) ↪●ML hist) ∗ + ("Hhpos●" ∷ γs.(γ_hpos) ↪●MN hpos) ∗ + ("%Hℓhpos" ∷ ⌜loc_at hist hpos = Some ℓ_head⌝) ∗ + ("%Hℓtpos" ∷ ⌜loc_at hist tpos = Some ℓ_tail⌝) ∗ + ("%Hvs" ∷ ⌜vs = (drop (S hpos) hist).*2⌝). + + Definition queue_repr ℓ_q (vs : list val) : iProp Σ := + ∃ (γs : gstate), meta ℓ_q nroot γs ∗ queue_repr_1 γs ℓ_q vs. + + #[global] Instance queue_repr_timeless ℓ_q vs : Timeless (queue_repr ℓ_q vs) := _. + + Lemma new_node_spec data : + {{{ True }}} + new_node data + {{{ (ℓ : loc), RET #ℓ; node_repr ℓ data None }}}. + Proof. + iIntros "%Φ _ HΦ". iUnfold new_node. wp_lam. + wp_alloc ℓ_node as "Hℓ_node"; first done. + iDestruct (array_cons with "Hℓ_node") as "[Hℓ_node0 Hℓ_node1]". + iDestruct (array_cons with "Hℓ_node1") as "[Hℓ_node1 _]". + wp_let. do 2 wp_store. + iMod (pointsto_persist with "Hℓ_node0") as "Hℓ_node0". + iModIntro. iApply "HΦ". by iFrame. + Qed. + + Lemma new_spec : + {{{ True }}} + new #() + {{{ (ℓ : loc), RET #ℓ; queue_repr ℓ [] }}}. + Proof. + iIntros "%Φ _ HΦ". iUnfold new. + wp_lam. wp_apply (new_node_spec with "[//]"). + iIntros (ℓ_node) "Hnode". wp_let. + + set ℓ_head := ℓ_node. set ℓ_tail := ℓ_node. + set hpos := 0. set tpos := 0. + set hist := [(ℓ_node, #())] : list (loc * val). + iAssert (hist_repr hist) with "[$Hnode //]" as "Hrepr". + + iMod (mono_list_own_alloc hist) as "[%γ_hist [Hhist● _]]". + iMod (mono_nat_own_alloc hpos) as "[%γ_hpos [Hhpos● _]]". + set γs := {| γ_hist := γ_hist; γ_hpos := γ_hpos |}. + + iApply wp_fupd. iApply wp_allocN; [lia|done|]. + iIntros "!> %ℓ [Hℓ [Htok _]]". + iDestruct (array_cons with "Hℓ") as "[Hℓ0 Hℓ1]". + iDestruct (array_cons with "Hℓ1") as "[Hℓ1 _]". + rewrite Loc.add_0. + + iMod (meta_set ⊤ ℓ γs nroot with "Htok") as "Hmeta"; first done. + + iApply "HΦ". iModIntro. iFrame. by iExists tpos. + Qed. + + Lemma try_bump_tail_spec hist0 tpos ℓ_old ℓ_new ℓ_q γs : + loc_at hist0 tpos = Some ℓ_old → + loc_at hist0 (S tpos) = Some ℓ_new → + γs.(γ_hist) ↪◯ML hist0 -∗ + <<{ ∀∀ vs, queue_repr_1 γs ℓ_q vs }>> + CAS #(ℓ_q +ₗ 1) #ℓ_old #ℓ_new @ ∅ + <<{ ∃∃ (b : bool), queue_repr_1 γs ℓ_q vs | RET #b }>>. + Proof. + iIntros "%Hold %Hnew #Hhist◯ %Φ AU". + wp_bind (CmpXchg _ _ _)%E. + iMod "AU" as "(%vs & (%hist1 & %ℓ_head & %ℓ_tail & %hpos & %tpos' & @) & [_ Hclose])". + iAssert ⌜hist0 `prefix_of` hist1⌝%I as %Hhist01. + { by iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist◯") as "[_ ?]". } + + destruct (decide (ℓ_tail = ℓ_old)) as [->|]. + - (* The tail has not been updated yet *) + wp_cmpxchg_suc. + + iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq". + { iPureIntro. + repeat split; try done || lia. + exists (S tpos). repeat split; try done. + by eapply loc_at_prefix. } + iMod ("Hclose" with "[$Hq]") as "HΦ". + iModIntro. wp_pures. iApply "HΦ". + - (* The tail has been updated in the meantime *) + wp_cmpxchg_fail. + iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq". + { iExists tpos'. by iFrameNamed. } + iMod ("Hclose" with "[$Hq]") as "HΦ". + iModIntro. wp_pures. iApply "HΦ". + Qed. + + (* Given a history that is represented, after updating the [next] + pointer of the current tail node to a new tail node, we obtain a + new (extended) history (with the new tail node appended). *) + Lemma hist_repr_snoc hist tpos (ℓ_tail ℓ_new : loc) data : + length hist = S tpos → + loc_at hist tpos = Some ℓ_tail → + node_repr ℓ_new data None -∗ + hist_repr hist -∗ + (ℓ_tail +ₗ 1) ↦ loc_opt_hl None ∗ + ((ℓ_tail +ₗ 1) ↦ loc_opt_hl (Some ℓ_new) -∗ hist_repr (hist ++ [(ℓ_new, data)])). + Proof. + unfold loc_at. + iIntros "%Hhistlen %Hloc @ Hhist". + rewrite list_lookup_fmap in Hloc. + destruct (hist !! tpos) as [[ℓ_tail' v_tail]|] eqn:Htpos; last done. + injection Hloc as ->. + apply list_elem_of_split_length in Htpos as (hist' & empty & -> & Htpos). + rewrite length_app length_cons -Htpos in Hhistlen. + assert (empty = []) as ->. { apply nil_length_inv. lia. } + clear Hhistlen Htpos. + + iPoseProof (big_sepL_snoc with "Hhist") as "[Hinit Htail]". + iNamedSuffix "Htail" "_tail". + + iSimplifyEq. + assert (loc_at (hist' ++ [(ℓ_tail, v_tail)]) (S (length hist')) = None) as ->. + { apply lookup_ge_None_2. rewrite length_fmap length_app length_cons /=. lia. } + iFrame "Hnnext_tail". iIntros "Hnnext_tail". + iSimplifyEq. rewrite /hist_repr. + iApply big_sepL_snoc. + iSplitR "Hndata Hnnext". + - iApply big_sepL_snoc. iSplitL "Hinit". + + iApply (big_sepL_mono with "Hinit"). + iIntros (k [ℓ v] Hk) "Hrepr". + assert (loc_at ((hist' ++ [(ℓ_tail, v_tail)]) ++ [(ℓ_new, data)]) (S k) = loc_at (hist' ++ [(ℓ_tail, v_tail)]) (S k)) as ->. + { rewrite /loc_at !list_lookup_fmap lookup_app_l // length_app /=. + apply lookup_lt_Some in Hk. lia. } + done. + + iFrame. + rewrite /loc_at list_lookup_fmap lookup_app_r; last first. + { rewrite length_app /=. lia. } + by rewrite length_app /= Nat.add_1_r Nat.sub_diag. + - iFrame. + rewrite /= /loc_at length_app /= Nat.add_1_r list_lookup_fmap lookup_app_r. + * by rewrite !length_app /= !Nat.add_1_r Nat.sub_succ -Arith_base.minus_Sn_m_stt // Nat.sub_diag. + * rewrite length_app /= Nat.add_1_r. lia. + Qed. + + Lemma set_tail_spec (ℓ_q ℓ_node : loc) data : + node_repr ℓ_node data None -∗ + <<{ ∀∀ vs, queue_repr ℓ_q vs }>> + set_tail #ℓ_q #ℓ_node @ ∅ + <<{ queue_repr ℓ_q (vs ++ [data]) | RET #() }>>. + Proof. + iIntros "@ %Φ AU". iLöb as "IH". wp_rec. + + wp_pures. wp_bind (! _)%E. + iMod "AU" as "(%vs & (%γs & #Hγs & %hist0 & %ℓ_head & %ℓ_tail & %hpos & %tpos & @) & [Hclose _])". + iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist0◯". + wp_load. iSimpl in "Hrepr". + rename Hℓtpos into Hℓtpos0. + iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq". + { iExists tpos. by iFrameNamed. } + iMod ("Hclose" with "[$]") as "AU". clear Hvs Hℓhpos hpos vs ℓ_head. + iModIntro. wp_let. wp_pure. + + wp_bind (! _)%E. + iMod "AU" as "(%vs & (%γs' & Hγs' & %hist2 & %ℓ_head & %ℓ_tail'' & %hpos & %tpos'' & @) & [Hclose _])". + iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}". + iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist0◯") as %Hhist02. + iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist2◯". + destruct Hhist02 as [_ Hhist02]. rename Hℓtpos into Hℓtpos2. + assert (Hℓtpos0'' : loc_at hist2 tpos = Some ℓ_tail). + { by eapply loc_at_prefix. } clear Hℓtpos0. + wp_pures. + iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%w & Hnrepr & Hrepr)"; first done. + iNamedSuffix "Hnrepr" "_tail". + wp_load. + iPoseProof ("Hrepr" with "[$]") as "Hrepr". + iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq". + { iExists tpos''. by iFrameNamed. } + iMod ("Hclose" with "[$]") as "AU". clear Hvs Hℓhpos Hℓtpos2 hpos vs ℓ_head ℓ_tail''. + iModIntro. + + destruct (loc_at hist2 (S tpos)) as [ℓ_next|] eqn:Htpos2. + + (* it is not the last node *) + simpl. wp_pures. wp_bind (Snd (CmpXchg _ _ _))%E. + awp_apply (try_bump_tail_spec with "[//]"). + { apply Hℓtpos0''. } + { done. } + rewrite /atomic_acc /=. + iMod "AU" as "(%vs & (%γs' & Hγs' & Hrepr) & [Hclose _])". + iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}". + iModIntro. iExists vs. iFrame "Hrepr". iSplit. + * iFrame. iIntros "Hrepr". by iApply ("Hclose" with "[$Hrepr]"). + * iIntros "%b Hrepr". + iMod ("Hclose" with "[$Hrepr //]") as "AU". + iModIntro. wp_pures. + by iApply ("IH" with "[$] [$] [$]"). + + (* it is the last (non-final) node *) + simpl. wp_pures. wp_bind (CmpXchg _ _ _)%E. + + iMod "AU" as "(%vs & (%γs' & Hγs' & %hist3 & %ℓ_head & %ℓ_tail''' & %hpos & %tpos''' & @) & Hclose)". + iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}". + iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist2◯") as %Hhist23. + destruct Hhist23 as [_ Hhist23]. rename Hℓtpos into Hℓtpos3. + + destruct (loc_at hist3 (S tpos)) as [ℓ_tail''''|] eqn:Hrace. + * (* Another item has been enqueued in the meantime, so the CAS is poised to fail. *) + iDestruct "Hclose" as "[Hclose _]". + + iDestruct (hist_repr_peek_3 with "[$Hrepr]") as "[Hℓ_tail1 Hrepr]". + { eapply prefix_lookup_Some; first apply Hℓtpos0''. by apply prefix_of_fmap. } + rewrite Hrace /=. + wp_cmpxchg_fail. + iSpecialize ("Hrepr" with "Hℓ_tail1"). + iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq". + { iExists tpos'''. by iFrameNamed. } + iMod ("Hclose" with "[$]") as "AU". iModIntro. + wp_pures. iApply ("IH" with "Hndata Hnnext AU"). + * (* This node is still the tail, so the CAS will succeed. *) + iDestruct "Hclose" as "[_ Hclose]". + + iAssert ⌜length hist3 = S tpos⌝%I as %Hhist3. + { apply loc_at_length in Hrace as Hhist3. + iPureIntro. apply loc_at_prefix with (xs':=hist3) in Hℓtpos0''; last done. + apply lookup_lt_Some in Hℓtpos0''. rewrite length_fmap in Hℓtpos0''. lia. } + + iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%w' & Hℓ_tail3 & Hrepr)". + { eapply prefix_lookup_Some; first apply Hℓtpos0''. by apply prefix_of_fmap. } + iNamedSuffix "Hℓ_tail3" "_tail3". + iPoseProof ("Hrepr" with "[$]") as "Hrepr". clear w. + + iPoseProof (hist_repr_snoc with "[$Hndata $Hnnext] [$Hrepr]") as "[Htnode Henq]". + { apply Hhist3. } + { eapply prefix_lookup_Some. apply Hℓtpos0''. by apply prefix_of_fmap. } + wp_cmpxchg_suc. iSpecialize ("Henq" with "Htnode"). + + iMod (mono_list_auth_own_update_app [(ℓ_node, data)] with "Hhist●") as "[Hhist● _]". + + iAssert (queue_repr_1 γs ℓ_q (vs ++ [data])) with "[$Hhead $Htail $Hhist● $Hhpos● $Henq]" as "Hq". + { iExists tpos'''. iPureIntro. + repeat split; try done. + - eapply loc_at_prefix; first done. + by apply prefix_app_r. + - eapply loc_at_prefix; first done. + by apply prefix_app_r. + - rewrite drop_app fmap_app -Hvs. + f_equal. + assert (Hhpos : hpos < length hist3). + { apply lookup_lt_Some in Hℓhpos. + by rewrite length_fmap in Hℓhpos. } + by assert (S hpos - length hist3 = 0) as -> by lia. } + iMod ("Hclose" with "[$]") as "HΦ". + iModIntro. wp_pures. done. + Qed. + + Lemma enqueue_spec (ℓ_q : loc) (data : val) : + ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>> + enqueue #ℓ_q data @ ∅ + <<{ queue_repr ℓ_q (vs ++ [data]) | RET #() }>>. + Proof. + iIntros "%Φ AU". wp_lam. wp_pures. + wp_apply (new_node_spec with "[//]") as "%ℓ_node Hnode". + awp_apply (set_tail_spec with "[$Hnode]"). + rewrite /atomic_acc /=. iMod "AU" as "(%vs & Hrepr & Hclose)". + iModIntro. iFrame. + Qed. + + Lemma try_dequeue_spec (ℓ_q : loc) : + ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>> + try_dequeue #ℓ_q @ ∅ + <<{ queue_repr ℓ_q (tail vs) | RET (val_opt_hl (head vs)) }>>. + Proof. + iIntros "%Φ AU". iLöb as "IH". wp_rec. + + wp_bind (! _)%E. + iMod "AU" as "(%vs0 & (%γs & #Hγs & %hist0 & %ℓ_head0 & %ℓ_tail0 & %hpos0 & %tpos0 & @) & [Hclose _])". + iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist0◯". + iDestruct (mono_nat_lb_own_get with "Hhpos●") as "#Hhpos0◯". + rename Hℓhpos into Hℓhpos0. + wp_load. + iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU". + { iExists tpos0. by iFrameNamed. } + iModIntro. clear vs0 Hvs tpos0 Hℓtpos ℓ_tail0. + + wp_pures. wp_bind (! _)%E. + iMod "AU" as "(%vs1 & (%γs' & Hγs' & %hist1 & %ℓ_head1 & %ℓ_tail1 & %hpos1 & %tpos1 & @) & Hclose)". + iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}". + iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist1◯". + iDestruct (mono_nat_auth_lb_own_valid with "Hhpos● Hhpos0◯") as %Hhpos01. + iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist0◯") as %Hhist01. + destruct Hhpos01 as [_ Hhpos01]. destruct Hhist01 as [_ Hhist01]. + assert (Hℓhpos0' : loc_at hist1 hpos0 = Some ℓ_head0). + { by eapply loc_at_prefix. } clear Hℓhpos0. + iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%u & @ & Hrepr)"; first done. + wp_load. + iSpecialize ("Hrepr" with "[$]"). + + destruct (loc_at hist1 (S hpos0)) as [ℓ_headS0|] eqn:Hℓ_headS0. + - simpl. iDestruct "Hclose" as "[Hclose _]". + iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU". + { iExists tpos1. by iFrameNamed. } + iModIntro. clear u vs1 Hvs tpos1 Hℓtpos ℓ_tail1. + + wp_pures. wp_bind (! _)%E. + iMod "AU" as "(%vs2 & (%γs' & Hγs' & %hist2 & %ℓ_head2 & %ℓ_tail2 & %hpos2 & %tpos2 & @) & Hclose)". + iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}". + iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist2◯". + iDestruct (mono_nat_auth_lb_own_valid with "Hhpos● Hhpos0◯") as %Hhpos02. + iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist1◯") as %Hhist12. + destruct Hhpos02 as [_ Hhpos02]. destruct Hhist12 as [_ Hhist12]. + assert (Hℓ_headS0' : loc_at hist2 (S hpos0) = Some ℓ_headS0). + { by eapply loc_at_prefix. } clear Hℓ_headS0. + apply loc_at_val_at_Some in Hℓ_headS0' as Hval_headS0'. + destruct Hval_headS0' as [w Hval_headS0']. + iDestruct (hist_repr_peek_1 with "[$Hrepr]") as "(@ & Hrepr)"; try done. + iDestruct "Hndata" as "#Hndata_head". + wp_load. + + iDestruct "Hclose" as "[Hclose _]". + + iSpecialize ("Hrepr" with "[$]"). + iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU". + { iExists tpos2. by iFrameNamed. } + iModIntro. + clear vs2 Hvs tpos2 Hℓtpos ℓ_tail2. + + wp_pures. + + wp_bind (CmpXchg _ _ _)%E. + iMod "AU" as "(%vs3 & (%γs' & Hγs' & %hist3 & %ℓ_head3 & %ℓ_tail3 & %hpos3 & %tpos3 & @) & Hclose)". + iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}". + iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist2◯") as %Hhist23. + destruct Hhist23 as [_ Hhist23]. + assert (Hhist13 : hist1 `prefix_of` hist3). + { by trans hist2. } + + destruct (decide (ℓ_head0 = ℓ_head3)) as [->|Hhead03]. + + iDestruct "Hclose" as "[_ Hclose]". + + wp_cmpxchg_suc. + + assert (Hℓhpos0'' : loc_at hist3 hpos0 = Some ℓ_head3). + { by eapply loc_at_prefix. } clear Hℓhpos0'. + iAssert ⌜hpos0 = hpos3⌝%I as %->. + { by iApply (loc_at_inj with "Hrepr"). } + + simplify_eq/=. + + iMod (mono_nat_own_update (S hpos3) with "Hhpos●") as "[Hhpos● _]". { lia. } + iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ". + { iExists tpos3. iFrameNamed. + iPureIntro. repeat split; try done. + - by eapply loc_at_prefix. + - by rewrite -[S (S _)]Nat.add_1_r -drop_drop [(drop 1 _).*2]fmap_drop. } + + iModIntro. wp_pures. + + assert (Hval_headS0'' : val_at hist3 (S hpos3) = Some w). + { by eapply val_at_prefix. } clear Hval_headS0'. + unfold val_at in Hval_headS0''. + rewrite -[S hpos3]Nat.add_0_r -lookup_drop -fmap_drop /= -head_lookup in Hval_headS0''. + by rewrite Hval_headS0'' /=. + + + iDestruct "Hclose" as "[Hclose _]". + + wp_cmpxchg_fail. + + iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU". + { iExists tpos3. by iFrameNamed. } + + iModIntro. wp_pures. iApply ("IH" with "AU"). + - apply loc_at_length in Hℓ_headS0 as Hhistlen. + rewrite drop_ge /= in Hvs; last lia. destruct vs1; try done. + simplify_eq/=. + + iDestruct "Hclose" as "[_ Hclose]". + iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ". + { iExists tpos1. iFrameNamed. iPureIntro. + rewrite drop_ge //=. lia. } + + iModIntro. wp_pures. iApply "HΦ". + Qed. + +End basic_queue. + +Definition basic_queue `{!heapGS Σ, !basic_queueG Σ} : basic_queue_spec.basic_queue Σ. +Proof. + refine {| basic_queue_spec.new_spec := new_spec; + basic_queue_spec.enqueue_spec := enqueue_spec; + basic_queue_spec.try_dequeue_spec := try_dequeue_spec |}. +Defined. + +#[global] Typeclasses Opaque queue_repr. diff --git a/theories/basic_queue_spec.v b/theories/basic_queue_spec.v new file mode 100644 index 0000000..d7a38e1 --- /dev/null +++ b/theories/basic_queue_spec.v @@ -0,0 +1,30 @@ +From iris.program_logic Require Import atomic. +From iris.heap_lang Require Import notation proofmode. + +From lmpmc Require Import util. + +Record basic_queue {Σ} `{!heapGS Σ} := + BasicQueue + { new : val; + enqueue : val; + try_dequeue : val; + + queue_repr : loc → list val → iProp Σ; + #[global] queue_repr_timeless ℓ vs :: Timeless (queue_repr ℓ vs); + + new_spec : + {{{ True }}} + new #() + {{{ (ℓ_q : loc), RET #ℓ_q; queue_repr ℓ_q [] }}}; + + enqueue_spec (ℓ_q : loc) (data : val) : + ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>> + enqueue #ℓ_q data @ ∅ + <<{ queue_repr ℓ_q (vs ++ [data]) | RET #() }>>; + + try_dequeue_spec (ℓ_q : loc) : + ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>> + try_dequeue #ℓ_q @ ∅ + <<{ queue_repr ℓ_q (tail vs) | RET (val_opt_hl (head vs)) }>>; + }. +#[global] Arguments basic_queue _ {_} : assert. diff --git a/theories/example.v b/theories/example.v new file mode 100644 index 0000000..7857118 --- /dev/null +++ b/theories/example.v @@ -0,0 +1,723 @@ +From iris.program_logic Require Import atomic. +From iris.heap_lang Require Import notation proofmode adequacy. +From iris.algebra Require Import list gmultiset. +From iris.algebra.lib Require Import excl_auth. +From iris.base_logic.lib Require Import invariants mono_list. +From iris_named_props Require Import custom_syntax. +From iris.heap_lang.lib Require Import assert par. + +From lmpmc Require lmpmc_queue_spec lmpmc_queue_proof fin_queue_proof lmpmc_blocking_dequeue. +From lmpmc Require Import upstream. + +Definition somes {A} (xs : list (option A)) : list A := xs ≫= option_list. +Definition option_le {A} (mx my : option A) := option_relation (=) (const False) (const True) mx my. +Definition option_nat (x : nat) : option nat := guard (x ≠ 0);; Some x. +Definition vals_of_nats : list nat → list val := fmap (LitV ∘ LitInt ∘ Z.of_nat). + +Lemma option_le_None {A} (x : A) : option_le None (Some x). +Proof. done. Qed. +Lemma option_le_Some {A} (x : A) : option_le (Some x) (Some x). +Proof. done. Qed. +Lemma option_le_inv {A} (mx my : option A) : option_le mx my → mx = None ∨ mx = my. +Proof. induction mx, my; intros ?; simplify_eq/=; done || (by right) || by left. Qed. + +#[global] Instance timeless_if_bool {PROP : bi} {b : bool} {Q R : PROP} : Timeless Q → Timeless R → Timeless (if b then Q else R). +Proof. by destruct b. Qed. + +Section hl. + Context (lq : lmpmc_queue_spec.lmpmc_queue_hl). + Import lmpmc_blocking_dequeue lmpmc_queue_spec. + + Notation "'let2:' x1 , x2 := e1 'in' e2" := + (Lam (BNamed x2) (Lam (BNamed x1) (Lam (BNamed x2) e2 (Snd (Var x2))) (Fst (Var x2))) e1)%E + (at level 200, x1, x2 at level 1, e1, e2 at level 200, + format "'[' 'let2:' x1 ',' x2 := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope. + + Definition simple_example_2_1 : expr := + let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in + let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in + lq.(enqueue) "ℓ_enq1" #10;; + lq.(link) "ℓ_enq1" "ℓ_deq2";; + lq.(enqueue) "ℓ_enq2" #20;; + let: "x" := dequeue lq "ℓ_deq1" in + let: "y" := dequeue lq "ℓ_deq1" in + ("x", "y"). + + Definition simple_example_2_2 : expr := + let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in + let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in + (( lq.(enqueue) "ℓ_enq1" #10;; + lq.(link) "ℓ_enq1" "ℓ_deq2") (* thread A *) + ||| lq.(enqueue) "ℓ_enq2" #20 (* thread B *) + );; + let: "x" := dequeue lq "ℓ_deq1" in + let: "y" := dequeue lq "ℓ_deq1" in + ("x", "y"). + + Definition mt_example_1 : expr := + let: "ℓ_sum" := Alloc #0 in + let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in + let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in + (( lq.(enqueue) "ℓ_enq1" #1;; + lq.(link) "ℓ_enq1" "ℓ_deq2") (* thread A *) + ||| lq.(enqueue) "ℓ_enq2" #2 (* thread B *) + ||| lq.(enqueue) "ℓ_enq2" #3 (* thread C *) + ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1") (* thread D *) + ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1") (* thread E *) + ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1") (* thread F *) + );; + ! "ℓ_sum". + +End hl. + +Section proofs. + Context `{!heapGS Σ, !spawnG Σ, + !mono_listG natO Σ, + !inG Σ (excl_authR (gmultisetO nat)), + !inG Σ (excl_authR natO), + !inG Σ (excl_authR boolO), + !inG Σ (excl_authR (listO natO)), + !inG Σ (excl_authR (optionO natO)), + !inG Σ (exclR (listO natO))}. + Context {lq : lmpmc_queue_spec.lmpmc_queue_hl} + {lqp : lmpmc_queue_spec.lmpmc_queue_iris Σ lq}. + Import lmpmc_blocking_dequeue lmpmc_queue_spec. + + Lemma simple_example_2_1_safe : + ⊢ WP simple_example_2_1 lq {{ v, ⌜v = (#10, #20)%V⌝ }}. + Proof. + iUnfold simple_example_2_1. + wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures. + wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures. + awp_apply lqp.(enqueue_spec lq). iAaccIntro with "Hq1"; iIntros "Hq1"; first by iFrame. + simpl. iModIntro. wp_pures. + awp_apply lqp.(link_spec lq). + rewrite /atomic_acc /=. + iExists true. iFrame. + iApply fupd_mask_intro; first done. + iIntros "Hupd". iSplit. { iIntros "[? ?]". iFrame. } + iIntros "Hq". simpl. iMod "Hupd" as "_". iModIntro. + wp_pures. awp_apply lqp.(enqueue_spec lq). + iAaccIntro with "Hq"; iIntros "Hq"; first by iFrame. + simpl. + + iModIntro. wp_pures. awp_apply (dequeue_spec lq lqp). + iAaccIntro with "Hq"; first by iIntros "Hq"; iFrame. + iIntros (? ?) "[%Hvs Hq]". iSimplifyEq. + iModIntro. wp_pures. awp_apply (dequeue_spec lq lqp). + iAaccIntro with "Hq"; first by iIntros "Hq"; iFrame. + iIntros (? ?) "[%Hvs Hq]". iSimplifyEq. + + iModIntro. by wp_pures. + Qed. + + Record smp_gstate := + SmpGstate + { γ1_linked : gname; (* (●E) whether Q1 and Q2 have been linked already *) + γ1_contA : gname; (* (●E) (list nat) contribution of thread A *) + γ1_contB : gname; (* (●E) (list nat) contribution of thread B *) + }. + + Definition smp_inv γs (ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2 : loc) : iProp Σ := + ∃ (linked : bool) (contA contB : list nat), + ("Hlinked●" ∷ own γs.(γ1_linked) (●E linked)) ∗ + ("HcontA●" ∷ own γs.(γ1_contA) (●E contA)) ∗ + ("HcontB●" ∷ own γs.(γ1_contB) (●E contB)) ∗ + ("Hq1" ∷ lqp.(queue_repr lq) ℓ_deq1 (if linked then ℓ_enq2 else ℓ_enq1) (vals_of_nats (if linked then contA ++ contB else contA))) ∗ + ("Hq2" ∷ if linked then True else lqp.(queue_repr lq) ℓ_deq2 ℓ_enq2 (vals_of_nats contB)). + + Lemma simple_example_2_2_safe : + ⊢ WP simple_example_2_2 lq {{ v, ⌜v = (#10, #20)%V⌝ }}. + Proof. + iUnfold simple_example_2_2. + wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures. + wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures. + + iMod (own_alloc (●E false ⋅ ◯E false)) as (γ1_linked') "[Hlinked● Hlinked◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E [] ⋅ ◯E [])) as (γ1_contA') "[HcontA● HcontA◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E [] ⋅ ◯E [])) as (γ1_contB') "[HcontB● HcontB◯]"; first apply excl_auth_valid. + + pose γs := SmpGstate γ1_linked' γ1_contA' γ1_contB'. + replace γ1_linked' with γs.(γ1_linked) by done. + replace γ1_contA' with γs.(γ1_contA) by done. + replace γ1_contB' with γs.(γ1_contB) by done. + clearbody γs. clear γ1_linked' γ1_contA' γ1_contB'. + iAssert (smp_inv γs ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "[$]" as "Hinv". + iMod (inv_alloc nroot _ (smp_inv γs ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "Hinv") as "#Hinv". + + wp_smart_apply (wp_par (λ _, own γs.(γ1_linked) (◯E true) ∗ own γs.(γ1_contA) (◯E [10]))%I + (λ _, own γs.(γ1_contB) (◯E [20])) + with "[Hlinked◯ HcontA◯] [HcontB◯]"). + { awp_apply lqp.(enqueue_spec lq). + iInv "Hinv" as (linked contA contB) ">H". + iNamedSuffix "H" "_1". + iCombine "Hlinked◯ Hlinked●_1" gives %->%excl_auth_agree_L. + iCombine "HcontA◯ HcontA●_1" gives %->%excl_auth_agree_L. + iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. } + iIntros "Hq1_1". + iCombine "HcontA●_1 HcontA◯" as "HcontA". + iMod (own_update with "HcontA") as "[HcontA●_1 HcontA◯]". + { apply (excl_auth_update _ _ [10]). } + iIntros "!>". + iSimplifyEq. replace ([ #10 ] : list val) with (vals_of_nats [10]) by done. + iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1 Hq2_1". wp_pures. clear contB. + + awp_apply lqp.(link_spec lq). + iInv "Hinv" as (linked contA contB) ">H". + iNamedSuffix "H" "_2". + iCombine "Hlinked◯ Hlinked●_2" gives %->%excl_auth_agree_L. + iCombine "HcontA◯ HcontA●_2" gives %->%excl_auth_agree_L. + rewrite /atomic_acc /=. iApply fupd_mask_intro; first set_solver. iIntros "Hclose". + iExists true. iFrame "Hq1_2 Hq2_2". iSplit. + { iIntros "[Hq1 Hq2]". iMod "Hclose" as "_". iModIntro. do 2 iFrame. } + iIntros "Hq1". iMod "Hclose" as "_". + iCombine "Hlinked●_2 Hlinked◯" as "Hlinked". + iMod (own_update with "Hlinked") as "[Hlinked●_2 Hlinked◯]". + { apply (excl_auth_update _ _ true). } + iFrame "Hlinked●_2 HcontA●_2 HcontB●_2 Hq1". by iFrame. } + { awp_apply lqp.(enqueue_spec lq). + iInv "Hinv" as (linked contA contB) ">H". + iNamedSuffix "H" "_1". + iCombine "HcontB◯ HcontB●_1" gives %->%excl_auth_agree_L. + destruct linked eqn:Hlinked. + { iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. } + iIntros "Hq1_1". + iCombine "HcontB◯ HcontB●_1" as "HcontB". + iMod (own_update with "HcontB") as "[HcontB●_1 HcontB◯]". + { apply (excl_auth_update _ _ [20]). } + iIntros "!>". + iSimplifyEq. + replace [ #20 ] with (vals_of_nats [20]) by done. + iEval (rewrite app_nil_r /vals_of_nats -fmap_app -/vals_of_nats) in "Hq1_1". + by iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1". } + { iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". by iFrame. } + iIntros "Hq2_1". + iCombine "HcontB◯ HcontB●_1" as "HcontB". + iMod (own_update with "HcontB") as "[HcontB●_1 HcontB◯]". + { apply (excl_auth_update _ _ [20]). } + iIntros "!>". + iSimplifyEq. + replace [ #20 ] with (vals_of_nats [20]) by done. + by iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1 Hq2_1". } } + { iIntros (v1 v2) "[[Hlinked◯ HcontA◯] HcontB◯]". + iModIntro. wp_pures. clear v1 v2. + awp_apply (dequeue_spec lq lqp). + iInv "Hinv" as (linked contA contB) ">H". + iNamedSuffix "H" "_1". + iCombine "Hlinked◯ Hlinked●_1" gives %->%excl_auth_agree_L. + iCombine "HcontA◯ HcontA●_1" gives %->%excl_auth_agree_L. + iCombine "HcontB◯ HcontB●_1" gives %->%excl_auth_agree_L. + iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. } + iIntros (v0 vs) "[%Hvs Hq1]". + simpl in Hvs. injection Hvs as <- <-. + replace [ #20%nat ] with (vals_of_nats [20]) by done. + iCombine "HcontA●_1 HcontA◯" as "HcontA". + iMod (own_update with "HcontA") as "[HcontA●_1 HcontA◯]". + { apply (excl_auth_update _ _ []). } + iIntros "!>". + iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1". wp_pures. + + awp_apply (dequeue_spec lq lqp). + iInv "Hinv" as (linked contA contB) ">H". + iNamedSuffix "H" "_2". + iCombine "Hlinked◯ Hlinked●_2" gives %->%excl_auth_agree_L. + iCombine "HcontA◯ HcontA●_2" gives %->%excl_auth_agree_L. + iCombine "HcontB◯ HcontB●_2" gives %->%excl_auth_agree_L. + iAaccIntro with "Hq1_2". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. } + iIntros (v0 vs) "[%Hvs Hq1]". + simpl in Hvs. injection Hvs as <- <-. + replace [ #20%nat ] with (vals_of_nats [20]) by done. + iCombine "HcontB●_2 HcontB◯" as "HcontB". + iMod (own_update with "HcontB") as "[HcontB●_2 HcontB◯]". + { apply (excl_auth_update _ _ []). } + iIntros "!>". + iFrame "Hlinked●_2 HcontB●_2 HcontA●_2 Hq1". wp_pures. + done. } + Qed. + + Record mt_gstate := + Gstate + { γ2_hist1 : gname; (* (●ML) (list nat) succesfully enqueued items (Q1) *) + γ2_hist2 : gname; (* (●E ) (list nat) sucessfully enqueued items (Q2) *) + γ2_linked : gname; (* (●E ) (bool) whether Q1 and Q2 have been linked *) + γ2_venqA : gname; (* (●E ) (gmultiset nat) of items enqueued by thread A *) + γ2_venqB : gname; (* (●E ) (gmultiset nat) of items enqueued by thread B *) + γ2_venqC : gname; (* (●E ) (gmultiset nat) of items enqueued by thread C *) + γ2_vdeqD : gname; (* (●E ) (option nat) poised contribution of first dequeueing thread *) + γ2_vdeqE : gname; (* (●E ) (option nat) poised contribution of second dequeueing thread *) + γ2_vdeqF : gname; (* (●E ) (option nat) poised contribution of third dequeueing thread *) + γ2_contD : gname; (* (●E ) (nat) as-is contribution of first dequeueing thread *) + γ2_contE : gname; (* (●E ) (nat) as-is contribution of second dequeueing thread *) + γ2_contF : gname; (* (●E ) (nat) as-is contribution of third dequeueing thread *) + }. + + Definition mt_inv γs ℓ_sum (ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2 : loc) : iProp Σ := + ∃ (hist1 hist2 : list nat) (ndeq : nat) (linked : bool) (ecsA ecsB ecsC : gmultiset nat) (npD npE npF : option nat) (nD nE nF : nat) (vs1 : list nat), + ("Hq1" ∷ lqp.(queue_repr lq) ℓ_deq1 (if linked then ℓ_enq2 else ℓ_enq1) (vals_of_nats vs1)) ∗ + ("Hq2" ∷ if linked then True else lqp.(queue_repr lq) ℓ_deq2 ℓ_enq2 (vals_of_nats hist2)) ∗ + ("Hhist1●" ∷ γs.(γ2_hist1) ↪●ML hist1) ∗ + ("Hhist2E" ∷ own γs.(γ2_hist2) (Excl hist2)) ∗ + ("Hlinked●" ∷ own γs.(γ2_linked) (●E linked)) ∗ + ("HvenqA●" ∷ own γs.(γ2_venqA) (●E ecsA)) ∗ + ("HvenqB●" ∷ own γs.(γ2_venqB) (●E ecsB)) ∗ + ("HvenqC●" ∷ own γs.(γ2_venqC) (●E ecsC)) ∗ + ("HvdeqD●" ∷ own γs.(γ2_vdeqD) (●E npD)) ∗ + ("HvdeqE●" ∷ own γs.(γ2_vdeqE) (●E npE)) ∗ + ("HvdeqF●" ∷ own γs.(γ2_vdeqF) (●E npF)) ∗ + ("HcontD●" ∷ own γs.(γ2_contD) (●E nD)) ∗ + ("HcontE●" ∷ own γs.(γ2_contE) (●E nE)) ∗ + ("HcontF●" ∷ own γs.(γ2_contF) (●E nF)) ∗ + ("Hsum" ∷ ℓ_sum ↦ #(nD + nE + nF)) ∗ + ("%Hhist1" ∷ ⌜list_to_set_disj hist1 ⊆ if linked then ecsA ⊎ ecsB ⊎ ecsC else ecsA⌝) ∗ + ("%Hhist2" ∷ ⌜list_to_set_disj hist2 ⊆ ecsB ⊎ ecsC⌝) ∗ + ("%Hhist1n0" ∷ ⌜Forall (.≠ 0) hist1⌝) ∗ + ("%Hhist2n0" ∷ ⌜Forall (.≠ 0) hist2⌝) ∗ + ("%HnDEF" ∷ ⌜somes [npD; npE; npF] ⊆+ take ndeq hist1⌝) ∗ + ("%HD" ∷ ⌜option_le (option_nat nD) npD⌝) ∗ + ("%HE" ∷ ⌜option_le (option_nat nE) npE⌝) ∗ + ("%HF" ∷ ⌜option_le (option_nat nF) npF⌝) ∗ + ("%Hndeq" ∷ ⌜ndeq ≤ length hist1⌝) ∗ + ("%Hhistvs" ∷ ⌜drop ndeq hist1 = vs1⌝). + + (* Post, we expect: + linked = true + nD, nE, nF ≠ 0 (hence npD, npE, npF ≠ None and all are unique, adding up to 6) *) + + Lemma mt_example_1_safe : + ⊢ WP mt_example_1 lq {{ v, ⌜v = #6⌝ }}. + Proof. + iUnfold mt_example_1. + wp_alloc ℓ_sum as "Hsum". wp_pures. + wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures. + wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures. + iEval (replace [] with (vals_of_nats [])) in "Hq1 Hq2". + iMod (mono_list_own_alloc []) as "[%γ2_hist1 [Hhist1● _]]". + iMod (own_alloc (Excl [])) as "[%γ2_hist2 Hhist2E]"; first done. + iMod (own_alloc (●E false ⋅ ◯E false)) as (γ2_linked') "[Hlinked● Hlinked◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqA') "[HvenqA● HvenqA◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqB') "[HvenqB● HvenqB◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqC') "[HvenqC● HvenqC◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqD' [HvdeqD● HvdeqD◯]]"; first apply excl_auth_valid. + iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqE' [HvdeqE● HvdeqE◯]]"; first apply excl_auth_valid. + iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqF' [HvdeqF● HvdeqF◯]]"; first apply excl_auth_valid. + iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contD') "[HcontD● HcontD◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contE') "[HcontE● HcontE◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contF') "[HcontF● HcontF◯]"; first apply excl_auth_valid. + pose γs := Gstate γ2_hist1 γ2_hist2 γ2_linked' γ2_venqA' γ2_venqB' γ2_venqC' γ2_vdeqD' γ2_vdeqE' γ2_vdeqF' γ2_contD' γ2_contE' γ2_contF'. + replace γ2_linked' with γs.(γ2_linked) by done. + replace γ2_venqA' with γs.(γ2_venqA) by done. + replace γ2_venqB' with γs.(γ2_venqB) by done. + replace γ2_venqC' with γs.(γ2_venqC) by done. + replace γ2_vdeqD' with γs.(γ2_vdeqD) by done. + replace γ2_vdeqE' with γs.(γ2_vdeqE) by done. + replace γ2_vdeqF' with γs.(γ2_vdeqF) by done. + replace γ2_contD' with γs.(γ2_contD) by done. + replace γ2_contE' with γs.(γ2_contE) by done. + replace γ2_contF' with γs.(γ2_contF) by done. + iAssert (mt_inv γs ℓ_sum ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) + with "[$Hhist1● $Hhist2E $Hlinked● $HvenqA● $HvenqB● $HvenqC● $HvdeqD● $HvdeqE● $HvdeqF● $HcontD● $HcontE● $HcontF● $Hq1 $Hq2 $Hsum]" + as "Hinv". + { iPureIntro. exists 0. split; try done. } + clearbody γs. + clear γ2_hist1 γ2_hist2 γ2_linked' γ2_venqA' γ2_venqB' γ2_venqC' γ2_vdeqD' γ2_vdeqE' γ2_vdeqF' γ2_contD' γ2_contE' γ2_contF'. + iMod (inv_alloc nroot _ (mt_inv γs ℓ_sum ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "Hinv") as "#Hinv". + + pose (P1 := (own (γ2_venqA γs) (◯E {[+ 1 +]}) ∗ own (γ2_linked γs) (◯E true))%I). + pose (P2 := own (γ2_venqB γs) (◯E {[+ 2 +]})). + pose (P3 := own (γ2_venqC γs) (◯E {[+ 3 +]})). + pose (P4 := (∃ nD : nat, own γs.(γ2_contD) (◯E nD) ∗ ⌜nD ≠ 0⌝)%I). + pose (P5 := (∃ nE : nat, own γs.(γ2_contE) (◯E nE) ∗ ⌜nE ≠ 0⌝)%I). + pose (P6 := (∃ nF : nat, own γs.(γ2_contF) (◯E nF) ∗ ⌜nF ≠ 0⌝)%I). + + wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3 ∗ P4 ∗ P5)%I (λ _, P6)%I with "[- HcontF◯ HvdeqF◯] [HcontF◯ HvdeqF◯]"). + { wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3 ∗ P4)%I (λ _, P5)%I with "[- HcontE◯ HvdeqE◯] [HcontE◯ HvdeqE◯]"). + { wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3)%I (λ _, P4)%I with "[- HcontD◯ HvdeqD◯] [HcontD◯ HvdeqD◯]"). + { wp_smart_apply (wp_par (λ _, P1 ∗ P2)%I (λ _, P3)%I with "[- HvenqC◯] [HvenqC◯]"). + { wp_smart_apply (wp_par (λ _, P1) (λ _, P2) with "[- HvenqB◯] [HvenqB◯]"). + { awp_apply lqp.(enqueue_spec lq). + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H". + iNamedSuffix "H" "_1". iCombine "HvenqA◯ HvenqA●_1" gives %->%excl_auth_agree_L. + iCombine "Hlinked●_1 Hlinked◯" gives %->%excl_auth_agree_L. + iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. } + iIntros "Hq1". + + iMod (mono_list_auth_own_update (hist1 ++ [1]) with "Hhist1●_1") as "[Hhist1●_1 _]". + { by apply prefix_app_r. } + iCombine "HvenqA●_1 HvenqA◯" as "HvenqA". + iMod (own_update with "HvenqA") as "[HvenqA●_1 HvenqA◯]". + { apply (excl_auth_update _ _ {[+ 1 +]}). } + replace (vals_of_nats vs1 ++ [ #1 ]) with (vals_of_nats (vs1 ++ [1])) + by rewrite /vals_of_nats fmap_app //. + iModIntro. iFrame "HvenqA◯". iFrame. iFrame "Hq1". iSplit. + { iPureIntro. exists ndeq. repeat split; try done. + + rewrite list_to_set_disj_app. + multiset_solver. + + apply Forall_app. by split; last apply Forall_singleton. + + etrans; first apply HnDEF_1. + apply prefix_submseteq, take_app_prefix. + + rewrite ->!length_app in *. lia. + + by rewrite drop_app_le // Hhistvs_1. } + wp_pures. + clear. + + awp_apply lqp.(link_spec lq). + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H". + iNamedSuffix "H" "_2". + iCombine "Hlinked●_2 Hlinked◯" gives %->%excl_auth_agree_L. + rewrite /atomic_acc /=. iApply fupd_mask_intro; first set_solver. iIntros "Hclose". + iExists true. iFrame "Hq1_2 Hq2_2". iSplit. + { iIntros "[Hq1 Hq2]". iMod "Hclose" as "_". iModIntro. + iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. } + iIntros "Hq1". iMod "Hclose" as "_". + + iCombine "Hlinked●_2 Hlinked◯" as "Hlinked". + iMod (own_update with "Hlinked") as "[Hlinked●_2 Hlinked◯]". + { apply (excl_auth_update _ _ true). } + iEval (rewrite /vals_of_nats -fmap_app -/vals_of_nats) in "Hq1". + iMod (mono_list_auth_own_update (hist1 ++ hist2) with "Hhist1●_2") as "[Hhist1●_2 _]"; first by apply prefix_app_r. + iFrame. iModIntro. iModIntro. iPureIntro. exists ndeq. repeat split; try done. + - rewrite list_to_set_disj_app. multiset_solver. + - by rewrite Forall_app. + - etrans; first apply HnDEF_2. + apply prefix_submseteq, take_app_prefix. + - rewrite length_app. lia. + - by rewrite drop_app_le // Hhistvs_2. + } + { awp_apply lqp.(enqueue_spec lq). + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H". + iNamedSuffix "H" "_1". iCombine "HvenqB◯ HvenqB●_1" gives %->%excl_auth_agree_L. + + destruct linked eqn:Hlinked. + - iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. } + iIntros "Hq1". + iCombine "HvenqB●_1 HvenqB◯" as "HvenqB". + iMod (mono_list_auth_own_update (hist1 ++ [2]) with "Hhist1●_1") as "[Hhist1●_1 _]". + { by apply prefix_app_r. } + iMod (own_update with "HvenqB") as "[HvenqB●_1 HvenqB◯]". + { apply (excl_auth_update _ _ {[+ 2 +]}). } + replace (vals_of_nats vs1 ++ [ #2 ]) with (vals_of_nats (vs1 ++ [2])) + by rewrite /vals_of_nats fmap_app //. + iModIntro. iFrame "HvenqB◯". iModIntro. iFrame. iExists ndeq, (vs1 ++ [2]). iFrame. + iPureIntro. repeat split; try done. + + rewrite list_to_set_disj_app. + multiset_solver + + apply Forall_app. + + multiset_solver. + + apply Forall_app. by split; last apply Forall_singleton. + + etrans; first apply HnDEF_1. + apply prefix_submseteq, take_app_prefix. + + rewrite length_app. lia. + + by rewrite drop_app_le // Hhistvs_1. + - iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". iExists ndeq. by iFrame. } + iIntros "Hq1". + iCombine "HvenqB●_1 HvenqB◯" as "HvenqB". + iMod (own_update _ _ (Excl (hist2 ++ [2])) with "Hhist2E_1") as "Hhist2E_1"; first by intros ? [[]|]. + iMod (own_update with "HvenqB") as "[HvenqB●_1 HvenqB◯]". + { apply (excl_auth_update _ _ {[+ 2 +]}). } + replace (vals_of_nats hist2 ++ [ #2 ]) with (vals_of_nats (hist2 ++ [2])) + by rewrite /vals_of_nats fmap_app //. + iModIntro. iFrame "HvenqB◯". iModIntro. iFrame. iFrame. + iPureIntro. exists ndeq. repeat split; try done. + + rewrite list_to_set_disj_app. + multiset_solver. + + apply Forall_app. split; first done. + by apply Forall_singleton. + } + { by iIntros (_ _) "H !>". } + } + { awp_apply lqp.(enqueue_spec lq). + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H". + iNamedSuffix "H" "_1". iCombine "HvenqC◯ HvenqC●_1" gives %->%excl_auth_agree_L. + + destruct linked eqn:Hlinked. + - iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. } + iIntros "Hq1". + iCombine "HvenqC●_1 HvenqC◯" as "HvenqC". + iMod (mono_list_auth_own_update (hist1 ++ [3]) with "Hhist1●_1") as "[Hhist1●_1 _]". + { by apply prefix_app_r. } + iMod (own_update with "HvenqC") as "[HvenqC●_1 HvenqC◯]". + { apply (excl_auth_update _ _ {[+ 3 +]}). } + replace (vals_of_nats vs1 ++ [ #3 ]) with (vals_of_nats (vs1 ++ [3])) + by rewrite /vals_of_nats fmap_app //. + iModIntro. iFrame "HvenqC◯". iModIntro. iFrame. iExists ndeq, (vs1 ++ [3]). iFrame. + iPureIntro. repeat split; try done. + + rewrite list_to_set_disj_app. + multiset_solver. + + multiset_solver. + + apply Forall_app. by split; last apply Forall_singleton. + + etrans; first apply HnDEF_1. + apply prefix_submseteq, take_app_prefix. + + rewrite length_app. lia. + + by rewrite drop_app_le // Hhistvs_1. + - iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". iExists ndeq. by iFrame. } + iIntros "Hq1". + iCombine "HvenqC●_1 HvenqC◯" as "HvenqC". + iMod (own_update _ _ (Excl (hist2 ++ [3])) with "Hhist2E_1") as "Hhist2E_1"; first by intros ? [[]|]. + iMod (own_update with "HvenqC") as "[HvenqC●_1 HvenqC◯]". + { apply (excl_auth_update _ _ {[+ 3 +]}). } + replace (vals_of_nats hist2 ++ [ #3 ]) with (vals_of_nats (hist2 ++ [3])) + by rewrite /vals_of_nats fmap_app //. + iModIntro. iFrame "HvenqC◯". iModIntro. iFrame. iFrame. + iPureIntro. exists ndeq. repeat split; try done. + + rewrite list_to_set_disj_app. + multiset_solver. + + apply Forall_app. split; first done. + by apply Forall_singleton. + } + { iIntros (_ _) "[H1 H2] !>". iFrame. } + } + { awp_apply (dequeue_spec lq lqp). + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H". + iNamedSuffix "H" "_1". + iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. } + iIntros (v0 vs') "[%Hvs Hq1]". + destruct vs1; simplify_eq/=. + iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1". + iCombine "HcontD◯ HcontD●_1" gives %->%excl_auth_agree_L. + + iCombine "HvdeqD●_1 HvdeqD◯" as "HvdeqD" gives %->%excl_auth_agree_L. + iMod (own_update with "HvdeqD") as "[HvdeqD●_1 HvdeqD◯]". + { apply (excl_auth_update _ _ (Some n)). } + + apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1]. + iModIntro. iFrame. iFrameNamed. iSplit. + { iPureIntro. exists (S ndeq). repeat split; try done. + - etrans; first done. + simplify_eq/=. rewrite ->app_nil_r in *. + etrans. { apply Permutation_submseteq, Permutation_cons_append. } + rewrite (take_S_r _ _ n) //. + by apply submseteq_skips_r. + - by apply lookup_lt_Some in Hhistndeq_1. } + + clear - Hhistndeq_1 Hhistvs_1. + iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H". + iNamedSuffix "H" "_2". + wp_faa. + + iCombine "HcontD●_2 HcontD◯" as "HcontD" gives %->%excl_auth_agree_L. + iMod (own_update with "HcontD") as "[HcontD●_2 HcontD◯]". + { apply (excl_auth_update _ _ n). } + + iEval (rewrite Z.add_0_l Z.add_comm Z.add_assoc) in "Hsum_2". + + iCombine "HvdeqD●_2 HvdeqD◯" gives %->%excl_auth_agree_L. + + iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre]. + assert (Hn : n ≠ 0). + { eapply (Forall_lookup (.≠ 0)); last done. + by eapply Forall_prefix. } + + iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro. + iPureIntro. exists ndeq'. repeat split; try done. + by rewrite /option_nat option_guard_True. + } + { iIntros (_ _) "[H1 H2] !>". iFrame. } + } + { awp_apply (dequeue_spec lq lqp). + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H". + iNamedSuffix "H" "_1". + iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. } + iIntros (v0 vs') "[%Hvs Hq1]". + destruct vs1; simplify_eq/=. + iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1". + iCombine "HcontE◯ HcontE●_1" gives %->%excl_auth_agree_L. + + iCombine "HvdeqE●_1 HvdeqE◯" as "HvdeqE" gives %->%excl_auth_agree_L. + iMod (own_update with "HvdeqE") as "[HvdeqE●_1 HvdeqE◯]". + { apply (excl_auth_update _ _ (Some n)). } + + apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1]. + iModIntro. iFrame. iFrameNamed. iSplit. + { iPureIntro. exists (S ndeq). repeat split; try done. etrans; first done. + - simplify_eq/=. rewrite app_nil_r in HnDEF_1. + rewrite app_nil_r. + etrans. { apply submseteq_skips_l, Permutation_submseteq, Permutation_cons_append. } + rewrite (take_S_r _ _ n) // app_assoc. + by apply submseteq_skips_r. + - by apply lookup_lt_Some in Hhistndeq_1. } + + clear - Hhistndeq_1 Hhistvs_1. + iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H". + iNamedSuffix "H" "_2". + wp_faa. + + iCombine "HcontE●_2 HcontE◯" as "HcontE" gives %->%excl_auth_agree_L. + iMod (own_update with "HcontE") as "[HcontE●_2 HcontE◯]". + { apply (excl_auth_update _ _ n). } + + iEval (rewrite Z.add_0_r -Z.add_assoc [(nF + n)%Z]Z.add_comm Z.add_assoc) in "Hsum_2". + + iCombine "HvdeqE●_2 HvdeqE◯" gives %->%excl_auth_agree_L. + + iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre]. + assert (Hn : n ≠ 0). + { eapply (Forall_lookup (.≠ 0)); last done. + by eapply Forall_prefix. } + + iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro. + iPureIntro. exists ndeq'. repeat split; try done. + by rewrite /option_nat option_guard_True. + } + { iIntros (_ _) "[H1 H2] !>". iFrame. } + } + { awp_apply (dequeue_spec lq lqp). + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H". + iNamedSuffix "H" "_1". + iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. } + iIntros (v0 vs') "[%Hvs Hq1]". + destruct vs1; simplify_eq/=. + iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1". + iCombine "HcontF◯ HcontF●_1" gives %->%excl_auth_agree_L. + + iCombine "HvdeqF●_1 HvdeqF◯" as "HvdeqF" gives %->%excl_auth_agree_L. + iMod (own_update with "HvdeqF") as "[HvdeqF●_1 HvdeqF◯]". + { apply (excl_auth_update _ _ (Some n)). } + + apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1]. + iModIntro. iFrame. iFrameNamed. iSplit. + { iPureIntro. exists (S ndeq). repeat split; try done. etrans; first done. + - simplify_eq/=. rewrite app_nil_r in HnDEF_1. + rewrite (take_S_r _ _ n) // app_assoc. + by apply submseteq_skips_r. + - by apply lookup_lt_Some in Hhistndeq_1. } + + clear - Hhistndeq_1 Hhistvs_1. + iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H". + iNamedSuffix "H" "_2". + wp_faa. + + iCombine "HcontF●_2 HcontF◯" as "HcontF" gives %->%excl_auth_agree_L. + iMod (own_update with "HcontF") as "[HcontF●_2 HcontF◯]". + { apply (excl_auth_update _ _ n). } + + iEval (rewrite Z.add_0_r) in "Hsum_2". + + iCombine "HvdeqF●_2 HvdeqF◯" gives %->%excl_auth_agree_L. + + iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre]. + assert (Hn : n ≠ 0). + { eapply (Forall_lookup (.≠ 0)); last done. + by eapply Forall_prefix. } + + iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro. + iPureIntro. exists ndeq'. repeat split; try done. + by rewrite /option_nat option_guard_True. + } + + iIntros (v1 v2) "[(H1 & HvenqB◯ & HvenqC◯ & H4 & H5) H6]". + unfold P1, P2, P3, P4, P5, P6. clear P1 P2 P3 P4 P5 P6. + iDestruct "H1" as "[HvenqA◯ Hlinked◯]". + iDestruct "H4" as "(%nD' & HnD'◯ & %HcontD)". + iDestruct "H5" as "(%nE' & HnE'◯ & %HcontE)". + iDestruct "H6" as "(%nF' & HnF'◯ & %HcontF)". + iModIntro. wp_pures. + + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">@". + wp_load. iModIntro. iSplit; [by iFrame; iExists ndeq|]. + iCombine "HnD'◯ HcontD●" gives %<-%excl_auth_agree_L. iClear "HnD'◯ HcontD●". + iCombine "HnE'◯ HcontE●" gives %<-%excl_auth_agree_L. iClear "HnE'◯ HcontE●". + iCombine "HnF'◯ HcontF●" gives %<-%excl_auth_agree_L. iClear "HnF'◯ HcontF●". + + rewrite /option_nat !option_guard_True // in HD HE HF. + apply option_le_inv in HD as [HD|<-]; first done. + apply option_le_inv in HE as [HE|<-]; first done. + apply option_le_inv in HF as [HF|<-]; first done. + simplify_eq/=. + + iCombine "Hlinked● Hlinked◯" gives %->%excl_auth_agree_L. + iClear "Hq2 Hlinked● Hlinked◯". + + iCombine "HvenqA● HvenqA◯" gives %->%excl_auth_agree_L. iClear "HvenqA◯ HvenqA●". + iCombine "HvenqB● HvenqB◯" gives %->%excl_auth_agree_L. iClear "HvenqB◯ HvenqB●". + iCombine "HvenqC● HvenqC◯" gives %->%excl_auth_agree_L. iClear "HvenqC◯ HvenqC●". + iPureIntro. enough (nD + nE + nF = 6). { do 2 f_equal. lia. } + + assert (ndeq ≥ 3 ∧ length hist1 ≥ 3) as [Hndeq' Hhist1']. + { apply submseteq_length in HnDEF as Hndeq'. + rewrite /= length_take in Hndeq'. lia. } + apply gmultiset_subseteq_size in Hhist1 as Hhist1''. + rewrite list_to_set_disj_size !gmultiset_size_disj_union !gmultiset_size_singleton /= in Hhist1''. + have {Hhist1''}Hhist1' : length hist1 = 3 by lia. + apply gmultiset_subseteq_size_eq in Hhist1; last first. + { rewrite !gmultiset_size_disj_union !gmultiset_size_singleton /= list_to_set_disj_size. lia. } + + assert (HnDEF' : [nD; nE; nF] ≡ₚ hist1). + { apply submseteq_length_Permutation; last (simpl; lia). + etrans; [apply HnDEF | apply submseteq_take]. } + + assert (Hhist1'' : hist1 ≡ₚ elements ({[+ 1; 2; 3 +]} : gmultiset nat)). + { erewrite elements_list_to_set_disj_perm. + by rewrite Hhist1. } + + assert (H123 : elements ({[+ 1; 2; 3 +]} : gmultiset nat) ≡ₚ [1; 2; 3]). + { by rewrite !gmultiset_elements_disj_union !gmultiset_elements_singleton /=. } + + trans (foldr Nat.add 0 [nD; nE; nF]). { simpl. lia. } + by rewrite HnDEF' Hhist1'' H123. + Qed. + +End proofs. + +Definition fq := fin_queue_proof.fin_queue_hl. +Definition lq := lmpmc_queue_proof.lmpmc_queue_hl fq. + +(** First example *) + +Definition simple_clientΣ : gFunctors := #[ heapΣ; fin_queue_proof.fin_queueΣ ]. +Lemma simple_client_adequate σ : adequate NotStuck (simple_example_2_1 lq) σ (λ v _, v = (#10, #20)%V). +Proof. + eapply (heap_adequacy simple_clientΣ). iIntros (?) "_". iApply simple_example_2_1_safe. + Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris. +Qed. + +(** Second example *) + +Definition simple_mt_clientΣ : gFunctors := + #[ heapΣ; spawnΣ; + fin_queue_proof.fin_queueΣ; + GFunctor (excl_authRF boolO); + GFunctor (excl_authRF (listO natO)) ]. + +Instance smc_inG_excl_auth_bool Σ : subG simple_mt_clientΣ Σ → inG Σ (excl_authR boolO). +Proof. solve_inG. Qed. +Instance smc_inG_excl_auth_nat_list Σ : subG simple_mt_clientΣ Σ → inG Σ (excl_authR (listO natO)). +Proof. solve_inG. Qed. + +Lemma simple_mt_client_adequate σ : adequate NotStuck (simple_example_2_2 lq) σ (λ v _, v = (#10, #20)%V). +Proof. + eapply (heap_adequacy simple_mt_clientΣ). iIntros (?) "_". iApply simple_example_2_2_safe. + Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris. +Qed. + +(** Third example *) + +Definition mt_example_1Σ : gFunctors := + #[ heapΣ; spawnΣ; + fin_queue_proof.fin_queueΣ; + mono_listΣ natO; + GFunctor (excl_authRF (gmultisetO nat)); + GFunctor (excl_authRF natO); + GFunctor (excl_authRF boolO); + GFunctor (excl_authRF (optionO natO)); + GFunctor (exclR (listO natO)) ]. + +Instance me_inG_excl_auth_multiset Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR (gmultisetO nat)). +Proof. solve_inG. Qed. +Instance me_inG_excl_auth_nat Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR natO). +Proof. solve_inG. Qed. +Instance me_inG_excl_auth_bool Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR boolO). +Proof. solve_inG. Qed. +Instance me_inG_excl_auth_option_nat Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR (optionO natO)). +Proof. solve_inG. Qed. +Instance me_inG_excl_list_nat Σ : subG mt_example_1Σ Σ → inG Σ (exclR (listO natO)). +Proof. solve_inG. Qed. + +Lemma mt_example_1_adequate σ : adequate NotStuck (mt_example_1 lq) σ (λ v _, v = #6%V). +Proof. + eapply (heap_adequacy mt_example_1Σ). iIntros (?) "_". iApply mt_example_1_safe. + Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris. +Qed. + +Print Assumptions simple_client_adequate. +Print Assumptions simple_mt_client_adequate. +Print Assumptions mt_example_1_adequate. diff --git a/theories/fin_queue_proof.v b/theories/fin_queue_proof.v new file mode 100644 index 0000000..64646ae --- /dev/null +++ b/theories/fin_queue_proof.v @@ -0,0 +1,932 @@ +From iris.program_logic Require Import atomic. +From iris.heap_lang Require Import notation proofmode. +From iris.algebra.lib Require Import excl_auth. +From iris.base_logic.lib Require Import invariants. +From iris.base_logic.lib Require Import invariants mono_nat mono_list. +From iris_named_props Require Import custom_syntax. + +From lmpmc Require Import fin_queue_spec upstream util. + +Definition new_node : val := λ: "data" "final", + let: "ℓ_node" := AllocN #3 #() in + "ℓ_node" <- "data";; + "ℓ_node" +ₗ #1 <- NONE;; + "ℓ_node" +ₗ #2 <- "final";; + "ℓ_node". + +Definition new : val := λ: <>, + let: "ℓ_node" := new_node #() #false in + AllocN #2 "ℓ_node". + +Definition set_tail : val := rec: "go" "ℓ_q" "ℓ_node" := + let: "ℓ_tail" := !("ℓ_q" +ₗ #1) in + match: !("ℓ_tail" +ₗ #1) with + NONE => + if: CAS ("ℓ_tail" +ₗ #1) NONE (SOME "ℓ_node") then + #() + else + "go" "ℓ_q" "ℓ_node" + | SOME "ℓ_next" => + CAS ("ℓ_q" +ₗ #1) "ℓ_tail" "ℓ_next";; + "go" "ℓ_q" "ℓ_node" + end. + +Definition enqueue : val := λ: "ℓ_q" "data", + set_tail "ℓ_q" (new_node "data" #false). + +Definition finalize : val := λ: "ℓ_q" "data", + set_tail "ℓ_q" (new_node "data" #true). + +Definition try_dequeue : val := rec: "go" "ℓ_q" := + let: "ℓ_head" := !"ℓ_q" in + match: !("ℓ_head" +ₗ #1) with + NONE => InjR NONE + | SOME "ℓ_next" => + if: !("ℓ_next" +ₗ #2) then + (* The next node is the final node. We refuse to dequeue and + return the data of the final node. *) + InjR (SOME !"ℓ_next") + else (* [ℓ_next] node type = normal *) + let: "v" := !"ℓ_next" in + if: CAS "ℓ_q" "ℓ_head" "ℓ_next" then + InjL "v" + else + "go" "ℓ_q" + end. + +Class fin_queueG Σ := FinQueueG + { fin_queue_mono_natG :: mono_natG Σ; + fin_queue_mono_listG :: mono_listG (prodO locO valO) Σ; }. + +Definition fin_queueΣ : gFunctors := + #[ mono_natΣ; mono_listΣ (prodO locO valO) ]. + +#[global] Instance subG_fin_queueΣ {Σ} : subG fin_queueΣ Σ → fin_queueG Σ. +Proof. solve_inG. Qed. + +Section fin_queue. + Context `{!heapGS Σ, !fin_queueG Σ}. + + Record gstate := + { γ_hist : gname; + γ_hpos : gname; }. + Definition gstate_to_pair (γ : gstate) := + (γ.(γ_hist), γ.(γ_hpos)). + Definition gstate_of_pair '(γ_hist, γ_hpos) := + {| γ_hist := γ_hist; γ_hpos := γ_hpos |}. + Instance gstate_eq_dec : EqDecision gstate := ltac:(solve_decision). + Instance gstate_countable : Countable gstate. + Proof. + refine {| encode := encode ∘ gstate_to_pair; + decode := fmap gstate_of_pair ∘ decode; |}. + intros []. by rewrite /= decode_encode. + Qed. + + Variant node_next := + | Normal (mℓ_next : option loc) + | Final. + Instance node_next_eq_dec : EqDecision node_next. + Proof. solve_decision. Defined. + Definition node_final_hl (n : node_next) := #(bool_decide (n = Final)). + Definition node_next_hl (n : node_next) := + match n with + | Normal mℓ_next => loc_opt_hl mℓ_next + | Final => NONEV + end. + + Definition node_repr (ℓ : loc) (data : val) (n : node_next) : iProp Σ := + ("Hndata" ∷ ℓ ↦□ data) ∗ + ("Hnnext" ∷ (ℓ +ₗ 1) ↦ node_next_hl n) ∗ + ("Hnfinal" ∷ (ℓ +ₗ 2) ↦□ #(bool_decide (n = Final))). + + Definition loc_at (hist : list (loc * val)) i := + hist.*1 !! i. + Definition val_at (hist : list (loc * val)) i := + hist.*2 !! i. + + Lemma loc_at_prefix xs xs' i ℓ : + loc_at xs i = Some ℓ → xs `prefix_of` xs' → loc_at xs' i = Some ℓ. + Proof. + unfold loc_at. intros Hxs Hpre. + eapply prefix_lookup_Some; first exact Hxs. + by apply prefix_of_fmap. + Qed. + + Lemma val_at_prefix xs xs' i ℓ : + val_at xs i = Some ℓ → xs `prefix_of` xs' → val_at xs' i = Some ℓ. + Proof. + unfold val_at. intros Hxs Hpre. + eapply prefix_lookup_Some; first exact Hxs. + by apply prefix_of_fmap. + Qed. + + Lemma loc_at_val_at_Some xs i ℓ : + loc_at xs i = Some ℓ → ∃ v, val_at xs i = Some v. + Proof. + unfold loc_at, val_at. rewrite [xs.*2 !! i]list_lookup_fmap. + intros [[ℓ' v] [-> ->]]%list_lookup_fmap_Some_1. by exists v. + Qed. + + Lemma loc_at_val_at_combine {hist i ℓ v} : + loc_at hist i = Some ℓ → + val_at hist i = Some v → + hist !! i = Some (ℓ, v). + Proof. + unfold loc_at, val_at. intros Hloc Hval. + rewrite list_lookup_fmap in Hloc. + rewrite list_lookup_fmap in Hval. + destruct (hist !! i) as [[ℓ' v']|]; last done. + simpl in *. congruence. + Qed. + + Lemma loc_at_Some_length hist i ℓ : + loc_at hist i = Some ℓ → i < length hist. + Proof. + intros Hloc%lookup_lt_Some. + by rewrite length_fmap in Hloc. + Qed. + + Lemma loc_at_drop hist n i ℓ : + loc_at hist (n + i) = Some ℓ → + loc_at (drop n hist) i = Some ℓ. + Proof. + unfold loc_at. intros Hloc. + by rewrite list_lookup_fmap lookup_drop -list_lookup_fmap. + Qed. + + Lemma val_at_drop hist n i ℓ : + val_at hist (n + i) = Some ℓ → + val_at (drop n hist) i = Some ℓ. + Proof. + unfold val_at. intros Hval. + by rewrite list_lookup_fmap lookup_drop -list_lookup_fmap. + Qed. + + Definition next_from (hist : list (loc * val)) fin i := + if fin && bool_decide (S i = length hist) then Final else Normal (loc_at hist (S i)). + + Definition next_from_normal hist fin i v : + next_from hist fin i = Normal v → + (fin = false ∨ S i ≠ length hist) ∧ loc_at hist (S i) = v. + Proof. + rewrite /next_from. intros H. + destruct fin, (decide (S i = length hist)). + - rewrite bool_decide_true //= in H. + - rewrite bool_decide_false //= in H. + injection H as <-. split; last done. by right. + - injection H as <-. split; last done. by left. + - injection H as <-. split; last done. by left. + Qed. + + Lemma next_from_S ℓv ℓvs fin n : + next_from (ℓv :: ℓvs) fin (S n) = next_from ℓvs fin n. + Proof. + rewrite /next_from /loc_at list_lookup_fmap /= -list_lookup_fmap. + erewrite bool_decide_ext; first done. lia. + Qed. + + Lemma node_next_hl_next_from hist fin i : + node_next_hl (next_from hist fin i) = loc_opt_hl (loc_at hist (S i)). + Proof. + unfold node_next_hl, next_from. + destruct fin, (decide (S i = length hist)) as [Hhist|Hhist]; simpl; try done. + - by rewrite bool_decide_true // /loc_at list_lookup_fmap lookup_ge_None_2; last lia. + - by rewrite bool_decide_false. + Qed. + + Definition hist_repr (hist : list (loc * val)) (fin : bool) : iProp Σ := + [∗ list] i ↦ '(ℓ, data) ∈ hist, node_repr ℓ data (next_from hist fin i). + + Lemma hist_repr_peek_1 hist fin i ℓ data : + loc_at hist i = Some ℓ → + val_at hist i = Some data → + hist_repr hist fin -∗ + node_repr ℓ data (next_from hist fin i) ∗ + (node_repr ℓ data (next_from hist fin i) -∗ hist_repr hist fin). + Proof. + iIntros "%Hloc %Hval Hrepr". + pose proof (loc_at_val_at_combine Hloc Hval) as Hi. + iPoseProof (big_sepL_lookup_acc with "Hrepr") as "[Hnode Hclose]". + { apply Hi. } + iFrame. + Qed. + + Lemma hist_repr_peek_2 hist fin i ℓ : + loc_at hist i = Some ℓ → + hist_repr hist fin -∗ + ∃ data, node_repr ℓ data (next_from hist fin i) ∗ + (node_repr ℓ data (next_from hist fin i) -∗ hist_repr hist fin). + Proof. + iIntros "%Hloc Hrepr". + assert (∃ v, val_at hist i = Some v) as [v Hval]. + { by apply loc_at_val_at_Some in Hloc. } + iExists v. by iApply hist_repr_peek_1. + Qed. + + Lemma hist_repr_peek_3 hist fin i ℓ : + loc_at hist i = Some ℓ → + hist_repr hist fin -∗ + (ℓ +ₗ 1) ↦ node_next_hl (next_from hist fin i) ∗ + ((ℓ +ₗ 1) ↦ node_next_hl (next_from hist fin i) -∗ hist_repr hist fin). + Proof. + iIntros "%Hloc Hrepr". + iDestruct (hist_repr_peek_2 with "[$]") as "(%v & @ & Hclose)"; first done. + iFrame. iIntros "Hnnext". iApply "Hclose". iFrame. + Qed. + + Lemma loc_at_None hist pos : + loc_at hist pos = None → hist !! pos = None. + Proof. + rewrite /loc_at list_lookup_fmap. + by destruct (hist !! pos). + Qed. + + Lemma loc_at_length hist pos : + loc_at hist pos = None → length hist ≤ pos. + Proof. + intros H%loc_at_None. + by apply lookup_ge_None. + Qed. + + Lemma next_from_drop ℓvs fin n i : + next_from ℓvs fin (n + i) = next_from (drop n ℓvs) fin i. + Proof. + rewrite /next_from /loc_at list_lookup_fmap /= -list_lookup_fmap. + erewrite bool_decide_ext with (Q:=S i = length (drop n ℓvs)); last first. + { rewrite length_drop. lia. } + by rewrite fmap_drop list_lookup_fmap lookup_drop -list_lookup_fmap plus_n_Sm. + Qed. + + Lemma hist_repr_proj hist i ℓ fin : + loc_at hist i = Some ℓ → + hist_repr hist fin -∗ + (∃ v, (ℓ +ₗ 1) ↦ v) ∗ hist_repr (drop (S i) hist) fin. + Proof. + iIntros "%Hℓi Hrepr". + iDestruct (big_sepL_take_drop _ _ (S i) with "Hrepr") as "[Hrepr1 Hrepr2]". + + rewrite /loc_at list_lookup_fmap in Hℓi. + destruct (hist !! i) as [[ℓ' v]|] eqn:Hi; last done. + simpl in *. injection Hℓi as ->. + + iDestruct (big_sepL_lookup_acc with "Hrepr1") as "[Hrepr Hclose]". + { rewrite lookup_take_lt //. lia. } + iSimplifyEq. iDestruct "Hrepr" as "@". iFrame. + iClear "Hndata Hnfinal Hclose". + + iAssert (hist_repr (drop (S i) hist) fin) with "[Hrepr2]" as "Hrepr2". + { unfold hist_repr. iApply (big_sepL_mono with "Hrepr2"). + iIntros (k [ℓ' v'] Hk) "Hrepr". + rewrite -next_from_drop; first done. } + done. + Qed. + + Lemma loc_at_inj_aux hist i j ℓ fin : + i < j → + loc_at hist i = Some ℓ → + loc_at hist j = Some ℓ → + hist_repr hist fin -∗ + False. + Proof. + iIntros "%ij %Hloci %Hlocj Hrepr". + assert (i < length hist). { by eapply loc_at_Some_length. } + assert (j < length hist). { by eapply loc_at_Some_length. } + assert (∃ n, j = S i + n) as [n ->]. + { exists (j - i - 1). lia. } + iPoseProof (hist_repr_proj hist i ℓ fin Hloci with "Hrepr") as "[[%ni Hℓi] Hrepr']". + + assert (Hlocj' : loc_at (drop (S i) hist) n = Some ℓ). + { by apply loc_at_drop. } + + iPoseProof (hist_repr_proj _ n ℓ fin Hlocj' with "Hrepr'") as "[[%nj Hℓj] _]". + by iCombine "Hℓi Hℓj" gives %[? _]. + Qed. + + Lemma loc_at_inj {hist i j ℓ fin} : + loc_at hist i = Some ℓ → + loc_at hist j = Some ℓ → + hist_repr hist fin -∗ + ⌜i = j⌝. + Proof. + iIntros "%Hloci %Hlocj Hrepr". + destruct (loc_at_val_at_Some hist i ℓ Hloci) as [vi Hvali]. + destruct (loc_at_val_at_Some hist j ℓ Hlocj) as [vj Hvalj]. + destruct (decide (i < j)) as [Hij|Hij]. + - (* i < j *) + by iPoseProof (loc_at_inj_aux with "Hrepr") as "H". + - (* i ≥ j *) + destruct (decide (j < i)) as [Hji|Hji]. + + (* j < i *) + by iPoseProof (loc_at_inj_aux with "Hrepr") as "H". + + (* i = j *) + iPureIntro. lia. + Qed. + + Definition queue_γs_dq (hist : list (loc * val)) (hpos : nat) (mfin : option val) : dfrac := + match mfin with + | None => DfracOwn 1 + | Some _ => + if decide (S (S hpos) = length hist) + then DfracDiscarded + else DfracOwn 1 + end. + + Lemma queue_γs_dq_cases hist hpos mfin : + queue_γs_dq hist hpos mfin = DfracOwn 1 ∨ + queue_γs_dq hist hpos mfin = DfracDiscarded. + Proof. + unfold queue_γs_dq. + destruct mfin, (decide (S (S hpos) = length hist)); + (by left) || by right. + Qed. + + Definition queue_repr_1 (γs : gstate) ℓ_q (vs : list val) (mfin : option val) : iProp Σ := + ∃ (hist : list (loc * val)) (ℓ_head ℓ_tail : loc) (hpos tpos : nat), + ("Hhead" ∷ ℓ_q ↦ #ℓ_head) ∗ + (* Not immediately clear whether this can be discarded when the queue is + finalized and otherwise emptied *) + ("Htail" ∷ (ℓ_q +ₗ 1) ↦ #ℓ_tail) ∗ + ("Hrepr" ∷ hist_repr hist (bool_decide (is_Some mfin))) ∗ + ("Hhist●" ∷ γs.(γ_hist) ↪●ML{queue_γs_dq hist hpos mfin} hist) ∗ + ("Hhpos●" ∷ γs.(γ_hpos) ↪●MN{queue_γs_dq hist hpos mfin} hpos) ∗ + ("%Hℓhpos" ∷ ⌜loc_at hist hpos = Some ℓ_head⌝) ∗ + ("%Hℓtpos" ∷ ⌜loc_at hist tpos = Some ℓ_tail⌝) ∗ + ("%Hvs" ∷ ⌜vs ++ option_list mfin = (drop (S hpos) hist).*2⌝). + + Definition queue_fin_1 (γs : gstate) (fin : val) : iProp Σ := + ∃ (hist : list (loc * val)) (hpos : nat), + ("Hhist" ∷ γs.(γ_hist) ↪●ML□ hist) ∗ + ("Hhpos" ∷ γs.(γ_hpos) ↪●MN□ hpos) ∗ + ("%Hfin" ∷ ⌜val_at hist (S hpos) = Some fin⌝). + + Definition queue_repr ℓ_q (vs : list val) (mfin : option val) : iProp Σ := + ∃ (γs : gstate), meta ℓ_q nroot γs ∗ queue_repr_1 γs ℓ_q vs mfin. + + #[global] Instance queue_repr_timeless ℓ_q vs mfin : Timeless (queue_repr ℓ_q vs mfin) := _. + + Definition queue_fin ℓ_q (fin : val) : iProp Σ := + ∃ (γs : gstate), meta ℓ_q nroot γs ∗ queue_fin_1 γs fin. + + #[global] Instance queue_fin_persistent ℓ_q fin : Persistent (queue_fin ℓ_q fin) := _. + #[global] Instance queue_fin_timeless ℓ_q fin : Timeless (queue_fin ℓ_q fin) := _. + + Lemma queue_fin_obtain ℓ fin : queue_repr ℓ [] (Some fin) -∗ queue_fin ℓ fin. + Proof. + iIntros "(%γs & Hγs & @)". simplify_eq/=. + assert (Hlen : length (drop (S hpos) hist).*2 = 1) by rewrite -Hvs //. + rewrite fmap_drop length_drop length_fmap in Hlen. + case_decide; last lia. iFrame. iPureIntro. + by rewrite /val_at -[S hpos]Nat.add_0_r -lookup_drop -fmap_drop -Hvs. + Qed. + + Lemma queue_fin_agree ℓ vs fin mfin : + queue_fin ℓ fin -∗ + queue_repr ℓ vs mfin -∗ + ⌜vs = []⌝ ∗ ⌜mfin = Some fin⌝. + Proof. + iIntros "(%γs & Hγs & @) (%γs' & Hγs' & @)". + iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}". + iDestruct (mono_list_auth_own_agree with "Hhist Hhist●") as %[Hfracs <-]. + iDestruct (mono_nat_auth_own_agree with "Hhpos Hhpos●") as %[_ <-]. + iPureIntro. + + unfold queue_γs_dq in Hfracs. + destruct mfin as [fin'|]; last done. + destruct (decide (S (S hpos) = length hist)); last done. + + assert (Hlen : S (length vs) = 1). + { rewrite -Nat.add_1_r -(length_app _ [fin']) Hvs length_fmap length_drop -e. lia. } + destruct vs; last done. simplify_eq/=. + + by rewrite -Hfin /val_at -[S hpos]Nat.add_0_r -lookup_drop -fmap_drop -Hvs. + Qed. + + Lemma hist_weaken {γs} hist hpos mfin : + γs.(γ_hist) ↪●ML hist ==∗ γs.(γ_hist) ↪●ML{queue_γs_dq hist hpos mfin} hist. + Proof. + iIntros "Hhist". + destruct (queue_γs_dq_cases hist hpos mfin) as [-> | ->]; first done. + by iApply mono_list_auth_own_persist. + Qed. + + Lemma hpos_weaken {γs hpos} hist mfin : + γs.(γ_hpos) ↪●MN hpos ==∗ γs.(γ_hpos) ↪●MN{queue_γs_dq hist hpos mfin} hpos. + Proof. + iIntros "Hhist". + destruct (queue_γs_dq_cases hist hpos mfin) as [-> | ->]; first done. + by iApply mono_nat_own_persist. + Qed. + + Variant new_node_next := NonFinalType | FinalType. + Definition new_node_next_red (n : new_node_next) := + match n with + | NonFinalType => Normal None + | FinalType => Final + end. + Instance new_node_next_eq_dec : EqDecision new_node_next. + Proof. solve_decision. Defined. + + Lemma new_node_spec data (final : bool) : + {{{ True }}} + new_node data #final + {{{ (ℓ : loc), RET #ℓ; node_repr ℓ data (new_node_next_red (if final then FinalType else NonFinalType)) }}}. + Proof. + iIntros "%Φ _ HΦ". iUnfold new_node. wp_lam. + wp_alloc ℓ_node as "Hℓ_node"; first done. + iDestruct (array_cons with "Hℓ_node") as "[Hℓ_node0 Hℓ_node12]". + iDestruct (array_cons with "Hℓ_node12") as "[Hℓ_node1 Hℓ_node2]". + iDestruct (array_cons with "Hℓ_node2") as "[Hℓ_node2 _]". + rewrite Loc.add_assoc. + wp_let. do 3 wp_store. + iMod (pointsto_persist with "Hℓ_node0") as "Hℓ_node0". + iMod (pointsto_persist with "Hℓ_node2") as "Hℓ_node2". + iModIntro. iApply "HΦ". destruct final; by iFrame. + Qed. + + Lemma new_spec : + {{{ True }}} + new #() + {{{ (ℓ : loc), RET #ℓ; queue_repr ℓ [] None }}}. + Proof. + iIntros "%Φ _ HΦ". iUnfold new. + wp_lam. wp_apply (new_node_spec with "[//]") as (ℓ_node) "Hnode". wp_let. + + set ℓ_head := ℓ_node. set ℓ_tail := ℓ_node. + set hpos := 0. set tpos := 0. + set hist := [(ℓ_node, #())] : list (loc * val). + iAssert (hist_repr hist false) with "[$Hnode //]" as "Hrepr". + + iMod (mono_list_own_alloc hist) as "[%γ_hist [Hhist● _]]". + iMod (mono_nat_own_alloc hpos) as "[%γ_hpos [Hhpos● _]]". + set γs := {| γ_hist := γ_hist; γ_hpos := γ_hpos |}. + + iApply wp_fupd. iApply wp_allocN; [lia|done|]. + iIntros "!> %ℓ [Hℓ [Htok _]]". + iDestruct (array_cons with "Hℓ") as "[Hℓ0 Hℓ1]". + iDestruct (array_cons with "Hℓ1") as "[Hℓ1 _]". + rewrite Loc.add_0. + + iMod (meta_set ⊤ ℓ γs nroot with "Htok") as "Hmeta"; first done. + + iApply "HΦ". iModIntro. iFrame. by iExists tpos. + Qed. + + Lemma try_bump_tail_spec hist0 tpos ℓ_old ℓ_new ℓ_q γs : + loc_at hist0 tpos = Some ℓ_old → + loc_at hist0 (S tpos) = Some ℓ_new → + γs.(γ_hist) ↪◯ML hist0 -∗ + <<{ ∀∀ vs mfin, queue_repr_1 γs ℓ_q vs mfin }>> + CAS #(ℓ_q +ₗ 1) #ℓ_old #ℓ_new @ ∅ + <<{ ∃∃ (b : bool), queue_repr_1 γs ℓ_q vs mfin | RET #b }>>. + Proof. + iIntros "%Hold %Hnew #Hhist◯ %Φ AU". + wp_bind (CmpXchg _ _ _)%E. + iMod "AU" as "(%vs & %fin & (%hist1 & %ℓ_head & %ℓ_tail & %hpos & %tpos' & @) & [_ Hclose])". + iAssert ⌜hist0 `prefix_of` hist1⌝%I as %Hhist01. + { by iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist◯") as "[_ ?]". } + + destruct (decide (ℓ_tail = ℓ_old)) as [->|]. + - (* The tail has not been updated yet *) + wp_cmpxchg_suc. + + iAssert (queue_repr_1 γs ℓ_q vs fin) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq". + { iPureIntro. + repeat split; try done || lia. + exists (S tpos). repeat split; try done. + by eapply loc_at_prefix. } + iMod ("Hclose" with "[$Hq]") as "HΦ". + iModIntro. wp_pures. iApply "HΦ". + - (* The tail has been updated in the meantime *) + wp_cmpxchg_fail. + iAssert (queue_repr_1 γs ℓ_q vs fin) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq". + { iExists tpos'. by iFrameNamed. } + iMod ("Hclose" with "[$Hq]") as "HΦ". + iModIntro. wp_pures. iApply "HΦ". + Qed. + + (* Given a history that is represented, after updating the [next] + pointer of the current tail node to a new tail node, we obtain a + new (extended) history (with the new tail node appended). *) + Lemma hist_repr_snoc hist tpos (ℓ_tail ℓ_new : loc) data next : + length hist = S tpos → + loc_at hist tpos = Some ℓ_tail → + node_repr ℓ_new data (new_node_next_red next) -∗ + hist_repr hist false -∗ + (ℓ_tail +ₗ 1) ↦ node_next_hl (Normal None) ∗ + ((ℓ_tail +ₗ 1) ↦ node_next_hl (Normal (Some ℓ_new)) -∗ hist_repr (hist ++ [(ℓ_new, data)]) (bool_decide (next = FinalType))). + Proof. + unfold loc_at. + iIntros "%Hhistlen %Hloc @ Hhist". + rewrite list_lookup_fmap in Hloc. + destruct (hist !! tpos) as [[ℓ_tail' v_tail]|] eqn:Htpos; last done. + injection Hloc as ->. + apply list_elem_of_split_length in Htpos as (hist' & empty & -> & Htpos). + rewrite length_app length_cons -Htpos in Hhistlen. + assert (empty = []) as ->. { apply nil_length_inv. lia. } + clear Hhistlen Htpos. + + iPoseProof (big_sepL_snoc with "Hhist") as "[Hinit Htail]". + iNamedSuffix "Htail" "_tail". + + iSimplifyEq. + assert (loc_at (hist' ++ [(ℓ_tail, v_tail)]) (S (length hist')) = None) as ->. + { apply lookup_ge_None_2. rewrite length_fmap length_app length_cons /=. lia. } + iFrame "Hnnext_tail". iIntros "Hnnext_tail". + iSimplifyEq. rewrite /hist_repr. + iApply big_sepL_snoc. + iSplitR "Hndata Hnfinal Hnnext". + - iApply big_sepL_snoc. iSplitL "Hinit". + + iApply (big_sepL_mono with "Hinit"). + iIntros (k [ℓ v] Hk) "Hrepr". + unfold next_from. simpl. rewrite [bool_decide (S k = _)]bool_decide_false; last first. + { apply lookup_lt_Some in Hk. rewrite !length_app /=. lia. } + rewrite andb_false_r /=. + assert (loc_at ((hist' ++ [(ℓ_tail, v_tail)]) ++ [(ℓ_new, data)]) (S k) = loc_at (hist' ++ [(ℓ_tail, v_tail)]) (S k)) as ->. + { rewrite /loc_at !list_lookup_fmap lookup_app_l // length_app /=. + apply lookup_lt_Some in Hk. lia. } + done. + + iFrame. + rewrite /next_from /= [bool_decide (S (length hist') = _)]bool_decide_false; last first. + { rewrite !length_app /=. lia. } + rewrite andb_false_r /= /loc_at list_lookup_fmap lookup_app_r; last first. + { rewrite length_app /=. lia. } + rewrite length_app /= Nat.add_1_r Nat.sub_diag /=. + by iFrame. + - iFrame. + rewrite /next_from /= /loc_at length_app /= Nat.add_1_r list_lookup_fmap lookup_app_r. + * rewrite !length_app /= !Nat.add_1_r [bool_decide (S _ = S _)]bool_decide_true // + andb_true_r Nat.sub_succ -Arith_base.minus_Sn_m_stt // Nat.sub_diag /=. + destruct next; simpl; iFrame. + * rewrite length_app /= Nat.add_1_r. lia. + Qed. + + Definition iffinal {A} (n : new_node_next) (a b : A) := + match n with + | FinalType => a + | NonFinalType => b + end. + + Lemma set_tail_spec (ℓ_q ℓ_node : loc) data next : + node_repr ℓ_node data (new_node_next_red next) -∗ + <<{ ∀∀ vs, queue_repr ℓ_q vs None }>> + set_tail #ℓ_q #ℓ_node @ ∅ + <<{ queue_repr ℓ_q (vs ++ iffinal next [] [data]) (iffinal next (Some data) None) | RET #() }>>. + Proof. + iIntros "@ %Φ AU". iLöb as "IH". wp_rec. + + wp_pures. wp_bind (! _)%E. + iMod "AU" as "(%vs & (%γs & #Hγs & %hist0 & %ℓ_head & %ℓ_tail & %hpos & %tpos & @) & [Hclose _])". + iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist0◯". + wp_load. iSimpl in "Hrepr". + rename Hℓtpos into Hℓtpos0. + iAssert (queue_repr_1 γs ℓ_q vs None) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq". + { iExists tpos. by iFrameNamed. } + iMod ("Hclose" with "[$]") as "AU". clear Hvs Hℓhpos hpos vs ℓ_head. + iModIntro. wp_let. wp_pure. + + wp_bind (! _)%E. + iMod "AU" as "(%vs & (%γs' & Hγs' & %hist2 & %ℓ_head & %ℓ_tail'' & %hpos & %tpos'' & @) & [Hclose _])". + iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}". + iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist0◯") as %Hhist02. + iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist2◯". + destruct Hhist02 as [_ Hhist02]. rename Hℓtpos into Hℓtpos2. + assert (Hℓtpos0'' : loc_at hist2 tpos = Some ℓ_tail). + { by eapply loc_at_prefix. } clear Hℓtpos0. + wp_pures. + iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%w & Hnrepr & Hrepr)"; first done. + iNamedSuffix "Hnrepr" "_tail". + wp_load. + iDestruct "Hnfinal_tail" as "#Hnfinal_tail2". + iPoseProof ("Hrepr" with "[$]") as "Hrepr". + iAssert (queue_repr_1 γs ℓ_q vs None) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq". + { iExists tpos''. by iFrameNamed. } + iMod ("Hclose" with "[$]") as "AU". clear Hvs Hℓhpos hpos vs ℓ_head. + iModIntro. + + destruct (next_from hist2 false tpos) as [[ℓ_next|]|] eqn:Htpos2; last done. + + (* it is not the last node *) + simpl. apply next_from_normal in Htpos2 as [Hnext HStpos2]. rewrite HStpos2 /=. + + wp_pures. wp_bind (Snd (CmpXchg _ _ _))%E. + awp_apply (try_bump_tail_spec with "[//]"). + { apply Hℓtpos0''. } + { done. } + rewrite /atomic_acc /=. + iMod "AU" as "(%vs & (%γs' & Hγs' & Hrepr) & [Hclose _])". + iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}". + iModIntro. iExists vs. iFrame "Hrepr". iSplit. + * iFrame. iIntros "Hrepr". by iApply ("Hclose" with "[$Hrepr]"). + * iIntros "%b Hrepr". + iMod ("Hclose" with "[$Hrepr //]") as "AU". + iModIntro. wp_pures. + by iApply ("IH" with "[$] [$] [$]"). + + (* it is the last (non-final) node *) + simpl. apply next_from_normal in Htpos2 as [Hnext HStpos2]. rewrite HStpos2 /=. + wp_pures. wp_bind (CmpXchg _ _ _)%E. + + iMod "AU" as "(%vs & (%γs' & Hγs' & %hist3 & %ℓ_head & %ℓ_tail''' & %hpos & %tpos''' & @) & Hclose)". + iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}". + iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist2◯") as %Hhist23. + destruct Hhist23 as [_ Hhist23]. rename Hℓtpos into Hℓtpos3. + + destruct (loc_at hist3 (S tpos)) as [ℓ_tail''''|] eqn:Hrace. + * (* Another item has been enqueued in the meantime, so the CAS is poised to fail. *) + iDestruct "Hclose" as "[Hclose _]". + + iDestruct (hist_repr_peek_3 with "[$Hrepr]") as "[Hℓ_tail1 Hrepr]". + { eapply prefix_lookup_Some; first apply Hℓtpos0''. by apply prefix_of_fmap. } + rewrite /next_from [bool_decide (S _ = _)]bool_decide_false; last first. + { apply lookup_lt_Some in Hrace. rewrite length_fmap in Hrace. lia. } + rewrite andb_false_r Hrace /=. + wp_cmpxchg_fail. + iSpecialize ("Hrepr" with "Hℓ_tail1"). + iAssert (queue_repr_1 γs ℓ_q vs None) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq". + { iExists tpos'''. by iFrameNamed. } + iMod ("Hclose" with "[$]") as "AU". iModIntro. + wp_pures. iApply ("IH" with "Hndata Hnnext Hnfinal AU"). + * (* This node is still the tail, so the CAS will succeed. *) + iDestruct "Hclose" as "[_ Hclose]". + + iAssert ⌜length hist3 = S tpos⌝%I as %Hhist3. + { apply loc_at_length in Hrace as Hhist3. + iPureIntro. apply loc_at_prefix with (xs':=hist3) in Hℓtpos0''; last done. + apply lookup_lt_Some in Hℓtpos0''. rewrite length_fmap in Hℓtpos0''. lia. } + + iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%w' & Hℓ_tail3 & Hrepr)". + { eapply prefix_lookup_Some; first apply Hℓtpos0''. by apply prefix_of_fmap. } + rewrite /next_from [bool_decide (S _ = _)]bool_decide_true // andb_true_r Hrace /=. + iNamedSuffix "Hℓ_tail3" "_tail3". + iPoseProof ("Hrepr" with "[$]") as "Hrepr". clear w. + + iPoseProof (hist_repr_snoc with "[$Hndata $Hnfinal $Hnnext] [$Hrepr]") as "[Htnode Henq]". + { apply Hhist3. } + { eapply prefix_lookup_Some. apply Hℓtpos0''. by apply prefix_of_fmap. } + wp_cmpxchg_suc. iSpecialize ("Henq" with "Htnode"). + + pose mfin := iffinal next (Some data) None. + + iMod (mono_list_auth_own_update_app [(ℓ_node, data)] with "Hhist●") as "[Hhist● _]". + iMod (hpos_weaken (hist3 ++ [(ℓ_node, data)]) mfin with "Hhpos●") as "Hhpos●". + iMod (hist_weaken (hist3 ++ [(ℓ_node, data)]) hpos mfin with "Hhist●") as "Hhist●". + replace (bool_decide (next = FinalType)) with (bool_decide (is_Some mfin)); last first. + { apply bool_decide_ext. destruct next; by cbn. } + + iAssert (queue_repr_1 γs ℓ_q (vs ++ iffinal next [] [data]) mfin) with "[$Hhead $Htail $Hhist● $Hhpos● $Henq]" as "Hq". + { iExists tpos'''. iPureIntro. + repeat split; try done. + - eapply loc_at_prefix; first done. + by apply prefix_app_r. + - eapply loc_at_prefix; first done. + by apply prefix_app_r. + - rewrite drop_app fmap_app -Hvs. rewrite /= app_nil_r -app_assoc. + f_equal. + assert (Hhpos : hpos < length hist3). + { apply lookup_lt_Some in Hℓhpos. + by rewrite length_fmap in Hℓhpos. } + assert (S hpos - length hist3 = 0) as -> by lia. + simpl. by destruct next. } + iMod ("Hclose" with "[$]") as "HΦ". + iModIntro. wp_pures. done. + Qed. + + Lemma enqueue_spec (ℓ_q : loc) (data : val) : + ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>> + enqueue #ℓ_q data @ ∅ + <<{ queue_repr ℓ_q (vs ++ [data]) None | RET #() }>>. + Proof. + iIntros "%Φ AU". wp_lam. wp_pures. + wp_apply (new_node_spec with "[//]") as "%ℓ_node Hnode". + awp_apply (set_tail_spec with "[$Hnode]"). + rewrite /atomic_acc /=. iMod "AU" as "(%vs & Hrepr & Hclose)". + iModIntro. iFrame. + Qed. + + Lemma finalize_spec (ℓ_q : loc) (data : val) : + ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>> + finalize #ℓ_q data @ ∅ + <<{ queue_repr ℓ_q vs (Some data) | RET #() }>>. + Proof. + iIntros "%Φ AU". wp_lam. wp_pures. + wp_apply (new_node_spec with "[//]") as "%ℓ_node Hnode". + awp_apply (set_tail_spec with "[$Hnode]"). + rewrite /atomic_acc /=. iMod "AU" as "(%vs & Hrepr & Hclose)". + iModIntro. iFrame. by rewrite app_nil_r. + Qed. + + Lemma try_dequeue_spec (ℓ_q : loc) : + ⊢ <<{ ∀∀ vs mfin, queue_repr ℓ_q vs mfin }>> + try_dequeue #ℓ_q @ ∅ + <<{ queue_repr ℓ_q (tail vs) mfin + | RET (if head vs is Some v then InjLV v else InjRV (val_opt_hl mfin)) }>>. + Proof. + iIntros "%Φ AU". iLöb as "IH". wp_rec. + + wp_bind (! _)%E. + iMod "AU" as "(%vs0 & %fin0 & (%γs & #Hγs & %hist0 & %ℓ_head0 & %ℓ_tail0 & %hpos0 & %tpos0 & @) & [Hclose _])". + iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist0◯". + iDestruct (mono_nat_lb_own_get with "Hhpos●") as "#Hhpos0◯". + rename Hℓhpos into Hℓhpos0. + wp_load. + iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU". + { iExists tpos0. by iFrameNamed. } + iModIntro. clear fin0 vs0 Hvs tpos0 Hℓtpos ℓ_tail0. + + wp_pures. wp_bind (! _)%E. + iMod "AU" as "(%vs1 & %fin1 & (%γs' & Hγs' & %hist1 & %ℓ_head1 & %ℓ_tail1 & %hpos1 & %tpos1 & @) & Hclose)". + iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}". + iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist1◯". + iDestruct (mono_nat_auth_lb_own_valid with "Hhpos● Hhpos0◯") as %Hhpos01. + iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist0◯") as %Hhist01. + destruct Hhpos01 as [_ Hhpos01]. destruct Hhist01 as [_ Hhist01]. + assert (Hℓhpos0' : loc_at hist1 hpos0 = Some ℓ_head0). + { by eapply loc_at_prefix. } clear Hℓhpos0. + iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%u & @ & Hrepr)"; first done. + wp_load. + iSpecialize ("Hrepr" with "[$]"). + + rewrite node_next_hl_next_from. + destruct (loc_at hist1 (S hpos0)) as [ℓ_headS0|] eqn:Hℓ_headS0. + - simpl. iDestruct "Hclose" as "[Hclose _]". + iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU". + { iExists tpos1. by iFrameNamed. } + iModIntro. clear u fin1 vs1 Hvs tpos1 Hℓtpos ℓ_tail1. + + wp_pures. wp_bind (! _)%E. + iMod "AU" as "(%vs2 & %fin2 & (%γs' & Hγs' & %hist2 & %ℓ_head2 & %ℓ_tail2 & %hpos2 & %tpos2 & @) & Hclose)". + iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}". + iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist2◯". + iDestruct (mono_nat_auth_lb_own_valid with "Hhpos● Hhpos0◯") as %Hhpos02. + iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist1◯") as %Hhist12. + destruct Hhpos02 as [_ Hhpos02]. destruct Hhist12 as [_ Hhist12]. + assert (Hℓ_headS0' : loc_at hist2 (S hpos0) = Some ℓ_headS0). + { by eapply loc_at_prefix. } clear Hℓ_headS0. + apply loc_at_val_at_Some in Hℓ_headS0' as Hval_headS0'. + destruct Hval_headS0' as [w Hval_headS0']. + iDestruct (hist_repr_peek_1 with "[$Hrepr]") as "(@ & Hrepr)"; try done. + iDestruct "Hndata" as "#Hndata_head". + wp_load. + + destruct (next_from hist2 (bool_decide (is_Some fin2)) (S hpos0)) as [mℓ_next|] eqn:Hnext2. + + iDestruct "Hclose" as "[Hclose _]". + iEval (rewrite bool_decide_false //). + + iDestruct "Hnfinal" as "#Hnfinal_head". + iEval (rewrite bool_decide_false //) in "Hnfinal_head". + + iSpecialize ("Hrepr" with "[$]"). + iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU". + { iExists tpos2. by iFrameNamed. } + iModIntro. + clear fin2 vs2 Hvs tpos2 Hℓtpos ℓ_tail2 Hnext2. + + wp_pures. wp_load. wp_pures. + + wp_bind (CmpXchg _ _ _)%E. + iMod "AU" as "(%vs3 & %fin3 & (%γs' & Hγs' & %hist3 & %ℓ_head3 & %ℓ_tail3 & %hpos3 & %tpos3 & @) & Hclose)". + iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}". + iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist2◯") as %Hhist23. + destruct Hhist23 as [_ Hhist23]. + assert (Hhist13 : hist1 `prefix_of` hist3). + { by trans hist2. } + + destruct (decide (ℓ_head0 = ℓ_head3)) as [->|Hhead03]. + * iDestruct "Hclose" as "[_ Hclose]". + + wp_cmpxchg_suc. + + assert (Hℓhpos0'' : loc_at hist3 hpos0 = Some ℓ_head3). + { by eapply loc_at_prefix. } clear Hℓhpos0'. + iAssert ⌜hpos0 = hpos3⌝%I as %->. + { by iApply (loc_at_inj with "Hrepr"). } + + destruct (decide (length (vs3 ++ option_list fin3) = 1)) as [Hvs3|Hvs3]. + -- destruct fin3 eqn:Hfin3. + ++ assert (Hℓ_headS0'' : loc_at hist3 (S hpos3) = Some ℓ_headS0). + { by eapply loc_at_prefix. } clear Hℓ_headS0'. + assert (Hval_headS0'' : val_at hist3 (S hpos3) = Some w). + { by eapply val_at_prefix. } clear Hval_headS0'. + + simplify_eq/=. + destruct vs3; last first. + { rewrite length_app /= Nat.add_1_r in Hvs3. lia. } + + assert (length hist3 = S (S hpos3)). + { apply (f_equal length), symmetry in Hvs. + rewrite /= length_fmap length_drop in Hvs. lia. } + + iDestruct (hist_repr_peek_1 with "[$Hrepr]") as "(@ & Hrepr)"; try done. + iClear "Hnnext". + rewrite /next_from !andb_true_l [bool_decide (S _ = _)]bool_decide_true //=. + by iCombine "Hnfinal_head Hnfinal" gives "[_ %contra]". + ++ simplify_eq/=. rewrite app_nil_r in Hvs Hvs3. + + iMod (mono_nat_own_update (S hpos3) with "Hhpos●") as "[Hhpos● _]". { lia. } + iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ". + { iExists tpos3. iFrameNamed. + iPureIntro. repeat split; try done. + - by eapply loc_at_prefix. + - by rewrite /= fmap_drop /= -Nat.add_1_r -drop_drop -fmap_drop -Hvs app_nil_r. } + + iModIntro. wp_pures. + + assert (Hval_headS0'' : val_at hist3 (S hpos3) = Some w). + { by eapply val_at_prefix. } clear Hval_headS0'. + unfold val_at in Hval_headS0''. + destruct vs3; try done. + rewrite -[S hpos3]Nat.add_0_r -lookup_drop -fmap_drop -Hvs /= in Hval_headS0''. + by simplify_eq/=. + -- assert (S (S hpos3) ≠ length hist3). + { rewrite Hvs length_fmap length_drop in Hvs3. lia. } + + assert (queue_γs_dq hist3 hpos3 fin3 = DfracOwn 1) as ->. + { unfold queue_γs_dq. by repeat case_match. } + iMod (mono_nat_own_update (S hpos3) with "Hhpos●") as "[Hhpos● _]". { lia. } + iMod (hpos_weaken hist3 fin3 with "Hhpos●") as "Hhpos●". + iMod (hist_weaken hist3 (S hpos3) fin3 with "Hhist●") as "Hhist●". + + iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ". + { iExists tpos3. iFrameNamed. + iPureIntro. repeat split; try done. + - by eapply loc_at_prefix. + - rewrite -Nat.add_1_r -drop_drop fmap_drop -Hvs. + destruct fin3; last by rewrite /= !app_nil_r. + by destruct vs3. } + + iModIntro. wp_pures. + + assert (Hval_headS0'' : val_at hist3 (S hpos3) = Some w). + { by eapply val_at_prefix. } clear Hval_headS0'. + unfold val_at in Hval_headS0''. + rewrite -[S hpos3]Nat.add_0_r -lookup_drop -fmap_drop -Hvs in Hval_headS0''. + + destruct vs3; simplify_eq/=; last done. + by destruct fin3. + + * iDestruct "Hclose" as "[Hclose _]". + + wp_cmpxchg_fail. + + iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU". + { iExists tpos3. by iFrameNamed. } + + iModIntro. wp_pures. iApply ("IH" with "AU"). + + + iDestruct "Hclose" as "[_ Hclose]". + + destruct fin2 as [fin2|]; last done. simplify_eq/=. + assert (Hhist2 : length hist2 = S (S hpos0)). + { destruct (decide (length hist2 = S (S hpos0))); first done. + by rewrite /next_from bool_decide_false in Hnext2. } + assert (S hpos2 < length hist2). + { rewrite -(length_fmap snd). + apply lookup_lt_is_Some_1. + rewrite -[S hpos2]Nat.add_0_r -lookup_drop -fmap_drop -Hvs. + by destruct vs2, fin2. } + assert (hpos0 = hpos2) as -> by lia. + assert (Hvs2 : length vs2 = 0). + { apply eq_add_S. rewrite -Nat.add_1_r -(length_app _ [fin2]) Hvs length_fmap length_drop Hhist2. lia. } + destruct vs2; last done. clear Hvs2. + + iSpecialize ("Hrepr" with "[$]"). + iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ". + { iExists tpos2. by iFrameNamed. } + + iModIntro. clear tpos2 Hℓhpos Hℓtpos ℓ_tail2. + + wp_pures. wp_load. + rewrite /val_at in Hval_headS0'. + rewrite -[S hpos2]Nat.add_0_r -lookup_drop -fmap_drop -Hvs in Hval_headS0'. + simplify_eq/=. wp_pures. iApply "HΦ". + - apply loc_at_length in Hℓ_headS0 as Hhistlen. + rewrite drop_ge /= in Hvs; last lia. destruct vs1, fin1; try done. + simplify_eq/=. + + iDestruct "Hclose" as "[_ Hclose]". + iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ". + { iExists tpos1. iFrameNamed. iPureIntro. + rewrite drop_ge //=. lia. } + + iModIntro. wp_pures. iApply "HΦ". + Qed. + +End fin_queue. + +Definition fin_queue_hl := + {| fin_queue_spec.new := new; + fin_queue_spec.enqueue := enqueue; + fin_queue_spec.finalize := finalize; + fin_queue_spec.try_dequeue := try_dequeue; |}. + +Definition fin_queue_iris `{!heapGS Σ, !fin_queueG Σ} : fin_queue_spec.fin_queue_iris Σ fin_queue_hl. +Proof. + refine (FinQueueIris _ _ + fin_queue_hl _ _ _ _ _ + queue_fin_obtain + queue_fin_agree + new_spec + enqueue_spec + finalize_spec + try_dequeue_spec). +Defined. + +#[global] Typeclasses Opaque queue_repr queue_fin. diff --git a/theories/fin_queue_spec.v b/theories/fin_queue_spec.v new file mode 100644 index 0000000..f7e0886 --- /dev/null +++ b/theories/fin_queue_spec.v @@ -0,0 +1,67 @@ +From iris.program_logic Require Import atomic. +From iris.heap_lang Require Import notation proofmode. + +From lmpmc Require Import util. + +(* Doing this split because I don't know how to otherwise get a nice + closed proof. *) + +Record fin_queue_hl := + FinQueueHl + { new : val; + enqueue : val; + finalize : val; + try_dequeue : val;}. +Record fin_queue_iris {Σ} `{!heapGS Σ} (hl : fin_queue_hl) := + FinQueueIris + { (** If [⊢ queue_repr ℓ vs mfin], then there is a queue at [ℓ] + which currently holds the values [vs], and possibly a final + value [mfin]. The dequeue and enqueue operations work in + FIFO fashion, with [head vs] (if any) representing the next + value that would be dequeued by a [try_dequeue ℓ] operation. + + Only non-finalized queues can be enqueued in. Non-finalized queues + can be finalized using the [finalize ℓ v] operation, which sets + [mfin] to [v]. Subsequent [try_dequeue ℓ] operations then first + dequeue the remainder of [vs]; when [vs] is empty, they return [mfin] + (but, critically, do not unset it). *) + queue_repr : loc → list val → option val → iProp Σ; + #[global] queue_repr_timeless ℓ vs mfin :: Timeless (queue_repr ℓ vs mfin); + + (** If [⊢ queue_fin ℓ v], then the queue at [ℓ] has been + finalized and all elements except for the final element [v] + have been dequeued. + + Queues that enter this state never leave this state; this + allows [queue_fin ℓ v] to be a persistent proposition. *) + queue_fin : loc → val → iProp Σ; + #[global] queue_fin_persistent ℓ v :: Persistent (queue_fin ℓ v); + #[global] queue_fin_timeless ℓ v :: Timeless (queue_fin ℓ v); + queue_fin_obtain ℓ fin : queue_repr ℓ [] (Some fin) -∗ queue_fin ℓ fin; + queue_fin_agree ℓ vs fin mfin : + queue_fin ℓ fin -∗ + queue_repr ℓ vs mfin -∗ + ⌜vs = []⌝ ∗ ⌜mfin = Some fin⌝; + + new_spec : + {{{ True }}} + hl.(new) #() + {{{ (ℓ : loc), RET #ℓ; queue_repr ℓ [] None }}}; + + enqueue_spec (ℓ_q : loc) (data : val) : + ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>> + hl.(enqueue) #ℓ_q data @ ∅ + <<{ queue_repr ℓ_q (vs ++ [data]) None | RET #() }>>; + + finalize_spec (ℓ_q : loc) (data : val) : + ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>> + hl.(finalize) #ℓ_q data @ ∅ + <<{ queue_repr ℓ_q vs (Some data) | RET #() }>>; + + try_dequeue_spec (ℓ_q : loc) : + ⊢ <<{ ∀∀ vs mfin, queue_repr ℓ_q vs mfin }>> + hl.(try_dequeue) #ℓ_q @ ∅ + <<{ queue_repr ℓ_q (tail vs) mfin + | RET (if head vs is Some v then InjLV v else InjRV (val_opt_hl mfin)) }>>; + }. +#[global] Arguments fin_queue_iris _ {_} _ : assert. diff --git a/theories/lmpmc_blocking_dequeue.v b/theories/lmpmc_blocking_dequeue.v new file mode 100644 index 0000000..5051c6a --- /dev/null +++ b/theories/lmpmc_blocking_dequeue.v @@ -0,0 +1,40 @@ +From iris.program_logic Require Import atomic. +From iris.heap_lang Require Import notation proofmode. + +From lmpmc Require Import lmpmc_queue_spec util. + +Section lmpmc_blocking. + Context (lq : lmpmc_queue_spec.lmpmc_queue_hl). + + (* https://types.pl/@pigworker/115629120124299549 *) + Definition dequeue : val := rec: "go" "ℓ_deq" := + match: lq.(try_dequeue) "ℓ_deq" with + NONE => "go" "ℓ_deq" + | SOME "v" => "v" + end. + + Section proofs. + Context `{heapGS Σ} (lqp : lmpmc_queue_spec.lmpmc_queue_iris Σ lq). + + Lemma dequeue_spec (ℓ_deq : loc) : + ⊢ <<{ ∀∀ ℓ_enq cvs, lqp.(queue_repr lq) ℓ_deq ℓ_enq cvs }>> + dequeue #ℓ_deq @ ∅ + <<{ ∃∃ cv cvs', ⌜cvs = cv :: cvs'⌝ ∗ lqp.(queue_repr lq) ℓ_deq ℓ_enq cvs' | RET cv }>>. + Proof. + iIntros (Φ) "AU". iLöb as "IH". wp_rec. + awp_apply lqp.(try_dequeue_spec lq). + rewrite /atomic_acc /=. + iMod "AU" as "(%ℓ_enq & %cvs & Hcvs & Hclose)". + iFrame. iModIntro. iSplit; iIntros "Hrepr". + - by iMod ("Hclose" with "Hrepr") as "AU". + - destruct cvs as [|cv cvs']; simplify_list_eq. + + iMod ("Hclose" with "Hrepr") as "AU". iModIntro. + wp_pures. by iApply "IH". + + iDestruct "Hclose" as "[_ Hclose]". + iMod ("Hclose" $! cv cvs' with "[$Hrepr //]") as "HΦ". + iModIntro. by wp_pures. + Qed. + + End proofs. + +End lmpmc_blocking. diff --git a/theories/lmpmc_queue_proof.v b/theories/lmpmc_queue_proof.v new file mode 100644 index 0000000..fa732cc --- /dev/null +++ b/theories/lmpmc_queue_proof.v @@ -0,0 +1,362 @@ +From iris.program_logic Require Import atomic. +From iris.heap_lang Require Import notation proofmode. +From iris.algebra.lib Require Import excl_auth. +From iris.base_logic.lib Require Import invariants. +From iris.base_logic.lib Require Import invariants mono_nat mono_list. +From iris_named_props Require Import custom_syntax. + +From lmpmc Require fin_queue_spec lmpmc_queue_spec. +From lmpmc Require Import upstream util. + +Section lmpmc_queue. + Context {fq : fin_queue_spec.fin_queue_hl}. + + Definition new : val := λ: <>, + let: "ℓ_q" := fq.(fin_queue_spec.new) #() in ("ℓ_q", "ℓ_q"). + + Definition enqueue : val := (* passing arguments [ℓ_enq data] *) + fq.(fin_queue_spec.enqueue). + + Definition try_dequeue : val := rec: "go" "ℓ_q" := + match: fq.(fin_queue_spec.try_dequeue) "ℓ_q" with + InjL "v" => + SOME "v" + | InjR "mℓ_nextq" => + match: "mℓ_nextq" with + NONE => NONE + | SOME "ℓ_nextq" => "go" "ℓ_nextq" + end + end. + + Definition link : val := (* passing arguments [ℓ_enq1 ℓ_deq2] *) + fq.(fin_queue_spec.finalize). + + Section proofs. + Context `{!heapGS Σ} {fqp : fin_queue_spec.fin_queue_iris Σ fq}. + + Record node := Node { ℓ_node : loc; vs_node : list val }. + Add Printing Constructor node. + Definition linked_single_queue_repr (n : node) (mℓ_nextq : option loc) : iProp Σ := + fqp.(fin_queue_spec.queue_repr fq) n.(ℓ_node) n.(vs_node) (loc_to_val <$> mℓ_nextq). + + Definition chain := list node. + Definition queue_repr ℓ_deq ℓ_enq (cvs : list val) : iProp Σ := + ∃ (c : chain), + ⌜length c > 0⌝ ∗ ⌜ℓ_node <$> head c = Some ℓ_deq⌝ ∗ + ⌜ℓ_node <$> last c = Some ℓ_enq⌝ ∗ ⌜cvs = c ≫= vs_node⌝ ∗ + [∗ list] i ↦ l ∈ c, linked_single_queue_repr l (ℓ_node <$> c !! S i). + + #[global] Instance queue_repr_timeless ℓ_deq ℓ_enq cvs : Timeless (queue_repr ℓ_deq ℓ_enq cvs) := _. + + Lemma new_spec : + {{{ True }}} + new #() + {{{ (ℓ_deq ℓ_enq : loc), RET (#ℓ_deq, #ℓ_enq); queue_repr ℓ_deq ℓ_enq [] }}}. + Proof. + iIntros (Φ _) "HΦ". iUnfold new. wp_pures. + wp_apply (fqp.(fin_queue_spec.new_spec fq) with "[//]"). + iIntros (ℓ) "H". wp_pures. iModIntro. iApply "HΦ". + unfold queue_repr. iExists [Node ℓ []]. + iFrame. iSimplifyEq. by iSplit; first (iPureIntro; lia). + Qed. + + Lemma enqueue_spec (ℓ_enq : loc) (data : val) : + ⊢ <<{ ∀∀ ℓ_deq cvs, queue_repr ℓ_deq ℓ_enq cvs }>> + enqueue #ℓ_enq data @ ∅ + <<{ queue_repr ℓ_deq ℓ_enq (cvs ++ [data]) | RET #() }>>. + Proof. + iIntros "%Φ AU". iUnfold enqueue. + + wp_bind (fin_queue_spec.enqueue _ _ _)%E. + awp_apply fqp.(fin_queue_spec.enqueue_spec fq). + rewrite /atomic_acc /=. + iMod "AU" as "(%ℓ_deq & %cvs & (%c & %Hclen & %Hhead & %Hlast & %Hcvs & Hqs) & Hclose)". + iModIntro. + + destruct (last c) as [n_last|] eqn:Hlastn; last done. + iExists n_last.(vs_node). + + apply last_Some in Hlastn as [c' ->]. + iDestruct (big_sepL_insert_acc _ _ (length c') with "Hqs") as "[Hnode Hrepr]". + { by rewrite lookup_app_r // Nat.sub_diag. } + iSimplifyEq. iUnfold linked_single_queue_repr in "Hnode". + + rewrite lookup_app_r; last lia. + replace (S (length c') - length c') with 1 by lia. + simplify_eq/=. iFrame. + + iSplit. + - iDestruct "Hclose" as "[Hclose _]". + iIntros "Hnode". + iDestruct ("Hrepr" with "[Hnode //]") as "Hrepr". + rewrite list_insert_id; last first. + { by rewrite lookup_app_r // Nat.sub_diag. } + iMod ("Hclose" with "[$Hrepr]") as "AU". + { by rewrite last_snoc. } + done. + - iDestruct "Hclose" as "[_ Hclose]". + iIntros "Hnode". + + set n_last' := Node n_last.(ℓ_node) (n_last.(vs_node) ++ [data]). + set c := c' ++ [n_last']. + + iDestruct ("Hrepr" with "[Hnode]") as "Hrepr". + { rewrite /linked_single_queue_repr /=. + replace (ℓ_node n_last) with n_last'.(ℓ_node) by done. + by replace (vs_node n_last ++ [data]) with n_last'.(vs_node). } + + iMod ("Hclose" with "[Hrepr]") as "HΦ". + { unfold queue_repr. iExists c. repeat iSplit; try done. + - iPureIntro. rewrite length_app /=. lia. + - iPureIntro. rewrite /c. by destruct c'; simplify_eq/=. + - iPureIntro. by rewrite /c last_snoc. + - iPureIntro. by rewrite /c !bind_app /= !app_nil_r app_assoc. + - rewrite insert_app_r_alt // Nat.sub_diag /=. + iApply (big_sepL_mono with "Hrepr"). + { iIntros (i n Hi) "Hrepr". + rewrite -list_lookup_fmap fmap_app. + replace (ℓ_node <$> [n_last]) with (ℓ_node <$> [n_last']) by done. + by rewrite -fmap_app list_lookup_fmap. } } + + iModIntro. iApply "HΦ". + Qed. + + Lemma try_dequeue_spec (ℓ_deq : loc) : + ⊢ <<{ ∀∀ ℓ_enq cvs, queue_repr ℓ_deq ℓ_enq cvs }>> + try_dequeue #ℓ_deq @ ∅ + <<{ queue_repr ℓ_deq ℓ_enq (tail cvs) | RET (val_opt_hl (head cvs)) }>>. + Proof. + revert ℓ_deq. iLöb as "IH". iIntros (ℓ_deq Φ) "AU". wp_rec. + + awp_apply (fqp.(fin_queue_spec.try_dequeue_spec fq)). + rewrite /atomic_acc /=. + iMod "AU" as "(%ℓ_enq & %cvs & (%c & %Hclen & %Hhead & %Hlast & %Hcvs & Hqs) & Hclose)". iModIntro. + + destruct c as [|n_head c']; first done. + iDestruct (big_sepL_cons with "Hqs") as "[Hnode Hqs]". + simpl. destruct (c' !! 0) as [n_next|] eqn:Hnextq. + - iExists n_head.(vs_node), (Some #n_next.(ℓ_node)). iSplitL "Hnode"; last iSplit. + + simplify_eq/=. by rewrite /linked_single_queue_repr /=. + + simplify_eq/=. iIntros "Hnode". iDestruct "Hclose" as "[Hclose _]". + pose c := n_head :: c'. + iAssert (linked_single_queue_repr n_head (ℓ_node <$> c !! S 0)) with "[Hnode]" as "Hnode". + { by rewrite /linked_single_queue_repr /= Hnextq. } + iAssert ([∗ list] i↦n ∈ c', linked_single_queue_repr n (ℓ_node <$> c !! S (S i)))%I with "[Hqs //]" as "Hqs". + iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hnode Hqs]" as "Hqs". + { iApply big_sepL_cons. iFrame. } + iAssert (queue_repr n_head.(ℓ_node) ℓ_enq (vs_node n_head ++ c' ≫= vs_node)) with "[$Hqs //]" as "Hrepr". + by iMod ("Hclose" with "Hrepr") as "Hrepr". + + simplify_eq/=. iIntros "Hnode". + destruct n_head.(vs_node) as [|x vs_head'] eqn:Hvs_head. + * simplify_eq/=. iDestruct "Hclose" as "[Hclose _]". + + iDestruct (fqp.(fin_queue_spec.queue_fin_obtain fq) with "Hnode") as "#Hfin". + + pose c := n_head :: c'. + iAssert (linked_single_queue_repr n_head (ℓ_node <$> c !! S 0)) with "[Hnode]" as "Hnode". + { by rewrite /linked_single_queue_repr /= Hnextq Hvs_head /=. } + iAssert ([∗ list] i↦n ∈ c', linked_single_queue_repr n (ℓ_node <$> c !! S (S i)))%I with "[Hqs //]" as "Hqs". + iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hnode Hqs]" as "Hqs". + { iApply big_sepL_cons. iFrame. } + iAssert (queue_repr n_head.(ℓ_node) ℓ_enq (vs_node n_head ++ c' ≫= vs_node)) with "[$Hqs //]" as "Hrepr". + rewrite Hvs_head /=. iMod ("Hclose" with "Hrepr") as "AU". iModIntro. wp_pures. + clear c c' Hclen Hlast Hnextq Hvs_head. + + awp_apply "IH". rewrite /atomic_acc /=. + iMod "AU" as "(%ℓ_enq' & %cvs' & (%c'' & _ & %Hhead' & %Hlast' & %Hcvs' & Hqs') & Hclose)". + destruct c'' as [|n_head' c'']; first done. + iDestruct (big_sepL_cons with "Hqs'") as "[Hq0 Hqs']". simplify_eq/=. + iEval (rewrite /linked_single_queue_repr /=) in "Hq0". + rewrite -Hhead'. + iDestruct (fqp.(fin_queue_spec.queue_fin_agree fq) with "Hfin Hq0") as %[Hhead Hc'']. + destruct (c'' !! 0) as [n_next'|] eqn:Hc''head; last done. simplify_eq/=. + rewrite -Hc''. clear Hhead' Hc'' n_next n_head. + assert (Hc''len : length c'' > 0). { by apply lookup_lt_Some in Hc''head. } + + iAssert (queue_repr n_next'.(ℓ_node) ℓ_enq' (c'' ≫= vs_node)) with "[$Hqs']" as "Hrepr'". + { iPureIntro. repeat split; try done. + - by rewrite head_lookup Hc''head. + - enough (last c'' = last (n_head' :: c'')) as ->; first done. + destruct c''; first done. by rewrite last_cons_cons. } + + iModIntro. iFrame. iSplit. + -- iIntros "(%d & %Hdlen & %Hdhead & %Hdlast & %Hdvs & Hrepr)". + rewrite Hhead /=. simplify_eq/=. + pose c := n_head' :: d. + iAssert (linked_single_queue_repr n_head' (ℓ_node <$> c !! S 0)) with "[Hq0]" as "Hq0". + { by rewrite /linked_single_queue_repr /= Hhead /= -head_lookup Hdhead /=. } + iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hq0 Hrepr]" as "Hrepr". + { iApply big_sepL_cons. iFrame. } + iAssert (queue_repr (ℓ_node n_head') ℓ_enq' (c'' ≫= vs_node)) with "[$Hrepr]" as "Hrepr". + { iPureIntro. repeat split; try done. + - unfold c. simpl. lia. + - unfold c. rewrite -Hdlast. by destruct d. + - unfold c. rewrite Hdvs. simplify_eq/=. + by rewrite Hhead. } + by iMod ("Hclose" with "Hrepr") as "AU". + -- iIntros "(%d & %Hdlen & %Hdhead & %Hdlast & %Hdvs & Hrepr)". + rewrite Hhead /=. simplify_eq/=. + pose c := n_head' :: d. + iAssert (linked_single_queue_repr n_head' (ℓ_node <$> c !! S 0)) with "[Hq0]" as "Hq0". + { by rewrite /linked_single_queue_repr /= Hhead /= -head_lookup Hdhead /=. } + iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hq0 Hrepr]" as "Hrepr". + { iApply big_sepL_cons. iFrame. } + iAssert (queue_repr (ℓ_node n_head') ℓ_enq' (tail (c'' ≫= vs_node))) with "[$Hrepr]" as "Hrepr". + { iPureIntro. repeat split; try done. + - unfold c. simpl. lia. + - unfold c. rewrite -Hdlast. by destruct d. + - unfold c. rewrite Hdvs. simplify_eq/=. + by rewrite Hhead. } + by iMod ("Hclose" with "Hrepr") as "AU". + * simplify_eq/=. iDestruct "Hclose" as "[_ Hclose]". + + pose n_head' := Node (ℓ_node n_head) vs_head'. + pose c := n_head' :: c'. + + iAssert (linked_single_queue_repr n_head' (ℓ_node <$> c !! S 0)) with "[Hnode]" as "Hnode". + { by rewrite /linked_single_queue_repr /= Hnextq /=. } + iAssert ([∗ list] i↦n ∈ c', linked_single_queue_repr n (ℓ_node <$> c !! S (S i)))%I with "[Hqs //]" as "Hqs". + iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hnode Hqs]" as "Hqs". + { iApply big_sepL_cons. iFrame. } + iAssert (queue_repr n_head.(ℓ_node) ℓ_enq (vs_node n_head' ++ c' ≫= vs_node)) with "[$Hqs]" as "Hrepr". + { iPureIntro. repeat split; try done. by destruct c'. } + + iMod ("Hclose" with "Hrepr") as "Hrepr". + iModIntro. wp_pures. iApply "Hrepr". + - destruct c'; last done. simplify_eq/=. iClear "Hqs". + rewrite app_nil_r. clear Hclen. + iExists n_head.(vs_node), None. iSplitL "Hnode". + + by rewrite /linked_single_queue_repr /=. + + iSplit. + * iIntros "Hrepr". iDestruct "Hclose" as "[Hclose _]". + iMod ("Hclose" with "[Hrepr]") as "AU". + { iExists [n_head]. iFrame. + repeat iSplit; try done. + - iPureIntro. simpl. lia. + - simpl. by rewrite app_nil_r. } + done. + * iIntros "Hrepr". iDestruct "Hclose" as "[_ Hclose]". + set n_head' := Node n_head.(ℓ_node) (tail n_head.(vs_node)). + iMod ("Hclose" with "[Hrepr]") as "HΦ". + { iExists [n_head']. iFrame. + repeat iSplit; try done. + - iPureIntro. simpl. lia. + - simpl. by rewrite app_nil_r. } + destruct n_head.(vs_node) as [|v vs']; + iModIntro; wp_pures; iApply "HΦ". + Qed. + + (** Linking two queues: + * _______________ _______________ + * / Q1 \ / Q2 \ + * ℓ_deq1 ... ℓ_enq1 <> ℓ_deq2 ... ℓ_enq2 + * \ \ link op args / / + * \ \____________/ / + * \ Q1 <> Q2 / + * \______________________________/ + *) + Lemma link_spec (ℓ_enq1 ℓ_deq2 : loc) : + ⊢ <<{ ∀∀ (b : bool) ℓ_deq1 ℓ_enq2 cvs1 cvs2, queue_repr ℓ_deq1 ℓ_enq1 cvs1 ∗ + if b then queue_repr ℓ_deq2 ℓ_enq2 cvs2 else ⌜ℓ_deq1 = ℓ_deq2 ∧ ℓ_enq1 = ℓ_enq2⌝ }>> + link #ℓ_enq1 #ℓ_deq2 @ ∅ + <<{ if b then queue_repr ℓ_deq1 ℓ_enq2 (cvs1 ++ cvs2) else True | RET #() }>>. + Proof. + iIntros "%Φ AU". iUnfold link. + + wp_bind (fin_queue_spec.finalize _ _ _)%E. + awp_apply fqp.(fin_queue_spec.finalize_spec fq). + rewrite /atomic_acc /=. + iMod "AU" as (b ℓ_deq1 ℓ_enq2 cvs1 cvs2) "[[(%c1 & %Hclen1 & %Hhead1 & %Hlast1 & %Hcvs1 & Hqs1) Hqs2] Hclose]". + iModIntro. + + destruct (last c1) as [n_last1|] eqn:Hlastn1; last done. + iExists n_last1.(vs_node). + + apply last_Some in Hlastn1 as [c1' ->]. + iDestruct (big_sepL_app with "Hqs1") as "[Hqs1 Hnode]". + iSimplifyEq. iDestruct "Hnode" as "[Hnode _]". + rewrite Nat.add_0_r. + + rewrite lookup_ge_None_2 /=; last first. + { rewrite length_app /=. lia. } + iUnfold linked_single_queue_repr in "Hnode". + iSimplifyEq. iFrame. + + iSplit. + - iDestruct "Hclose" as "[Hclose _]". + iIntros "Hnode". + + iAssert (linked_single_queue_repr n_last1 (ℓ_node <$> (c1' ++ [n_last1]) !! S (length c1'))) with "[Hnode]" as "Hnode". + { rewrite /linked_single_queue_repr !lookup_app_r; last lia. + by assert (S (length c1') - length c1' = 1) as -> by lia. } + + iDestruct (big_sepL_snoc with "[$Hqs1 $Hnode]") as "Hqs1'". + + iPoseProof ("Hclose" with "[$Hqs1' $Hqs2]") as "Hqs". + { iPureIntro. repeat split; try done. by rewrite last_app. } + done. + + - iDestruct "Hclose" as "[_ Hclose]". + iIntros "Hnode". + + destruct b; last by iApply "Hclose". + iDestruct "Hqs2" as "(%c2 & %Hclen2 & %Hhead2 & %Hlast2 & %Hcvs2 & Hqs2)". + + pose c := (c1' ++ [n_last1]) ++ c2. + + iAssert (linked_single_queue_repr n_last1 (ℓ_node <$> c !! S (length c1'))) with "[Hnode]" as "Hnode". + { rewrite /linked_single_queue_repr /c !lookup_app_r; try (rewrite length_app /=; lia). + rewrite length_app /=. assert (S (length c1') - (length c1' + 1) = 0) as -> by lia. + rewrite -head_lookup Hhead2 //=. } + + iDestruct (big_sepL_mono with "Hqs1") as "Hqs1". + { iIntros (i l Hi) "Hrepr". + iAssert (linked_single_queue_repr l (ℓ_node <$> c !! S i))%I with "[Hrepr]" as "Hrepr". + { rewrite /c lookup_app_l // length_app /=. apply lookup_lt_Some in Hi. lia. } + iExact "Hrepr". } + + iDestruct (big_sepL_snoc with "[$Hqs1 $Hnode]") as "Hqs1'". + + iDestruct (big_sepL_mono with "Hqs2") as "Hqs2". + { iIntros (i l Hi) "Hrepr". + iAssert (linked_single_queue_repr l (ℓ_node <$> c !! S (length (c1' ++ [n_last1]) + i)))%I with "[Hrepr]" as "Hrepr". + { rewrite /c length_app /= lookup_app_r length_app /=; last lia. + by assert (S i = S (length c1' + 1 + i) - (length c1' + 1)) as -> by lia. } + iExact "Hrepr". } + iSimplifyEq. + + iDestruct (big_sepL_app with "[$Hqs1' $Hqs2]") as "Hqs". fold c. + rewrite -bind_app -/c. + iMod ("Hclose" with "[Hqs]") as "HΦ". + { iFrame. iPureIntro. repeat split; try done. + - rewrite /c !length_app /=. lia. + - rewrite /c head_app. case_match; last done. congruence. + - rewrite /c last_app. case_match; last done. congruence. } + iModIntro. iApply "HΦ". + Qed. + + End proofs. + +End lmpmc_queue. + +Definition lmpmc_queue_hl (fq : fin_queue_spec.fin_queue_hl) : lmpmc_queue_spec.lmpmc_queue_hl. +Proof. + by refine {| lmpmc_queue_spec.new := new; + lmpmc_queue_spec.enqueue := enqueue; + lmpmc_queue_spec.try_dequeue := try_dequeue; + lmpmc_queue_spec.link := link |}. +Defined. + +Definition lmpmc_queue_iris `{!heapGS Σ} + (fq : fin_queue_spec.fin_queue_hl) + (fqp : fin_queue_spec.fin_queue_iris Σ fq) : lmpmc_queue_spec.lmpmc_queue_iris Σ (lmpmc_queue_hl fq). +Proof. + by refine (lmpmc_queue_spec.LmpmcQueueIris _ _ + (lmpmc_queue_hl fq) _ _ + new_spec + enqueue_spec + try_dequeue_spec + link_spec). +Defined. + +#[global] Typeclasses Opaque queue_repr. diff --git a/theories/lmpmc_queue_spec.v b/theories/lmpmc_queue_spec.v new file mode 100644 index 0000000..0ea3a4a --- /dev/null +++ b/theories/lmpmc_queue_spec.v @@ -0,0 +1,49 @@ +From iris.program_logic Require Import atomic. +From iris.heap_lang Require Import notation proofmode. + +From lmpmc Require Import util. + +Record lmpmc_queue_hl := + LmpmcQueueHl + { new : val; + enqueue : val; + try_dequeue : val; + link : val; + }. + +Record lmpmc_queue_iris {Σ} `{!heapGS Σ} (hl : lmpmc_queue_hl) := + LmpmcQueueIris + { queue_repr : loc → loc → list val → iProp Σ; + #[global] queue_repr_timeless ℓ_deq ℓ_enq vs :: Timeless (queue_repr ℓ_deq ℓ_enq vs); + + new_spec : + {{{ True }}} + hl.(new) #() + {{{ (ℓ_deq ℓ_enq : loc), RET (#ℓ_deq, #ℓ_enq); queue_repr ℓ_deq ℓ_enq [] }}}; + + enqueue_spec (ℓ_enq : loc) (data : val) : + ⊢ <<{ ∀∀ ℓ_deq cvs, queue_repr ℓ_deq ℓ_enq cvs }>> + hl.(enqueue) #ℓ_enq data @ ∅ + <<{ queue_repr ℓ_deq ℓ_enq (cvs ++ [data]) | RET #() }>>; + + try_dequeue_spec (ℓ_deq : loc) : + ⊢ <<{ ∀∀ ℓ_enq cvs, queue_repr ℓ_deq ℓ_enq cvs }>> + hl.(try_dequeue) #ℓ_deq @ ∅ + <<{ queue_repr ℓ_deq ℓ_enq (tail cvs) | RET (val_opt_hl (head cvs)) }>>; + + (** Linking two queues: + * _______________ _______________ + * / Q1 \ / Q2 \ + * ℓ_deq1 ... ℓ_enq1 <> ℓ_deq2 ... ℓ_enq2 + * \ \ link op args / / + * \ \____________/ / + * \ Q1 <> Q2 / + * \______________________________/ + *) + link_spec (ℓ_enq1 ℓ_deq2 : loc) : + ⊢ <<{ ∀∀ (b : bool) ℓ_deq1 ℓ_enq2 cvs1 cvs2, queue_repr ℓ_deq1 ℓ_enq1 cvs1 ∗ + if b then queue_repr ℓ_deq2 ℓ_enq2 cvs2 else ⌜ℓ_deq1 = ℓ_deq2 ∧ ℓ_enq1 = ℓ_enq2⌝ }>> + hl.(link) #ℓ_enq1 #ℓ_deq2 @ ∅ + <<{ if b then queue_repr ℓ_deq1 ℓ_enq2 (cvs1 ++ cvs2) else True | RET #() }>>; + }. +#[global] Arguments lmpmc_queue_iris _ {_} _ : assert. diff --git a/theories/upstream.v b/theories/upstream.v new file mode 100644 index 0000000..b74add5 --- /dev/null +++ b/theories/upstream.v @@ -0,0 +1,60 @@ +From stdpp Require Import prelude ssreflect gmultiset. +From stdpp Require Import options. + +Lemma prefix_of_fmap {A B} (f : A → B) (xs xs' : list A) : + xs `prefix_of` xs' → + f <$> xs `prefix_of` f <$> xs'. +Proof. intros [ys ->]. exists (f <$> ys). apply fmap_app. Qed. + +Lemma prefix_sublist {A} (l1 l2 : list A) : l1 `prefix_of` l2 → l1 `sublist_of` l2. +Proof. intros [k ->]. by apply sublist_inserts_r. Qed. + +Lemma prefix_submseteq {A} (l1 l2 : list A) : l1 `prefix_of` l2 → l1 ⊆+ l2. +Proof. intros [k ->]. by apply submseteq_inserts_r. Qed. + +Lemma take_less_prefix {A} n m (xs : list A) : n ≤ m → take n xs `prefix_of` take m xs. +Proof. + intros Hnm. + replace n with (n `min` m); last lia. + rewrite -take_take. + apply prefix_take. +Qed. + +Lemma take_app_prefix {A} n (xs ys : list A) : take n xs `prefix_of` take n (xs ++ ys). +Proof. unfold prefix. exists (take (n - length xs) ys). apply firstn_app. Qed. + +Lemma Forall_prefix {A} (xs xs' : list A) Φ : xs `prefix_of` xs' → Forall Φ xs' → Forall Φ xs. +Proof. by intros [? ->] [? _]%Forall_app. Qed. + +Lemma drop_cons_inv {A} n x (xs xs' : list A) : + drop n xs = x :: xs' → xs !! n = Some x ∧ drop (S n) xs = xs'. +Proof. + intros Hxs. split. + - by rewrite -[n]Nat.add_0_r -lookup_drop Hxs. + - by rewrite -Nat.add_1_r -drop_drop Hxs. +Qed. + +Lemma list_to_set_disj_size `{Countable A} (l : list A) : + size (list_to_set_disj l : gmultiset A) = length l. +Proof. + induction l; first done. + by rewrite /= gmultiset_size_disj_union IHl gmultiset_size_singleton. +Qed. + +Lemma gmultiset_subseteq_size_eq `{Countable A, LeibnizEquiv A} (X Y : gmultiset A) : + X ⊆ Y → size Y ≤ size X → X = Y. +Proof. + revert Y. induction X using gmultiset_ind; intros Y HY Hsize. + - rewrite gmultiset_size_empty in Hsize. + apply symmetry, gmultiset_size_empty_inv. lia. + - rewrite gmultiset_size_disj_union gmultiset_size_singleton in Hsize. + assert (X ⊆ Y ∖ {[+ x +]}) as HXY%IHX; [multiset_solver..|]. + rewrite gmultiset_size_difference; last multiset_solver. + rewrite gmultiset_size_singleton. lia. +Qed. + +Lemma elements_list_to_set_disj_perm `{Countable A} (l : list A) : l ≡ₚ elements (list_to_set_disj l : gmultiset A). +Proof. + induction l; first done. + by rewrite list_to_set_disj_cons gmultiset_elements_disj_union gmultiset_elements_singleton -IHl. +Qed. diff --git a/theories/util.v b/theories/util.v new file mode 100644 index 0000000..c718622 --- /dev/null +++ b/theories/util.v @@ -0,0 +1,12 @@ +From iris.heap_lang Require Import notation. + +Definition loc_to_val (ℓ : loc) : val := #ℓ. +Definition val_opt_hl (mv : option val) : val := + match mv with + | None => NONEV + | Some v => SOMEV v + end. +Definition loc_opt_hl : option loc → val := + val_opt_hl ∘ fmap loc_to_val. +Arguments loc_to_val _ / : assert. +Arguments loc_opt_hl !_ / : assert. -- cgit v1.3