summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.envrc1
-rw-r--r--.gitignore17
-rw-r--r--Makefile55
-rw-r--r--_CoqProject12
-rw-r--r--flake.lock61
-rw-r--r--flake.nix44
-rw-r--r--theories/basic_queue_proof.v652
-rw-r--r--theories/basic_queue_spec.v30
-rw-r--r--theories/example.v723
-rw-r--r--theories/fin_queue_proof.v932
-rw-r--r--theories/fin_queue_spec.v67
-rw-r--r--theories/lmpmc_blocking_dequeue.v40
-rw-r--r--theories/lmpmc_queue_proof.v362
-rw-r--r--theories/lmpmc_queue_spec.v49
-rw-r--r--theories/upstream.v60
-rw-r--r--theories/util.v12
16 files changed, 3117 insertions, 0 deletions
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 @@
1*.aux
2*.glob
3*.vio
4*.vo
5*.vok
6*.vos
7.CoqMakefile.d
8.Makefile.coq.d
9.direnv
10.lia.cache
11Makefile.coq
12Makefile.coq.conf
13*#*.v#
14*#*.vok#
15*~
16.#*
17\#*#
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..ac8dba0
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,55 @@
1# Default target
2all: Makefile.coq
3 +@$(MAKE) -f Makefile.coq all
4.PHONY: all
5
6# Permit local customization
7-include Makefile.local
8
9# Forward most targets to Coq makefile (with some trick to make this phony)
10%: Makefile.coq phony
11 @#echo "Forwarding $@"
12 +@$(MAKE) -f Makefile.coq $@
13phony: ;
14.PHONY: phony
15
16clean: Makefile.coq
17 +@$(MAKE) -f Makefile.coq clean
18 @# Make sure not to enter the `_opam` folder.
19 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
20 rm -f Makefile.coq .lia.cache builddep/*
21.PHONY: clean
22
23# Create Coq Makefile.
24Makefile.coq: _CoqProject Makefile
25 "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
26
27# Install build-dependencies
28OPAMFILES=$(wildcard *.opam)
29BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
30
31builddep/%-builddep.opam: %.opam Makefile
32 @echo "# Creating builddep package for $<."
33 @mkdir -p builddep
34 @sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
35
36builddep-opamfiles: $(BUILDDEPFILES)
37.PHONY: builddep-opamfiles
38
39builddep: builddep-opamfiles
40 @# We want opam to not just install the build-deps now, but to also keep satisfying these
41 @# constraints. Otherwise, `opam upgrade` may well update some packages to versions
42 @# that are incompatible with our build requirements.
43 @# To achieve this, we create a fake opam package that has our build-dependencies as
44 @# dependencies, but does not actually install anything itself.
45 @echo "# Installing builddep packages."
46 @opam install $(OPAMFLAGS) $(BUILDDEPFILES)
47.PHONY: builddep
48
49# Backwards compatibility target
50build-dep: builddep
51.PHONY: build-dep
52
53# Some files that do *not* need to be forwarded to Makefile.coq.
54# ("::" lets Makefile.local overwrite this.)
55Makefile 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 @@
1-Q theories lmpmc
2
3theories/util.v
4theories/upstream.v
5theories/basic_queue_spec.v
6theories/fin_queue_spec.v
7theories/lmpmc_queue_spec.v
8theories/basic_queue_proof.v
9theories/fin_queue_proof.v
10theories/lmpmc_queue_proof.v
11theories/lmpmc_blocking_dequeue.v
12theories/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 @@
1{
2 "nodes": {
3 "flake-utils": {
4 "inputs": {
5 "systems": "systems"
6 },
7 "locked": {
8 "lastModified": 1731533236,
9 "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
10 "owner": "numtide",
11 "repo": "flake-utils",
12 "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
13 "type": "github"
14 },
15 "original": {
16 "owner": "numtide",
17 "repo": "flake-utils",
18 "type": "github"
19 }
20 },
21 "nixpkgs": {
22 "locked": {
23 "lastModified": 1777077449,
24 "narHash": "sha256-AIiMJiqvGrN4HyLEbKAoCSRRYn0rnlW5VbKNIMIYqm4=",
25 "owner": "NixOS",
26 "repo": "nixpkgs",
27 "rev": "a4bf06618f0b5ee50f14ed8f0da77d34ecc19160",
28 "type": "github"
29 },
30 "original": {
31 "owner": "NixOS",
32 "ref": "nixos-25.11",
33 "repo": "nixpkgs",
34 "type": "github"
35 }
36 },
37 "root": {
38 "inputs": {
39 "flake-utils": "flake-utils",
40 "nixpkgs": "nixpkgs"
41 }
42 },
43 "systems": {
44 "locked": {
45 "lastModified": 1681028828,
46 "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
47 "owner": "nix-systems",
48 "repo": "default",
49 "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
50 "type": "github"
51 },
52 "original": {
53 "owner": "nix-systems",
54 "repo": "default",
55 "type": "github"
56 }
57 }
58 },
59 "root": "root",
60 "version": 7
61}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..4fcc282
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,44 @@
1{
2 inputs = {
3 nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.11";
4 flake-utils.url = "github:numtide/flake-utils";
5 };
6
7 outputs = { self, nixpkgs, flake-utils, ... }:
8 flake-utils.lib.eachDefaultSystem (system:
9 let
10 pkgs = import nixpkgs { inherit system; };
11
12 # From 22-04-2026
13 stdpp = with pkgs; coqPackages.lib.overrideCoqDerivation {
14 version = "dev";
15 release."dev".sha256 = "hN+sEZcIaFoFF2+4dStTc0TRz5A03US6csEk5q0r/z8=";
16 release."dev".rev = "d3c67aa46ed22b1e593457cd34fc711f1a53b8be";
17 } coqPackages.stdpp;
18
19 # From 04-05-2026
20 iris = with pkgs; coqPackages.lib.overrideCoqDerivation {
21 version = "dev";
22 release."dev".sha256 = "P2cELkPl8RcHE1PzoswhMjXS5l8RBInW9q7Es0wtkus=";
23 release."dev".rev = "306c37bfc12b0d459d302dabad9de5ab09d6a6d4";
24 propagatedBuildInputs = [ stdpp ];
25 } coqPackages.iris;
26
27 # From 11-03-2026
28 iris-named-props = with pkgs; coqPackages.mkCoqDerivation rec {
29 pname = "iris-named-props";
30 owner = "tchajed";
31 version = "dev";
32 release."dev".sha256 = "1YHAItQ9XsCy+0M/pG2ib/GeaLTFJOrGJwF8noViwKg=";
33 release."dev".rev = "ca663d2709888a789a03edc861b7bde86ddd56e5";
34 propagatedBuildInputs = [ iris ];
35 };
36 in
37 {
38 devShells.default = with pkgs; mkShell {
39 buildInputs = [ coq iris iris-named-props ];
40 };
41
42 formatter = pkgs.nixpkgs-fmt;
43 });
44}
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 @@
1From iris.program_logic Require Import atomic.
2From iris.heap_lang Require Import notation proofmode.
3From iris.algebra.lib Require Import excl_auth.
4From iris.base_logic.lib Require Import invariants.
5From iris.base_logic.lib Require Import invariants mono_nat mono_list.
6From iris_named_props Require Import custom_syntax.
7
8From lmpmc Require Import basic_queue_spec upstream util.
9
10Definition new_node : val := λ: "data",
11 let: "ℓ_node" := AllocN #2 #() in
12 "ℓ_node" <- "data";;
13 "ℓ_node" +ₗ #1 <- NONE;;
14 "ℓ_node".
15
16Definition new : val := λ: <>,
17 let: "ℓ_node" := new_node #() in
18 AllocN #2 "ℓ_node".
19
20Definition set_tail : val := rec: "go" "ℓ_q" "ℓ_node" :=
21 let: "ℓ_tail" := !("ℓ_q" +ₗ #1) in
22 match: !("ℓ_tail" +ₗ #1) with
23 NONE =>
24 if: CAS ("ℓ_tail" +ₗ #1) NONE (SOME "ℓ_node") then
25 #()
26 else
27 "go" "ℓ_q" "ℓ_node"
28 | SOME "ℓ_next" =>
29 CAS ("ℓ_q" +ₗ #1) "ℓ_tail" "ℓ_next";;
30 "go" "ℓ_q" "ℓ_node"
31 end.
32
33Definition enqueue : val := λ: "ℓ_q" "data",
34 set_tail "ℓ_q" (new_node "data").
35
36Definition try_dequeue : val := rec: "go" "ℓ_q" :=
37 let: "ℓ_head" := !"ℓ_q" in
38 match: !("ℓ_head" +ₗ #1) with
39 NONE => NONE
40 | SOME "ℓ_next" =>
41 let: "v" := !"ℓ_next" in
42 if: CAS "ℓ_q" "ℓ_head" "ℓ_next" then
43 SOME "v"
44 else
45 "go" "ℓ_q"
46 end.
47
48Class basic_queueG Σ := BasicQueueG
49 { basic_queue_mono_natG :: mono_natG Σ;
50 basic_queue_mono_listG :: mono_listG (prodO locO valO) Σ; }.
51
52Definition basic_queueΣ : gFunctors :=
53 #[ mono_natΣ; mono_listΣ (prodO locO valO) ].
54
55#[global] Instance subG_basic_queueΣ {Σ} : subG basic_queueΣ Σ → basic_queueG Σ.
56Proof. solve_inG. Qed.
57
58Section basic_queue.
59 Context `{!heapGS Σ, !basic_queueG Σ}.
60
61 Record gstate :=
62 { γ_hist : gname;
63 γ_hpos : gname; }.
64 Definition gstate_to_pair (γ : gstate) :=
65 (γ.(γ_hist), γ.(γ_hpos)).
66 Definition gstate_of_pair '(γ_hist, γ_hpos) :=
67 {| γ_hist := γ_hist; γ_hpos := γ_hpos |}.
68 Instance gstate_eq_dec : EqDecision gstate := ltac:(solve_decision).
69 Instance gstate_countable : Countable gstate.
70 Proof.
71 refine {| encode := encode ∘ gstate_to_pair;
72 decode := fmap gstate_of_pair ∘ decode; |}.
73 intros []. by rewrite /= decode_encode.
74 Qed.
75
76 Definition node_repr (ℓ : loc) (data : val) (mℓ_next : option loc) : iProp Σ :=
77 ("Hndata" ∷ ℓ ↦□ data) ∗
78 ("Hnnext" ∷ (ℓ +ₗ 1) ↦ loc_opt_hl mℓ_next).
79
80 Definition loc_at (hist : list (loc * val)) i :=
81 hist.*1 !! i.
82 Definition val_at (hist : list (loc * val)) i :=
83 hist.*2 !! i.
84
85 Lemma loc_at_prefix xs xs' i ℓ :
86 loc_at xs i = Some ℓ → xs `prefix_of` xs' → loc_at xs' i = Some ℓ.
87 Proof.
88 unfold loc_at. intros Hxs Hpre.
89 eapply prefix_lookup_Some; first exact Hxs.
90 by apply prefix_of_fmap.
91 Qed.
92
93 Lemma val_at_prefix xs xs' i ℓ :
94 val_at xs i = Some ℓ → xs `prefix_of` xs' → val_at xs' i = Some ℓ.
95 Proof.
96 unfold val_at. intros Hxs Hpre.
97 eapply prefix_lookup_Some; first exact Hxs.
98 by apply prefix_of_fmap.
99 Qed.
100
101 Lemma loc_at_val_at_Some xs i ℓ :
102 loc_at xs i = Some ℓ → ∃ v, val_at xs i = Some v.
103 Proof.
104 unfold loc_at, val_at. rewrite [xs.*2 !! i]list_lookup_fmap.
105 intros [[ℓ' v] [-> ->]]%list_lookup_fmap_Some_1. by exists v.
106 Qed.
107
108 Lemma loc_at_val_at_combine {hist i ℓ v} :
109 loc_at hist i = Some ℓ →
110 val_at hist i = Some v →
111 hist !! i = Some (ℓ, v).
112 Proof.
113 unfold loc_at, val_at. intros Hloc Hval.
114 rewrite list_lookup_fmap in Hloc.
115 rewrite list_lookup_fmap in Hval.
116 destruct (hist !! i) as [[ℓ' v']|]; last done.
117 simpl in *. congruence.
118 Qed.
119
120 Lemma loc_at_Some_length hist i ℓ :
121 loc_at hist i = Some ℓ → i < length hist.
122 Proof.
123 intros Hloc%lookup_lt_Some.
124 by rewrite length_fmap in Hloc.
125 Qed.
126
127 Lemma loc_at_drop hist n i ℓ :
128 loc_at hist (n + i) = Some ℓ →
129 loc_at (drop n hist) i = Some ℓ.
130 Proof.
131 unfold loc_at. intros Hloc.
132 by rewrite list_lookup_fmap lookup_drop -list_lookup_fmap.
133 Qed.
134
135 Lemma loc_at_drop_2 hist n i :
136 loc_at (drop n hist) i = loc_at hist (n + i).
137 Proof. by rewrite /loc_at list_lookup_fmap lookup_drop -list_lookup_fmap. Qed.
138
139 Lemma val_at_drop hist n i ℓ :
140 val_at hist (n + i) = Some ℓ →
141 val_at (drop n hist) i = Some ℓ.
142 Proof.
143 unfold val_at. intros Hval.
144 by rewrite list_lookup_fmap lookup_drop -list_lookup_fmap.
145 Qed.
146
147 Definition hist_repr (hist : list (loc * val)) : iProp Σ :=
148 [∗ list] i ↦ '(ℓ, data) ∈ hist, node_repr ℓ data (loc_at hist (S i)).
149
150 Lemma hist_repr_peek_1 hist i ℓ data :
151 loc_at hist i = Some ℓ →
152 val_at hist i = Some data →
153 hist_repr hist -∗
154 node_repr ℓ data (loc_at hist (S i)) ∗
155 (node_repr ℓ data (loc_at hist (S i)) -∗ hist_repr hist).
156 Proof.
157 iIntros "%Hloc %Hval Hrepr".
158 pose proof (loc_at_val_at_combine Hloc Hval) as Hi.
159 iPoseProof (big_sepL_lookup_acc with "Hrepr") as "[Hnode Hclose]".
160 { apply Hi. }
161 iFrame.
162 Qed.
163
164 Lemma hist_repr_peek_2 hist i ℓ :
165 loc_at hist i = Some ℓ →
166 hist_repr hist -∗
167 ∃ data, node_repr ℓ data (loc_at hist (S i)) ∗
168 (node_repr ℓ data (loc_at hist (S i)) -∗ hist_repr hist).
169 Proof.
170 iIntros "%Hloc Hrepr".
171 assert (∃ v, val_at hist i = Some v) as [v Hval].
172 { by apply loc_at_val_at_Some in Hloc. }
173 iExists v. by iApply hist_repr_peek_1.
174 Qed.
175
176 Lemma hist_repr_peek_3 hist i ℓ :
177 loc_at hist i = Some ℓ →
178 hist_repr hist -∗
179 (ℓ +ₗ 1) ↦ loc_opt_hl (loc_at hist (S i)) ∗
180 ((ℓ +ₗ 1) ↦ loc_opt_hl (loc_at hist (S i)) -∗ hist_repr hist).
181 Proof.
182 iIntros "%Hloc Hrepr".
183 iDestruct (hist_repr_peek_2 with "[$]") as "(%v & @ & Hclose)"; first done.
184 iFrame. iIntros "Hnnext". iApply "Hclose". iFrame.
185 Qed.
186
187 Lemma loc_at_None hist pos :
188 loc_at hist pos = None → hist !! pos = None.
189 Proof.
190 rewrite /loc_at list_lookup_fmap.
191 by destruct (hist !! pos).
192 Qed.
193
194 Lemma loc_at_length hist pos :
195 loc_at hist pos = None → length hist ≤ pos.
196 Proof.
197 intros H%loc_at_None.
198 by apply lookup_ge_None.
199 Qed.
200
201 Lemma hist_repr_proj hist i ℓ :
202 loc_at hist i = Some ℓ →
203 hist_repr hist -∗
204 (∃ v, (ℓ +ₗ 1) ↦ v) ∗ hist_repr (drop (S i) hist).
205 Proof.
206 iIntros "%Hℓi Hrepr".
207 iDestruct (big_sepL_take_drop _ _ (S i) with "Hrepr") as "[Hrepr1 Hrepr2]".
208
209 rewrite /loc_at list_lookup_fmap in Hℓi.
210 destruct (hist !! i) as [[ℓ' v]|] eqn:Hi; last done.
211 simpl in *. injection Hℓi as ->.
212
213 iDestruct (big_sepL_lookup_acc with "Hrepr1") as "[Hrepr Hclose]".
214 { rewrite lookup_take_lt //. lia. }
215 iSimplifyEq. iDestruct "Hrepr" as "@". iFrame.
216 iClear "Hndata Hclose".
217
218 iAssert (hist_repr (drop (S i) hist)) with "[Hrepr2]" as "Hrepr2".
219 { unfold hist_repr. iApply (big_sepL_mono with "Hrepr2").
220 iIntros (k [ℓ' v'] Hk) "Hrepr".
221 by rewrite loc_at_drop_2 Nat.add_succ_l Nat.add_succ_r. }
222 done.
223 Qed.
224
225 Lemma loc_at_inj_aux hist i j ℓ :
226 i < j →
227 loc_at hist i = Some ℓ →
228 loc_at hist j = Some ℓ →
229 hist_repr hist -∗
230 False.
231 Proof.
232 iIntros "%ij %Hloci %Hlocj Hrepr".
233 assert (i < length hist). { by eapply loc_at_Some_length. }
234 assert (j < length hist). { by eapply loc_at_Some_length. }
235 assert (∃ n, j = S i + n) as [n ->].
236 { exists (j - i - 1). lia. }
237 iPoseProof (hist_repr_proj hist i ℓ Hloci with "Hrepr") as "[[%ni Hℓi] Hrepr']".
238
239 assert (Hlocj' : loc_at (drop (S i) hist) n = Some ℓ).
240 { by apply loc_at_drop. }
241
242 iPoseProof (hist_repr_proj _ n ℓ Hlocj' with "Hrepr'") as "[[%nj Hℓj] _]".
243 by iCombine "Hℓi Hℓj" gives %[? _].
244 Qed.
245
246 Lemma loc_at_inj {hist i j ℓ} :
247 loc_at hist i = Some ℓ →
248 loc_at hist j = Some ℓ →
249 hist_repr hist -∗
250 ⌜i = j⌝.
251 Proof.
252 iIntros "%Hloci %Hlocj Hrepr".
253 destruct (loc_at_val_at_Some hist i ℓ Hloci) as [vi Hvali].
254 destruct (loc_at_val_at_Some hist j ℓ Hlocj) as [vj Hvalj].
255 destruct (decide (i < j)) as [Hij|Hij].
256 - (* i < j *)
257 by iPoseProof (loc_at_inj_aux with "Hrepr") as "H".
258 - (* i ≥ j *)
259 destruct (decide (j < i)) as [Hji|Hji].
260 + (* j < i *)
261 by iPoseProof (loc_at_inj_aux with "Hrepr") as "H".
262 + (* i = j *)
263 iPureIntro. lia.
264 Qed.
265
266 Definition queue_repr_1 (γs : gstate) ℓ_q (vs : list val) : iProp Σ :=
267 ∃ (hist : list (loc * val)) (ℓ_head ℓ_tail : loc) (hpos tpos : nat),
268 ("Hhead" ∷ ℓ_q ↦ #ℓ_head) ∗
269 ("Htail" ∷ (ℓ_q +ₗ 1) ↦ #ℓ_tail) ∗
270 ("Hrepr" ∷ hist_repr hist) ∗
271 ("Hhist●" ∷ γs.(γ_hist) ↪●ML hist) ∗
272 ("Hhpos●" ∷ γs.(γ_hpos) ↪●MN hpos) ∗
273 ("%Hℓhpos" ∷ ⌜loc_at hist hpos = Some ℓ_head⌝) ∗
274 ("%Hℓtpos" ∷ ⌜loc_at hist tpos = Some ℓ_tail⌝) ∗
275 ("%Hvs" ∷ ⌜vs = (drop (S hpos) hist).*2⌝).
276
277 Definition queue_repr ℓ_q (vs : list val) : iProp Σ :=
278 ∃ (γs : gstate), meta ℓ_q nroot γs ∗ queue_repr_1 γs ℓ_q vs.
279
280 #[global] Instance queue_repr_timeless ℓ_q vs : Timeless (queue_repr ℓ_q vs) := _.
281
282 Lemma new_node_spec data :
283 {{{ True }}}
284 new_node data
285 {{{ (ℓ : loc), RET #ℓ; node_repr ℓ data None }}}.
286 Proof.
287 iIntros "%Φ _ HΦ". iUnfold new_node. wp_lam.
288 wp_alloc ℓ_node as "Hℓ_node"; first done.
289 iDestruct (array_cons with "Hℓ_node") as "[Hℓ_node0 Hℓ_node1]".
290 iDestruct (array_cons with "Hℓ_node1") as "[Hℓ_node1 _]".
291 wp_let. do 2 wp_store.
292 iMod (pointsto_persist with "Hℓ_node0") as "Hℓ_node0".
293 iModIntro. iApply "HΦ". by iFrame.
294 Qed.
295
296 Lemma new_spec :
297 {{{ True }}}
298 new #()
299 {{{ (ℓ : loc), RET #ℓ; queue_repr ℓ [] }}}.
300 Proof.
301 iIntros "%Φ _ HΦ". iUnfold new.
302 wp_lam. wp_apply (new_node_spec with "[//]").
303 iIntros (ℓ_node) "Hnode". wp_let.
304
305 set ℓ_head := ℓ_node. set ℓ_tail := ℓ_node.
306 set hpos := 0. set tpos := 0.
307 set hist := [(ℓ_node, #())] : list (loc * val).
308 iAssert (hist_repr hist) with "[$Hnode //]" as "Hrepr".
309
310 iMod (mono_list_own_alloc hist) as "[%γ_hist [Hhist● _]]".
311 iMod (mono_nat_own_alloc hpos) as "[%γ_hpos [Hhpos● _]]".
312 set γs := {| γ_hist := γ_hist; γ_hpos := γ_hpos |}.
313
314 iApply wp_fupd. iApply wp_allocN; [lia|done|].
315 iIntros "!> %ℓ [Hℓ [Htok _]]".
316 iDestruct (array_cons with "Hℓ") as "[Hℓ0 Hℓ1]".
317 iDestruct (array_cons with "Hℓ1") as "[Hℓ1 _]".
318 rewrite Loc.add_0.
319
320 iMod (meta_set ⊤ ℓ γs nroot with "Htok") as "Hmeta"; first done.
321
322 iApply "HΦ". iModIntro. iFrame. by iExists tpos.
323 Qed.
324
325 Lemma try_bump_tail_spec hist0 tpos ℓ_old ℓ_new ℓ_q γs :
326 loc_at hist0 tpos = Some ℓ_old →
327 loc_at hist0 (S tpos) = Some ℓ_new →
328 γs.(γ_hist) ↪◯ML hist0 -∗
329 <<{ ∀∀ vs, queue_repr_1 γs ℓ_q vs }>>
330 CAS #(ℓ_q +ₗ 1) #ℓ_old #ℓ_new @ ∅
331 <<{ ∃∃ (b : bool), queue_repr_1 γs ℓ_q vs | RET #b }>>.
332 Proof.
333 iIntros "%Hold %Hnew #Hhist◯ %Φ AU".
334 wp_bind (CmpXchg _ _ _)%E.
335 iMod "AU" as "(%vs & (%hist1 & %ℓ_head & %ℓ_tail & %hpos & %tpos' & @) & [_ Hclose])".
336 iAssert ⌜hist0 `prefix_of` hist1⌝%I as %Hhist01.
337 { by iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist◯") as "[_ ?]". }
338
339 destruct (decide (ℓ_tail = ℓ_old)) as [->|].
340 - (* The tail has not been updated yet *)
341 wp_cmpxchg_suc.
342
343 iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
344 { iPureIntro.
345 repeat split; try done || lia.
346 exists (S tpos). repeat split; try done.
347 by eapply loc_at_prefix. }
348 iMod ("Hclose" with "[$Hq]") as "HΦ".
349 iModIntro. wp_pures. iApply "HΦ".
350 - (* The tail has been updated in the meantime *)
351 wp_cmpxchg_fail.
352 iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
353 { iExists tpos'. by iFrameNamed. }
354 iMod ("Hclose" with "[$Hq]") as "HΦ".
355 iModIntro. wp_pures. iApply "HΦ".
356 Qed.
357
358 (* Given a history that is represented, after updating the [next]
359 pointer of the current tail node to a new tail node, we obtain a
360 new (extended) history (with the new tail node appended). *)
361 Lemma hist_repr_snoc hist tpos (ℓ_tail ℓ_new : loc) data :
362 length hist = S tpos →
363 loc_at hist tpos = Some ℓ_tail →
364 node_repr ℓ_new data None -∗
365 hist_repr hist -∗
366 (ℓ_tail +ₗ 1) ↦ loc_opt_hl None ∗
367 ((ℓ_tail +ₗ 1) ↦ loc_opt_hl (Some ℓ_new) -∗ hist_repr (hist ++ [(ℓ_new, data)])).
368 Proof.
369 unfold loc_at.
370 iIntros "%Hhistlen %Hloc @ Hhist".
371 rewrite list_lookup_fmap in Hloc.
372 destruct (hist !! tpos) as [[ℓ_tail' v_tail]|] eqn:Htpos; last done.
373 injection Hloc as ->.
374 apply list_elem_of_split_length in Htpos as (hist' & empty & -> & Htpos).
375 rewrite length_app length_cons -Htpos in Hhistlen.
376 assert (empty = []) as ->. { apply nil_length_inv. lia. }
377 clear Hhistlen Htpos.
378
379 iPoseProof (big_sepL_snoc with "Hhist") as "[Hinit Htail]".
380 iNamedSuffix "Htail" "_tail".
381
382 iSimplifyEq.
383 assert (loc_at (hist' ++ [(ℓ_tail, v_tail)]) (S (length hist')) = None) as ->.
384 { apply lookup_ge_None_2. rewrite length_fmap length_app length_cons /=. lia. }
385 iFrame "Hnnext_tail". iIntros "Hnnext_tail".
386 iSimplifyEq. rewrite /hist_repr.
387 iApply big_sepL_snoc.
388 iSplitR "Hndata Hnnext".
389 - iApply big_sepL_snoc. iSplitL "Hinit".
390 + iApply (big_sepL_mono with "Hinit").
391 iIntros (k [ℓ v] Hk) "Hrepr".
392 assert (loc_at ((hist' ++ [(ℓ_tail, v_tail)]) ++ [(ℓ_new, data)]) (S k) = loc_at (hist' ++ [(ℓ_tail, v_tail)]) (S k)) as ->.
393 { rewrite /loc_at !list_lookup_fmap lookup_app_l // length_app /=.
394 apply lookup_lt_Some in Hk. lia. }
395 done.
396 + iFrame.
397 rewrite /loc_at list_lookup_fmap lookup_app_r; last first.
398 { rewrite length_app /=. lia. }
399 by rewrite length_app /= Nat.add_1_r Nat.sub_diag.
400 - iFrame.
401 rewrite /= /loc_at length_app /= Nat.add_1_r list_lookup_fmap lookup_app_r.
402 * by rewrite !length_app /= !Nat.add_1_r Nat.sub_succ -Arith_base.minus_Sn_m_stt // Nat.sub_diag.
403 * rewrite length_app /= Nat.add_1_r. lia.
404 Qed.
405
406 Lemma set_tail_spec (ℓ_q ℓ_node : loc) data :
407 node_repr ℓ_node data None -∗
408 <<{ ∀∀ vs, queue_repr ℓ_q vs }>>
409 set_tail #ℓ_q #ℓ_node @ ∅
410 <<{ queue_repr ℓ_q (vs ++ [data]) | RET #() }>>.
411 Proof.
412 iIntros "@ %Φ AU". iLöb as "IH". wp_rec.
413
414 wp_pures. wp_bind (! _)%E.
415 iMod "AU" as "(%vs & (%γs & #Hγs & %hist0 & %ℓ_head & %ℓ_tail & %hpos & %tpos & @) & [Hclose _])".
416 iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist0◯".
417 wp_load. iSimpl in "Hrepr".
418 rename Hℓtpos into Hℓtpos0.
419 iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
420 { iExists tpos. by iFrameNamed. }
421 iMod ("Hclose" with "[$]") as "AU". clear Hvs Hℓhpos hpos vs ℓ_head.
422 iModIntro. wp_let. wp_pure.
423
424 wp_bind (! _)%E.
425 iMod "AU" as "(%vs & (%γs' & Hγs' & %hist2 & %ℓ_head & %ℓ_tail'' & %hpos & %tpos'' & @) & [Hclose _])".
426 iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
427 iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist0◯") as %Hhist02.
428 iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist2◯".
429 destruct Hhist02 as [_ Hhist02]. rename Hℓtpos into Hℓtpos2.
430 assert (Hℓtpos0'' : loc_at hist2 tpos = Some ℓ_tail).
431 { by eapply loc_at_prefix. } clear Hℓtpos0.
432 wp_pures.
433 iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%w & Hnrepr & Hrepr)"; first done.
434 iNamedSuffix "Hnrepr" "_tail".
435 wp_load.
436 iPoseProof ("Hrepr" with "[$]") as "Hrepr".
437 iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
438 { iExists tpos''. by iFrameNamed. }
439 iMod ("Hclose" with "[$]") as "AU". clear Hvs Hℓhpos Hℓtpos2 hpos vs ℓ_head ℓ_tail''.
440 iModIntro.
441
442 destruct (loc_at hist2 (S tpos)) as [ℓ_next|] eqn:Htpos2.
443 + (* it is not the last node *)
444 simpl. wp_pures. wp_bind (Snd (CmpXchg _ _ _))%E.
445 awp_apply (try_bump_tail_spec with "[//]").
446 { apply Hℓtpos0''. }
447 { done. }
448 rewrite /atomic_acc /=.
449 iMod "AU" as "(%vs & (%γs' & Hγs' & Hrepr) & [Hclose _])".
450 iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
451 iModIntro. iExists vs. iFrame "Hrepr". iSplit.
452 * iFrame. iIntros "Hrepr". by iApply ("Hclose" with "[$Hrepr]").
453 * iIntros "%b Hrepr".
454 iMod ("Hclose" with "[$Hrepr //]") as "AU".
455 iModIntro. wp_pures.
456 by iApply ("IH" with "[$] [$] [$]").
457 + (* it is the last (non-final) node *)
458 simpl. wp_pures. wp_bind (CmpXchg _ _ _)%E.
459
460 iMod "AU" as "(%vs & (%γs' & Hγs' & %hist3 & %ℓ_head & %ℓ_tail''' & %hpos & %tpos''' & @) & Hclose)".
461 iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
462 iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist2◯") as %Hhist23.
463 destruct Hhist23 as [_ Hhist23]. rename Hℓtpos into Hℓtpos3.
464
465 destruct (loc_at hist3 (S tpos)) as [ℓ_tail''''|] eqn:Hrace.
466 * (* Another item has been enqueued in the meantime, so the CAS is poised to fail. *)
467 iDestruct "Hclose" as "[Hclose _]".
468
469 iDestruct (hist_repr_peek_3 with "[$Hrepr]") as "[Hℓ_tail1 Hrepr]".
470 { eapply prefix_lookup_Some; first apply Hℓtpos0''. by apply prefix_of_fmap. }
471 rewrite Hrace /=.
472 wp_cmpxchg_fail.
473 iSpecialize ("Hrepr" with "Hℓ_tail1").
474 iAssert (queue_repr_1 γs ℓ_q vs) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
475 { iExists tpos'''. by iFrameNamed. }
476 iMod ("Hclose" with "[$]") as "AU". iModIntro.
477 wp_pures. iApply ("IH" with "Hndata Hnnext AU").
478 * (* This node is still the tail, so the CAS will succeed. *)
479 iDestruct "Hclose" as "[_ Hclose]".
480
481 iAssert ⌜length hist3 = S tpos⌝%I as %Hhist3.
482 { apply loc_at_length in Hrace as Hhist3.
483 iPureIntro. apply loc_at_prefix with (xs':=hist3) in Hℓtpos0''; last done.
484 apply lookup_lt_Some in Hℓtpos0''. rewrite length_fmap in Hℓtpos0''. lia. }
485
486 iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%w' & Hℓ_tail3 & Hrepr)".
487 { eapply prefix_lookup_Some; first apply Hℓtpos0''. by apply prefix_of_fmap. }
488 iNamedSuffix "Hℓ_tail3" "_tail3".
489 iPoseProof ("Hrepr" with "[$]") as "Hrepr". clear w.
490
491 iPoseProof (hist_repr_snoc with "[$Hndata $Hnnext] [$Hrepr]") as "[Htnode Henq]".
492 { apply Hhist3. }
493 { eapply prefix_lookup_Some. apply Hℓtpos0''. by apply prefix_of_fmap. }
494 wp_cmpxchg_suc. iSpecialize ("Henq" with "Htnode").
495
496 iMod (mono_list_auth_own_update_app [(ℓ_node, data)] with "Hhist●") as "[Hhist● _]".
497
498 iAssert (queue_repr_1 γs ℓ_q (vs ++ [data])) with "[$Hhead $Htail $Hhist● $Hhpos● $Henq]" as "Hq".
499 { iExists tpos'''. iPureIntro.
500 repeat split; try done.
501 - eapply loc_at_prefix; first done.
502 by apply prefix_app_r.
503 - eapply loc_at_prefix; first done.
504 by apply prefix_app_r.
505 - rewrite drop_app fmap_app -Hvs.
506 f_equal.
507 assert (Hhpos : hpos < length hist3).
508 { apply lookup_lt_Some in Hℓhpos.
509 by rewrite length_fmap in Hℓhpos. }
510 by assert (S hpos - length hist3 = 0) as -> by lia. }
511 iMod ("Hclose" with "[$]") as "HΦ".
512 iModIntro. wp_pures. done.
513 Qed.
514
515 Lemma enqueue_spec (ℓ_q : loc) (data : val) :
516 ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>>
517 enqueue #ℓ_q data @ ∅
518 <<{ queue_repr ℓ_q (vs ++ [data]) | RET #() }>>.
519 Proof.
520 iIntros "%Φ AU". wp_lam. wp_pures.
521 wp_apply (new_node_spec with "[//]") as "%ℓ_node Hnode".
522 awp_apply (set_tail_spec with "[$Hnode]").
523 rewrite /atomic_acc /=. iMod "AU" as "(%vs & Hrepr & Hclose)".
524 iModIntro. iFrame.
525 Qed.
526
527 Lemma try_dequeue_spec (ℓ_q : loc) :
528 ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>>
529 try_dequeue #ℓ_q @ ∅
530 <<{ queue_repr ℓ_q (tail vs) | RET (val_opt_hl (head vs)) }>>.
531 Proof.
532 iIntros "%Φ AU". iLöb as "IH". wp_rec.
533
534 wp_bind (! _)%E.
535 iMod "AU" as "(%vs0 & (%γs & #Hγs & %hist0 & %ℓ_head0 & %ℓ_tail0 & %hpos0 & %tpos0 & @) & [Hclose _])".
536 iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist0◯".
537 iDestruct (mono_nat_lb_own_get with "Hhpos●") as "#Hhpos0◯".
538 rename Hℓhpos into Hℓhpos0.
539 wp_load.
540 iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU".
541 { iExists tpos0. by iFrameNamed. }
542 iModIntro. clear vs0 Hvs tpos0 Hℓtpos ℓ_tail0.
543
544 wp_pures. wp_bind (! _)%E.
545 iMod "AU" as "(%vs1 & (%γs' & Hγs' & %hist1 & %ℓ_head1 & %ℓ_tail1 & %hpos1 & %tpos1 & @) & Hclose)".
546 iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
547 iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist1◯".
548 iDestruct (mono_nat_auth_lb_own_valid with "Hhpos● Hhpos0◯") as %Hhpos01.
549 iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist0◯") as %Hhist01.
550 destruct Hhpos01 as [_ Hhpos01]. destruct Hhist01 as [_ Hhist01].
551 assert (Hℓhpos0' : loc_at hist1 hpos0 = Some ℓ_head0).
552 { by eapply loc_at_prefix. } clear Hℓhpos0.
553 iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%u & @ & Hrepr)"; first done.
554 wp_load.
555 iSpecialize ("Hrepr" with "[$]").
556
557 destruct (loc_at hist1 (S hpos0)) as [ℓ_headS0|] eqn:Hℓ_headS0.
558 - simpl. iDestruct "Hclose" as "[Hclose _]".
559 iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU".
560 { iExists tpos1. by iFrameNamed. }
561 iModIntro. clear u vs1 Hvs tpos1 Hℓtpos ℓ_tail1.
562
563 wp_pures. wp_bind (! _)%E.
564 iMod "AU" as "(%vs2 & (%γs' & Hγs' & %hist2 & %ℓ_head2 & %ℓ_tail2 & %hpos2 & %tpos2 & @) & Hclose)".
565 iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
566 iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist2◯".
567 iDestruct (mono_nat_auth_lb_own_valid with "Hhpos● Hhpos0◯") as %Hhpos02.
568 iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist1◯") as %Hhist12.
569 destruct Hhpos02 as [_ Hhpos02]. destruct Hhist12 as [_ Hhist12].
570 assert (Hℓ_headS0' : loc_at hist2 (S hpos0) = Some ℓ_headS0).
571 { by eapply loc_at_prefix. } clear Hℓ_headS0.
572 apply loc_at_val_at_Some in Hℓ_headS0' as Hval_headS0'.
573 destruct Hval_headS0' as [w Hval_headS0'].
574 iDestruct (hist_repr_peek_1 with "[$Hrepr]") as "(@ & Hrepr)"; try done.
575 iDestruct "Hndata" as "#Hndata_head".
576 wp_load.
577
578 iDestruct "Hclose" as "[Hclose _]".
579
580 iSpecialize ("Hrepr" with "[$]").
581 iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU".
582 { iExists tpos2. by iFrameNamed. }
583 iModIntro.
584 clear vs2 Hvs tpos2 Hℓtpos ℓ_tail2.
585
586 wp_pures.
587
588 wp_bind (CmpXchg _ _ _)%E.
589 iMod "AU" as "(%vs3 & (%γs' & Hγs' & %hist3 & %ℓ_head3 & %ℓ_tail3 & %hpos3 & %tpos3 & @) & Hclose)".
590 iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
591 iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist2◯") as %Hhist23.
592 destruct Hhist23 as [_ Hhist23].
593 assert (Hhist13 : hist1 `prefix_of` hist3).
594 { by trans hist2. }
595
596 destruct (decide (ℓ_head0 = ℓ_head3)) as [->|Hhead03].
597 + iDestruct "Hclose" as "[_ Hclose]".
598
599 wp_cmpxchg_suc.
600
601 assert (Hℓhpos0'' : loc_at hist3 hpos0 = Some ℓ_head3).
602 { by eapply loc_at_prefix. } clear Hℓhpos0'.
603 iAssert ⌜hpos0 = hpos3⌝%I as %->.
604 { by iApply (loc_at_inj with "Hrepr"). }
605
606 simplify_eq/=.
607
608 iMod (mono_nat_own_update (S hpos3) with "Hhpos●") as "[Hhpos● _]". { lia. }
609 iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ".
610 { iExists tpos3. iFrameNamed.
611 iPureIntro. repeat split; try done.
612 - by eapply loc_at_prefix.
613 - by rewrite -[S (S _)]Nat.add_1_r -drop_drop [(drop 1 _).*2]fmap_drop. }
614
615 iModIntro. wp_pures.
616
617 assert (Hval_headS0'' : val_at hist3 (S hpos3) = Some w).
618 { by eapply val_at_prefix. } clear Hval_headS0'.
619 unfold val_at in Hval_headS0''.
620 rewrite -[S hpos3]Nat.add_0_r -lookup_drop -fmap_drop /= -head_lookup in Hval_headS0''.
621 by rewrite Hval_headS0'' /=.
622
623 + iDestruct "Hclose" as "[Hclose _]".
624
625 wp_cmpxchg_fail.
626
627 iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU".
628 { iExists tpos3. by iFrameNamed. }
629
630 iModIntro. wp_pures. iApply ("IH" with "AU").
631 - apply loc_at_length in Hℓ_headS0 as Hhistlen.
632 rewrite drop_ge /= in Hvs; last lia. destruct vs1; try done.
633 simplify_eq/=.
634
635 iDestruct "Hclose" as "[_ Hclose]".
636 iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ".
637 { iExists tpos1. iFrameNamed. iPureIntro.
638 rewrite drop_ge //=. lia. }
639
640 iModIntro. wp_pures. iApply "HΦ".
641 Qed.
642
643End basic_queue.
644
645Definition basic_queue `{!heapGS Σ, !basic_queueG Σ} : basic_queue_spec.basic_queue Σ.
646Proof.
647 refine {| basic_queue_spec.new_spec := new_spec;
648 basic_queue_spec.enqueue_spec := enqueue_spec;
649 basic_queue_spec.try_dequeue_spec := try_dequeue_spec |}.
650Defined.
651
652#[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 @@
1From iris.program_logic Require Import atomic.
2From iris.heap_lang Require Import notation proofmode.
3
4From lmpmc Require Import util.
5
6Record basic_queue {Σ} `{!heapGS Σ} :=
7 BasicQueue
8 { new : val;
9 enqueue : val;
10 try_dequeue : val;
11
12 queue_repr : loc → list val → iProp Σ;
13 #[global] queue_repr_timeless ℓ vs :: Timeless (queue_repr ℓ vs);
14
15 new_spec :
16 {{{ True }}}
17 new #()
18 {{{ (ℓ_q : loc), RET #ℓ_q; queue_repr ℓ_q [] }}};
19
20 enqueue_spec (ℓ_q : loc) (data : val) :
21 ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>>
22 enqueue #ℓ_q data @ ∅
23 <<{ queue_repr ℓ_q (vs ++ [data]) | RET #() }>>;
24
25 try_dequeue_spec (ℓ_q : loc) :
26 ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>>
27 try_dequeue #ℓ_q @ ∅
28 <<{ queue_repr ℓ_q (tail vs) | RET (val_opt_hl (head vs)) }>>;
29 }.
30#[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 @@
1From iris.program_logic Require Import atomic.
2From iris.heap_lang Require Import notation proofmode adequacy.
3From iris.algebra Require Import list gmultiset.
4From iris.algebra.lib Require Import excl_auth.
5From iris.base_logic.lib Require Import invariants mono_list.
6From iris_named_props Require Import custom_syntax.
7From iris.heap_lang.lib Require Import assert par.
8
9From lmpmc Require lmpmc_queue_spec lmpmc_queue_proof fin_queue_proof lmpmc_blocking_dequeue.
10From lmpmc Require Import upstream.
11
12Definition somes {A} (xs : list (option A)) : list A := xs ≫= option_list.
13Definition option_le {A} (mx my : option A) := option_relation (=) (const False) (const True) mx my.
14Definition option_nat (x : nat) : option nat := guard (x ≠ 0);; Some x.
15Definition vals_of_nats : list nat → list val := fmap (LitV ∘ LitInt ∘ Z.of_nat).
16
17Lemma option_le_None {A} (x : A) : option_le None (Some x).
18Proof. done. Qed.
19Lemma option_le_Some {A} (x : A) : option_le (Some x) (Some x).
20Proof. done. Qed.
21Lemma option_le_inv {A} (mx my : option A) : option_le mx my → mx = None ∨ mx = my.
22Proof. induction mx, my; intros ?; simplify_eq/=; done || (by right) || by left. Qed.
23
24#[global] Instance timeless_if_bool {PROP : bi} {b : bool} {Q R : PROP} : Timeless Q → Timeless R → Timeless (if b then Q else R).
25Proof. by destruct b. Qed.
26
27Section hl.
28 Context (lq : lmpmc_queue_spec.lmpmc_queue_hl).
29 Import lmpmc_blocking_dequeue lmpmc_queue_spec.
30
31 Notation "'let2:' x1 , x2 := e1 'in' e2" :=
32 (Lam (BNamed x2) (Lam (BNamed x1) (Lam (BNamed x2) e2 (Snd (Var x2))) (Fst (Var x2))) e1)%E
33 (at level 200, x1, x2 at level 1, e1, e2 at level 200,
34 format "'[' 'let2:' x1 ',' x2 := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope.
35
36 Definition simple_example_2_1 : expr :=
37 let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in
38 let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in
39 lq.(enqueue) "ℓ_enq1" #10;;
40 lq.(link) "ℓ_enq1" "ℓ_deq2";;
41 lq.(enqueue) "ℓ_enq2" #20;;
42 let: "x" := dequeue lq "ℓ_deq1" in
43 let: "y" := dequeue lq "ℓ_deq1" in
44 ("x", "y").
45
46 Definition simple_example_2_2 : expr :=
47 let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in
48 let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in
49 (( lq.(enqueue) "ℓ_enq1" #10;;
50 lq.(link) "ℓ_enq1" "ℓ_deq2") (* thread A *)
51 ||| lq.(enqueue) "ℓ_enq2" #20 (* thread B *)
52 );;
53 let: "x" := dequeue lq "ℓ_deq1" in
54 let: "y" := dequeue lq "ℓ_deq1" in
55 ("x", "y").
56
57 Definition mt_example_1 : expr :=
58 let: "ℓ_sum" := Alloc #0 in
59 let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in
60 let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in
61 (( lq.(enqueue) "ℓ_enq1" #1;;
62 lq.(link) "ℓ_enq1" "ℓ_deq2") (* thread A *)
63 ||| lq.(enqueue) "ℓ_enq2" #2 (* thread B *)
64 ||| lq.(enqueue) "ℓ_enq2" #3 (* thread C *)
65 ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1") (* thread D *)
66 ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1") (* thread E *)
67 ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1") (* thread F *)
68 );;
69 ! "ℓ_sum".
70
71End hl.
72
73Section proofs.
74 Context `{!heapGS Σ, !spawnG Σ,
75 !mono_listG natO Σ,
76 !inG Σ (excl_authR (gmultisetO nat)),
77 !inG Σ (excl_authR natO),
78 !inG Σ (excl_authR boolO),
79 !inG Σ (excl_authR (listO natO)),
80 !inG Σ (excl_authR (optionO natO)),
81 !inG Σ (exclR (listO natO))}.
82 Context {lq : lmpmc_queue_spec.lmpmc_queue_hl}
83 {lqp : lmpmc_queue_spec.lmpmc_queue_iris Σ lq}.
84 Import lmpmc_blocking_dequeue lmpmc_queue_spec.
85
86 Lemma simple_example_2_1_safe :
87 ⊢ WP simple_example_2_1 lq {{ v, ⌜v = (#10, #20)%V⌝ }}.
88 Proof.
89 iUnfold simple_example_2_1.
90 wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures.
91 wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures.
92 awp_apply lqp.(enqueue_spec lq). iAaccIntro with "Hq1"; iIntros "Hq1"; first by iFrame.
93 simpl. iModIntro. wp_pures.
94 awp_apply lqp.(link_spec lq).
95 rewrite /atomic_acc /=.
96 iExists true. iFrame.
97 iApply fupd_mask_intro; first done.
98 iIntros "Hupd". iSplit. { iIntros "[? ?]". iFrame. }
99 iIntros "Hq". simpl. iMod "Hupd" as "_". iModIntro.
100 wp_pures. awp_apply lqp.(enqueue_spec lq).
101 iAaccIntro with "Hq"; iIntros "Hq"; first by iFrame.
102 simpl.
103
104 iModIntro. wp_pures. awp_apply (dequeue_spec lq lqp).
105 iAaccIntro with "Hq"; first by iIntros "Hq"; iFrame.
106 iIntros (? ?) "[%Hvs Hq]". iSimplifyEq.
107 iModIntro. wp_pures. awp_apply (dequeue_spec lq lqp).
108 iAaccIntro with "Hq"; first by iIntros "Hq"; iFrame.
109 iIntros (? ?) "[%Hvs Hq]". iSimplifyEq.
110
111 iModIntro. by wp_pures.
112 Qed.
113
114 Record smp_gstate :=
115 SmpGstate
116 { γ1_linked : gname; (* (●E) whether Q1 and Q2 have been linked already *)
117 γ1_contA : gname; (* (●E) (list nat) contribution of thread A *)
118 γ1_contB : gname; (* (●E) (list nat) contribution of thread B *)
119 }.
120
121 Definition smp_inv γs (ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2 : loc) : iProp Σ :=
122 ∃ (linked : bool) (contA contB : list nat),
123 ("Hlinked●" ∷ own γs.(γ1_linked) (●E linked)) ∗
124 ("HcontA●" ∷ own γs.(γ1_contA) (●E contA)) ∗
125 ("HcontB●" ∷ own γs.(γ1_contB) (●E contB)) ∗
126 ("Hq1" ∷ lqp.(queue_repr lq) ℓ_deq1 (if linked then ℓ_enq2 else ℓ_enq1) (vals_of_nats (if linked then contA ++ contB else contA))) ∗
127 ("Hq2" ∷ if linked then True else lqp.(queue_repr lq) ℓ_deq2 ℓ_enq2 (vals_of_nats contB)).
128
129 Lemma simple_example_2_2_safe :
130 ⊢ WP simple_example_2_2 lq {{ v, ⌜v = (#10, #20)%V⌝ }}.
131 Proof.
132 iUnfold simple_example_2_2.
133 wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures.
134 wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures.
135
136 iMod (own_alloc (●E false ⋅ ◯E false)) as (γ1_linked') "[Hlinked● Hlinked◯]"; first apply excl_auth_valid.
137 iMod (own_alloc (●E [] ⋅ ◯E [])) as (γ1_contA') "[HcontA● HcontA◯]"; first apply excl_auth_valid.
138 iMod (own_alloc (●E [] ⋅ ◯E [])) as (γ1_contB') "[HcontB● HcontB◯]"; first apply excl_auth_valid.
139
140 pose γs := SmpGstate γ1_linked' γ1_contA' γ1_contB'.
141 replace γ1_linked' with γs.(γ1_linked) by done.
142 replace γ1_contA' with γs.(γ1_contA) by done.
143 replace γ1_contB' with γs.(γ1_contB) by done.
144 clearbody γs. clear γ1_linked' γ1_contA' γ1_contB'.
145 iAssert (smp_inv γs ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "[$]" as "Hinv".
146 iMod (inv_alloc nroot _ (smp_inv γs ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "Hinv") as "#Hinv".
147
148 wp_smart_apply (wp_par (λ _, own γs.(γ1_linked) (◯E true) ∗ own γs.(γ1_contA) (◯E [10]))%I
149 (λ _, own γs.(γ1_contB) (◯E [20]))
150 with "[Hlinked◯ HcontA◯] [HcontB◯]").
151 { awp_apply lqp.(enqueue_spec lq).
152 iInv "Hinv" as (linked contA contB) ">H".
153 iNamedSuffix "H" "_1".
154 iCombine "Hlinked◯ Hlinked●_1" gives %->%excl_auth_agree_L.
155 iCombine "HcontA◯ HcontA●_1" gives %->%excl_auth_agree_L.
156 iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. }
157 iIntros "Hq1_1".
158 iCombine "HcontA●_1 HcontA◯" as "HcontA".
159 iMod (own_update with "HcontA") as "[HcontA●_1 HcontA◯]".
160 { apply (excl_auth_update _ _ [10]). }
161 iIntros "!>".
162 iSimplifyEq. replace ([ #10 ] : list val) with (vals_of_nats [10]) by done.
163 iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1 Hq2_1". wp_pures. clear contB.
164
165 awp_apply lqp.(link_spec lq).
166 iInv "Hinv" as (linked contA contB) ">H".
167 iNamedSuffix "H" "_2".
168 iCombine "Hlinked◯ Hlinked●_2" gives %->%excl_auth_agree_L.
169 iCombine "HcontA◯ HcontA●_2" gives %->%excl_auth_agree_L.
170 rewrite /atomic_acc /=. iApply fupd_mask_intro; first set_solver. iIntros "Hclose".
171 iExists true. iFrame "Hq1_2 Hq2_2". iSplit.
172 { iIntros "[Hq1 Hq2]". iMod "Hclose" as "_". iModIntro. do 2 iFrame. }
173 iIntros "Hq1". iMod "Hclose" as "_".
174 iCombine "Hlinked●_2 Hlinked◯" as "Hlinked".
175 iMod (own_update with "Hlinked") as "[Hlinked●_2 Hlinked◯]".
176 { apply (excl_auth_update _ _ true). }
177 iFrame "Hlinked●_2 HcontA●_2 HcontB●_2 Hq1". by iFrame. }
178 { awp_apply lqp.(enqueue_spec lq).
179 iInv "Hinv" as (linked contA contB) ">H".
180 iNamedSuffix "H" "_1".
181 iCombine "HcontB◯ HcontB●_1" gives %->%excl_auth_agree_L.
182 destruct linked eqn:Hlinked.
183 { iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. }
184 iIntros "Hq1_1".
185 iCombine "HcontB◯ HcontB●_1" as "HcontB".
186 iMod (own_update with "HcontB") as "[HcontB●_1 HcontB◯]".
187 { apply (excl_auth_update _ _ [20]). }
188 iIntros "!>".
189 iSimplifyEq.
190 replace [ #20 ] with (vals_of_nats [20]) by done.
191 iEval (rewrite app_nil_r /vals_of_nats -fmap_app -/vals_of_nats) in "Hq1_1".
192 by iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1". }
193 { iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". by iFrame. }
194 iIntros "Hq2_1".
195 iCombine "HcontB◯ HcontB●_1" as "HcontB".
196 iMod (own_update with "HcontB") as "[HcontB●_1 HcontB◯]".
197 { apply (excl_auth_update _ _ [20]). }
198 iIntros "!>".
199 iSimplifyEq.
200 replace [ #20 ] with (vals_of_nats [20]) by done.
201 by iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1 Hq2_1". } }
202 { iIntros (v1 v2) "[[Hlinked◯ HcontA◯] HcontB◯]".
203 iModIntro. wp_pures. clear v1 v2.
204 awp_apply (dequeue_spec lq lqp).
205 iInv "Hinv" as (linked contA contB) ">H".
206 iNamedSuffix "H" "_1".
207 iCombine "Hlinked◯ Hlinked●_1" gives %->%excl_auth_agree_L.
208 iCombine "HcontA◯ HcontA●_1" gives %->%excl_auth_agree_L.
209 iCombine "HcontB◯ HcontB●_1" gives %->%excl_auth_agree_L.
210 iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. }
211 iIntros (v0 vs) "[%Hvs Hq1]".
212 simpl in Hvs. injection Hvs as <- <-.
213 replace [ #20%nat ] with (vals_of_nats [20]) by done.
214 iCombine "HcontA●_1 HcontA◯" as "HcontA".
215 iMod (own_update with "HcontA") as "[HcontA●_1 HcontA◯]".
216 { apply (excl_auth_update _ _ []). }
217 iIntros "!>".
218 iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1". wp_pures.
219
220 awp_apply (dequeue_spec lq lqp).
221 iInv "Hinv" as (linked contA contB) ">H".
222 iNamedSuffix "H" "_2".
223 iCombine "Hlinked◯ Hlinked●_2" gives %->%excl_auth_agree_L.
224 iCombine "HcontA◯ HcontA●_2" gives %->%excl_auth_agree_L.
225 iCombine "HcontB◯ HcontB●_2" gives %->%excl_auth_agree_L.
226 iAaccIntro with "Hq1_2". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. }
227 iIntros (v0 vs) "[%Hvs Hq1]".
228 simpl in Hvs. injection Hvs as <- <-.
229 replace [ #20%nat ] with (vals_of_nats [20]) by done.
230 iCombine "HcontB●_2 HcontB◯" as "HcontB".
231 iMod (own_update with "HcontB") as "[HcontB●_2 HcontB◯]".
232 { apply (excl_auth_update _ _ []). }
233 iIntros "!>".
234 iFrame "Hlinked●_2 HcontB●_2 HcontA●_2 Hq1". wp_pures.
235 done. }
236 Qed.
237
238 Record mt_gstate :=
239 Gstate
240 { γ2_hist1 : gname; (* (●ML) (list nat) succesfully enqueued items (Q1) *)
241 γ2_hist2 : gname; (* (●E ) (list nat) sucessfully enqueued items (Q2) *)
242 γ2_linked : gname; (* (●E ) (bool) whether Q1 and Q2 have been linked *)
243 γ2_venqA : gname; (* (●E ) (gmultiset nat) of items enqueued by thread A *)
244 γ2_venqB : gname; (* (●E ) (gmultiset nat) of items enqueued by thread B *)
245 γ2_venqC : gname; (* (●E ) (gmultiset nat) of items enqueued by thread C *)
246 γ2_vdeqD : gname; (* (●E ) (option nat) poised contribution of first dequeueing thread *)
247 γ2_vdeqE : gname; (* (●E ) (option nat) poised contribution of second dequeueing thread *)
248 γ2_vdeqF : gname; (* (●E ) (option nat) poised contribution of third dequeueing thread *)
249 γ2_contD : gname; (* (●E ) (nat) as-is contribution of first dequeueing thread *)
250 γ2_contE : gname; (* (●E ) (nat) as-is contribution of second dequeueing thread *)
251 γ2_contF : gname; (* (●E ) (nat) as-is contribution of third dequeueing thread *)
252 }.
253
254 Definition mt_inv γs ℓ_sum (ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2 : loc) : iProp Σ :=
255 ∃ (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),
256 ("Hq1" ∷ lqp.(queue_repr lq) ℓ_deq1 (if linked then ℓ_enq2 else ℓ_enq1) (vals_of_nats vs1)) ∗
257 ("Hq2" ∷ if linked then True else lqp.(queue_repr lq) ℓ_deq2 ℓ_enq2 (vals_of_nats hist2)) ∗
258 ("Hhist1●" ∷ γs.(γ2_hist1) ↪●ML hist1) ∗
259 ("Hhist2E" ∷ own γs.(γ2_hist2) (Excl hist2)) ∗
260 ("Hlinked●" ∷ own γs.(γ2_linked) (●E linked)) ∗
261 ("HvenqA●" ∷ own γs.(γ2_venqA) (●E ecsA)) ∗
262 ("HvenqB●" ∷ own γs.(γ2_venqB) (●E ecsB)) ∗
263 ("HvenqC●" ∷ own γs.(γ2_venqC) (●E ecsC)) ∗
264 ("HvdeqD●" ∷ own γs.(γ2_vdeqD) (●E npD)) ∗
265 ("HvdeqE●" ∷ own γs.(γ2_vdeqE) (●E npE)) ∗
266 ("HvdeqF●" ∷ own γs.(γ2_vdeqF) (●E npF)) ∗
267 ("HcontD●" ∷ own γs.(γ2_contD) (●E nD)) ∗
268 ("HcontE●" ∷ own γs.(γ2_contE) (●E nE)) ∗
269 ("HcontF●" ∷ own γs.(γ2_contF) (●E nF)) ∗
270 ("Hsum" ∷ ℓ_sum ↦ #(nD + nE + nF)) ∗
271 ("%Hhist1" ∷ ⌜list_to_set_disj hist1 ⊆ if linked then ecsA ⊎ ecsB ⊎ ecsC else ecsA⌝) ∗
272 ("%Hhist2" ∷ ⌜list_to_set_disj hist2 ⊆ ecsB ⊎ ecsC⌝) ∗
273 ("%Hhist1n0" ∷ ⌜Forall (.≠ 0) hist1⌝) ∗
274 ("%Hhist2n0" ∷ ⌜Forall (.≠ 0) hist2⌝) ∗
275 ("%HnDEF" ∷ ⌜somes [npD; npE; npF] ⊆+ take ndeq hist1⌝) ∗
276 ("%HD" ∷ ⌜option_le (option_nat nD) npD⌝) ∗
277 ("%HE" ∷ ⌜option_le (option_nat nE) npE⌝) ∗
278 ("%HF" ∷ ⌜option_le (option_nat nF) npF⌝) ∗
279 ("%Hndeq" ∷ ⌜ndeq ≤ length hist1⌝) ∗
280 ("%Hhistvs" ∷ ⌜drop ndeq hist1 = vs1⌝).
281
282 (* Post, we expect:
283 linked = true
284 nD, nE, nF ≠ 0 (hence npD, npE, npF ≠ None and all are unique, adding up to 6) *)
285
286 Lemma mt_example_1_safe :
287 ⊢ WP mt_example_1 lq {{ v, ⌜v = #6⌝ }}.
288 Proof.
289 iUnfold mt_example_1.
290 wp_alloc ℓ_sum as "Hsum". wp_pures.
291 wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures.
292 wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures.
293 iEval (replace [] with (vals_of_nats [])) in "Hq1 Hq2".
294 iMod (mono_list_own_alloc []) as "[%γ2_hist1 [Hhist1● _]]".
295 iMod (own_alloc (Excl [])) as "[%γ2_hist2 Hhist2E]"; first done.
296 iMod (own_alloc (●E false ⋅ ◯E false)) as (γ2_linked') "[Hlinked● Hlinked◯]"; first apply excl_auth_valid.
297 iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqA') "[HvenqA● HvenqA◯]"; first apply excl_auth_valid.
298 iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqB') "[HvenqB● HvenqB◯]"; first apply excl_auth_valid.
299 iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqC') "[HvenqC● HvenqC◯]"; first apply excl_auth_valid.
300 iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqD' [HvdeqD● HvdeqD◯]]"; first apply excl_auth_valid.
301 iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqE' [HvdeqE● HvdeqE◯]]"; first apply excl_auth_valid.
302 iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqF' [HvdeqF● HvdeqF◯]]"; first apply excl_auth_valid.
303 iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contD') "[HcontD● HcontD◯]"; first apply excl_auth_valid.
304 iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contE') "[HcontE● HcontE◯]"; first apply excl_auth_valid.
305 iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contF') "[HcontF● HcontF◯]"; first apply excl_auth_valid.
306 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'.
307 replace γ2_linked' with γs.(γ2_linked) by done.
308 replace γ2_venqA' with γs.(γ2_venqA) by done.
309 replace γ2_venqB' with γs.(γ2_venqB) by done.
310 replace γ2_venqC' with γs.(γ2_venqC) by done.
311 replace γ2_vdeqD' with γs.(γ2_vdeqD) by done.
312 replace γ2_vdeqE' with γs.(γ2_vdeqE) by done.
313 replace γ2_vdeqF' with γs.(γ2_vdeqF) by done.
314 replace γ2_contD' with γs.(γ2_contD) by done.
315 replace γ2_contE' with γs.(γ2_contE) by done.
316 replace γ2_contF' with γs.(γ2_contF) by done.
317 iAssert (mt_inv γs ℓ_sum ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2)
318 with "[$Hhist1● $Hhist2E $Hlinked● $HvenqA● $HvenqB● $HvenqC● $HvdeqD● $HvdeqE● $HvdeqF● $HcontD● $HcontE● $HcontF● $Hq1 $Hq2 $Hsum]"
319 as "Hinv".
320 { iPureIntro. exists 0. split; try done. }
321 clearbody γs.
322 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'.
323 iMod (inv_alloc nroot _ (mt_inv γs ℓ_sum ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "Hinv") as "#Hinv".
324
325 pose (P1 := (own (γ2_venqA γs) (◯E {[+ 1 +]}) ∗ own (γ2_linked γs) (◯E true))%I).
326 pose (P2 := own (γ2_venqB γs) (◯E {[+ 2 +]})).
327 pose (P3 := own (γ2_venqC γs) (◯E {[+ 3 +]})).
328 pose (P4 := (∃ nD : nat, own γs.(γ2_contD) (◯E nD) ∗ ⌜nD ≠ 0⌝)%I).
329 pose (P5 := (∃ nE : nat, own γs.(γ2_contE) (◯E nE) ∗ ⌜nE ≠ 0⌝)%I).
330 pose (P6 := (∃ nF : nat, own γs.(γ2_contF) (◯E nF) ∗ ⌜nF ≠ 0⌝)%I).
331
332 wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3 ∗ P4 ∗ P5)%I (λ _, P6)%I with "[- HcontF◯ HvdeqF◯] [HcontF◯ HvdeqF◯]").
333 { wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3 ∗ P4)%I (λ _, P5)%I with "[- HcontE◯ HvdeqE◯] [HcontE◯ HvdeqE◯]").
334 { wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3)%I (λ _, P4)%I with "[- HcontD◯ HvdeqD◯] [HcontD◯ HvdeqD◯]").
335 { wp_smart_apply (wp_par (λ _, P1 ∗ P2)%I (λ _, P3)%I with "[- HvenqC◯] [HvenqC◯]").
336 { wp_smart_apply (wp_par (λ _, P1) (λ _, P2) with "[- HvenqB◯] [HvenqB◯]").
337 { awp_apply lqp.(enqueue_spec lq).
338 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
339 iNamedSuffix "H" "_1". iCombine "HvenqA◯ HvenqA●_1" gives %->%excl_auth_agree_L.
340 iCombine "Hlinked●_1 Hlinked◯" gives %->%excl_auth_agree_L.
341 iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. }
342 iIntros "Hq1".
343
344 iMod (mono_list_auth_own_update (hist1 ++ [1]) with "Hhist1●_1") as "[Hhist1●_1 _]".
345 { by apply prefix_app_r. }
346 iCombine "HvenqA●_1 HvenqA◯" as "HvenqA".
347 iMod (own_update with "HvenqA") as "[HvenqA●_1 HvenqA◯]".
348 { apply (excl_auth_update _ _ {[+ 1 +]}). }
349 replace (vals_of_nats vs1 ++ [ #1 ]) with (vals_of_nats (vs1 ++ [1]))
350 by rewrite /vals_of_nats fmap_app //.
351 iModIntro. iFrame "HvenqA◯". iFrame. iFrame "Hq1". iSplit.
352 { iPureIntro. exists ndeq. repeat split; try done.
353 + rewrite list_to_set_disj_app.
354 multiset_solver.
355 + apply Forall_app. by split; last apply Forall_singleton.
356 + etrans; first apply HnDEF_1.
357 apply prefix_submseteq, take_app_prefix.
358 + rewrite ->!length_app in *. lia.
359 + by rewrite drop_app_le // Hhistvs_1. }
360 wp_pures.
361 clear.
362
363 awp_apply lqp.(link_spec lq).
364 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
365 iNamedSuffix "H" "_2".
366 iCombine "Hlinked●_2 Hlinked◯" gives %->%excl_auth_agree_L.
367 rewrite /atomic_acc /=. iApply fupd_mask_intro; first set_solver. iIntros "Hclose".
368 iExists true. iFrame "Hq1_2 Hq2_2". iSplit.
369 { iIntros "[Hq1 Hq2]". iMod "Hclose" as "_". iModIntro.
370 iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. }
371 iIntros "Hq1". iMod "Hclose" as "_".
372
373 iCombine "Hlinked●_2 Hlinked◯" as "Hlinked".
374 iMod (own_update with "Hlinked") as "[Hlinked●_2 Hlinked◯]".
375 { apply (excl_auth_update _ _ true). }
376 iEval (rewrite /vals_of_nats -fmap_app -/vals_of_nats) in "Hq1".
377 iMod (mono_list_auth_own_update (hist1 ++ hist2) with "Hhist1●_2") as "[Hhist1●_2 _]"; first by apply prefix_app_r.
378 iFrame. iModIntro. iModIntro. iPureIntro. exists ndeq. repeat split; try done.
379 - rewrite list_to_set_disj_app. multiset_solver.
380 - by rewrite Forall_app.
381 - etrans; first apply HnDEF_2.
382 apply prefix_submseteq, take_app_prefix.
383 - rewrite length_app. lia.
384 - by rewrite drop_app_le // Hhistvs_2.
385 }
386 { awp_apply lqp.(enqueue_spec lq).
387 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
388 iNamedSuffix "H" "_1". iCombine "HvenqB◯ HvenqB●_1" gives %->%excl_auth_agree_L.
389
390 destruct linked eqn:Hlinked.
391 - iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. }
392 iIntros "Hq1".
393 iCombine "HvenqB●_1 HvenqB◯" as "HvenqB".
394 iMod (mono_list_auth_own_update (hist1 ++ [2]) with "Hhist1●_1") as "[Hhist1●_1 _]".
395 { by apply prefix_app_r. }
396 iMod (own_update with "HvenqB") as "[HvenqB●_1 HvenqB◯]".
397 { apply (excl_auth_update _ _ {[+ 2 +]}). }
398 replace (vals_of_nats vs1 ++ [ #2 ]) with (vals_of_nats (vs1 ++ [2]))
399 by rewrite /vals_of_nats fmap_app //.
400 iModIntro. iFrame "HvenqB◯". iModIntro. iFrame. iExists ndeq, (vs1 ++ [2]). iFrame.
401 iPureIntro. repeat split; try done.
402 + rewrite list_to_set_disj_app.
403 multiset_solver
404 + apply Forall_app.
405 + multiset_solver.
406 + apply Forall_app. by split; last apply Forall_singleton.
407 + etrans; first apply HnDEF_1.
408 apply prefix_submseteq, take_app_prefix.
409 + rewrite length_app. lia.
410 + by rewrite drop_app_le // Hhistvs_1.
411 - iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". iExists ndeq. by iFrame. }
412 iIntros "Hq1".
413 iCombine "HvenqB●_1 HvenqB◯" as "HvenqB".
414 iMod (own_update _ _ (Excl (hist2 ++ [2])) with "Hhist2E_1") as "Hhist2E_1"; first by intros ? [[]|].
415 iMod (own_update with "HvenqB") as "[HvenqB●_1 HvenqB◯]".
416 { apply (excl_auth_update _ _ {[+ 2 +]}). }
417 replace (vals_of_nats hist2 ++ [ #2 ]) with (vals_of_nats (hist2 ++ [2]))
418 by rewrite /vals_of_nats fmap_app //.
419 iModIntro. iFrame "HvenqB◯". iModIntro. iFrame. iFrame.
420 iPureIntro. exists ndeq. repeat split; try done.
421 + rewrite list_to_set_disj_app.
422 multiset_solver.
423 + apply Forall_app. split; first done.
424 by apply Forall_singleton.
425 }
426 { by iIntros (_ _) "H !>". }
427 }
428 { awp_apply lqp.(enqueue_spec lq).
429 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
430 iNamedSuffix "H" "_1". iCombine "HvenqC◯ HvenqC●_1" gives %->%excl_auth_agree_L.
431
432 destruct linked eqn:Hlinked.
433 - iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. }
434 iIntros "Hq1".
435 iCombine "HvenqC●_1 HvenqC◯" as "HvenqC".
436 iMod (mono_list_auth_own_update (hist1 ++ [3]) with "Hhist1●_1") as "[Hhist1●_1 _]".
437 { by apply prefix_app_r. }
438 iMod (own_update with "HvenqC") as "[HvenqC●_1 HvenqC◯]".
439 { apply (excl_auth_update _ _ {[+ 3 +]}). }
440 replace (vals_of_nats vs1 ++ [ #3 ]) with (vals_of_nats (vs1 ++ [3]))
441 by rewrite /vals_of_nats fmap_app //.
442 iModIntro. iFrame "HvenqC◯". iModIntro. iFrame. iExists ndeq, (vs1 ++ [3]). iFrame.
443 iPureIntro. repeat split; try done.
444 + rewrite list_to_set_disj_app.
445 multiset_solver.
446 + multiset_solver.
447 + apply Forall_app. by split; last apply Forall_singleton.
448 + etrans; first apply HnDEF_1.
449 apply prefix_submseteq, take_app_prefix.
450 + rewrite length_app. lia.
451 + by rewrite drop_app_le // Hhistvs_1.
452 - iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". iExists ndeq. by iFrame. }
453 iIntros "Hq1".
454 iCombine "HvenqC●_1 HvenqC◯" as "HvenqC".
455 iMod (own_update _ _ (Excl (hist2 ++ [3])) with "Hhist2E_1") as "Hhist2E_1"; first by intros ? [[]|].
456 iMod (own_update with "HvenqC") as "[HvenqC●_1 HvenqC◯]".
457 { apply (excl_auth_update _ _ {[+ 3 +]}). }
458 replace (vals_of_nats hist2 ++ [ #3 ]) with (vals_of_nats (hist2 ++ [3]))
459 by rewrite /vals_of_nats fmap_app //.
460 iModIntro. iFrame "HvenqC◯". iModIntro. iFrame. iFrame.
461 iPureIntro. exists ndeq. repeat split; try done.
462 + rewrite list_to_set_disj_app.
463 multiset_solver.
464 + apply Forall_app. split; first done.
465 by apply Forall_singleton.
466 }
467 { iIntros (_ _) "[H1 H2] !>". iFrame. }
468 }
469 { awp_apply (dequeue_spec lq lqp).
470 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
471 iNamedSuffix "H" "_1".
472 iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. }
473 iIntros (v0 vs') "[%Hvs Hq1]".
474 destruct vs1; simplify_eq/=.
475 iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1".
476 iCombine "HcontD◯ HcontD●_1" gives %->%excl_auth_agree_L.
477
478 iCombine "HvdeqD●_1 HvdeqD◯" as "HvdeqD" gives %->%excl_auth_agree_L.
479 iMod (own_update with "HvdeqD") as "[HvdeqD●_1 HvdeqD◯]".
480 { apply (excl_auth_update _ _ (Some n)). }
481
482 apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1].
483 iModIntro. iFrame. iFrameNamed. iSplit.
484 { iPureIntro. exists (S ndeq). repeat split; try done.
485 - etrans; first done.
486 simplify_eq/=. rewrite ->app_nil_r in *.
487 etrans. { apply Permutation_submseteq, Permutation_cons_append. }
488 rewrite (take_S_r _ _ n) //.
489 by apply submseteq_skips_r.
490 - by apply lookup_lt_Some in Hhistndeq_1. }
491
492 clear - Hhistndeq_1 Hhistvs_1.
493 iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H".
494 iNamedSuffix "H" "_2".
495 wp_faa.
496
497 iCombine "HcontD●_2 HcontD◯" as "HcontD" gives %->%excl_auth_agree_L.
498 iMod (own_update with "HcontD") as "[HcontD●_2 HcontD◯]".
499 { apply (excl_auth_update _ _ n). }
500
501 iEval (rewrite Z.add_0_l Z.add_comm Z.add_assoc) in "Hsum_2".
502
503 iCombine "HvdeqD●_2 HvdeqD◯" gives %->%excl_auth_agree_L.
504
505 iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre].
506 assert (Hn : n ≠ 0).
507 { eapply (Forall_lookup (.≠ 0)); last done.
508 by eapply Forall_prefix. }
509
510 iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro.
511 iPureIntro. exists ndeq'. repeat split; try done.
512 by rewrite /option_nat option_guard_True.
513 }
514 { iIntros (_ _) "[H1 H2] !>". iFrame. }
515 }
516 { awp_apply (dequeue_spec lq lqp).
517 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
518 iNamedSuffix "H" "_1".
519 iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. }
520 iIntros (v0 vs') "[%Hvs Hq1]".
521 destruct vs1; simplify_eq/=.
522 iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1".
523 iCombine "HcontE◯ HcontE●_1" gives %->%excl_auth_agree_L.
524
525 iCombine "HvdeqE●_1 HvdeqE◯" as "HvdeqE" gives %->%excl_auth_agree_L.
526 iMod (own_update with "HvdeqE") as "[HvdeqE●_1 HvdeqE◯]".
527 { apply (excl_auth_update _ _ (Some n)). }
528
529 apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1].
530 iModIntro. iFrame. iFrameNamed. iSplit.
531 { iPureIntro. exists (S ndeq). repeat split; try done. etrans; first done.
532 - simplify_eq/=. rewrite app_nil_r in HnDEF_1.
533 rewrite app_nil_r.
534 etrans. { apply submseteq_skips_l, Permutation_submseteq, Permutation_cons_append. }
535 rewrite (take_S_r _ _ n) // app_assoc.
536 by apply submseteq_skips_r.
537 - by apply lookup_lt_Some in Hhistndeq_1. }
538
539 clear - Hhistndeq_1 Hhistvs_1.
540 iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H".
541 iNamedSuffix "H" "_2".
542 wp_faa.
543
544 iCombine "HcontE●_2 HcontE◯" as "HcontE" gives %->%excl_auth_agree_L.
545 iMod (own_update with "HcontE") as "[HcontE●_2 HcontE◯]".
546 { apply (excl_auth_update _ _ n). }
547
548 iEval (rewrite Z.add_0_r -Z.add_assoc [(nF + n)%Z]Z.add_comm Z.add_assoc) in "Hsum_2".
549
550 iCombine "HvdeqE●_2 HvdeqE◯" gives %->%excl_auth_agree_L.
551
552 iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre].
553 assert (Hn : n ≠ 0).
554 { eapply (Forall_lookup (.≠ 0)); last done.
555 by eapply Forall_prefix. }
556
557 iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro.
558 iPureIntro. exists ndeq'. repeat split; try done.
559 by rewrite /option_nat option_guard_True.
560 }
561 { iIntros (_ _) "[H1 H2] !>". iFrame. }
562 }
563 { awp_apply (dequeue_spec lq lqp).
564 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
565 iNamedSuffix "H" "_1".
566 iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. }
567 iIntros (v0 vs') "[%Hvs Hq1]".
568 destruct vs1; simplify_eq/=.
569 iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1".
570 iCombine "HcontF◯ HcontF●_1" gives %->%excl_auth_agree_L.
571
572 iCombine "HvdeqF●_1 HvdeqF◯" as "HvdeqF" gives %->%excl_auth_agree_L.
573 iMod (own_update with "HvdeqF") as "[HvdeqF●_1 HvdeqF◯]".
574 { apply (excl_auth_update _ _ (Some n)). }
575
576 apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1].
577 iModIntro. iFrame. iFrameNamed. iSplit.
578 { iPureIntro. exists (S ndeq). repeat split; try done. etrans; first done.
579 - simplify_eq/=. rewrite app_nil_r in HnDEF_1.
580 rewrite (take_S_r _ _ n) // app_assoc.
581 by apply submseteq_skips_r.
582 - by apply lookup_lt_Some in Hhistndeq_1. }
583
584 clear - Hhistndeq_1 Hhistvs_1.
585 iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H".
586 iNamedSuffix "H" "_2".
587 wp_faa.
588
589 iCombine "HcontF●_2 HcontF◯" as "HcontF" gives %->%excl_auth_agree_L.
590 iMod (own_update with "HcontF") as "[HcontF●_2 HcontF◯]".
591 { apply (excl_auth_update _ _ n). }
592
593 iEval (rewrite Z.add_0_r) in "Hsum_2".
594
595 iCombine "HvdeqF●_2 HvdeqF◯" gives %->%excl_auth_agree_L.
596
597 iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre].
598 assert (Hn : n ≠ 0).
599 { eapply (Forall_lookup (.≠ 0)); last done.
600 by eapply Forall_prefix. }
601
602 iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro.
603 iPureIntro. exists ndeq'. repeat split; try done.
604 by rewrite /option_nat option_guard_True.
605 }
606
607 iIntros (v1 v2) "[(H1 & HvenqB◯ & HvenqC◯ & H4 & H5) H6]".
608 unfold P1, P2, P3, P4, P5, P6. clear P1 P2 P3 P4 P5 P6.
609 iDestruct "H1" as "[HvenqA◯ Hlinked◯]".
610 iDestruct "H4" as "(%nD' & HnD'◯ & %HcontD)".
611 iDestruct "H5" as "(%nE' & HnE'◯ & %HcontE)".
612 iDestruct "H6" as "(%nF' & HnF'◯ & %HcontF)".
613 iModIntro. wp_pures.
614
615 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">@".
616 wp_load. iModIntro. iSplit; [by iFrame; iExists ndeq|].
617 iCombine "HnD'◯ HcontD●" gives %<-%excl_auth_agree_L. iClear "HnD'◯ HcontD●".
618 iCombine "HnE'◯ HcontE●" gives %<-%excl_auth_agree_L. iClear "HnE'◯ HcontE●".
619 iCombine "HnF'◯ HcontF●" gives %<-%excl_auth_agree_L. iClear "HnF'◯ HcontF●".
620
621 rewrite /option_nat !option_guard_True // in HD HE HF.
622 apply option_le_inv in HD as [HD|<-]; first done.
623 apply option_le_inv in HE as [HE|<-]; first done.
624 apply option_le_inv in HF as [HF|<-]; first done.
625 simplify_eq/=.
626
627 iCombine "Hlinked● Hlinked◯" gives %->%excl_auth_agree_L.
628 iClear "Hq2 Hlinked● Hlinked◯".
629
630 iCombine "HvenqA● HvenqA◯" gives %->%excl_auth_agree_L. iClear "HvenqA◯ HvenqA●".
631 iCombine "HvenqB● HvenqB◯" gives %->%excl_auth_agree_L. iClear "HvenqB◯ HvenqB●".
632 iCombine "HvenqC● HvenqC◯" gives %->%excl_auth_agree_L. iClear "HvenqC◯ HvenqC●".
633 iPureIntro. enough (nD + nE + nF = 6). { do 2 f_equal. lia. }
634
635 assert (ndeq ≥ 3 ∧ length hist1 ≥ 3) as [Hndeq' Hhist1'].
636 { apply submseteq_length in HnDEF as Hndeq'.
637 rewrite /= length_take in Hndeq'. lia. }
638 apply gmultiset_subseteq_size in Hhist1 as Hhist1''.
639 rewrite list_to_set_disj_size !gmultiset_size_disj_union !gmultiset_size_singleton /= in Hhist1''.
640 have {Hhist1''}Hhist1' : length hist1 = 3 by lia.
641 apply gmultiset_subseteq_size_eq in Hhist1; last first.
642 { rewrite !gmultiset_size_disj_union !gmultiset_size_singleton /= list_to_set_disj_size. lia. }
643
644 assert (HnDEF' : [nD; nE; nF] ≡ₚ hist1).
645 { apply submseteq_length_Permutation; last (simpl; lia).
646 etrans; [apply HnDEF | apply submseteq_take]. }
647
648 assert (Hhist1'' : hist1 ≡ₚ elements ({[+ 1; 2; 3 +]} : gmultiset nat)).
649 { erewrite elements_list_to_set_disj_perm.
650 by rewrite Hhist1. }
651
652 assert (H123 : elements ({[+ 1; 2; 3 +]} : gmultiset nat) ≡ₚ [1; 2; 3]).
653 { by rewrite !gmultiset_elements_disj_union !gmultiset_elements_singleton /=. }
654
655 trans (foldr Nat.add 0 [nD; nE; nF]). { simpl. lia. }
656 by rewrite HnDEF' Hhist1'' H123.
657 Qed.
658
659End proofs.
660
661Definition fq := fin_queue_proof.fin_queue_hl.
662Definition lq := lmpmc_queue_proof.lmpmc_queue_hl fq.
663
664(** First example *)
665
666Definition simple_clientΣ : gFunctors := #[ heapΣ; fin_queue_proof.fin_queueΣ ].
667Lemma simple_client_adequate σ : adequate NotStuck (simple_example_2_1 lq) σ (λ v _, v = (#10, #20)%V).
668Proof.
669 eapply (heap_adequacy simple_clientΣ). iIntros (?) "_". iApply simple_example_2_1_safe.
670 Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris.
671Qed.
672
673(** Second example *)
674
675Definition simple_mt_clientΣ : gFunctors :=
676 #[ heapΣ; spawnΣ;
677 fin_queue_proof.fin_queueΣ;
678 GFunctor (excl_authRF boolO);
679 GFunctor (excl_authRF (listO natO)) ].
680
681Instance smc_inG_excl_auth_bool Σ : subG simple_mt_clientΣ Σ → inG Σ (excl_authR boolO).
682Proof. solve_inG. Qed.
683Instance smc_inG_excl_auth_nat_list Σ : subG simple_mt_clientΣ Σ → inG Σ (excl_authR (listO natO)).
684Proof. solve_inG. Qed.
685
686Lemma simple_mt_client_adequate σ : adequate NotStuck (simple_example_2_2 lq) σ (λ v _, v = (#10, #20)%V).
687Proof.
688 eapply (heap_adequacy simple_mt_clientΣ). iIntros (?) "_". iApply simple_example_2_2_safe.
689 Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris.
690Qed.
691
692(** Third example *)
693
694Definition mt_example_1Σ : gFunctors :=
695 #[ heapΣ; spawnΣ;
696 fin_queue_proof.fin_queueΣ;
697 mono_listΣ natO;
698 GFunctor (excl_authRF (gmultisetO nat));
699 GFunctor (excl_authRF natO);
700 GFunctor (excl_authRF boolO);
701 GFunctor (excl_authRF (optionO natO));
702 GFunctor (exclR (listO natO)) ].
703
704Instance me_inG_excl_auth_multiset Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR (gmultisetO nat)).
705Proof. solve_inG. Qed.
706Instance me_inG_excl_auth_nat Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR natO).
707Proof. solve_inG. Qed.
708Instance me_inG_excl_auth_bool Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR boolO).
709Proof. solve_inG. Qed.
710Instance me_inG_excl_auth_option_nat Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR (optionO natO)).
711Proof. solve_inG. Qed.
712Instance me_inG_excl_list_nat Σ : subG mt_example_1Σ Σ → inG Σ (exclR (listO natO)).
713Proof. solve_inG. Qed.
714
715Lemma mt_example_1_adequate σ : adequate NotStuck (mt_example_1 lq) σ (λ v _, v = #6%V).
716Proof.
717 eapply (heap_adequacy mt_example_1Σ). iIntros (?) "_". iApply mt_example_1_safe.
718 Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris.
719Qed.
720
721Print Assumptions simple_client_adequate.
722Print Assumptions simple_mt_client_adequate.
723Print 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 @@
1From iris.program_logic Require Import atomic.
2From iris.heap_lang Require Import notation proofmode.
3From iris.algebra.lib Require Import excl_auth.
4From iris.base_logic.lib Require Import invariants.
5From iris.base_logic.lib Require Import invariants mono_nat mono_list.
6From iris_named_props Require Import custom_syntax.
7
8From lmpmc Require Import fin_queue_spec upstream util.
9
10Definition new_node : val := λ: "data" "final",
11 let: "ℓ_node" := AllocN #3 #() in
12 "ℓ_node" <- "data";;
13 "ℓ_node" +ₗ #1 <- NONE;;
14 "ℓ_node" +ₗ #2 <- "final";;
15 "ℓ_node".
16
17Definition new : val := λ: <>,
18 let: "ℓ_node" := new_node #() #false in
19 AllocN #2 "ℓ_node".
20
21Definition set_tail : val := rec: "go" "ℓ_q" "ℓ_node" :=
22 let: "ℓ_tail" := !("ℓ_q" +ₗ #1) in
23 match: !("ℓ_tail" +ₗ #1) with
24 NONE =>
25 if: CAS ("ℓ_tail" +ₗ #1) NONE (SOME "ℓ_node") then
26 #()
27 else
28 "go" "ℓ_q" "ℓ_node"
29 | SOME "ℓ_next" =>
30 CAS ("ℓ_q" +ₗ #1) "ℓ_tail" "ℓ_next";;
31 "go" "ℓ_q" "ℓ_node"
32 end.
33
34Definition enqueue : val := λ: "ℓ_q" "data",
35 set_tail "ℓ_q" (new_node "data" #false).
36
37Definition finalize : val := λ: "ℓ_q" "data",
38 set_tail "ℓ_q" (new_node "data" #true).
39
40Definition try_dequeue : val := rec: "go" "ℓ_q" :=
41 let: "ℓ_head" := !"ℓ_q" in
42 match: !("ℓ_head" +ₗ #1) with
43 NONE => InjR NONE
44 | SOME "ℓ_next" =>
45 if: !("ℓ_next" +ₗ #2) then
46 (* The next node is the final node. We refuse to dequeue and
47 return the data of the final node. *)
48 InjR (SOME !"ℓ_next")
49 else (* [ℓ_next] node type = normal *)
50 let: "v" := !"ℓ_next" in
51 if: CAS "ℓ_q" "ℓ_head" "ℓ_next" then
52 InjL "v"
53 else
54 "go" "ℓ_q"
55 end.
56
57Class fin_queueG Σ := FinQueueG
58 { fin_queue_mono_natG :: mono_natG Σ;
59 fin_queue_mono_listG :: mono_listG (prodO locO valO) Σ; }.
60
61Definition fin_queueΣ : gFunctors :=
62 #[ mono_natΣ; mono_listΣ (prodO locO valO) ].
63
64#[global] Instance subG_fin_queueΣ {Σ} : subG fin_queueΣ Σ → fin_queueG Σ.
65Proof. solve_inG. Qed.
66
67Section fin_queue.
68 Context `{!heapGS Σ, !fin_queueG Σ}.
69
70 Record gstate :=
71 { γ_hist : gname;
72 γ_hpos : gname; }.
73 Definition gstate_to_pair (γ : gstate) :=
74 (γ.(γ_hist), γ.(γ_hpos)).
75 Definition gstate_of_pair '(γ_hist, γ_hpos) :=
76 {| γ_hist := γ_hist; γ_hpos := γ_hpos |}.
77 Instance gstate_eq_dec : EqDecision gstate := ltac:(solve_decision).
78 Instance gstate_countable : Countable gstate.
79 Proof.
80 refine {| encode := encode ∘ gstate_to_pair;
81 decode := fmap gstate_of_pair ∘ decode; |}.
82 intros []. by rewrite /= decode_encode.
83 Qed.
84
85 Variant node_next :=
86 | Normal (mℓ_next : option loc)
87 | Final.
88 Instance node_next_eq_dec : EqDecision node_next.
89 Proof. solve_decision. Defined.
90 Definition node_final_hl (n : node_next) := #(bool_decide (n = Final)).
91 Definition node_next_hl (n : node_next) :=
92 match n with
93 | Normal mℓ_next => loc_opt_hl mℓ_next
94 | Final => NONEV
95 end.
96
97 Definition node_repr (ℓ : loc) (data : val) (n : node_next) : iProp Σ :=
98 ("Hndata" ∷ ℓ ↦□ data) ∗
99 ("Hnnext" ∷ (ℓ +ₗ 1) ↦ node_next_hl n) ∗
100 ("Hnfinal" ∷ (ℓ +ₗ 2) ↦□ #(bool_decide (n = Final))).
101
102 Definition loc_at (hist : list (loc * val)) i :=
103 hist.*1 !! i.
104 Definition val_at (hist : list (loc * val)) i :=
105 hist.*2 !! i.
106
107 Lemma loc_at_prefix xs xs' i ℓ :
108 loc_at xs i = Some ℓ → xs `prefix_of` xs' → loc_at xs' i = Some ℓ.
109 Proof.
110 unfold loc_at. intros Hxs Hpre.
111 eapply prefix_lookup_Some; first exact Hxs.
112 by apply prefix_of_fmap.
113 Qed.
114
115 Lemma val_at_prefix xs xs' i ℓ :
116 val_at xs i = Some ℓ → xs `prefix_of` xs' → val_at xs' i = Some ℓ.
117 Proof.
118 unfold val_at. intros Hxs Hpre.
119 eapply prefix_lookup_Some; first exact Hxs.
120 by apply prefix_of_fmap.
121 Qed.
122
123 Lemma loc_at_val_at_Some xs i ℓ :
124 loc_at xs i = Some ℓ → ∃ v, val_at xs i = Some v.
125 Proof.
126 unfold loc_at, val_at. rewrite [xs.*2 !! i]list_lookup_fmap.
127 intros [[ℓ' v] [-> ->]]%list_lookup_fmap_Some_1. by exists v.
128 Qed.
129
130 Lemma loc_at_val_at_combine {hist i ℓ v} :
131 loc_at hist i = Some ℓ →
132 val_at hist i = Some v →
133 hist !! i = Some (ℓ, v).
134 Proof.
135 unfold loc_at, val_at. intros Hloc Hval.
136 rewrite list_lookup_fmap in Hloc.
137 rewrite list_lookup_fmap in Hval.
138 destruct (hist !! i) as [[ℓ' v']|]; last done.
139 simpl in *. congruence.
140 Qed.
141
142 Lemma loc_at_Some_length hist i ℓ :
143 loc_at hist i = Some ℓ → i < length hist.
144 Proof.
145 intros Hloc%lookup_lt_Some.
146 by rewrite length_fmap in Hloc.
147 Qed.
148
149 Lemma loc_at_drop hist n i ℓ :
150 loc_at hist (n + i) = Some ℓ →
151 loc_at (drop n hist) i = Some ℓ.
152 Proof.
153 unfold loc_at. intros Hloc.
154 by rewrite list_lookup_fmap lookup_drop -list_lookup_fmap.
155 Qed.
156
157 Lemma val_at_drop hist n i ℓ :
158 val_at hist (n + i) = Some ℓ →
159 val_at (drop n hist) i = Some ℓ.
160 Proof.
161 unfold val_at. intros Hval.
162 by rewrite list_lookup_fmap lookup_drop -list_lookup_fmap.
163 Qed.
164
165 Definition next_from (hist : list (loc * val)) fin i :=
166 if fin && bool_decide (S i = length hist) then Final else Normal (loc_at hist (S i)).
167
168 Definition next_from_normal hist fin i v :
169 next_from hist fin i = Normal v →
170 (fin = false ∨ S i ≠ length hist) ∧ loc_at hist (S i) = v.
171 Proof.
172 rewrite /next_from. intros H.
173 destruct fin, (decide (S i = length hist)).
174 - rewrite bool_decide_true //= in H.
175 - rewrite bool_decide_false //= in H.
176 injection H as <-. split; last done. by right.
177 - injection H as <-. split; last done. by left.
178 - injection H as <-. split; last done. by left.
179 Qed.
180
181 Lemma next_from_S ℓv ℓvs fin n :
182 next_from (ℓv :: ℓvs) fin (S n) = next_from ℓvs fin n.
183 Proof.
184 rewrite /next_from /loc_at list_lookup_fmap /= -list_lookup_fmap.
185 erewrite bool_decide_ext; first done. lia.
186 Qed.
187
188 Lemma node_next_hl_next_from hist fin i :
189 node_next_hl (next_from hist fin i) = loc_opt_hl (loc_at hist (S i)).
190 Proof.
191 unfold node_next_hl, next_from.
192 destruct fin, (decide (S i = length hist)) as [Hhist|Hhist]; simpl; try done.
193 - by rewrite bool_decide_true // /loc_at list_lookup_fmap lookup_ge_None_2; last lia.
194 - by rewrite bool_decide_false.
195 Qed.
196
197 Definition hist_repr (hist : list (loc * val)) (fin : bool) : iProp Σ :=
198 [∗ list] i ↦ '(ℓ, data) ∈ hist, node_repr ℓ data (next_from hist fin i).
199
200 Lemma hist_repr_peek_1 hist fin i ℓ data :
201 loc_at hist i = Some ℓ →
202 val_at hist i = Some data →
203 hist_repr hist fin -∗
204 node_repr ℓ data (next_from hist fin i) ∗
205 (node_repr ℓ data (next_from hist fin i) -∗ hist_repr hist fin).
206 Proof.
207 iIntros "%Hloc %Hval Hrepr".
208 pose proof (loc_at_val_at_combine Hloc Hval) as Hi.
209 iPoseProof (big_sepL_lookup_acc with "Hrepr") as "[Hnode Hclose]".
210 { apply Hi. }
211 iFrame.
212 Qed.
213
214 Lemma hist_repr_peek_2 hist fin i ℓ :
215 loc_at hist i = Some ℓ →
216 hist_repr hist fin -∗
217 ∃ data, node_repr ℓ data (next_from hist fin i) ∗
218 (node_repr ℓ data (next_from hist fin i) -∗ hist_repr hist fin).
219 Proof.
220 iIntros "%Hloc Hrepr".
221 assert (∃ v, val_at hist i = Some v) as [v Hval].
222 { by apply loc_at_val_at_Some in Hloc. }
223 iExists v. by iApply hist_repr_peek_1.
224 Qed.
225
226 Lemma hist_repr_peek_3 hist fin i ℓ :
227 loc_at hist i = Some ℓ →
228 hist_repr hist fin -∗
229 (ℓ +ₗ 1) ↦ node_next_hl (next_from hist fin i) ∗
230 ((ℓ +ₗ 1) ↦ node_next_hl (next_from hist fin i) -∗ hist_repr hist fin).
231 Proof.
232 iIntros "%Hloc Hrepr".
233 iDestruct (hist_repr_peek_2 with "[$]") as "(%v & @ & Hclose)"; first done.
234 iFrame. iIntros "Hnnext". iApply "Hclose". iFrame.
235 Qed.
236
237 Lemma loc_at_None hist pos :
238 loc_at hist pos = None → hist !! pos = None.
239 Proof.
240 rewrite /loc_at list_lookup_fmap.
241 by destruct (hist !! pos).
242 Qed.
243
244 Lemma loc_at_length hist pos :
245 loc_at hist pos = None → length hist ≤ pos.
246 Proof.
247 intros H%loc_at_None.
248 by apply lookup_ge_None.
249 Qed.
250
251 Lemma next_from_drop ℓvs fin n i :
252 next_from ℓvs fin (n + i) = next_from (drop n ℓvs) fin i.
253 Proof.
254 rewrite /next_from /loc_at list_lookup_fmap /= -list_lookup_fmap.
255 erewrite bool_decide_ext with (Q:=S i = length (drop n ℓvs)); last first.
256 { rewrite length_drop. lia. }
257 by rewrite fmap_drop list_lookup_fmap lookup_drop -list_lookup_fmap plus_n_Sm.
258 Qed.
259
260 Lemma hist_repr_proj hist i ℓ fin :
261 loc_at hist i = Some ℓ →
262 hist_repr hist fin -∗
263 (∃ v, (ℓ +ₗ 1) ↦ v) ∗ hist_repr (drop (S i) hist) fin.
264 Proof.
265 iIntros "%Hℓi Hrepr".
266 iDestruct (big_sepL_take_drop _ _ (S i) with "Hrepr") as "[Hrepr1 Hrepr2]".
267
268 rewrite /loc_at list_lookup_fmap in Hℓi.
269 destruct (hist !! i) as [[ℓ' v]|] eqn:Hi; last done.
270 simpl in *. injection Hℓi as ->.
271
272 iDestruct (big_sepL_lookup_acc with "Hrepr1") as "[Hrepr Hclose]".
273 { rewrite lookup_take_lt //. lia. }
274 iSimplifyEq. iDestruct "Hrepr" as "@". iFrame.
275 iClear "Hndata Hnfinal Hclose".
276
277 iAssert (hist_repr (drop (S i) hist) fin) with "[Hrepr2]" as "Hrepr2".
278 { unfold hist_repr. iApply (big_sepL_mono with "Hrepr2").
279 iIntros (k [ℓ' v'] Hk) "Hrepr".
280 rewrite -next_from_drop; first done. }
281 done.
282 Qed.
283
284 Lemma loc_at_inj_aux hist i j ℓ fin :
285 i < j →
286 loc_at hist i = Some ℓ →
287 loc_at hist j = Some ℓ →
288 hist_repr hist fin -∗
289 False.
290 Proof.
291 iIntros "%ij %Hloci %Hlocj Hrepr".
292 assert (i < length hist). { by eapply loc_at_Some_length. }
293 assert (j < length hist). { by eapply loc_at_Some_length. }
294 assert (∃ n, j = S i + n) as [n ->].
295 { exists (j - i - 1). lia. }
296 iPoseProof (hist_repr_proj hist i ℓ fin Hloci with "Hrepr") as "[[%ni Hℓi] Hrepr']".
297
298 assert (Hlocj' : loc_at (drop (S i) hist) n = Some ℓ).
299 { by apply loc_at_drop. }
300
301 iPoseProof (hist_repr_proj _ n ℓ fin Hlocj' with "Hrepr'") as "[[%nj Hℓj] _]".
302 by iCombine "Hℓi Hℓj" gives %[? _].
303 Qed.
304
305 Lemma loc_at_inj {hist i j ℓ fin} :
306 loc_at hist i = Some ℓ →
307 loc_at hist j = Some ℓ →
308 hist_repr hist fin -∗
309 ⌜i = j⌝.
310 Proof.
311 iIntros "%Hloci %Hlocj Hrepr".
312 destruct (loc_at_val_at_Some hist i ℓ Hloci) as [vi Hvali].
313 destruct (loc_at_val_at_Some hist j ℓ Hlocj) as [vj Hvalj].
314 destruct (decide (i < j)) as [Hij|Hij].
315 - (* i < j *)
316 by iPoseProof (loc_at_inj_aux with "Hrepr") as "H".
317 - (* i ≥ j *)
318 destruct (decide (j < i)) as [Hji|Hji].
319 + (* j < i *)
320 by iPoseProof (loc_at_inj_aux with "Hrepr") as "H".
321 + (* i = j *)
322 iPureIntro. lia.
323 Qed.
324
325 Definition queue_γs_dq (hist : list (loc * val)) (hpos : nat) (mfin : option val) : dfrac :=
326 match mfin with
327 | None => DfracOwn 1
328 | Some _ =>
329 if decide (S (S hpos) = length hist)
330 then DfracDiscarded
331 else DfracOwn 1
332 end.
333
334 Lemma queue_γs_dq_cases hist hpos mfin :
335 queue_γs_dq hist hpos mfin = DfracOwn 1 ∨
336 queue_γs_dq hist hpos mfin = DfracDiscarded.
337 Proof.
338 unfold queue_γs_dq.
339 destruct mfin, (decide (S (S hpos) = length hist));
340 (by left) || by right.
341 Qed.
342
343 Definition queue_repr_1 (γs : gstate) ℓ_q (vs : list val) (mfin : option val) : iProp Σ :=
344 ∃ (hist : list (loc * val)) (ℓ_head ℓ_tail : loc) (hpos tpos : nat),
345 ("Hhead" ∷ ℓ_q ↦ #ℓ_head) ∗
346 (* Not immediately clear whether this can be discarded when the queue is
347 finalized and otherwise emptied *)
348 ("Htail" ∷ (ℓ_q +ₗ 1) ↦ #ℓ_tail) ∗
349 ("Hrepr" ∷ hist_repr hist (bool_decide (is_Some mfin))) ∗
350 ("Hhist●" ∷ γs.(γ_hist) ↪●ML{queue_γs_dq hist hpos mfin} hist) ∗
351 ("Hhpos●" ∷ γs.(γ_hpos) ↪●MN{queue_γs_dq hist hpos mfin} hpos) ∗
352 ("%Hℓhpos" ∷ ⌜loc_at hist hpos = Some ℓ_head⌝) ∗
353 ("%Hℓtpos" ∷ ⌜loc_at hist tpos = Some ℓ_tail⌝) ∗
354 ("%Hvs" ∷ ⌜vs ++ option_list mfin = (drop (S hpos) hist).*2⌝).
355
356 Definition queue_fin_1 (γs : gstate) (fin : val) : iProp Σ :=
357 ∃ (hist : list (loc * val)) (hpos : nat),
358 ("Hhist" ∷ γs.(γ_hist) ↪●ML□ hist) ∗
359 ("Hhpos" ∷ γs.(γ_hpos) ↪●MN□ hpos) ∗
360 ("%Hfin" ∷ ⌜val_at hist (S hpos) = Some fin⌝).
361
362 Definition queue_repr ℓ_q (vs : list val) (mfin : option val) : iProp Σ :=
363 ∃ (γs : gstate), meta ℓ_q nroot γs ∗ queue_repr_1 γs ℓ_q vs mfin.
364
365 #[global] Instance queue_repr_timeless ℓ_q vs mfin : Timeless (queue_repr ℓ_q vs mfin) := _.
366
367 Definition queue_fin ℓ_q (fin : val) : iProp Σ :=
368 ∃ (γs : gstate), meta ℓ_q nroot γs ∗ queue_fin_1 γs fin.
369
370 #[global] Instance queue_fin_persistent ℓ_q fin : Persistent (queue_fin ℓ_q fin) := _.
371 #[global] Instance queue_fin_timeless ℓ_q fin : Timeless (queue_fin ℓ_q fin) := _.
372
373 Lemma queue_fin_obtain ℓ fin : queue_repr ℓ [] (Some fin) -∗ queue_fin ℓ fin.
374 Proof.
375 iIntros "(%γs & Hγs & @)". simplify_eq/=.
376 assert (Hlen : length (drop (S hpos) hist).*2 = 1) by rewrite -Hvs //.
377 rewrite fmap_drop length_drop length_fmap in Hlen.
378 case_decide; last lia. iFrame. iPureIntro.
379 by rewrite /val_at -[S hpos]Nat.add_0_r -lookup_drop -fmap_drop -Hvs.
380 Qed.
381
382 Lemma queue_fin_agree ℓ vs fin mfin :
383 queue_fin ℓ fin -∗
384 queue_repr ℓ vs mfin -∗
385 ⌜vs = []⌝ ∗ ⌜mfin = Some fin⌝.
386 Proof.
387 iIntros "(%γs & Hγs & @) (%γs' & Hγs' & @)".
388 iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
389 iDestruct (mono_list_auth_own_agree with "Hhist Hhist●") as %[Hfracs <-].
390 iDestruct (mono_nat_auth_own_agree with "Hhpos Hhpos●") as %[_ <-].
391 iPureIntro.
392
393 unfold queue_γs_dq in Hfracs.
394 destruct mfin as [fin'|]; last done.
395 destruct (decide (S (S hpos) = length hist)); last done.
396
397 assert (Hlen : S (length vs) = 1).
398 { rewrite -Nat.add_1_r -(length_app _ [fin']) Hvs length_fmap length_drop -e. lia. }
399 destruct vs; last done. simplify_eq/=.
400
401 by rewrite -Hfin /val_at -[S hpos]Nat.add_0_r -lookup_drop -fmap_drop -Hvs.
402 Qed.
403
404 Lemma hist_weaken {γs} hist hpos mfin :
405 γs.(γ_hist) ↪●ML hist ==∗ γs.(γ_hist) ↪●ML{queue_γs_dq hist hpos mfin} hist.
406 Proof.
407 iIntros "Hhist".
408 destruct (queue_γs_dq_cases hist hpos mfin) as [-> | ->]; first done.
409 by iApply mono_list_auth_own_persist.
410 Qed.
411
412 Lemma hpos_weaken {γs hpos} hist mfin :
413 γs.(γ_hpos) ↪●MN hpos ==∗ γs.(γ_hpos) ↪●MN{queue_γs_dq hist hpos mfin} hpos.
414 Proof.
415 iIntros "Hhist".
416 destruct (queue_γs_dq_cases hist hpos mfin) as [-> | ->]; first done.
417 by iApply mono_nat_own_persist.
418 Qed.
419
420 Variant new_node_next := NonFinalType | FinalType.
421 Definition new_node_next_red (n : new_node_next) :=
422 match n with
423 | NonFinalType => Normal None
424 | FinalType => Final
425 end.
426 Instance new_node_next_eq_dec : EqDecision new_node_next.
427 Proof. solve_decision. Defined.
428
429 Lemma new_node_spec data (final : bool) :
430 {{{ True }}}
431 new_node data #final
432 {{{ (ℓ : loc), RET #ℓ; node_repr ℓ data (new_node_next_red (if final then FinalType else NonFinalType)) }}}.
433 Proof.
434 iIntros "%Φ _ HΦ". iUnfold new_node. wp_lam.
435 wp_alloc ℓ_node as "Hℓ_node"; first done.
436 iDestruct (array_cons with "Hℓ_node") as "[Hℓ_node0 Hℓ_node12]".
437 iDestruct (array_cons with "Hℓ_node12") as "[Hℓ_node1 Hℓ_node2]".
438 iDestruct (array_cons with "Hℓ_node2") as "[Hℓ_node2 _]".
439 rewrite Loc.add_assoc.
440 wp_let. do 3 wp_store.
441 iMod (pointsto_persist with "Hℓ_node0") as "Hℓ_node0".
442 iMod (pointsto_persist with "Hℓ_node2") as "Hℓ_node2".
443 iModIntro. iApply "HΦ". destruct final; by iFrame.
444 Qed.
445
446 Lemma new_spec :
447 {{{ True }}}
448 new #()
449 {{{ (ℓ : loc), RET #ℓ; queue_repr ℓ [] None }}}.
450 Proof.
451 iIntros "%Φ _ HΦ". iUnfold new.
452 wp_lam. wp_apply (new_node_spec with "[//]") as (ℓ_node) "Hnode". wp_let.
453
454 set ℓ_head := ℓ_node. set ℓ_tail := ℓ_node.
455 set hpos := 0. set tpos := 0.
456 set hist := [(ℓ_node, #())] : list (loc * val).
457 iAssert (hist_repr hist false) with "[$Hnode //]" as "Hrepr".
458
459 iMod (mono_list_own_alloc hist) as "[%γ_hist [Hhist● _]]".
460 iMod (mono_nat_own_alloc hpos) as "[%γ_hpos [Hhpos● _]]".
461 set γs := {| γ_hist := γ_hist; γ_hpos := γ_hpos |}.
462
463 iApply wp_fupd. iApply wp_allocN; [lia|done|].
464 iIntros "!> %ℓ [Hℓ [Htok _]]".
465 iDestruct (array_cons with "Hℓ") as "[Hℓ0 Hℓ1]".
466 iDestruct (array_cons with "Hℓ1") as "[Hℓ1 _]".
467 rewrite Loc.add_0.
468
469 iMod (meta_set ⊤ ℓ γs nroot with "Htok") as "Hmeta"; first done.
470
471 iApply "HΦ". iModIntro. iFrame. by iExists tpos.
472 Qed.
473
474 Lemma try_bump_tail_spec hist0 tpos ℓ_old ℓ_new ℓ_q γs :
475 loc_at hist0 tpos = Some ℓ_old →
476 loc_at hist0 (S tpos) = Some ℓ_new →
477 γs.(γ_hist) ↪◯ML hist0 -∗
478 <<{ ∀∀ vs mfin, queue_repr_1 γs ℓ_q vs mfin }>>
479 CAS #(ℓ_q +ₗ 1) #ℓ_old #ℓ_new @ ∅
480 <<{ ∃∃ (b : bool), queue_repr_1 γs ℓ_q vs mfin | RET #b }>>.
481 Proof.
482 iIntros "%Hold %Hnew #Hhist◯ %Φ AU".
483 wp_bind (CmpXchg _ _ _)%E.
484 iMod "AU" as "(%vs & %fin & (%hist1 & %ℓ_head & %ℓ_tail & %hpos & %tpos' & @) & [_ Hclose])".
485 iAssert ⌜hist0 `prefix_of` hist1⌝%I as %Hhist01.
486 { by iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist◯") as "[_ ?]". }
487
488 destruct (decide (ℓ_tail = ℓ_old)) as [->|].
489 - (* The tail has not been updated yet *)
490 wp_cmpxchg_suc.
491
492 iAssert (queue_repr_1 γs ℓ_q vs fin) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
493 { iPureIntro.
494 repeat split; try done || lia.
495 exists (S tpos). repeat split; try done.
496 by eapply loc_at_prefix. }
497 iMod ("Hclose" with "[$Hq]") as "HΦ".
498 iModIntro. wp_pures. iApply "HΦ".
499 - (* The tail has been updated in the meantime *)
500 wp_cmpxchg_fail.
501 iAssert (queue_repr_1 γs ℓ_q vs fin) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
502 { iExists tpos'. by iFrameNamed. }
503 iMod ("Hclose" with "[$Hq]") as "HΦ".
504 iModIntro. wp_pures. iApply "HΦ".
505 Qed.
506
507 (* Given a history that is represented, after updating the [next]
508 pointer of the current tail node to a new tail node, we obtain a
509 new (extended) history (with the new tail node appended). *)
510 Lemma hist_repr_snoc hist tpos (ℓ_tail ℓ_new : loc) data next :
511 length hist = S tpos →
512 loc_at hist tpos = Some ℓ_tail →
513 node_repr ℓ_new data (new_node_next_red next) -∗
514 hist_repr hist false -∗
515 (ℓ_tail +ₗ 1) ↦ node_next_hl (Normal None) ∗
516 ((ℓ_tail +ₗ 1) ↦ node_next_hl (Normal (Some ℓ_new)) -∗ hist_repr (hist ++ [(ℓ_new, data)]) (bool_decide (next = FinalType))).
517 Proof.
518 unfold loc_at.
519 iIntros "%Hhistlen %Hloc @ Hhist".
520 rewrite list_lookup_fmap in Hloc.
521 destruct (hist !! tpos) as [[ℓ_tail' v_tail]|] eqn:Htpos; last done.
522 injection Hloc as ->.
523 apply list_elem_of_split_length in Htpos as (hist' & empty & -> & Htpos).
524 rewrite length_app length_cons -Htpos in Hhistlen.
525 assert (empty = []) as ->. { apply nil_length_inv. lia. }
526 clear Hhistlen Htpos.
527
528 iPoseProof (big_sepL_snoc with "Hhist") as "[Hinit Htail]".
529 iNamedSuffix "Htail" "_tail".
530
531 iSimplifyEq.
532 assert (loc_at (hist' ++ [(ℓ_tail, v_tail)]) (S (length hist')) = None) as ->.
533 { apply lookup_ge_None_2. rewrite length_fmap length_app length_cons /=. lia. }
534 iFrame "Hnnext_tail". iIntros "Hnnext_tail".
535 iSimplifyEq. rewrite /hist_repr.
536 iApply big_sepL_snoc.
537 iSplitR "Hndata Hnfinal Hnnext".
538 - iApply big_sepL_snoc. iSplitL "Hinit".
539 + iApply (big_sepL_mono with "Hinit").
540 iIntros (k [ℓ v] Hk) "Hrepr".
541 unfold next_from. simpl. rewrite [bool_decide (S k = _)]bool_decide_false; last first.
542 { apply lookup_lt_Some in Hk. rewrite !length_app /=. lia. }
543 rewrite andb_false_r /=.
544 assert (loc_at ((hist' ++ [(ℓ_tail, v_tail)]) ++ [(ℓ_new, data)]) (S k) = loc_at (hist' ++ [(ℓ_tail, v_tail)]) (S k)) as ->.
545 { rewrite /loc_at !list_lookup_fmap lookup_app_l // length_app /=.
546 apply lookup_lt_Some in Hk. lia. }
547 done.
548 + iFrame.
549 rewrite /next_from /= [bool_decide (S (length hist') = _)]bool_decide_false; last first.
550 { rewrite !length_app /=. lia. }
551 rewrite andb_false_r /= /loc_at list_lookup_fmap lookup_app_r; last first.
552 { rewrite length_app /=. lia. }
553 rewrite length_app /= Nat.add_1_r Nat.sub_diag /=.
554 by iFrame.
555 - iFrame.
556 rewrite /next_from /= /loc_at length_app /= Nat.add_1_r list_lookup_fmap lookup_app_r.
557 * rewrite !length_app /= !Nat.add_1_r [bool_decide (S _ = S _)]bool_decide_true //
558 andb_true_r Nat.sub_succ -Arith_base.minus_Sn_m_stt // Nat.sub_diag /=.
559 destruct next; simpl; iFrame.
560 * rewrite length_app /= Nat.add_1_r. lia.
561 Qed.
562
563 Definition iffinal {A} (n : new_node_next) (a b : A) :=
564 match n with
565 | FinalType => a
566 | NonFinalType => b
567 end.
568
569 Lemma set_tail_spec (ℓ_q ℓ_node : loc) data next :
570 node_repr ℓ_node data (new_node_next_red next) -∗
571 <<{ ∀∀ vs, queue_repr ℓ_q vs None }>>
572 set_tail #ℓ_q #ℓ_node @ ∅
573 <<{ queue_repr ℓ_q (vs ++ iffinal next [] [data]) (iffinal next (Some data) None) | RET #() }>>.
574 Proof.
575 iIntros "@ %Φ AU". iLöb as "IH". wp_rec.
576
577 wp_pures. wp_bind (! _)%E.
578 iMod "AU" as "(%vs & (%γs & #Hγs & %hist0 & %ℓ_head & %ℓ_tail & %hpos & %tpos & @) & [Hclose _])".
579 iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist0◯".
580 wp_load. iSimpl in "Hrepr".
581 rename Hℓtpos into Hℓtpos0.
582 iAssert (queue_repr_1 γs ℓ_q vs None) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
583 { iExists tpos. by iFrameNamed. }
584 iMod ("Hclose" with "[$]") as "AU". clear Hvs Hℓhpos hpos vs ℓ_head.
585 iModIntro. wp_let. wp_pure.
586
587 wp_bind (! _)%E.
588 iMod "AU" as "(%vs & (%γs' & Hγs' & %hist2 & %ℓ_head & %ℓ_tail'' & %hpos & %tpos'' & @) & [Hclose _])".
589 iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
590 iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist0◯") as %Hhist02.
591 iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist2◯".
592 destruct Hhist02 as [_ Hhist02]. rename Hℓtpos into Hℓtpos2.
593 assert (Hℓtpos0'' : loc_at hist2 tpos = Some ℓ_tail).
594 { by eapply loc_at_prefix. } clear Hℓtpos0.
595 wp_pures.
596 iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%w & Hnrepr & Hrepr)"; first done.
597 iNamedSuffix "Hnrepr" "_tail".
598 wp_load.
599 iDestruct "Hnfinal_tail" as "#Hnfinal_tail2".
600 iPoseProof ("Hrepr" with "[$]") as "Hrepr".
601 iAssert (queue_repr_1 γs ℓ_q vs None) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
602 { iExists tpos''. by iFrameNamed. }
603 iMod ("Hclose" with "[$]") as "AU". clear Hvs Hℓhpos hpos vs ℓ_head.
604 iModIntro.
605
606 destruct (next_from hist2 false tpos) as [[ℓ_next|]|] eqn:Htpos2; last done.
607 + (* it is not the last node *)
608 simpl. apply next_from_normal in Htpos2 as [Hnext HStpos2]. rewrite HStpos2 /=.
609
610 wp_pures. wp_bind (Snd (CmpXchg _ _ _))%E.
611 awp_apply (try_bump_tail_spec with "[//]").
612 { apply Hℓtpos0''. }
613 { done. }
614 rewrite /atomic_acc /=.
615 iMod "AU" as "(%vs & (%γs' & Hγs' & Hrepr) & [Hclose _])".
616 iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
617 iModIntro. iExists vs. iFrame "Hrepr". iSplit.
618 * iFrame. iIntros "Hrepr". by iApply ("Hclose" with "[$Hrepr]").
619 * iIntros "%b Hrepr".
620 iMod ("Hclose" with "[$Hrepr //]") as "AU".
621 iModIntro. wp_pures.
622 by iApply ("IH" with "[$] [$] [$]").
623 + (* it is the last (non-final) node *)
624 simpl. apply next_from_normal in Htpos2 as [Hnext HStpos2]. rewrite HStpos2 /=.
625 wp_pures. wp_bind (CmpXchg _ _ _)%E.
626
627 iMod "AU" as "(%vs & (%γs' & Hγs' & %hist3 & %ℓ_head & %ℓ_tail''' & %hpos & %tpos''' & @) & Hclose)".
628 iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
629 iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist2◯") as %Hhist23.
630 destruct Hhist23 as [_ Hhist23]. rename Hℓtpos into Hℓtpos3.
631
632 destruct (loc_at hist3 (S tpos)) as [ℓ_tail''''|] eqn:Hrace.
633 * (* Another item has been enqueued in the meantime, so the CAS is poised to fail. *)
634 iDestruct "Hclose" as "[Hclose _]".
635
636 iDestruct (hist_repr_peek_3 with "[$Hrepr]") as "[Hℓ_tail1 Hrepr]".
637 { eapply prefix_lookup_Some; first apply Hℓtpos0''. by apply prefix_of_fmap. }
638 rewrite /next_from [bool_decide (S _ = _)]bool_decide_false; last first.
639 { apply lookup_lt_Some in Hrace. rewrite length_fmap in Hrace. lia. }
640 rewrite andb_false_r Hrace /=.
641 wp_cmpxchg_fail.
642 iSpecialize ("Hrepr" with "Hℓ_tail1").
643 iAssert (queue_repr_1 γs ℓ_q vs None) with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr]" as "Hq".
644 { iExists tpos'''. by iFrameNamed. }
645 iMod ("Hclose" with "[$]") as "AU". iModIntro.
646 wp_pures. iApply ("IH" with "Hndata Hnnext Hnfinal AU").
647 * (* This node is still the tail, so the CAS will succeed. *)
648 iDestruct "Hclose" as "[_ Hclose]".
649
650 iAssert ⌜length hist3 = S tpos⌝%I as %Hhist3.
651 { apply loc_at_length in Hrace as Hhist3.
652 iPureIntro. apply loc_at_prefix with (xs':=hist3) in Hℓtpos0''; last done.
653 apply lookup_lt_Some in Hℓtpos0''. rewrite length_fmap in Hℓtpos0''. lia. }
654
655 iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%w' & Hℓ_tail3 & Hrepr)".
656 { eapply prefix_lookup_Some; first apply Hℓtpos0''. by apply prefix_of_fmap. }
657 rewrite /next_from [bool_decide (S _ = _)]bool_decide_true // andb_true_r Hrace /=.
658 iNamedSuffix "Hℓ_tail3" "_tail3".
659 iPoseProof ("Hrepr" with "[$]") as "Hrepr". clear w.
660
661 iPoseProof (hist_repr_snoc with "[$Hndata $Hnfinal $Hnnext] [$Hrepr]") as "[Htnode Henq]".
662 { apply Hhist3. }
663 { eapply prefix_lookup_Some. apply Hℓtpos0''. by apply prefix_of_fmap. }
664 wp_cmpxchg_suc. iSpecialize ("Henq" with "Htnode").
665
666 pose mfin := iffinal next (Some data) None.
667
668 iMod (mono_list_auth_own_update_app [(ℓ_node, data)] with "Hhist●") as "[Hhist● _]".
669 iMod (hpos_weaken (hist3 ++ [(ℓ_node, data)]) mfin with "Hhpos●") as "Hhpos●".
670 iMod (hist_weaken (hist3 ++ [(ℓ_node, data)]) hpos mfin with "Hhist●") as "Hhist●".
671 replace (bool_decide (next = FinalType)) with (bool_decide (is_Some mfin)); last first.
672 { apply bool_decide_ext. destruct next; by cbn. }
673
674 iAssert (queue_repr_1 γs ℓ_q (vs ++ iffinal next [] [data]) mfin) with "[$Hhead $Htail $Hhist● $Hhpos● $Henq]" as "Hq".
675 { iExists tpos'''. iPureIntro.
676 repeat split; try done.
677 - eapply loc_at_prefix; first done.
678 by apply prefix_app_r.
679 - eapply loc_at_prefix; first done.
680 by apply prefix_app_r.
681 - rewrite drop_app fmap_app -Hvs. rewrite /= app_nil_r -app_assoc.
682 f_equal.
683 assert (Hhpos : hpos < length hist3).
684 { apply lookup_lt_Some in Hℓhpos.
685 by rewrite length_fmap in Hℓhpos. }
686 assert (S hpos - length hist3 = 0) as -> by lia.
687 simpl. by destruct next. }
688 iMod ("Hclose" with "[$]") as "HΦ".
689 iModIntro. wp_pures. done.
690 Qed.
691
692 Lemma enqueue_spec (ℓ_q : loc) (data : val) :
693 ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>>
694 enqueue #ℓ_q data @ ∅
695 <<{ queue_repr ℓ_q (vs ++ [data]) None | RET #() }>>.
696 Proof.
697 iIntros "%Φ AU". wp_lam. wp_pures.
698 wp_apply (new_node_spec with "[//]") as "%ℓ_node Hnode".
699 awp_apply (set_tail_spec with "[$Hnode]").
700 rewrite /atomic_acc /=. iMod "AU" as "(%vs & Hrepr & Hclose)".
701 iModIntro. iFrame.
702 Qed.
703
704 Lemma finalize_spec (ℓ_q : loc) (data : val) :
705 ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>>
706 finalize #ℓ_q data @ ∅
707 <<{ queue_repr ℓ_q vs (Some data) | RET #() }>>.
708 Proof.
709 iIntros "%Φ AU". wp_lam. wp_pures.
710 wp_apply (new_node_spec with "[//]") as "%ℓ_node Hnode".
711 awp_apply (set_tail_spec with "[$Hnode]").
712 rewrite /atomic_acc /=. iMod "AU" as "(%vs & Hrepr & Hclose)".
713 iModIntro. iFrame. by rewrite app_nil_r.
714 Qed.
715
716 Lemma try_dequeue_spec (ℓ_q : loc) :
717 ⊢ <<{ ∀∀ vs mfin, queue_repr ℓ_q vs mfin }>>
718 try_dequeue #ℓ_q @ ∅
719 <<{ queue_repr ℓ_q (tail vs) mfin
720 | RET (if head vs is Some v then InjLV v else InjRV (val_opt_hl mfin)) }>>.
721 Proof.
722 iIntros "%Φ AU". iLöb as "IH". wp_rec.
723
724 wp_bind (! _)%E.
725 iMod "AU" as "(%vs0 & %fin0 & (%γs & #Hγs & %hist0 & %ℓ_head0 & %ℓ_tail0 & %hpos0 & %tpos0 & @) & [Hclose _])".
726 iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist0◯".
727 iDestruct (mono_nat_lb_own_get with "Hhpos●") as "#Hhpos0◯".
728 rename Hℓhpos into Hℓhpos0.
729 wp_load.
730 iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU".
731 { iExists tpos0. by iFrameNamed. }
732 iModIntro. clear fin0 vs0 Hvs tpos0 Hℓtpos ℓ_tail0.
733
734 wp_pures. wp_bind (! _)%E.
735 iMod "AU" as "(%vs1 & %fin1 & (%γs' & Hγs' & %hist1 & %ℓ_head1 & %ℓ_tail1 & %hpos1 & %tpos1 & @) & Hclose)".
736 iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
737 iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist1◯".
738 iDestruct (mono_nat_auth_lb_own_valid with "Hhpos● Hhpos0◯") as %Hhpos01.
739 iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist0◯") as %Hhist01.
740 destruct Hhpos01 as [_ Hhpos01]. destruct Hhist01 as [_ Hhist01].
741 assert (Hℓhpos0' : loc_at hist1 hpos0 = Some ℓ_head0).
742 { by eapply loc_at_prefix. } clear Hℓhpos0.
743 iDestruct (hist_repr_peek_2 with "[$Hrepr]") as "(%u & @ & Hrepr)"; first done.
744 wp_load.
745 iSpecialize ("Hrepr" with "[$]").
746
747 rewrite node_next_hl_next_from.
748 destruct (loc_at hist1 (S hpos0)) as [ℓ_headS0|] eqn:Hℓ_headS0.
749 - simpl. iDestruct "Hclose" as "[Hclose _]".
750 iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU".
751 { iExists tpos1. by iFrameNamed. }
752 iModIntro. clear u fin1 vs1 Hvs tpos1 Hℓtpos ℓ_tail1.
753
754 wp_pures. wp_bind (! _)%E.
755 iMod "AU" as "(%vs2 & %fin2 & (%γs' & Hγs' & %hist2 & %ℓ_head2 & %ℓ_tail2 & %hpos2 & %tpos2 & @) & Hclose)".
756 iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
757 iDestruct (mono_list_lb_own_get with "Hhist●") as "#Hhist2◯".
758 iDestruct (mono_nat_auth_lb_own_valid with "Hhpos● Hhpos0◯") as %Hhpos02.
759 iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist1◯") as %Hhist12.
760 destruct Hhpos02 as [_ Hhpos02]. destruct Hhist12 as [_ Hhist12].
761 assert (Hℓ_headS0' : loc_at hist2 (S hpos0) = Some ℓ_headS0).
762 { by eapply loc_at_prefix. } clear Hℓ_headS0.
763 apply loc_at_val_at_Some in Hℓ_headS0' as Hval_headS0'.
764 destruct Hval_headS0' as [w Hval_headS0'].
765 iDestruct (hist_repr_peek_1 with "[$Hrepr]") as "(@ & Hrepr)"; try done.
766 iDestruct "Hndata" as "#Hndata_head".
767 wp_load.
768
769 destruct (next_from hist2 (bool_decide (is_Some fin2)) (S hpos0)) as [mℓ_next|] eqn:Hnext2.
770 + iDestruct "Hclose" as "[Hclose _]".
771 iEval (rewrite bool_decide_false //).
772
773 iDestruct "Hnfinal" as "#Hnfinal_head".
774 iEval (rewrite bool_decide_false //) in "Hnfinal_head".
775
776 iSpecialize ("Hrepr" with "[$]").
777 iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU".
778 { iExists tpos2. by iFrameNamed. }
779 iModIntro.
780 clear fin2 vs2 Hvs tpos2 Hℓtpos ℓ_tail2 Hnext2.
781
782 wp_pures. wp_load. wp_pures.
783
784 wp_bind (CmpXchg _ _ _)%E.
785 iMod "AU" as "(%vs3 & %fin3 & (%γs' & Hγs' & %hist3 & %ℓ_head3 & %ℓ_tail3 & %hpos3 & %tpos3 & @) & Hclose)".
786 iDestruct (meta_agree with "Hγs Hγs'") as "<- {Hγs'}".
787 iDestruct (mono_list_auth_lb_own_valid with "Hhist● Hhist2◯") as %Hhist23.
788 destruct Hhist23 as [_ Hhist23].
789 assert (Hhist13 : hist1 `prefix_of` hist3).
790 { by trans hist2. }
791
792 destruct (decide (ℓ_head0 = ℓ_head3)) as [->|Hhead03].
793 * iDestruct "Hclose" as "[_ Hclose]".
794
795 wp_cmpxchg_suc.
796
797 assert (Hℓhpos0'' : loc_at hist3 hpos0 = Some ℓ_head3).
798 { by eapply loc_at_prefix. } clear Hℓhpos0'.
799 iAssert ⌜hpos0 = hpos3⌝%I as %->.
800 { by iApply (loc_at_inj with "Hrepr"). }
801
802 destruct (decide (length (vs3 ++ option_list fin3) = 1)) as [Hvs3|Hvs3].
803 -- destruct fin3 eqn:Hfin3.
804 ++ assert (Hℓ_headS0'' : loc_at hist3 (S hpos3) = Some ℓ_headS0).
805 { by eapply loc_at_prefix. } clear Hℓ_headS0'.
806 assert (Hval_headS0'' : val_at hist3 (S hpos3) = Some w).
807 { by eapply val_at_prefix. } clear Hval_headS0'.
808
809 simplify_eq/=.
810 destruct vs3; last first.
811 { rewrite length_app /= Nat.add_1_r in Hvs3. lia. }
812
813 assert (length hist3 = S (S hpos3)).
814 { apply (f_equal length), symmetry in Hvs.
815 rewrite /= length_fmap length_drop in Hvs. lia. }
816
817 iDestruct (hist_repr_peek_1 with "[$Hrepr]") as "(@ & Hrepr)"; try done.
818 iClear "Hnnext".
819 rewrite /next_from !andb_true_l [bool_decide (S _ = _)]bool_decide_true //=.
820 by iCombine "Hnfinal_head Hnfinal" gives "[_ %contra]".
821 ++ simplify_eq/=. rewrite app_nil_r in Hvs Hvs3.
822
823 iMod (mono_nat_own_update (S hpos3) with "Hhpos●") as "[Hhpos● _]". { lia. }
824 iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ".
825 { iExists tpos3. iFrameNamed.
826 iPureIntro. repeat split; try done.
827 - by eapply loc_at_prefix.
828 - by rewrite /= fmap_drop /= -Nat.add_1_r -drop_drop -fmap_drop -Hvs app_nil_r. }
829
830 iModIntro. wp_pures.
831
832 assert (Hval_headS0'' : val_at hist3 (S hpos3) = Some w).
833 { by eapply val_at_prefix. } clear Hval_headS0'.
834 unfold val_at in Hval_headS0''.
835 destruct vs3; try done.
836 rewrite -[S hpos3]Nat.add_0_r -lookup_drop -fmap_drop -Hvs /= in Hval_headS0''.
837 by simplify_eq/=.
838 -- assert (S (S hpos3) ≠ length hist3).
839 { rewrite Hvs length_fmap length_drop in Hvs3. lia. }
840
841 assert (queue_γs_dq hist3 hpos3 fin3 = DfracOwn 1) as ->.
842 { unfold queue_γs_dq. by repeat case_match. }
843 iMod (mono_nat_own_update (S hpos3) with "Hhpos●") as "[Hhpos● _]". { lia. }
844 iMod (hpos_weaken hist3 fin3 with "Hhpos●") as "Hhpos●".
845 iMod (hist_weaken hist3 (S hpos3) fin3 with "Hhist●") as "Hhist●".
846
847 iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ".
848 { iExists tpos3. iFrameNamed.
849 iPureIntro. repeat split; try done.
850 - by eapply loc_at_prefix.
851 - rewrite -Nat.add_1_r -drop_drop fmap_drop -Hvs.
852 destruct fin3; last by rewrite /= !app_nil_r.
853 by destruct vs3. }
854
855 iModIntro. wp_pures.
856
857 assert (Hval_headS0'' : val_at hist3 (S hpos3) = Some w).
858 { by eapply val_at_prefix. } clear Hval_headS0'.
859 unfold val_at in Hval_headS0''.
860 rewrite -[S hpos3]Nat.add_0_r -lookup_drop -fmap_drop -Hvs in Hval_headS0''.
861
862 destruct vs3; simplify_eq/=; last done.
863 by destruct fin3.
864
865 * iDestruct "Hclose" as "[Hclose _]".
866
867 wp_cmpxchg_fail.
868
869 iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "AU".
870 { iExists tpos3. by iFrameNamed. }
871
872 iModIntro. wp_pures. iApply ("IH" with "AU").
873
874 + iDestruct "Hclose" as "[_ Hclose]".
875
876 destruct fin2 as [fin2|]; last done. simplify_eq/=.
877 assert (Hhist2 : length hist2 = S (S hpos0)).
878 { destruct (decide (length hist2 = S (S hpos0))); first done.
879 by rewrite /next_from bool_decide_false in Hnext2. }
880 assert (S hpos2 < length hist2).
881 { rewrite -(length_fmap snd).
882 apply lookup_lt_is_Some_1.
883 rewrite -[S hpos2]Nat.add_0_r -lookup_drop -fmap_drop -Hvs.
884 by destruct vs2, fin2. }
885 assert (hpos0 = hpos2) as -> by lia.
886 assert (Hvs2 : length vs2 = 0).
887 { apply eq_add_S. rewrite -Nat.add_1_r -(length_app _ [fin2]) Hvs length_fmap length_drop Hhist2. lia. }
888 destruct vs2; last done. clear Hvs2.
889
890 iSpecialize ("Hrepr" with "[$]").
891 iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ".
892 { iExists tpos2. by iFrameNamed. }
893
894 iModIntro. clear tpos2 Hℓhpos Hℓtpos ℓ_tail2.
895
896 wp_pures. wp_load.
897 rewrite /val_at in Hval_headS0'.
898 rewrite -[S hpos2]Nat.add_0_r -lookup_drop -fmap_drop -Hvs in Hval_headS0'.
899 simplify_eq/=. wp_pures. iApply "HΦ".
900 - apply loc_at_length in Hℓ_headS0 as Hhistlen.
901 rewrite drop_ge /= in Hvs; last lia. destruct vs1, fin1; try done.
902 simplify_eq/=.
903
904 iDestruct "Hclose" as "[_ Hclose]".
905 iMod ("Hclose" with "[$Hhead $Htail $Hhist● $Hhpos● $Hrepr $Hγs]") as "HΦ".
906 { iExists tpos1. iFrameNamed. iPureIntro.
907 rewrite drop_ge //=. lia. }
908
909 iModIntro. wp_pures. iApply "HΦ".
910 Qed.
911
912End fin_queue.
913
914Definition fin_queue_hl :=
915 {| fin_queue_spec.new := new;
916 fin_queue_spec.enqueue := enqueue;
917 fin_queue_spec.finalize := finalize;
918 fin_queue_spec.try_dequeue := try_dequeue; |}.
919
920Definition fin_queue_iris `{!heapGS Σ, !fin_queueG Σ} : fin_queue_spec.fin_queue_iris Σ fin_queue_hl.
921Proof.
922 refine (FinQueueIris _ _
923 fin_queue_hl _ _ _ _ _
924 queue_fin_obtain
925 queue_fin_agree
926 new_spec
927 enqueue_spec
928 finalize_spec
929 try_dequeue_spec).
930Defined.
931
932#[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 @@
1From iris.program_logic Require Import atomic.
2From iris.heap_lang Require Import notation proofmode.
3
4From lmpmc Require Import util.
5
6(* Doing this split because I don't know how to otherwise get a nice
7 closed proof. *)
8
9Record fin_queue_hl :=
10 FinQueueHl
11 { new : val;
12 enqueue : val;
13 finalize : val;
14 try_dequeue : val;}.
15Record fin_queue_iris {Σ} `{!heapGS Σ} (hl : fin_queue_hl) :=
16 FinQueueIris
17 { (** If [⊢ queue_repr ℓ vs mfin], then there is a queue at [ℓ]
18 which currently holds the values [vs], and possibly a final
19 value [mfin]. The dequeue and enqueue operations work in
20 FIFO fashion, with [head vs] (if any) representing the next
21 value that would be dequeued by a [try_dequeue ℓ] operation.
22
23 Only non-finalized queues can be enqueued in. Non-finalized queues
24 can be finalized using the [finalize ℓ v] operation, which sets
25 [mfin] to [v]. Subsequent [try_dequeue ℓ] operations then first
26 dequeue the remainder of [vs]; when [vs] is empty, they return [mfin]
27 (but, critically, do not unset it). *)
28 queue_repr : loc → list val → option val → iProp Σ;
29 #[global] queue_repr_timeless ℓ vs mfin :: Timeless (queue_repr ℓ vs mfin);
30
31 (** If [⊢ queue_fin ℓ v], then the queue at [ℓ] has been
32 finalized and all elements except for the final element [v]
33 have been dequeued.
34
35 Queues that enter this state never leave this state; this
36 allows [queue_fin ℓ v] to be a persistent proposition. *)
37 queue_fin : loc → val → iProp Σ;
38 #[global] queue_fin_persistent ℓ v :: Persistent (queue_fin ℓ v);
39 #[global] queue_fin_timeless ℓ v :: Timeless (queue_fin ℓ v);
40 queue_fin_obtain ℓ fin : queue_repr ℓ [] (Some fin) -∗ queue_fin ℓ fin;
41 queue_fin_agree ℓ vs fin mfin :
42 queue_fin ℓ fin -∗
43 queue_repr ℓ vs mfin -∗
44 ⌜vs = []⌝ ∗ ⌜mfin = Some fin⌝;
45
46 new_spec :
47 {{{ True }}}
48 hl.(new) #()
49 {{{ (ℓ : loc), RET #ℓ; queue_repr ℓ [] None }}};
50
51 enqueue_spec (ℓ_q : loc) (data : val) :
52 ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>>
53 hl.(enqueue) #ℓ_q data @ ∅
54 <<{ queue_repr ℓ_q (vs ++ [data]) None | RET #() }>>;
55
56 finalize_spec (ℓ_q : loc) (data : val) :
57 ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>>
58 hl.(finalize) #ℓ_q data @ ∅
59 <<{ queue_repr ℓ_q vs (Some data) | RET #() }>>;
60
61 try_dequeue_spec (ℓ_q : loc) :
62 ⊢ <<{ ∀∀ vs mfin, queue_repr ℓ_q vs mfin }>>
63 hl.(try_dequeue) #ℓ_q @ ∅
64 <<{ queue_repr ℓ_q (tail vs) mfin
65 | RET (if head vs is Some v then InjLV v else InjRV (val_opt_hl mfin)) }>>;
66 }.
67#[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 @@
1From iris.program_logic Require Import atomic.
2From iris.heap_lang Require Import notation proofmode.
3
4From lmpmc Require Import lmpmc_queue_spec util.
5
6Section lmpmc_blocking.
7 Context (lq : lmpmc_queue_spec.lmpmc_queue_hl).
8
9 (* https://types.pl/@pigworker/115629120124299549 *)
10 Definition dequeue : val := rec: "go" "ℓ_deq" :=
11 match: lq.(try_dequeue) "ℓ_deq" with
12 NONE => "go" "ℓ_deq"
13 | SOME "v" => "v"
14 end.
15
16 Section proofs.
17 Context `{heapGS Σ} (lqp : lmpmc_queue_spec.lmpmc_queue_iris Σ lq).
18
19 Lemma dequeue_spec (ℓ_deq : loc) :
20 ⊢ <<{ ∀∀ ℓ_enq cvs, lqp.(queue_repr lq) ℓ_deq ℓ_enq cvs }>>
21 dequeue #ℓ_deq @ ∅
22 <<{ ∃∃ cv cvs', ⌜cvs = cv :: cvs'⌝ ∗ lqp.(queue_repr lq) ℓ_deq ℓ_enq cvs' | RET cv }>>.
23 Proof.
24 iIntros (Φ) "AU". iLöb as "IH". wp_rec.
25 awp_apply lqp.(try_dequeue_spec lq).
26 rewrite /atomic_acc /=.
27 iMod "AU" as "(%ℓ_enq & %cvs & Hcvs & Hclose)".
28 iFrame. iModIntro. iSplit; iIntros "Hrepr".
29 - by iMod ("Hclose" with "Hrepr") as "AU".
30 - destruct cvs as [|cv cvs']; simplify_list_eq.
31 + iMod ("Hclose" with "Hrepr") as "AU". iModIntro.
32 wp_pures. by iApply "IH".
33 + iDestruct "Hclose" as "[_ Hclose]".
34 iMod ("Hclose" $! cv cvs' with "[$Hrepr //]") as "HΦ".
35 iModIntro. by wp_pures.
36 Qed.
37
38 End proofs.
39
40End 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 @@
1From iris.program_logic Require Import atomic.
2From iris.heap_lang Require Import notation proofmode.
3From iris.algebra.lib Require Import excl_auth.
4From iris.base_logic.lib Require Import invariants.
5From iris.base_logic.lib Require Import invariants mono_nat mono_list.
6From iris_named_props Require Import custom_syntax.
7
8From lmpmc Require fin_queue_spec lmpmc_queue_spec.
9From lmpmc Require Import upstream util.
10
11Section lmpmc_queue.
12 Context {fq : fin_queue_spec.fin_queue_hl}.
13
14 Definition new : val := λ: <>,
15 let: "ℓ_q" := fq.(fin_queue_spec.new) #() in ("ℓ_q", "ℓ_q").
16
17 Definition enqueue : val := (* passing arguments [ℓ_enq data] *)
18 fq.(fin_queue_spec.enqueue).
19
20 Definition try_dequeue : val := rec: "go" "ℓ_q" :=
21 match: fq.(fin_queue_spec.try_dequeue) "ℓ_q" with
22 InjL "v" =>
23 SOME "v"
24 | InjR "mℓ_nextq" =>
25 match: "mℓ_nextq" with
26 NONE => NONE
27 | SOME "ℓ_nextq" => "go" "ℓ_nextq"
28 end
29 end.
30
31 Definition link : val := (* passing arguments [ℓ_enq1 ℓ_deq2] *)
32 fq.(fin_queue_spec.finalize).
33
34 Section proofs.
35 Context `{!heapGS Σ} {fqp : fin_queue_spec.fin_queue_iris Σ fq}.
36
37 Record node := Node { ℓ_node : loc; vs_node : list val }.
38 Add Printing Constructor node.
39 Definition linked_single_queue_repr (n : node) (mℓ_nextq : option loc) : iProp Σ :=
40 fqp.(fin_queue_spec.queue_repr fq) n.(ℓ_node) n.(vs_node) (loc_to_val <$> mℓ_nextq).
41
42 Definition chain := list node.
43 Definition queue_repr ℓ_deq ℓ_enq (cvs : list val) : iProp Σ :=
44 ∃ (c : chain),
45 ⌜length c > 0⌝ ∗ ⌜ℓ_node <$> head c = Some ℓ_deq⌝ ∗
46 ⌜ℓ_node <$> last c = Some ℓ_enq⌝ ∗ ⌜cvs = c ≫= vs_node⌝ ∗
47 [∗ list] i ↦ l ∈ c, linked_single_queue_repr l (ℓ_node <$> c !! S i).
48
49 #[global] Instance queue_repr_timeless ℓ_deq ℓ_enq cvs : Timeless (queue_repr ℓ_deq ℓ_enq cvs) := _.
50
51 Lemma new_spec :
52 {{{ True }}}
53 new #()
54 {{{ (ℓ_deq ℓ_enq : loc), RET (#ℓ_deq, #ℓ_enq); queue_repr ℓ_deq ℓ_enq [] }}}.
55 Proof.
56 iIntros (Φ _) "HΦ". iUnfold new. wp_pures.
57 wp_apply (fqp.(fin_queue_spec.new_spec fq) with "[//]").
58 iIntros (ℓ) "H". wp_pures. iModIntro. iApply "HΦ".
59 unfold queue_repr. iExists [Node ℓ []].
60 iFrame. iSimplifyEq. by iSplit; first (iPureIntro; lia).
61 Qed.
62
63 Lemma enqueue_spec (ℓ_enq : loc) (data : val) :
64 ⊢ <<{ ∀∀ ℓ_deq cvs, queue_repr ℓ_deq ℓ_enq cvs }>>
65 enqueue #ℓ_enq data @ ∅
66 <<{ queue_repr ℓ_deq ℓ_enq (cvs ++ [data]) | RET #() }>>.
67 Proof.
68 iIntros "%Φ AU". iUnfold enqueue.
69
70 wp_bind (fin_queue_spec.enqueue _ _ _)%E.
71 awp_apply fqp.(fin_queue_spec.enqueue_spec fq).
72 rewrite /atomic_acc /=.
73 iMod "AU" as "(%ℓ_deq & %cvs & (%c & %Hclen & %Hhead & %Hlast & %Hcvs & Hqs) & Hclose)".
74 iModIntro.
75
76 destruct (last c) as [n_last|] eqn:Hlastn; last done.
77 iExists n_last.(vs_node).
78
79 apply last_Some in Hlastn as [c' ->].
80 iDestruct (big_sepL_insert_acc _ _ (length c') with "Hqs") as "[Hnode Hrepr]".
81 { by rewrite lookup_app_r // Nat.sub_diag. }
82 iSimplifyEq. iUnfold linked_single_queue_repr in "Hnode".
83
84 rewrite lookup_app_r; last lia.
85 replace (S (length c') - length c') with 1 by lia.
86 simplify_eq/=. iFrame.
87
88 iSplit.
89 - iDestruct "Hclose" as "[Hclose _]".
90 iIntros "Hnode".
91 iDestruct ("Hrepr" with "[Hnode //]") as "Hrepr".
92 rewrite list_insert_id; last first.
93 { by rewrite lookup_app_r // Nat.sub_diag. }
94 iMod ("Hclose" with "[$Hrepr]") as "AU".
95 { by rewrite last_snoc. }
96 done.
97 - iDestruct "Hclose" as "[_ Hclose]".
98 iIntros "Hnode".
99
100 set n_last' := Node n_last.(ℓ_node) (n_last.(vs_node) ++ [data]).
101 set c := c' ++ [n_last'].
102
103 iDestruct ("Hrepr" with "[Hnode]") as "Hrepr".
104 { rewrite /linked_single_queue_repr /=.
105 replace (ℓ_node n_last) with n_last'.(ℓ_node) by done.
106 by replace (vs_node n_last ++ [data]) with n_last'.(vs_node). }
107
108 iMod ("Hclose" with "[Hrepr]") as "HΦ".
109 { unfold queue_repr. iExists c. repeat iSplit; try done.
110 - iPureIntro. rewrite length_app /=. lia.
111 - iPureIntro. rewrite /c. by destruct c'; simplify_eq/=.
112 - iPureIntro. by rewrite /c last_snoc.
113 - iPureIntro. by rewrite /c !bind_app /= !app_nil_r app_assoc.
114 - rewrite insert_app_r_alt // Nat.sub_diag /=.
115 iApply (big_sepL_mono with "Hrepr").
116 { iIntros (i n Hi) "Hrepr".
117 rewrite -list_lookup_fmap fmap_app.
118 replace (ℓ_node <$> [n_last]) with (ℓ_node <$> [n_last']) by done.
119 by rewrite -fmap_app list_lookup_fmap. } }
120
121 iModIntro. iApply "HΦ".
122 Qed.
123
124 Lemma try_dequeue_spec (ℓ_deq : loc) :
125 ⊢ <<{ ∀∀ ℓ_enq cvs, queue_repr ℓ_deq ℓ_enq cvs }>>
126 try_dequeue #ℓ_deq @ ∅
127 <<{ queue_repr ℓ_deq ℓ_enq (tail cvs) | RET (val_opt_hl (head cvs)) }>>.
128 Proof.
129 revert ℓ_deq. iLöb as "IH". iIntros (ℓ_deq Φ) "AU". wp_rec.
130
131 awp_apply (fqp.(fin_queue_spec.try_dequeue_spec fq)).
132 rewrite /atomic_acc /=.
133 iMod "AU" as "(%ℓ_enq & %cvs & (%c & %Hclen & %Hhead & %Hlast & %Hcvs & Hqs) & Hclose)". iModIntro.
134
135 destruct c as [|n_head c']; first done.
136 iDestruct (big_sepL_cons with "Hqs") as "[Hnode Hqs]".
137 simpl. destruct (c' !! 0) as [n_next|] eqn:Hnextq.
138 - iExists n_head.(vs_node), (Some #n_next.(ℓ_node)). iSplitL "Hnode"; last iSplit.
139 + simplify_eq/=. by rewrite /linked_single_queue_repr /=.
140 + simplify_eq/=. iIntros "Hnode". iDestruct "Hclose" as "[Hclose _]".
141 pose c := n_head :: c'.
142 iAssert (linked_single_queue_repr n_head (ℓ_node <$> c !! S 0)) with "[Hnode]" as "Hnode".
143 { by rewrite /linked_single_queue_repr /= Hnextq. }
144 iAssert ([∗ list] i↦n ∈ c', linked_single_queue_repr n (ℓ_node <$> c !! S (S i)))%I with "[Hqs //]" as "Hqs".
145 iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hnode Hqs]" as "Hqs".
146 { iApply big_sepL_cons. iFrame. }
147 iAssert (queue_repr n_head.(ℓ_node) ℓ_enq (vs_node n_head ++ c' ≫= vs_node)) with "[$Hqs //]" as "Hrepr".
148 by iMod ("Hclose" with "Hrepr") as "Hrepr".
149 + simplify_eq/=. iIntros "Hnode".
150 destruct n_head.(vs_node) as [|x vs_head'] eqn:Hvs_head.
151 * simplify_eq/=. iDestruct "Hclose" as "[Hclose _]".
152
153 iDestruct (fqp.(fin_queue_spec.queue_fin_obtain fq) with "Hnode") as "#Hfin".
154
155 pose c := n_head :: c'.
156 iAssert (linked_single_queue_repr n_head (ℓ_node <$> c !! S 0)) with "[Hnode]" as "Hnode".
157 { by rewrite /linked_single_queue_repr /= Hnextq Hvs_head /=. }
158 iAssert ([∗ list] i↦n ∈ c', linked_single_queue_repr n (ℓ_node <$> c !! S (S i)))%I with "[Hqs //]" as "Hqs".
159 iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hnode Hqs]" as "Hqs".
160 { iApply big_sepL_cons. iFrame. }
161 iAssert (queue_repr n_head.(ℓ_node) ℓ_enq (vs_node n_head ++ c' ≫= vs_node)) with "[$Hqs //]" as "Hrepr".
162 rewrite Hvs_head /=. iMod ("Hclose" with "Hrepr") as "AU". iModIntro. wp_pures.
163 clear c c' Hclen Hlast Hnextq Hvs_head.
164
165 awp_apply "IH". rewrite /atomic_acc /=.
166 iMod "AU" as "(%ℓ_enq' & %cvs' & (%c'' & _ & %Hhead' & %Hlast' & %Hcvs' & Hqs') & Hclose)".
167 destruct c'' as [|n_head' c'']; first done.
168 iDestruct (big_sepL_cons with "Hqs'") as "[Hq0 Hqs']". simplify_eq/=.
169 iEval (rewrite /linked_single_queue_repr /=) in "Hq0".
170 rewrite -Hhead'.
171 iDestruct (fqp.(fin_queue_spec.queue_fin_agree fq) with "Hfin Hq0") as %[Hhead Hc''].
172 destruct (c'' !! 0) as [n_next'|] eqn:Hc''head; last done. simplify_eq/=.
173 rewrite -Hc''. clear Hhead' Hc'' n_next n_head.
174 assert (Hc''len : length c'' > 0). { by apply lookup_lt_Some in Hc''head. }
175
176 iAssert (queue_repr n_next'.(ℓ_node) ℓ_enq' (c'' ≫= vs_node)) with "[$Hqs']" as "Hrepr'".
177 { iPureIntro. repeat split; try done.
178 - by rewrite head_lookup Hc''head.
179 - enough (last c'' = last (n_head' :: c'')) as ->; first done.
180 destruct c''; first done. by rewrite last_cons_cons. }
181
182 iModIntro. iFrame. iSplit.
183 -- iIntros "(%d & %Hdlen & %Hdhead & %Hdlast & %Hdvs & Hrepr)".
184 rewrite Hhead /=. simplify_eq/=.
185 pose c := n_head' :: d.
186 iAssert (linked_single_queue_repr n_head' (ℓ_node <$> c !! S 0)) with "[Hq0]" as "Hq0".
187 { by rewrite /linked_single_queue_repr /= Hhead /= -head_lookup Hdhead /=. }
188 iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hq0 Hrepr]" as "Hrepr".
189 { iApply big_sepL_cons. iFrame. }
190 iAssert (queue_repr (ℓ_node n_head') ℓ_enq' (c'' ≫= vs_node)) with "[$Hrepr]" as "Hrepr".
191 { iPureIntro. repeat split; try done.
192 - unfold c. simpl. lia.
193 - unfold c. rewrite -Hdlast. by destruct d.
194 - unfold c. rewrite Hdvs. simplify_eq/=.
195 by rewrite Hhead. }
196 by iMod ("Hclose" with "Hrepr") as "AU".
197 -- iIntros "(%d & %Hdlen & %Hdhead & %Hdlast & %Hdvs & Hrepr)".
198 rewrite Hhead /=. simplify_eq/=.
199 pose c := n_head' :: d.
200 iAssert (linked_single_queue_repr n_head' (ℓ_node <$> c !! S 0)) with "[Hq0]" as "Hq0".
201 { by rewrite /linked_single_queue_repr /= Hhead /= -head_lookup Hdhead /=. }
202 iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hq0 Hrepr]" as "Hrepr".
203 { iApply big_sepL_cons. iFrame. }
204 iAssert (queue_repr (ℓ_node n_head') ℓ_enq' (tail (c'' ≫= vs_node))) with "[$Hrepr]" as "Hrepr".
205 { iPureIntro. repeat split; try done.
206 - unfold c. simpl. lia.
207 - unfold c. rewrite -Hdlast. by destruct d.
208 - unfold c. rewrite Hdvs. simplify_eq/=.
209 by rewrite Hhead. }
210 by iMod ("Hclose" with "Hrepr") as "AU".
211 * simplify_eq/=. iDestruct "Hclose" as "[_ Hclose]".
212
213 pose n_head' := Node (ℓ_node n_head) vs_head'.
214 pose c := n_head' :: c'.
215
216 iAssert (linked_single_queue_repr n_head' (ℓ_node <$> c !! S 0)) with "[Hnode]" as "Hnode".
217 { by rewrite /linked_single_queue_repr /= Hnextq /=. }
218 iAssert ([∗ list] i↦n ∈ c', linked_single_queue_repr n (ℓ_node <$> c !! S (S i)))%I with "[Hqs //]" as "Hqs".
219 iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hnode Hqs]" as "Hqs".
220 { iApply big_sepL_cons. iFrame. }
221 iAssert (queue_repr n_head.(ℓ_node) ℓ_enq (vs_node n_head' ++ c' ≫= vs_node)) with "[$Hqs]" as "Hrepr".
222 { iPureIntro. repeat split; try done. by destruct c'. }
223
224 iMod ("Hclose" with "Hrepr") as "Hrepr".
225 iModIntro. wp_pures. iApply "Hrepr".
226 - destruct c'; last done. simplify_eq/=. iClear "Hqs".
227 rewrite app_nil_r. clear Hclen.
228 iExists n_head.(vs_node), None. iSplitL "Hnode".
229 + by rewrite /linked_single_queue_repr /=.
230 + iSplit.
231 * iIntros "Hrepr". iDestruct "Hclose" as "[Hclose _]".
232 iMod ("Hclose" with "[Hrepr]") as "AU".
233 { iExists [n_head]. iFrame.
234 repeat iSplit; try done.
235 - iPureIntro. simpl. lia.
236 - simpl. by rewrite app_nil_r. }
237 done.
238 * iIntros "Hrepr". iDestruct "Hclose" as "[_ Hclose]".
239 set n_head' := Node n_head.(ℓ_node) (tail n_head.(vs_node)).
240 iMod ("Hclose" with "[Hrepr]") as "HΦ".
241 { iExists [n_head']. iFrame.
242 repeat iSplit; try done.
243 - iPureIntro. simpl. lia.
244 - simpl. by rewrite app_nil_r. }
245 destruct n_head.(vs_node) as [|v vs'];
246 iModIntro; wp_pures; iApply "HΦ".
247 Qed.
248
249 (** Linking two queues:
250 * _______________ _______________
251 * / Q1 \ / Q2 \
252 * ℓ_deq1 ... ℓ_enq1 <> ℓ_deq2 ... ℓ_enq2
253 * \ \ link op args / /
254 * \ \____________/ /
255 * \ Q1 <> Q2 /
256 * \______________________________/
257 *)
258 Lemma link_spec (ℓ_enq1 ℓ_deq2 : loc) :
259 ⊢ <<{ ∀∀ (b : bool) ℓ_deq1 ℓ_enq2 cvs1 cvs2, queue_repr ℓ_deq1 ℓ_enq1 cvs1 ∗
260 if b then queue_repr ℓ_deq2 ℓ_enq2 cvs2 else ⌜ℓ_deq1 = ℓ_deq2 ∧ ℓ_enq1 = ℓ_enq2⌝ }>>
261 link #ℓ_enq1 #ℓ_deq2 @ ∅
262 <<{ if b then queue_repr ℓ_deq1 ℓ_enq2 (cvs1 ++ cvs2) else True | RET #() }>>.
263 Proof.
264 iIntros "%Φ AU". iUnfold link.
265
266 wp_bind (fin_queue_spec.finalize _ _ _)%E.
267 awp_apply fqp.(fin_queue_spec.finalize_spec fq).
268 rewrite /atomic_acc /=.
269 iMod "AU" as (b ℓ_deq1 ℓ_enq2 cvs1 cvs2) "[[(%c1 & %Hclen1 & %Hhead1 & %Hlast1 & %Hcvs1 & Hqs1) Hqs2] Hclose]".
270 iModIntro.
271
272 destruct (last c1) as [n_last1|] eqn:Hlastn1; last done.
273 iExists n_last1.(vs_node).
274
275 apply last_Some in Hlastn1 as [c1' ->].
276 iDestruct (big_sepL_app with "Hqs1") as "[Hqs1 Hnode]".
277 iSimplifyEq. iDestruct "Hnode" as "[Hnode _]".
278 rewrite Nat.add_0_r.
279
280 rewrite lookup_ge_None_2 /=; last first.
281 { rewrite length_app /=. lia. }
282 iUnfold linked_single_queue_repr in "Hnode".
283 iSimplifyEq. iFrame.
284
285 iSplit.
286 - iDestruct "Hclose" as "[Hclose _]".
287 iIntros "Hnode".
288
289 iAssert (linked_single_queue_repr n_last1 (ℓ_node <$> (c1' ++ [n_last1]) !! S (length c1'))) with "[Hnode]" as "Hnode".
290 { rewrite /linked_single_queue_repr !lookup_app_r; last lia.
291 by assert (S (length c1') - length c1' = 1) as -> by lia. }
292
293 iDestruct (big_sepL_snoc with "[$Hqs1 $Hnode]") as "Hqs1'".
294
295 iPoseProof ("Hclose" with "[$Hqs1' $Hqs2]") as "Hqs".
296 { iPureIntro. repeat split; try done. by rewrite last_app. }
297 done.
298
299 - iDestruct "Hclose" as "[_ Hclose]".
300 iIntros "Hnode".
301
302 destruct b; last by iApply "Hclose".
303 iDestruct "Hqs2" as "(%c2 & %Hclen2 & %Hhead2 & %Hlast2 & %Hcvs2 & Hqs2)".
304
305 pose c := (c1' ++ [n_last1]) ++ c2.
306
307 iAssert (linked_single_queue_repr n_last1 (ℓ_node <$> c !! S (length c1'))) with "[Hnode]" as "Hnode".
308 { rewrite /linked_single_queue_repr /c !lookup_app_r; try (rewrite length_app /=; lia).
309 rewrite length_app /=. assert (S (length c1') - (length c1' + 1) = 0) as -> by lia.
310 rewrite -head_lookup Hhead2 //=. }
311
312 iDestruct (big_sepL_mono with "Hqs1") as "Hqs1".
313 { iIntros (i l Hi) "Hrepr".
314 iAssert (linked_single_queue_repr l (ℓ_node <$> c !! S i))%I with "[Hrepr]" as "Hrepr".
315 { rewrite /c lookup_app_l // length_app /=. apply lookup_lt_Some in Hi. lia. }
316 iExact "Hrepr". }
317
318 iDestruct (big_sepL_snoc with "[$Hqs1 $Hnode]") as "Hqs1'".
319
320 iDestruct (big_sepL_mono with "Hqs2") as "Hqs2".
321 { iIntros (i l Hi) "Hrepr".
322 iAssert (linked_single_queue_repr l (ℓ_node <$> c !! S (length (c1' ++ [n_last1]) + i)))%I with "[Hrepr]" as "Hrepr".
323 { rewrite /c length_app /= lookup_app_r length_app /=; last lia.
324 by assert (S i = S (length c1' + 1 + i) - (length c1' + 1)) as -> by lia. }
325 iExact "Hrepr". }
326 iSimplifyEq.
327
328 iDestruct (big_sepL_app with "[$Hqs1' $Hqs2]") as "Hqs". fold c.
329 rewrite -bind_app -/c.
330 iMod ("Hclose" with "[Hqs]") as "HΦ".
331 { iFrame. iPureIntro. repeat split; try done.
332 - rewrite /c !length_app /=. lia.
333 - rewrite /c head_app. case_match; last done. congruence.
334 - rewrite /c last_app. case_match; last done. congruence. }
335 iModIntro. iApply "HΦ".
336 Qed.
337
338 End proofs.
339
340End lmpmc_queue.
341
342Definition lmpmc_queue_hl (fq : fin_queue_spec.fin_queue_hl) : lmpmc_queue_spec.lmpmc_queue_hl.
343Proof.
344 by refine {| lmpmc_queue_spec.new := new;
345 lmpmc_queue_spec.enqueue := enqueue;
346 lmpmc_queue_spec.try_dequeue := try_dequeue;
347 lmpmc_queue_spec.link := link |}.
348Defined.
349
350Definition lmpmc_queue_iris `{!heapGS Σ}
351 (fq : fin_queue_spec.fin_queue_hl)
352 (fqp : fin_queue_spec.fin_queue_iris Σ fq) : lmpmc_queue_spec.lmpmc_queue_iris Σ (lmpmc_queue_hl fq).
353Proof.
354 by refine (lmpmc_queue_spec.LmpmcQueueIris _ _
355 (lmpmc_queue_hl fq) _ _
356 new_spec
357 enqueue_spec
358 try_dequeue_spec
359 link_spec).
360Defined.
361
362#[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 @@
1From iris.program_logic Require Import atomic.
2From iris.heap_lang Require Import notation proofmode.
3
4From lmpmc Require Import util.
5
6Record lmpmc_queue_hl :=
7 LmpmcQueueHl
8 { new : val;
9 enqueue : val;
10 try_dequeue : val;
11 link : val;
12 }.
13
14Record lmpmc_queue_iris {Σ} `{!heapGS Σ} (hl : lmpmc_queue_hl) :=
15 LmpmcQueueIris
16 { queue_repr : loc → loc → list val → iProp Σ;
17 #[global] queue_repr_timeless ℓ_deq ℓ_enq vs :: Timeless (queue_repr ℓ_deq ℓ_enq vs);
18
19 new_spec :
20 {{{ True }}}
21 hl.(new) #()
22 {{{ (ℓ_deq ℓ_enq : loc), RET (#ℓ_deq, #ℓ_enq); queue_repr ℓ_deq ℓ_enq [] }}};
23
24 enqueue_spec (ℓ_enq : loc) (data : val) :
25 ⊢ <<{ ∀∀ ℓ_deq cvs, queue_repr ℓ_deq ℓ_enq cvs }>>
26 hl.(enqueue) #ℓ_enq data @ ∅
27 <<{ queue_repr ℓ_deq ℓ_enq (cvs ++ [data]) | RET #() }>>;
28
29 try_dequeue_spec (ℓ_deq : loc) :
30 ⊢ <<{ ∀∀ ℓ_enq cvs, queue_repr ℓ_deq ℓ_enq cvs }>>
31 hl.(try_dequeue) #ℓ_deq @ ∅
32 <<{ queue_repr ℓ_deq ℓ_enq (tail cvs) | RET (val_opt_hl (head cvs)) }>>;
33
34 (** Linking two queues:
35 * _______________ _______________
36 * / Q1 \ / Q2 \
37 * ℓ_deq1 ... ℓ_enq1 <> ℓ_deq2 ... ℓ_enq2
38 * \ \ link op args / /
39 * \ \____________/ /
40 * \ Q1 <> Q2 /
41 * \______________________________/
42 *)
43 link_spec (ℓ_enq1 ℓ_deq2 : loc) :
44 ⊢ <<{ ∀∀ (b : bool) ℓ_deq1 ℓ_enq2 cvs1 cvs2, queue_repr ℓ_deq1 ℓ_enq1 cvs1 ∗
45 if b then queue_repr ℓ_deq2 ℓ_enq2 cvs2 else ⌜ℓ_deq1 = ℓ_deq2 ∧ ℓ_enq1 = ℓ_enq2⌝ }>>
46 hl.(link) #ℓ_enq1 #ℓ_deq2 @ ∅
47 <<{ if b then queue_repr ℓ_deq1 ℓ_enq2 (cvs1 ++ cvs2) else True | RET #() }>>;
48 }.
49#[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 @@
1From stdpp Require Import prelude ssreflect gmultiset.
2From stdpp Require Import options.
3
4Lemma prefix_of_fmap {A B} (f : A → B) (xs xs' : list A) :
5 xs `prefix_of` xs' →
6 f <$> xs `prefix_of` f <$> xs'.
7Proof. intros [ys ->]. exists (f <$> ys). apply fmap_app. Qed.
8
9Lemma prefix_sublist {A} (l1 l2 : list A) : l1 `prefix_of` l2 → l1 `sublist_of` l2.
10Proof. intros [k ->]. by apply sublist_inserts_r. Qed.
11
12Lemma prefix_submseteq {A} (l1 l2 : list A) : l1 `prefix_of` l2 → l1 ⊆+ l2.
13Proof. intros [k ->]. by apply submseteq_inserts_r. Qed.
14
15Lemma take_less_prefix {A} n m (xs : list A) : n ≤ m → take n xs `prefix_of` take m xs.
16Proof.
17 intros Hnm.
18 replace n with (n `min` m); last lia.
19 rewrite -take_take.
20 apply prefix_take.
21Qed.
22
23Lemma take_app_prefix {A} n (xs ys : list A) : take n xs `prefix_of` take n (xs ++ ys).
24Proof. unfold prefix. exists (take (n - length xs) ys). apply firstn_app. Qed.
25
26Lemma Forall_prefix {A} (xs xs' : list A) Φ : xs `prefix_of` xs' → Forall Φ xs' → Forall Φ xs.
27Proof. by intros [? ->] [? _]%Forall_app. Qed.
28
29Lemma drop_cons_inv {A} n x (xs xs' : list A) :
30 drop n xs = x :: xs' → xs !! n = Some x ∧ drop (S n) xs = xs'.
31Proof.
32 intros Hxs. split.
33 - by rewrite -[n]Nat.add_0_r -lookup_drop Hxs.
34 - by rewrite -Nat.add_1_r -drop_drop Hxs.
35Qed.
36
37Lemma list_to_set_disj_size `{Countable A} (l : list A) :
38 size (list_to_set_disj l : gmultiset A) = length l.
39Proof.
40 induction l; first done.
41 by rewrite /= gmultiset_size_disj_union IHl gmultiset_size_singleton.
42Qed.
43
44Lemma gmultiset_subseteq_size_eq `{Countable A, LeibnizEquiv A} (X Y : gmultiset A) :
45 X ⊆ Y → size Y ≤ size X → X = Y.
46Proof.
47 revert Y. induction X using gmultiset_ind; intros Y HY Hsize.
48 - rewrite gmultiset_size_empty in Hsize.
49 apply symmetry, gmultiset_size_empty_inv. lia.
50 - rewrite gmultiset_size_disj_union gmultiset_size_singleton in Hsize.
51 assert (X ⊆ Y ∖ {[+ x +]}) as HXY%IHX; [multiset_solver..|].
52 rewrite gmultiset_size_difference; last multiset_solver.
53 rewrite gmultiset_size_singleton. lia.
54Qed.
55
56Lemma elements_list_to_set_disj_perm `{Countable A} (l : list A) : l ≡ₚ elements (list_to_set_disj l : gmultiset A).
57Proof.
58 induction l; first done.
59 by rewrite list_to_set_disj_cons gmultiset_elements_disj_union gmultiset_elements_singleton -IHl.
60Qed.
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 @@
1From iris.heap_lang Require Import notation.
2
3Definition loc_to_val (ℓ : loc) : val := #ℓ.
4Definition val_opt_hl (mv : option val) : val :=
5 match mv with
6 | None => NONEV
7 | Some v => SOMEV v
8 end.
9Definition loc_opt_hl : option loc → val :=
10 val_opt_hl ∘ fmap loc_to_val.
11Arguments loc_to_val _ / : assert.
12Arguments loc_opt_hl !_ / : assert.
generated by cgit v1.3 (git 2.53.0) at 2026-06-25 21:31:17 +0000