-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathproof_graph_piggyback.v
1900 lines (1667 loc) · 81.1 KB
/
proof_graph_piggyback.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
From iris.bi Require Import fractional.
From iris.algebra Require Import excl auth.
From iris.proofmode Require Import tactics.
From gpfsl.algebra Require Import to_agree.
From gpfsl.base_logic Require Import meta_data.
From gpfsl.logic Require Import logatom atomics invariants.
From gpfsl.logic Require Import new_delete.
From gpfsl.logic Require Import proofmode.
From gpfsl.examples Require Import uniq_token map_seq loc_helper.
From gpfsl.examples.exchanger Require Import spec_graph spec_graph_piggyback code.
Require Import iris.prelude.options.
Local Arguments lookup_weaken {_ _ _ _ _ _ _ _}.
#[local] Notation hole := 0%nat (only parsing).
#[local] Notation data := 1%nat (only parsing).
#[local] Notation event_list := (event_list xchg_event).
#[local] Notation graph_event := (graph_event xchg_event).
#[local] Notation graph := (graph xchg_event).
Implicit Types (tid : thread_id) (γ : gname) (x : loc).
Implicit Types (G : graph) (E : event_list).
Implicit Types (N : namespace).
(** Namespace for our internal invariants. *)
Definition xchgN N := N .@ "xchg".
Definition offN N := N .@ "offer".
(* CMRA we need *)
(* a persistent map of from main offers to its info *)
Definition offer_info : Type := gname * gname.
Implicit Types (T : gmap loc offer_info).
#[local] Notation xchg_mapUR' := (agreeMR loc offer_info).
#[local] Notation xchg_mapUR := (authUR xchg_mapUR').
Class xchgG Σ := XChgG {
xchg_graphG : inG Σ (graphR xchg_event) ;
xchg_uniqTokG : uniqTokG Σ;
xchg_mapG : inG Σ xchg_mapUR;
}.
Local Existing Instance xchg_graphG.
Definition xchgΣ : gFunctors :=
#[GFunctor (graphR xchg_event);
GFunctor (exclR unitO);
GFunctor xchg_mapUR ].
Global Instance subG_xchgΣ {Σ} : subG xchgΣ Σ → xchgG Σ.
Proof. solve_inG. Qed.
(** History of the exchange *)
Definition toXChgHist (start : time) (LVs : list (option loc * view)) : absHist :=
map_seqP start ((λ olv, (#(oloc_to_lit olv.1), olv.2)) <$> LVs).
(** State of the offer *)
Inductive OfferState :=
| OfferMatching
| OfferCancelled
| OfferAccepted (l : loc)
| OfferAcked (l : loc)
.
Global Instance OfferState_inhabited : Inhabited OfferState := populate OfferMatching.
Definition offer_hist (s : OfferState) t0 V0 V1 ζ : Prop :=
let ζ0 : absHist := {[t0 := (#MATCHING, V0)]} in
match s with
| OfferMatching => ζ = ζ0
| OfferCancelled => ζ = <[(t0 + 1)%positive := (#CANCELLED, V1)]> ζ0
| OfferAccepted l2 | OfferAcked l2 => ζ = <[(t0 + 1)%positive := (#l2, V1)]> ζ0
end.
Section interp.
Context `{!noprolG Σ, !xchgG Σ, !atomicG Σ}.
Local Existing Instances xchg_graphG xchg_uniqTokG xchg_mapG.
#[local] Notation iProp := (iProp Σ).
#[local] Notation vProp := (vProp Σ).
Implicit Types (EI : bool → vProp).
(* Ghost assertions *)
Definition LTM_snap γe T : iProp := own (A:=xchg_mapUR) γe (◯ (to_agreeM T)).
Definition LTM_snapv γe T : vProp := ⎡ LTM_snap γe T ⎤.
Definition LTM_ssnap γe l i : iProp := LTM_snap γe {[l := i]}.
Definition LTM_ssnapv γe l i : vProp := ⎡ LTM_ssnap γe l i ⎤.
Definition LTM_master γe T : iProp := own (A:=xchg_mapUR) γe (● (to_agreeM T)).
Definition LTM_masterv γe T : vProp := ⎡ LTM_master γe T ⎤.
(** Public inv : Only share the ghost state with the client. *)
Definition ExchangerInv (γg : gname) (q : frac) G : vProp :=
(* ⌜ ExchangerConsistent G ∧ eventgraph_consistent G ⌝ ∗ *)
graph_gmasterv γg (q/2) G.
#[global] Instance ExchangerInv_objective γg q G :
Objective (ExchangerInv γg q G) := _.
#[global] Instance ExchangerInv_fractional γg G :
Fractional (λ q, ExchangerInv γg q G).
Proof.
intros p q. rewrite /ExchangerInv -!embed_sep Qp.div_add_distr.
apply embed_proper. iSplit.
- iIntros "[$ $]".
- iIntros "[G1 G2]". iSplitL "G1"; by iFrame.
Qed.
#[global] Instance ExchangerInv_AsFractional γg q G :
AsFractional (ExchangerInv γg q G) (λ q, ExchangerInv γg q G) q.
Proof. constructor; [done|apply _]. Qed.
Definition ExchangerSeen γx x : vProp :=
∃ ζx, x sn⊒{γx} ζx.
#[global] Instance ExchangerSeen_persistent γx x :
Persistent (ExchangerSeen γx x) := _.
(** AU needed for helping with committing the exchange *)
(* TODO: this can be dealt with sufficiently with just the difference between
ExchangerLocal and ExchangerLocalLite *)
(* FIXME: AU notation doesn't parse. *)
Definition exchange_AU_atomic_post' γx γg x G1 M Vin1 v1 b1 b2 : exchange_postT :=
(λ G V' G' exId1 exId2 v2 Vex1 Vex2 M',
▷ ExchangerInv γg 1%Qp G' ∗
⊒V' ∗
⌜ G ⊑ G' ∧ M ⊑ M' ∧
Vex1.(dv_in) = Vin1 ∧ Vex1.(dv_comm) = V' ∧
exId1 = length G.(Es) ∧
G'.(Es) = G.(Es) ++ [mkGraphEvent (Exchange v1 v2) Vex1 M'] ∧
exId1 ∈ M' ∧ exId1 ∉ M ⌝ ∗
( ⌜ (* CANCELLED case *)
v2 = CANCELLED ∧ G'.(so) = G.(so) ∧ G'.(com) = G.(com) ∧
eventgraph_consistent G' ∧ ExchangerConsistent G' ∧
b1 = true ⌝ ∧
@{V'} (graph_snap γg G' M' ∗ ExchangerSeen γx x)
∨ (* SUCCESS case *)
⌜ 0 ≤ v2 ∧
(length G1.(Es) ≤ exId2)%nat ∧
exId2 ∈ M' ∧ exId2 ∉ M ∧ exId1 ≠ exId2
(* This fixes the order in which the AUs are committed.
TODO: generalize so that the client can pick the order *)
∧ (v1 ≠ v2 → v1 > v2 ↔ (exId1 < exId2)%nat)
∧ b1 = false ⌝ ∗
( (* if my event comes in later *)
⌜ (exId2 < exId1)%nat ∧ b2 = false ∧
G.(Es) !! exId2 = Some (mkGraphEvent (Exchange v2 v1) Vex2 M') ∧
G'.(so) = {[ (exId1, exId2); (exId2, exId1) ]} ∪ G.(so) ∧
G'.(com) = {[ (exId1, exId2); (exId2, exId1) ]} ∪ G.(com) ∧
exId1 ∉ (elements G.(so)).*1 ∧ exId2 ∉ (elements G.(so)).*1 ∧
eventgraph_consistent G' ∧ ExchangerConsistent G' ⌝ ∗
@{V'} (graph_snap γg G' M' ∗ ExchangerSeen γx x)
(* else if my event comes in earlier *)
∨ ⌜ (exId1 < exId2)%nat ∧ b2 = true ∧
G'.(so) = G.(so) ∧ G'.(com) = G.(com) ⌝ ∗
@{V'} (graph_snap γg G' (M' ∖ {[exId2]}) ∗ ExchangerSeen γx x)))
)%I.
Definition exchange_priv_post' γx γg x v1 (Q : Z → vProp) : exchange_postT :=
(λ G V' G' exId1 exId2 v2 Vex1 Vex2 M',
(⌜ 0 ≤ v2 ∧ (exId1 < exId2)%nat ⌝ → ∃ G'',
⌜ G' ⊑ G'' ∧
exId2 = length G'.(Es) ∧
G''.(Es) = G'.(Es) ++ [mkGraphEvent (Exchange v2 v1) Vex2 M'] ∧
G''.(so) = {[ (exId1, exId2); (exId2, exId1) ]} ∪ G.(so) ∧
G''.(com) = {[ (exId1, exId2); (exId2, exId1) ]} ∪ G.(com) ∧
exId1 ∉ (elements G'.(so)).*1 ∧ exId2 ∉ (elements G'.(so)).*1 ⌝ ∗
@{V'}(graph_snap γg G'' M' ∗ ExchangerSeen γx x)) -∗ Q v2
)%I.
Definition exchange_AU_proof' (EI : bool → vProp) (N : namespace)
γx γg x G1 M Vin1 v1
(Q : _ → vProp)
{TA' TB' : tele} (α' : TA' → vProp) (β' Φ' : TA' → TB' → vProp)
: vProp :=
atomic_update_proof EI (⊤ ∖ ↑N) (↑histN)
α' β' Φ'
(tele_app (TT:= [tele _]) (exchange_AU_atomic_pre ExchangerInv γg))
(λ b1 b2,
(tele_app (TT:= [tele _])
(λ G, tele_app (TT:= [tele _ _ _ _ _ _ _ _])
(exchange_AU_atomic_post' γx γg x G1 M Vin1 v1 b1 b2 G))))
(tele_app (TT:= [tele _])
(λ G, tele_app (TT:= [tele _ _ _ _ _ _ _ _])
(exchange_priv_post' γx γg x v1 Q G)))
.
Definition offer_res
o γk (P : vProp) (Q: Z → vProp) (v1 : Z) V0 V1 (s : OfferState) : vProp :=
match s with
| OfferMatching => @{V0} ((o >> data) ↦ #v1 ∗ P)
| OfferAccepted l2 => @{V1} (∃ v2 : Z, (l2 >> data) ↦ #v2 ∗ Q v2)
| _ => UTok γk
end
.
#[global] Instance offer_res_Objective o γk P Q v1 V0 V1 s :
Objective (offer_res o γk P Q v1 V0 V1 s).
Proof. destruct s; apply _. Qed.
(* Offer inv keeps the full writer permission, so that everyone can only CAS
using this invariant. *)
Definition offer_rep (o : loc) γo γk v1 t0 V0 P Q : vProp :=
∃ s ζo V1, ⌜ offer_hist s t0 V0 V1 ζo ∧ 0 ≤ v1 ⌝ ∗
(∃ Vo, @{Vo} o sw⊒{γo} ζo) ∗
offer_res o γk P Q v1 V0 V1 s.
(* Invariant of offer, created by the helpee.
We use invariant to have agreement on P Q; otherwise we would need saved predicate!
(where laters wouldn't be a problem, but ghost names are.) *)
Definition offer_inv EI N γx γg x o γo γk t0 V0 : vProp :=
∃ v P Q, inv (offN N) (offer_rep o γo γk v t0 V0 P Q) ∗
∃ M1 Vin1,
@{V0} (
⊒Vin1 ∗ (* store the Vin of the helpee *)
∃ G1, graph_snap γg G1 M1 ∗
∃ (TA' TB' : tele) (α' : TA' → vProp) (β' Φ' : TA' → TB' → vProp),
□ (P -∗ atomic_update (⊤ ∖ ↑N) (↑histN) α' β' Φ') ∗
□ (exchange_AU_proof' EI N γx γg x G1 M1 Vin1 v Q α' β' Φ')
).
(* Main offer is created by the helpee and write to the exchange.
A helper will just offer a match on a main offer. *)
Definition main_offer EI N γx γg x T o V : vProp :=
∃ γo γk,
⌜ T !! o = Some (γo, γk) ⌝ ∗ (* meta-data *)
(∃ ζo, @{V} o sn⊒{γo} ζo) ∗ (* atomic observation *)
(∃ ζ, o sw↦{γo} ζ) ∗ (* atomic ownership *)
∃ t0 V0, ⌜ V0 ⊑ V ⌝ ∗
offer_inv EI N γx γg x o γo γk t0 V0 (* offer invariant *)
.
Definition main_offers EI N γx γg x T (os : list (loc * view)) : vProp :=
[∗ list] oV ∈ os, let '(o, V) := oV in main_offer EI N γx γg x T o V.
Definition xchg_locs EI N γx γg x T LVs os : vProp :=
(∃ t0, let ζx := (toXChgHist t0 LVs) in x at↦{γx} ζx) ∗
main_offers EI N γx γg x T os ∗
⌜ filter (is_Some ∘ fst) LVs = (λ p, (Some p.1, p.2)) <$>os ∧
dom T ≡ list_to_set (os.*1)⌝.
Definition ExchangerBaseInv_no_exist
EI N γg x G γt γx LVs os T : vProp :=
LTM_masterv γt T ∗
∃ Vb, @{Vb} xchg_locs EI N γx γg x T LVs os
.
Definition ExchangerBaseInv EI N γt γx γg x G : vProp :=
∃ LVs os T, ExchangerBaseInv_no_exist EI N γg x G γt γx LVs os T.
(* Our internal invariant keeps all the physical resources, as well as enough
ghost resources (`ExchangerInv`) to maintain agreement with the client. *)
Definition ExchangerInternalInv EI N γt γx γg x : vProp :=
∃ G, ⌜ ExchangerConsistent G ∧ eventgraph_consistent G ⌝ ∗
ExchangerInv γg 1 G ∗ ExchangerBaseInv EI N γt γx γg x G.
#[global] Instance ExchangerInternalInv_objective EI N γt γx γg x :
Objective (ExchangerInternalInv EI N γt γx γg x) := _.
Definition InternInv EI N γt γx γg x :=
inv (xchgN N) (ExchangerInternalInv EI N γt γx γg x).
(** ExchangerLocal assertion, specific to this implementation---------------- *)
Definition ExchangerLocalLite γg x G logV : vProp :=
graph_snap γg G logV
∗ ∃ (γt γx : gname), ExchangerSeen γx x
∗ meta x nroot (γt,γx).
#[global] Instance ExchangerLocalLite_persistent γg x G M :
Persistent (ExchangerLocalLite γg x G M) := _.
#[global] Instance ExchangerLocalLite_timeless γg x G M :
Timeless (ExchangerLocalLite γg x G M) := _.
Definition ExchangerLocal EI N γg x G logV : vProp :=
graph_snap γg G logV
∗ ∃ (γt γx : gname), ExchangerSeen γx x
∗ meta x nroot (γt,γx)
∗ InternInv EI N γt γx γg x.
#[global] Instance ExchangerLocal_persistent EI N γg x G M :
Persistent (ExchangerLocal EI N γg x G M) := _.
End interp.
(** Properties of history *)
Lemma toXChgHist_lookup_Some t0 LVs t v V :
toXChgHist t0 LVs !! t = Some (v, V) ↔
(t0 ≤ t)%positive
∧ ∃ on, v = #(oloc_to_lit on)
∧ LVs !! (Pos.to_nat t - Pos.to_nat t0)%nat = Some (on, V).
Proof.
rewrite lookup_map_seqP_Some. f_equiv.
rewrite list_lookup_fmap fmap_Some. split.
- intros ([] & ? & ?). simplify_eq. naive_solver.
- intros (on & -> & ?). exists (on, V). naive_solver.
Qed.
Lemma toXChgHist_lookup_Some' {t0 LVs t v V} :
toXChgHist t0 LVs !! t = Some (v, V) →
∃ on, v = #(oloc_to_lit on) ∧ (on, V) ∈ LVs.
Proof.
rewrite toXChgHist_lookup_Some.
intros (_ & on & Eq & Eql). exists on. split; [done|].
revert Eql. apply elem_of_list_lookup_2.
Qed.
Lemma toXChgHist_lookup_Some_loc {t0 LVs t} {l : loc} {V} :
toXChgHist t0 LVs !! t = Some (#l, V) → (Some l, V) ∈ LVs.
Proof.
intros (on & Eq & In)%toXChgHist_lookup_Some'. by destruct on; simplify_eq.
Qed.
Lemma toXChgHist_lookup_None {t0 LVs t} :
toXChgHist t0 LVs !! t = None ↔
(t < t0)%positive ∨ (t0 +p (length LVs) ≤ t)%positive.
Proof. by rewrite lookup_map_seqP_None fmap_length. Qed.
Lemma toXChgHist_lookup_Some_None {t0 LVs t p} :
toXChgHist t0 LVs !! t = Some p →
toXChgHist t0 LVs !! (t + 1)%positive = None →
(Pos.to_nat (t + 1)%positive - Pos.to_nat t0)%nat = length LVs ∧ (1 ≤ length LVs)%nat.
Proof.
intros EqS EqN.
assert (EqL := lookup_map_seqP_last_idx _ _ _ _ EqS EqN).
destruct p as [v V].
apply toXChgHist_lookup_Some in EqS as [Letx0 [on [Eqv Eqt]]].
have EqL1 : (1 ≤ length LVs)%nat.
{ clear -Eqt Letx0. apply lookup_lt_Some in Eqt. lia. }
move : EqL. rewrite fmap_length /pos_add_nat; lia.
Qed.
Lemma toXChgHist_comparable_nullable_loc {LVs t0 t v} (on : option loc) :
fst <$> toXChgHist t0 LVs !! t = Some v →
∃ vl : lit, v = #vl ∧ lit_comparable (oloc_to_lit on) vl.
Proof.
rewrite -lookup_fmap lookup_fmap_Some.
move => [[? V] [/=-> /toXChgHist_lookup_Some'[on' [-> _]]]].
exists (oloc_to_lit on'). split; [done|].
destruct on, on'; constructor.
Qed.
Lemma toXChgHist_comparable_0 t0 LVs :
∀ t v, fst <$> toXChgHist t0 LVs !! t = Some v →
∃ vl : lit, v = #vl ∧ lit_comparable 0 vl.
Proof. intros ??. by apply (toXChgHist_comparable_nullable_loc None). Qed.
Lemma toXChgHist_comparable_loc t0 LVs (l : loc):
∀ t v, fst <$> toXChgHist t0 LVs !! t = Some v →
∃ vl : lit, v = #vl ∧ lit_comparable l vl.
Proof. intros ??. by apply (toXChgHist_comparable_nullable_loc (Some l)). Qed.
Lemma toXChgHist_insert t0 LVs t on V :
(Pos.to_nat t - Pos.to_nat t0)%nat = length LVs →
(1 ≤ length LVs)%nat →
<[t := (#(oloc_to_lit on), V)]>(toXChgHist t0 LVs) =
toXChgHist t0 (LVs ++ [(on, V)]).
Proof.
intros Eq ?. apply map_eq.
intros i. case (decide (i = t)) => [->|?].
- rewrite lookup_insert. symmetry.
apply toXChgHist_lookup_Some. split; [lia|].
rewrite Eq !lookup_app_r // Nat.sub_diag /=. naive_solver.
- rewrite lookup_insert_ne; [|done].
destruct (toXChgHist t0 LVs !! i) as [[vi Vi]|] eqn:Eqi; rewrite Eqi; symmetry.
+ apply toXChgHist_lookup_Some in Eqi as (Letn & on' & -> & Eq1).
apply toXChgHist_lookup_Some. split; [done|].
exists on'. split; [done|]. by apply (lookup_app_l_Some _ _ _ _ Eq1).
+ apply toXChgHist_lookup_None.
apply toXChgHist_lookup_None in Eqi as [?|Eqi]; [by left|right].
rewrite app_length /=. move : Eqi.
rewrite Nat.add_1_r pos_add_succ_r_2.
rewrite (_: t0 +p length LVs = t); [lia|]. rewrite -Eq /pos_add_nat; lia.
Qed.
Lemma toXChgHist_insert_next_fresh {t0 LVs t p} on V :
toXChgHist t0 LVs !! t = Some p →
toXChgHist t0 LVs !! (t + 1)%positive = None →
<[(t + 1)%positive := (#(oloc_to_lit on), V)]>(toXChgHist t0 LVs) =
toXChgHist t0 (LVs ++ [(on, V)]).
Proof.
intros EqS EqN. destruct (toXChgHist_lookup_Some_None EqS EqN).
by apply toXChgHist_insert.
Qed.
Lemma filter_is_Some_fst_in
{LVs : list (option loc * view)} {os : list (loc * view)} {l V} :
filter (is_Some ∘ fst) LVs = (λ p : loc * view, (Some p.1, p.2)) <$> os →
(Some l, V) ∈ LVs → (l, V) ∈ os.
Proof.
intros Eqso InlV.
assert (Inl2 : (Some l, V) ∈ (λ p, (Some p.1, p.2)) <$> os).
{ rewrite -Eqso elem_of_list_filter. split; [clear; eauto|done]. }
apply elem_of_list_fmap in Inl2 as ([] & Eql2 & ?).
simpl in Eql2. by inversion Eql2.
Qed.
Lemma filter_is_Some_None (LVs : list (option loc * view)) :
(∀ o V, (o, V) ∈ LVs → o = None) →
filter (is_Some ∘ fst) LVs = [].
Proof.
intros oV. apply filter_nil_iff, Forall_forall => [[o V] /oV ->].
by inversion 1.
Qed.
Lemma filter_is_Some_app_None (LVs : list (option loc * view)) V :
filter (is_Some ∘ fst) (LVs ++ [(None,V)]) = filter (is_Some ∘ fst) LVs.
Proof.
rewrite filter_app (filter_is_Some_None [(_,_)]).
- by rewrite app_nil_r.
- intros ?? Eq%elem_of_list_singleton. by inversion Eq.
Qed.
(** Properties of OfferState *)
(* Needed for CAS: any value in a history of the offer is comparable to 0. *)
Lemma offer_hist_comparable_0 {s t0 V0 V1 ζ} :
offer_hist s t0 V0 V1 ζ →
(∀ t v, fst <$> ζ !! t = Some v → ∃ vl : lit, v = #vl ∧ lit_comparable 0 vl).
Proof.
intros OH t v ([v2 V2] & Eq1 & Eqt)%lookup_fmap_Some'. simpl in Eq1. subst v2.
destruct s as [| |l|l]; simpl in OH; subst ζ.
- apply lookup_singleton_Some in Eqt as [-> Eqt]. inversion Eqt. subst.
exists 0. split; [done|constructor].
- assert (Eqv: v = #0 ∨ v = #CANCELLED).
{ apply lookup_insert_Some in Eqt as [[_ Eq1]|[_ Eq1%lookup_singleton_Some]];
naive_solver. }
destruct Eqv; subst v; eexists; (split;[done|constructor]).
- assert (Eqv: v = #0 ∨ v = #l).
{ apply lookup_insert_Some in Eqt as [[_ Eq1]|[_ Eq1%lookup_singleton_Some]];
naive_solver. }
destruct Eqv; subst v; eexists; (split;[done|constructor]).
- assert (Eqv: v = #0 ∨ v = #l).
{ apply lookup_insert_Some in Eqt as [[_ Eq1]|[_ Eq1%lookup_singleton_Some]];
naive_solver. }
destruct Eqv; subst v; eexists; (split;[done|constructor]).
Qed.
Lemma offer_hist_lookup_0 {s t0 V0 V1 ζ} :
offer_hist s t0 V0 V1 ζ →
∀ t' V', ζ !! t' = Some (#MATCHING, V') ↔ t' = t0 ∧ V' = V0.
Proof.
intros OF t' V'; destruct s; simpl in OF; subst ζ;
[rewrite lookup_singleton_Some; naive_solver|..];
(rewrite lookup_insert_Some lookup_singleton_Some;
split; [naive_solver|]; intros [-> ->];
right; split; [lia|naive_solver]).
Qed.
Lemma offer_hist_lookup_n0 {s t0 V0 V1 ζ} :
offer_hist s t0 V0 V1 ζ →
∀ t' (v' : lit) V',
ζ !! t' = Some (#v', V') → v' ≠ MATCHING →
s ≠ OfferMatching ∧ t' = (t0 + 1)%positive ∧ V' = V1.
Proof.
intros OF t' v' V'. destruct s; simpl in OF; subst ζ;
[rewrite lookup_singleton_Some; naive_solver|..];
rewrite lookup_insert_Some lookup_singleton_Some; naive_solver.
Qed.
Lemma offer_hist_lookup_cancelled {s t0 V0 V1 ζ} :
offer_hist s t0 V0 V1 ζ →
∀ t' V',
ζ !! t' = Some (#CANCELLED, V') →
s = OfferCancelled ∧ t' = (t0 + 1)%positive ∧ V' = V1.
Proof.
intros OF t' V'. destruct s; simpl in OF; subst ζ;
[rewrite lookup_singleton_Some; naive_solver|..];
rewrite lookup_insert_Some lookup_singleton_Some; naive_solver.
Qed.
Lemma offer_hist_lookup_matched {s t0 V0 V1 ζ} :
offer_hist s t0 V0 V1 ζ →
∀ t' (l' : loc) V',
ζ !! t' = Some (#l', V') →
(s = OfferAccepted l' ∨ s = OfferAcked l') ∧ t' = (t0 + 1)%positive ∧ V' = V1.
Proof.
intros OF t' l' V'. destruct s; simpl in OF; subst ζ;
[rewrite lookup_singleton_Some; naive_solver|..];
rewrite lookup_insert_Some lookup_singleton_Some; naive_solver.
Qed.
(** Graph insertions *)
Lemma exchange_cancel_graph_insert
G v (M : logView) (V : dataView) :
V.(dv_comm) ⊑ V.(dv_wrt) →
ExchangerConsistent G →
let e := length G.(Es) in
let eV := Exchange v CANCELLED in
let egV := mkGraphEvent eV V ({[e]} ⊔ M) in
let G' := graph_insert_event egV G in
ExchangerConsistent G'.
Proof.
intros ? [CONDv CON2a CON2b [CON3a CON3b] CON4 CON5].
intros e eV egV G'.
constructor; [ |done|..|done| |done].
- (* DView *) by apply graph_insert_event_is_releasing.
- (* 2b *)
intros e1 e2 (? & eV1 & eV2 & ve1 & ve2 & Eq1 & Eq2 & ?)%CON2b.
split; [done|].
exists eV1, eV2, ve1, ve2. split; last split; [..|done].
+ by eapply lookup_app_l_Some.
+ by eapply lookup_app_l_Some.
- (* 4 *)
intros e0 eV0. case (decide (e = e0)) => ?.
+ subst e0. rewrite lookup_app_1_eq. inversion 1. subst eV0.
intros ?. by exists v.
+ rewrite lookup_app_1_ne; [by apply CON4|done].
Qed.
Lemma exchange_commit_graph_insert
(b : bool) G v1 v2 (M1 M2 : logView) (V1 V2 : dataView) :
V1.(dv_comm) ⊑ V1.(dv_wrt) → V2.(dv_comm) ⊑ V2.(dv_wrt) →
V1.(dv_in) ⊏ V2.(dv_comm) → V2.(dv_in) ⊏ V1.(dv_comm) →
0 ≤ v1 → 0 ≤ v2 →
ExchangerConsistent G →
let emi := length G.(Es) in let emx := S (length G.(Es)) in
let M' := {[emi;emx]} ∪ (if b then M1 else M2) ∪ (if b then M2 else M1) in
let Ev1 := (Exchange v1 v2) in
let Ev2 := (Exchange v2 v1) in
let Emi := mkGraphEvent (if b then Ev1 else Ev2) (if b then V1 else V2) M' in
let Emx := mkGraphEvent (if b then Ev2 else Ev1) (if b then V2 else V1) M' in
let G' := graph_insert2 Emi Emx G in
ExchangerConsistent G'.
Proof.
intros LeV11 LeV22 LtV12 LtV21 Pos1 Pos2.
intros [CONDv [CON2a1 CON2a2] CON2b [CON3a CON3b] CON4 CON5].
intros emi emx M' Ev1 Ev2 Emi Emx G'.
have NEq12 : emi ≠ emx by lia.
have NIne12 : (emi, emx) ∉ G.(com). { move => /gcons_com_included [/=]. lia. }
have NIne21 : (emx, emi) ∉ G.(com). { move => /gcons_com_included [/=]. lia. }
have Eqe12 : (emi = S emx ∨ emx = S emi) by lia.
have EqEs' : G'.(Es) = (G.(Es) ++ [Emi]) ++ [Emx] by apply (app_assoc _ [_] [_]).
have Eqemx : emx = length (Es G ++ [Emi]). { rewrite app_length /=. lia. }
constructor; [|split| |split|..].
- (* DView *) rewrite /= (app_assoc _ [_]). clear -LeV11 LeV22 CONDv.
apply graph_insert_event_is_releasing;
[apply graph_insert_event_is_releasing|]; [done|..]; by destruct b.
- (* 2a1 *)
intros i j. rewrite /= elem_of_union CON2a1. clear. set_solver.
- (* 2a2 *)
intros e. clear -CON2a2 NEq12. specialize (CON2a2 e). rewrite elem_of_union.
set_solver.
- (* 2b *)
intros i j. rewrite !elem_of_union !elem_of_singleton.
rewrite -/emi -/emx.
intros [[Eq|Eq]|(? & eVi & eVj & ve1 & ve2 & Eq1 & Eq2 & ?)%CON2b].
+ rewrite EqEs'. inversion Eq. subst i j. split; [done|].
do 2 eexists. exists (if b then v1 else v2), (if b then v2 else v1).
split; [by rewrite lookup_app_1_ne; [rewrite lookup_app_1_eq|by rewrite -Eqemx]|].
split; [by rewrite Eqemx lookup_app_1_eq|]; destruct b; done.
+ rewrite EqEs'. inversion Eq. subst i j. split; [clear -Eqe12; naive_solver|].
do 2 eexists. exists (if b then v2 else v1), (if b then v1 else v2).
split; [by rewrite Eqemx lookup_app_1_eq|].
split; [by rewrite lookup_app_1_ne; [rewrite Eqemx lookup_app_1_eq|by rewrite -Eqemx]|].
destruct b; done.
+ split; [done|]. exists eVi, eVj, ve1, ve2.
split; last split; [..|done]; by apply lookup_app_l_Some.
- (* 3a *)
intros [] []. rewrite !elem_of_union !elem_of_singleton.
intros [[->| ->]|In1] [[->| ->]|In2]; simpl; auto.
+ move : In2 => /gcons_com_included [/=]. clear ; lia.
+ move : In2 => /gcons_com_included [/=]. clear ; lia.
+ move : In1 => /gcons_com_included [/=]. clear ; lia.
+ move : In1 => /gcons_com_included [/=]. clear ; lia.
+ apply (CON3a _ _ In1 In2).
- (* 3b *)
intros [] []. rewrite !elem_of_union !elem_of_singleton.
intros [[->| ->]|In1] [[->| ->]|In2]; simpl; auto.
+ move : In2 => /gcons_com_included [/=]. clear ; lia.
+ move : In2 => /gcons_com_included [/=]. clear ; lia.
+ move : In1 => /gcons_com_included [/=]. clear ; lia.
+ move : In1 => /gcons_com_included [/=]. clear ; lia.
+ apply (CON3b _ _ In1 In2).
- (* 4 *)
intros e eV EqeV NIG'.
have NIG : e ∉ (elements G.(com)).*1. { clear -NIG'. set_solver. }
have ? : e ≠ emi. {
clear -NIG'. intros => ?. subst e. simpl in NIG'.
apply NIG', elem_of_list_fmap. exists (emi, emx). set_solver. }
have ? : e ≠ emx. {
clear -NIG'. intros => ?. subst e. simpl in NIG'.
apply NIG', elem_of_list_fmap. exists (emx, emi). set_solver. }
revert EqeV NIG. rewrite EqEs'.
do 2 (rewrite lookup_app_1_ne; [|lia]).
apply CON4.
- by rewrite /= CON5.
Qed.
Section interp_props.
Context `{!noprolG Σ, !xchgG Σ, !atomicG Σ}.
Local Existing Instances xchg_graphG xchg_uniqTokG xchg_mapG.
#[local] Notation iProp := (iProp Σ).
#[local] Notation vProp := (vProp Σ).
Implicit Types (EI : bool → vProp).
(** * PROPERTIES OF ASSERTIONS -------------------------------------------------*)
(** * Ghost state rules *)
Lemma LTM_master_alloc T :
⊢ |==> ∃ γt, LTM_master γt T.
Proof. by apply own_alloc, auth_auth_valid, to_agreeM_valid. Qed.
Lemma LTM_master_snap_included γ T T' :
LTM_master γ T -∗ LTM_snap γ T' -∗ ⌜T' ⊆ T⌝.
Proof.
iIntros "o1 o2".
iCombine "o1 o2" gives %[INCL ?]%auth_both_valid_discrete.
iPureIntro. by move : INCL => /= /to_agreeM_included.
Qed.
Lemma LTM_master_ssnap_lookup γ M l i :
LTM_master γ M -∗ LTM_ssnap γ l i -∗ ⌜ M !! l = Some i ⌝.
Proof.
iIntros "LTm VMs". by iDestruct (LTM_master_snap_included with "LTm VMs")
as %SUB%map_singleton_subseteq_l.
Qed.
Lemma LTM_update γ T T' (SUB: T ⊆ T'):
LTM_master γ T ==∗ LTM_master γ T' ∗ LTM_snap γ T'.
Proof.
rewrite -own_op.
by apply own_update, auth_update_alloc, to_agreeM_local_update.
Qed.
Lemma LTM_snap_sub γ T T' (Le: T ⊆ T') : LTM_snap γ T' ⊢ LTM_snap γ T.
Proof.
by apply own_mono, auth_frag_mono, to_agreeM_included.
Qed.
Lemma LTM_update_insert γ T l i (FR: l ∉ dom T):
LTM_master γ T ==∗ LTM_master γ (<[l := i]>T) ∗ LTM_ssnap γ l i.
Proof.
iIntros "LTm".
iMod (LTM_update with "LTm") as "[$ Snap]".
{ by apply insert_subseteq, (not_elem_of_dom (D:= gset _)). }
iIntros "!>". iApply (LTM_snap_sub with "Snap").
by apply insert_mono, gmap_subseteq_empty.
Qed.
Lemma LTM_master_fork γ T :
LTM_master γ T ==∗ LTM_master γ T ∗ LTM_snap γ T.
Proof. by apply LTM_update. Qed.
(** * ExchangerInv *)
(* TODO: we should not go under graph_master *)
Lemma ExchangerInv_agree γg q G q' G' :
ExchangerInv γg q G -∗ ExchangerInv γg q' G' -∗ ⌜ G' = G ⌝.
Proof.
iIntros "G1 G2". by iDestruct (ghost_graph_master_agree with "G1 G2") as %?.
Qed.
Lemma ExchangerInv_graph_master γg q G :
⌜eventgraph_consistent G⌝ ∗ ExchangerInv γg q G
⊣⊢ graph_master γg (q/2) G.
Proof. rewrite /graph_master. iSplit; by iIntros "[$ $]". Qed.
Lemma ExchangerInv_graph_master' γg q G :
⌜eventgraph_consistent G⌝ ∗ ExchangerInv γg q G ⊢ graph_master γg (q/2) G.
Proof. by rewrite ExchangerInv_graph_master. Qed.
Lemma ExchangerInv_graph_master_agree γg q G q' G' :
graph_master γg q G -∗ ExchangerInv γg q' G' -∗
⌜ G' = G ⌝ ∗ graph_master γg q G ∗ graph_master γg (q'/2) G.
Proof.
rewrite -ExchangerInv_graph_master /graph_master.
iIntros "[G1 #F] G2".
iDestruct (ExchangerInv_agree _ (2 * q)%Qp with "[G1] G2") as %->.
{ rewrite /ExchangerInv -{2}(Qp.mul_1_r 2) Qp.div_mul_cancel_l Qp.div_1. iFrame. }
rewrite /ExchangerInv. by iFrame "F G1 G2".
Qed.
(** * Accessors *)
Lemma ExchangerBaseInv_unfold_snap EI N γg γt γx x G T0 :
ExchangerBaseInv EI N γt γx γg x G -∗
LTM_snapv γt T0 -∗
∃ LVs os T, ExchangerBaseInv_no_exist EI N γg x G γt γx LVs os T ∗ ⌜ T0 ⊆ T ⌝.
Proof.
iDestruct 1 as (???) "(LTm & Locs)". iIntros "LTs". iExists _, _, _.
iDestruct (LTM_master_snap_included with "LTm LTs") as %?. by iFrame.
Qed.
Lemma main_offer_own_loc_prim EI N γx γg x T n V :
main_offer EI N γx γg x T n V ⊢ ∃ C : cell, n p↦{1} C.
Proof.
iDestruct 1 as (γ ? _) "(_ & [%ζi Oi] & _)".
by iApply (AtomicPtsTo_own_loc_prim with "Oi").
Qed.
Lemma main_offers_app EI N γx γg x T os1 os2 :
main_offers EI N γx γg x T (os1 ++ os2) ⊣⊢
main_offers EI N γx γg x T os1 ∗ main_offers EI N γx γg x T os2.
Proof. by apply big_sepL_app. Qed.
Lemma main_offers_map_mono {EI N γx γg x T T' os} :
T ⊆ T' → main_offers EI N γx γg x T os ⊢ main_offers EI N γx γg x T' os.
Proof.
intros ?. apply big_sepL_mono => i [o V] Eqi.
iDestruct 1 as (γo γk Eqo) "I".
iExists γo, γk. iFrame. iPureIntro. by apply (lookup_weaken Eqo).
Qed.
Lemma main_offers_access {EI N γx γg x T os o V} :
(o, V) ∈ os →
main_offers EI N γx γg x T os ⊢
main_offer EI N γx γg x T o V ∗
(main_offer EI N γx γg x T o V -∗ main_offers EI N γx γg x T os).
Proof.
intros [i Eqi]%elem_of_list_lookup.
iIntros "Offs". by iApply (big_sepL_lookup_acc _ _ _ _ Eqi with "Offs").
Qed.
Lemma main_offers_own_loc_prim {EI N γx γg x T os o V} :
(o, V) ∈ os → main_offers EI N γx γg x T os ⊢ ∃ C : cell, o p↦{1} C.
Proof.
iIntros (Ino) "Off".
iDestruct (main_offers_access Ino with "Off") as "[Off _]".
iApply (main_offer_own_loc_prim with "Off").
Qed.
Lemma main_offer_disjoint EI N γx γg x T os V1 l q C V2 :
@{V1} main_offers EI N γx γg x T os -∗ @{V2} l p↦{q} C -∗ ⌜l ∉ os.*1⌝.
Proof.
iIntros "Hl Hl'" (([l' Vl] & Eql & Inos)%elem_of_list_fmap).
simpl in Eql. subst l'. rewrite (main_offers_own_loc_prim Inos).
iDestruct "Hl" as (C') "Hl".
iAssert (@{V1 ⊔ V2} (l p↦{1 + q} C'))%I with "[-]" as "O".
{ iApply (view_at_mono' with "Hl'"); [solve_lat|].
iApply (view_at_mono with "Hl"); [solve_lat|].
apply own_loc_prim_combine. }
rewrite own_loc_prim_frac_1. by iDestruct "O" as %Lt%Qp.not_add_le_l.
Qed.
End interp_props.
Section proof.
Context `{!noprolG Σ, !xchgG Σ, !atomicG Σ}.
#[local] Notation iProp := (iProp Σ).
#[local] Notation vProp := (vProp Σ).
Local Existing Instances xchg_graphG xchg_uniqTokG xchg_mapG.
Lemma ExchangerInv_ExchangerConsistent_instance :
∀ EI, ExchangerInv_ExchangerConsistent_piggyback (ExchangerLocal EI) ExchangerInv.
Proof.
iIntros (EI N γg x q G G' M') "GE [? EL]".
iDestruct "EL" as (γt γx) "(ES & MT & II)".
iInv "II" as (G0) "(>[%F1 %F2] & >GE0 & II)" "HClose".
iDestruct (ExchangerInv_agree with "GE GE0") as %->. iFrame "GE".
iMod ("HClose" with "[GE0 II]") as "_"; [|done].
iNext. iExists G. by iFrame "GE0 II".
Qed.
Lemma ExchangerInv_graph_master_acc_instance :
ExchangerInv_graph_master_acc' ExchangerInv.
Proof.
iIntros "* [I F]".
iDestruct (ExchangerInv_graph_master' with "[$F $I]") as "G".
iExists _. iFrame "G". rewrite -ExchangerInv_graph_master.
iIntros "[_ $]".
Qed.
Lemma ExchangerInv_graph_snap_instance :
ExchangerInv_graph_snap' ExchangerInv.
Proof.
iIntros "* G [G' _]".
by iDestruct (ghost_graph_master_snap_included with "G G'") as %?.
Qed.
Lemma ExchangerLocal_graph_snap_instance :
∀ EI N, ExchangerLocal_graph_snap' (ExchangerLocal EI N).
Proof. by iIntros "* [$ _]". Qed.
Lemma ExchangerLocalLite_graph_snap_instance :
ExchangerLocal_graph_snap' ExchangerLocalLite.
Proof. by iIntros "* [$ _]". Qed.
Lemma ExchangerLocalLite_from_instance :
∀ EI N, ExchangerLocal_from' (ExchangerLocal EI N) ExchangerLocalLite.
Proof.
iIntros "* [$ EL]". iDestruct "EL" as (γt γx) "(ES & MT & II)".
iExists γt, γx. iFrame.
Qed.
Lemma ExchangerLocalLite_to_instance :
∀ EI N, ExchangerLocal_to' (ExchangerLocal EI N) ExchangerLocalLite.
Proof.
iIntros "* [$ EL] [_ EL']". iDestruct "EL" as (γt γx) "[ES #MT]".
iExists γt, γx. iFrame.
iDestruct "EL'" as (γt' γx') "(_ & MT' & II)".
iDestruct (meta_agree with "MT MT'") as %[<- <-]%pair_inj.
by iFrame.
Qed.
Lemma ExchangerLocalLite_upgrade_instance :
ExchangerLocal_upgrade' ExchangerLocalLite ExchangerInv.
Proof.
iIntros "* GM [Gs $]".
iDestruct (ghost_graph_master_snap_included with "GM [Gs]") as %?.
{ by iDestruct "Gs" as "[$ _]". }
iApply (graph_snap_mono _ _ ∅ with "[GM] Gs"); [done|].
(* TODO: lemma *)
iDestruct (ghost_graph_master_snap with "GM") as "$".
by iApply SeenLogview_empty.
Qed.
Lemma ExchangerLocal_upgrade_instance :
∀ EI N, ExchangerLocal_upgrade' (ExchangerLocal EI N) ExchangerInv.
Proof.
iIntros "* EI #EL".
iDestruct (ExchangerLocalLite_from_instance with "EL") as "-#ELL".
iDestruct (ExchangerLocalLite_upgrade_instance with "EI ELL") as "ELL".
iApply (ExchangerLocalLite_to_instance with "ELL EL").
Qed.
Lemma ExchangerLocal_union_instance :
∀ EI, ExchangerLocal_union' (ExchangerLocal EI) ExchangerInv.
Proof.
iIntros "* [EI1 EI2] EL1 EL2".
iDestruct (ExchangerLocal_upgrade_instance with "EI1 EL1") as "[Gs1 EL1']".
iDestruct (ExchangerLocal_upgrade_instance with "EI2 EL2") as "[Gs2 _]".
iDestruct (graph_snap_union with "Gs1 Gs2") as "$". iFrame "EL1'".
Qed.
Lemma new_exchanger_spec :
new_exchanger_piggyback_spec' ExchangerLocal ExchangerInv new_exchanger.
Proof.
iIntros (tid Φ) "_ Post".
wp_lam.
(* allocate x *)
wp_apply wp_new; [done..|].
iIntros (x) "([H†|%] & Hs & Hm & _)"; [|done].
wp_let.
(* initialize x as null, and create protocol *)
rewrite own_loc_na_vec_singleton.
iApply wp_fupd.
wp_write.
iMod (AtomicPtsTo_CON_from_na with "Hs") as (γx t0 V0) "(sV0 & #xN & xA)".
iMod (LTM_master_alloc ∅) as (γt) "LTm".
iMod (LTM_master_fork with "LTm") as "[LTm #LTs]".
iMod graph_master_alloc_empty as (γg) "[[GM1 GM2] Gs]".
iMod (meta_set _ _ (γt, γx) nroot with "Hm") as "#Hm"; [done|].
have EC := ExchangerConsistent_empty.
iApply ("Post" $! γg).
iSplitL "GM2".
- (* ExchangerInv *)
by iDestruct (ExchangerInv_graph_master with "GM2") as "[% $]".
- iIntros "!>" (E EI N).
iMod (inv_alloc (xchgN N) _ (ExchangerInternalInv EI N γt γx γg x)
with "[xA GM1 LTm]") as "#I".
{ iNext. iExists ∅.
iDestruct (ExchangerInv_graph_master with "GM1") as "[% $]". iSplit; [done|].
iExists [(None,V0)], [], ∅. iFrame "LTm".
iDestruct (view_at_intro with "xA") as (Vb) "[InVb xA]".
iExists Vb. iSplitL; last iSplitL.
- iExists _. iFrame "xA".
- by rewrite /main_offers /=.
- by iPureIntro. }
(* ExchangerLocal *)
iDestruct (graph_snap_empty with "Gs") as "$".
iExists γt, γx. rewrite shift_0. iFrame "Hm I". iExists _. by iFrame "xN".
Qed.
Lemma exchange_spec :
exchange_piggyback_spec' ExchangerLocal ExchangerInv exchange.
Proof.
intros EI OBJ N DISJ x tid γg G1 M V v1 Posv1.
iIntros "#sV #(Gs & ES) #EXI" (Φ TA' TB' α' β' Φ') "Pr AU".
iDestruct (bi.persistent_sep_dup with "Pr") as "[#Pr AU']".
iDestruct "ES" as (γt γx) "(ES & MT & EII)".
iDestruct "ES" as (ζx0) "xN".
set E1 := G1.(Es).
(* allocate an offer *)
wp_lam. wp_apply (wp_new with "[//]"); [done..|].
iIntros (m) "([H†|%] & Hm & _)"; [|done].
iDestruct (own_loc_na_vec_cons with "Hm") as "[mL mD]".
rewrite own_loc_na_vec_singleton.
(* write hole as Null *)
wp_let. wp_op. rewrite shift_0. wp_write.
(* write data with v1 *)
wp_op. wp_write.
(* prepare to CAS to make an offer *)
wp_bind (casʳᵉˡ(_, _, _))%E.
(* open invariant *)
iInv "EII" as (G2) "(>%CON2 & GM & EBI)" "Close".
iDestruct "EBI" as (LVs2 os2 T2) "(LTm & Locs)".
iDestruct "Locs" as (Vb) "([%tx0 >xA] & Offs & >[%Eqos2 %EqD2])".
(* Prepare resources that we may release at the right view *)
iCombine "mL mD" as "mLD". iCombine "AU' AU mLD sV Gs xN" as "Hm".
iDestruct (view_at_intro_incl with "Hm sV") as (V1) "(#sV1 & %LeVV1 & AU' & AU & Hm & GE)".
(* prepare for rlx CASes later *)
iMod (rel_objectively_intro (⊒∅) tid with "[]") as "#HRE".
{ iApply objective_objectively. iApply monPred_in_bot. }
(* finally, CAS to make the offer *)
wp_apply (AtomicSeen_CON_CAS_int x γx ζx0 _ _ _ _ 0 #m tid ∅ V1 Vb
with "[$xN $xA $sV1]"); [done..|solve_ndisj| |done|].
{ intros ???. by apply toXChgHist_comparable_0. }
iIntros (b tx1 vx1 Vr2 V2 ζx2' ζx2) "(F & #sV2 & xN2' & xA & CASE)".
iDestruct "F" as %([Subζx0 Subζx2'] & Eqtx1 & _ & LeV1).
iDestruct (view_at_elim with "sV2 xN2'") as "#xN2 {xN2'}".
iDestruct "CASE" as "[[F _]|[F HVw]]".
- (* CAS fails, there may be an offer *)
iDestruct "F" as %(-> & _ & ->).
(* close the invariant *)
iMod ("Close" with "[GM LTm xA Offs]") as "_".
{ iNext. iExists _. iFrame "GM". iSplit; [done|].
iExists _, _, _. iFrame "LTm". iExists (Vb ⊔ V2).
iSplitL "xA". { iExists _; by iFrame "xA". }
iFrame "Offs". by iPureIntro. } clear Vb tx0 Subζx0 Subζx2' Eqtx1.
iIntros "!>". wp_if.
(* Prepare to read if the offer is there *)
wp_bind (!ᵃᶜ _)%E.
(* open invariant *)
iInv "EXI" as "XI" "CloseX".
iInv "EII" as (G3) "(>[%CON3 %EGCs] & GM & EBI)" "Close".
iDestruct "EBI" as (LVs3 os3 T3) "(LTm & Locs)".
iDestruct "Locs" as (Vb) "([%tx0 >xA] & Offs)".
(* read acquire the offer *)
wp_apply (AtomicSeen_acquire_read with "[$xN2 $xA $sV2]"); first solve_ndisj.
iIntros (tx3 vx3 V3' V3 ζx3') "(F & #sV3 & #xN3 & xA)".
iDestruct "F" as %([Subζx23' Subζx3'] & Eqtx3 & _ & LeV2).
apply (lookup_weaken Eqtx3), toXChgHist_lookup_Some' in Subζx3'
as (on & -> & InLVs3).
iDestruct (monPred_in_mono _ V3' with "sV3") as "#sV3'".
{ simpl; clear -LeV2; solve_lat. }
(* make a snapshot *)
iMod (LTM_master_fork with "LTm") as "[LTm #LT3]".
destruct on as [l2|]; last first.
{ (* read Null, the offer is already taken by someone else, fail completely *)
(* CANCEL_CASE 2 : COMMIT with CANCELLED event *)
iDestruct (view_at_elim with "sV1 AU") as "AU".
iMod ("Pr" $! true true with "AU XI") as (G3') "[>GM' HClose]".
iDestruct (ExchangerInv_agree with "GM GM'") as %->.
iDestruct (ExchangerInv_graph_master' with "[$GM //]") as "GM".
iDestruct (ExchangerInv_graph_master' with "[$GM' //]") as "GM'".
iDestruct (graph_master_snap_included with "GM Gs") as %SubG1.
set E3 := G3.(Es).
have SubE1 : E1 ⊑ E3 by apply SubG1.
set V' := V3.
have LeVV' : V ⊑ V'. { clear -LeV1 LeVV1 LeV2. rewrite /V'. by solve_lat. }
have bLeVV' : bool_decide (V ⊑ V') by eapply bool_decide_unpack; eauto.
set Vex1 := mkDView V V' V' bLeVV'.
set ExE := Exchange v1 CANCELLED.
iDestruct (bi.persistent_sep_dup with "Gs") as "[_ [_ PSV]]".
iDestruct (SeenLogview_closed with "PSV") as "%SubD1 {PSV}".
have SubM: set_in_bound M E3.
{ clear - SubD1 SubE1. by eapply set_in_bound_mono. }
assert (GIP:= graph_insert_props_base _ ExE _ Vex1 SubM EGCs).
destruct GIP as [xchgId M' egV' G' LeG' SubM' SUB' InId FRGe1 EGCs'].
have CON' : ExchangerConsistent G' by apply exchange_cancel_graph_insert.
set E' := G'.(Es).
have LeE' : E3 ⊑ E' by apply LeG'.
iCombine "GM GM'" as "GM".
iMod (graph_master_update _ _ _ LeG' EGCs' with "GM") as "[[GM GM'] Gs']".
have LeV1' : V1 ⊑ V'. { clear -LeV1 LeV2. rewrite /V'. solve_lat. }
iAssert (@{V'} SeenLogview E' M')%I with "[GE]" as "#SL".
{ iDestruct "GE" as "(_ & [_ SL] & _)".
rewrite -SeenLogview_insert'. iSplitL; [|done].
erewrite SeenLogview_map_mono; [iFrame "SL"|done..]. }
iAssert (@{V'} graph_snap γg G' M')%I as "#Gss'". { iFrame "Gs' SL". }
rewrite bi.and_elim_r.
iMod ("HClose" $! V' G' xchgId xchgId CANCELLED Vex1 Vex1 M'
with "[GM' Gs' $sV3]") as "[HΦ XI]".
{ (* Public Post *)
iDestruct (ExchangerInv_graph_master with "GM'") as "[_ $]".
iSplitR; [by iPureIntro|]. iLeft. iSplitR; [by iPureIntro|].
(* ExchangerLocal *)
iFrame "Gss'". iExists _, _. iFrame "MT EII". iExists _; by iFrame "xN3". }
(* close invariant *)
iMod ("Close" with "[GM LTm Offs xA]") as "_".
{ iNext. iExists G'. iSplit; [done|].
iDestruct (ExchangerInv_graph_master with "GM") as "[_ $]".
iExists _, _, _. iFrame "LTm". iExists (Vb ⊔ V3).
iSplitL "xA". - iExists _; iFrame "xA". - by iFrame "Offs". } clear Vb tx0.