-
Notifications
You must be signed in to change notification settings - Fork 0
/
append_only_loc.v
2383 lines (2177 loc) · 130 KB
/
append_only_loc.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 gpfsl.examples Require Import sflib.
From iris.algebra Require Import auth gset gmap agree.
From iris.algebra Require Import lib.mono_list.
From iris.proofmode Require Import tactics.
From iris.bi Require Import fractional.
From gpfsl.base_logic Require Import meta_data.
From gpfsl.examples.algebra Require Import mono_list mono_list_list.
From gpfsl.logic Require Import logatom atomics invariants.
From gpfsl.logic Require Import repeat_loop new_delete.
From gpfsl.examples Require Import map_seq loc_helper.
From stdpp Require Import namespaces.
From gpfsl.logic Require Import logatom.
From gpfsl.examples.omo Require Import omo omo_event omo_history omo_preds.
Require Import iris.prelude.options.
(* Append-only location: an abstraction of shared location with an invariant that new written messages are written at the latest timestamp *)
(** Definition of state transition system of append-only location **)
(* Note that it is very simple; precise semantics for memory accesses are described at the conclusion of each memory access rule *)
Notation loc_state := (event_id * (val * view))%type.
Inductive loc_event := ReadE (msg : (val * view)) | WriteE (msg : (val * view)) | UpdateE (e : event_id) (msg : (val * view)).
Definition loc_event_msg (ev : loc_event) :=
match ev with
| ReadE msg => msg
| WriteE msg => msg
| UpdateE e msg => msg
end.
Definition UpdateE_eid (ev : loc_event) :=
match ev with
| UpdateE e msg => Some e
| _ => None
end.
Global Instance loc_event_Inhabited : Inhabited loc_event := populate (WriteE (#0, ∅)).
Inductive loc_step : ∀ (e : event_id) (eV : omo_event loc_event) (st st' : loc_state), Prop :=
| loc_step_WriteE e eV msg st
(WRITE : eV.(type) = WriteE msg)
(LVIEW : e ∈ eV.(eview))
: loc_step e eV st (e, msg)
| loc_step_ReadE e eV st
(READ : eV.(type) = ReadE st.2)
(LVIEW : e ∈ eV.(eview))
: loc_step e eV st st
| loc_step_UpdateE e eV msg st
(UPDATE : eV.(type) = UpdateE st.1 msg)
(LVIEW : e ∈ eV.(eview))
: loc_step e eV st (e, msg)
.
Global Instance loc_interpretable : Interpretable loc_event loc_state :=
{
init := (0%nat, (#☠, ∅));
step := loc_step
}.
(** Ghost construction of append-only-location **)
(* Note that it does not involve `omoGeneralG`. It should be assumed in addition to `appendOnlyLocG` *)
Class appendOnlyLocG Σ := AppendOnlyLocG {
omo_predsG :> omoSpecificG Σ loc_event loc_state;
loc_writesG :> mono_listG event_id Σ;
mono_MLG :> mono_listG (time * val * view) Σ;
}.
Definition appendOnlyLocΣ : gFunctors := #[omoSpecificΣ loc_event loc_state; mono_listΣ event_id; mono_listΣ (time * val * view)].
Global Instance subG_appendOnlyLocΣ {Σ} : subG appendOnlyLocΣ Σ → appendOnlyLocG Σ.
Proof. solve_inG. Qed.
Section append_only_loc.
Context {Σ : gFunctors} `{!noprolG Σ, !atomicG Σ, !omoGeneralG Σ, !appendOnlyLocG Σ}.
Notation history := (history loc_event).
Notation iProp := (iProp Σ).
Notation vProp := (vProp Σ).
Implicit Types
(γe γx γl γw γm : gname)
(q : Qp)
(l : loc)
(ML : list (time * val * view))
(ζ : absHist)
(t : time)
(eV : omo_event loc_event)
(mo : list loc_state)
(es : list event_id)
(E : history)
(omo : omoT)
(M : eView)
(uf : gset val)
(eidx : event_idx).
Local Open Scope nat_scope.
(** There are two modes of append-only location:
1. cas_only: concurrent load, concurrent cas are allowed. store is disallowed.
2. swriter (single writer): store by a unique thread is additionally allowed. *)
Inductive append_only_type := cas_only | swriter.
Global Instance append_only_type_inhabited : Inhabited append_only_type := populate cas_only.
Global Instance append_only_type_eq_dec : EqDecision append_only_type.
Proof. solve_decision. Qed.
(* Exclusive permission to perform single-writer store *)
Definition swriter_token_def l γe es : vProp :=
∃ γx γl γw γm ML t v V,
⌜ γx = encode (γl,γw,γm) ∧ last ML = Some (t, v, V) ⌝ ∗
OmoGname γe γx ∗
⎡mono_list_auth_own γw (1/2 + 1/2/2)%Qp es⎤ ∗
⎡mono_list_auth_own γm (1/2 + 1/2/2)%Qp ML⎤ ∗
l sn⊒{γl} {[t := (v, V)]}.
Definition swriter_token_aux : seal (@swriter_token_def). Proof. by eexists. Qed.
Definition swriter_token := unseal (@swriter_token_aux).
Definition swriter_token_eq : @swriter_token = _ := seal_eq _.
(* ---- Definitions used internally by `append_only_loc` ---- *)
Definition ML_time_mono ML : Prop :=
∀ (i1 i2 : nat) (t1 t2 : time),
ML.*1.*1 !! i1 = Some t1 → ML.*1.*1 !! i2 = Some t2 → (i1 < i2)%nat → (t1 < t2)%positive.
Definition Hist_comparable ζ : Prop :=
∀ t v V, ζ !! t = Some (v, V) → ∃ vl : lit, v = #vl ∧ vl ≠ LitPoison.
Definition Hist_ML_valid ζ ML : Prop :=
∀ (t : time) (v : val) (V : view), ζ !! t = Some (v, V) ↔ (t, v, V) ∈ ML.
Definition uf_valid ζ uf : Prop :=
∀ t v V, ζ !! t = Some (v, V) → ζ !! (t + 1)%positive = None → v ∈ uf ∨ no_earlier_time ζ t.
Definition OMO_ML_valid γe γl γs l omo ML : vProp :=
[∗ list] ees; minfo ∈ omo; ML,
∃ e es eV t v V,
⌜ ees = (e, es) ∧ loc_event_msg eV.(type) = (v, V) ∧ minfo = (t, v, V) ⌝ ∗
OmoEinfo γe e eV ∗ OmoSnap γe γs e (e, (v, V)) ∗
@{eV.(sync)} l sn⊒{γl} {[t := (v, V)]} ∗
[∗ list] e' ∈ es,
∃ eV',
⌜ loc_event_msg eV'.(type) = (v, V) ⌝ ∗
OmoEinfo γe e' eV' ∗ OmoSnap γe γs e' (e, (v, V)) ∗
@{eV'.(sync)} l sn⊒{γl} {[t := (v, V)]}.
(* Main definition of `append_only_loc` *)
Definition append_only_loc_def l γe uf (ty : append_only_type) : vProp :=
∃ γx γl γw γm γs E omo mo q ML ζ,
⌜ γx = encode (γl,γw,γm) ⌝ ∗
OmoGname γe γx ∗
OmoAuth γe γs (1/2)%Qp E omo mo _ ∗
⎡mono_list_auth_own γw q (omo_write_op omo)⎤ ∗
⎡mono_list_auth_own γm q ML⎤ ∗
l at↦{γl} ζ ∗
OMO_ML_valid γe γl γs l omo ML ∗
⌜ ML_time_mono ML
∧ Hist_comparable ζ
∧ Hist_ML_valid ζ ML
∧ uf_valid ζ uf
∧ match ty with
| cas_only => q = 1%Qp
| swriter => q = (1/2/2)%Qp
end ⌝.
Definition append_only_loc_aux : seal (@append_only_loc_def). Proof. by eexists. Qed.
Definition append_only_loc := unseal (@append_only_loc_aux).
Definition append_only_loc_eq : @append_only_loc = _ := seal_eq _.
Global Instance swriter_timeless l γe es : Timeless (swriter_token l γe es).
Proof. rewrite swriter_token_eq. apply _. Qed.
Global Instance append_only_loc_timeless l γe uf ty : Timeless (append_only_loc l γe uf ty).
Proof. rewrite append_only_loc_eq. apply _. Qed.
Lemma swriter_token_exclusive_obj l γe V1 V2 es1 es2 :
@{V1} swriter_token l γe es1 -∗ @{V2} swriter_token l γe es2 -∗ False.
Proof.
iIntros "SW1 SW2". rewrite !swriter_token_eq.
iDestruct "SW1" as (????????) "([%Hγx %LAST] & #Hγx & ES● & _)".
iDestruct "SW2" as (????????) "([%Hγx' %LAST'] & #Hγx' & ES●' & _)".
rewrite !view_at_objective_iff.
iDestruct (OmoGname_agree with "Hγx Hγx'") as %<-. encode_agree Hγx.
iDestruct (mono_list_auth_own_agree with "ES● ES●'") as %[LE <-].
replace (1/2 + 1/2/2 + (1/2 + 1/2/2))%Qp with (1 + 1/2)%Qp in LE; [|compute_done].
exfalso.
rewrite Qp.le_ngt in LE.
specialize (Qp.lt_add_r 1 (1/2)%Qp). done.
Qed.
Lemma swriter_token_exclusive l γe es1 es2 :
swriter_token l γe es1 -∗ swriter_token l γe es2 -∗ False.
Proof.
iIntros "SW1 SW2".
iDestruct (view_at_intro with "SW1") as (?) "[_ SW1]".
iDestruct (view_at_intro with "SW2") as (?) "[_ SW2]".
iApply (swriter_token_exclusive_obj with "SW1 SW2").
Qed.
Lemma swriter_token_type_obj_1 l γe V1 V2 es uf ty :
@{V1} swriter_token l γe es -∗ @{V2} append_only_loc l γe uf ty -∗ ⌜ ty = swriter ⌝.
Proof.
iIntros "SW omo↦". rewrite swriter_token_eq append_only_loc_eq.
iDestruct "SW" as (????????) "([%Hγx %LASTes] & #Hγx & ES● & ML● & #l⊒)".
iDestruct "omo↦" as (??????????) "(%& %Hγx' & #Hγx' & M● & ES●' & ML●' & l↦ & #ML✓ & (%ML_t_valid & %ζ_comp & %ζ_ML_valid & %ζ_uf_valid & %Hty))".
destruct ty; try done. subst q.
rewrite !view_at_objective_iff.
iDestruct (OmoGname_agree with "Hγx Hγx'") as %<-. encode_agree Hγx.
iDestruct (mono_list_auth_own_agree with "ES● ES●'") as %[LE ->].
rewrite Qp.le_ngt in LE.
specialize (Qp.lt_add_r 1 (1/2 + 1/2/2)%Qp). done.
Qed.
Lemma swriter_token_type_obj_2 l γe V es uf ty :
swriter_token l γe es -∗ @{V} append_only_loc l γe uf ty -∗ ⌜ ty = swriter ⌝.
Proof.
iIntros "SW omo↦". iDestruct (view_at_intro with "SW") as (?) "[_ SW]".
iApply (swriter_token_type_obj_1 with "SW omo↦").
Qed.
Lemma swriter_token_type l γe es uf ty :
swriter_token l γe es -∗ append_only_loc l γe uf ty -∗ ⌜ ty = swriter ⌝.
Proof.
iIntros "SW omo↦".
iDestruct (view_at_intro with "SW") as (?) "[_ SW]".
iDestruct (view_at_intro with "omo↦") as (?) "[_ omo↦]".
iApply (swriter_token_type_obj_1 with "SW omo↦").
Qed.
Lemma OmoAuth_swriter_token_agree_obj_1 l γe γs V1 V2 uf ty q E omo mo es :
OmoAuth γe γs q E omo mo _ -∗
@{V1} append_only_loc l γe uf ty -∗
@{V2} swriter_token l γe es -∗
⌜ es = omo_write_op omo ⌝.
Proof.
iIntros "M● omo↦ SW". rewrite swriter_token_eq append_only_loc_eq.
iDestruct "SW" as (????????) "([%Hγx %LASTes] & #Hγx & ES● & ML● & #⊒e)".
iDestruct "omo↦" as (??????????) "(%& %Hγx' & #Hγx' & M●' & ES●' & ML●' & l↦ & #ML✓ & (%ML_t_valid & %ζ_comp & %ζ_ML_valid & %ζ_uf_valid & %Hty))".
rewrite !view_at_objective_iff.
iDestruct (OmoGname_agree with "Hγx Hγx'") as %<-. encode_agree Hγx.
iDestruct (OmoAuth_agree with "M● M●'") as %(<- & <- & <- & <-).
by iDestruct (mono_list_auth_own_agree with "ES● ES●'") as %[_ ->].
Qed.
Lemma OmoAuth_swriter_token_agree_obj_2 l γe γs V uf ty q E omo mo es :
OmoAuth γe γs q E omo mo _ -∗
@{V} append_only_loc l γe uf ty -∗
swriter_token l γe es -∗
⌜ es = omo_write_op omo ⌝.
Proof.
iIntros "M● omo↦ SW". iDestruct (view_at_intro with "SW") as (?) "[_ SW]".
iApply (OmoAuth_swriter_token_agree_obj_1 with "M● omo↦ SW").
Qed.
Lemma OmoAuth_swriter_token_agree l γe γs uf ty q E omo mo es :
OmoAuth γe γs q E omo mo _ -∗
append_only_loc l γe uf ty -∗
swriter_token l γe es -∗
⌜ es = omo_write_op omo ⌝.
Proof.
iIntros "M● omo↦ SW".
iDestruct (view_at_intro with "omo↦") as (?) "[_ omo↦]".
iDestruct (view_at_intro with "SW") as (?) "[_ SW]".
iApply (OmoAuth_swriter_token_agree_obj_1 with "M● omo↦ SW").
Qed.
Lemma OmoAuth_append_only_loc_frac_valid_obj γe γs q E omo mo V l uf ty :
OmoAuth γe γs q E omo mo _ -∗
@{V} append_only_loc l γe uf ty -∗
⌜ (q ≤ 1/2)%Qp ⌝.
Proof.
iIntros "M● omo↦". rewrite append_only_loc_eq.
iDestruct "omo↦" as (??????????)
"(%& %Hγx' & #Hγx' & M●' & ES●' & ML●' & l↦ & #ML✓ & (%ML_t_valid & %ζ_comp & %ζ_ML_valid & %ζ_uf_valid & %Hty))".
rewrite !view_at_objective_iff.
iDestruct (OmoAuth_agree with "M● M●'") as %(<- & <- & <- & <-).
iCombine "M● M●'" as "M●".
iDestruct (OmoAuth_frac_valid with "M●") as %LE.
by rewrite -{2}Qp.half_half -Qp.add_le_mono_r in LE.
Qed.
Lemma OmoAuth_append_only_loc_frac_valid γe γs q E omo mo l uf ty :
OmoAuth γe γs q E omo mo _ -∗
append_only_loc l γe uf ty -∗
⌜ (q ≤ 1/2)%Qp ⌝.
Proof.
iIntros "M● omo↦".
iDestruct (view_at_intro with "omo↦") as (?) "[_ omo↦]".
iApply (OmoAuth_append_only_loc_frac_valid_obj with "M● omo↦").
Qed.
Lemma swriter_to_cas_only_obj_1 l γe V0 V1 es uf :
@{V0} append_only_loc l γe uf swriter -∗ @{V1} swriter_token l γe es -∗ @{V0} append_only_loc l γe uf cas_only.
Proof.
iIntros "omo↦ SW". rewrite !append_only_loc_eq swriter_token_eq.
iDestruct "SW" as (????????) "([%Hγx %LASTes] & #Hγx & ES● & ML● & #⊒e)".
iDestruct "omo↦" as (??????????) "(%& %Hγx' & #Hγx' & M●' & ES●' & ML●' & l↦ & #ML✓ & (%ML_t_valid & %ζ_comp & %ζ_ML_valid & %ζ_uf_valid & %Hty))".
rewrite !view_at_objective_iff. subst q.
iDestruct (OmoGname_agree with "Hγx Hγx'") as %<-. encode_agree Hγx.
iDestruct (mono_list_auth_own_agree with "ES● ES●'") as %[_ ->].
iDestruct (mono_list_auth_own_agree with "ML● ML●'") as %[_ <-].
iCombine "ES● ES●'" as "ES●". iCombine "ML● ML●'" as "ML●".
replace (1/2 + 1/2/2 + 1/2/2)%Qp with 1%Qp by compute_done.
iExists γx,γl,γw,γm,γs,E,omo,mo. iExists 1%Qp,ML,ζ. iFrame "∗#%". done.
Qed.
Lemma swriter_to_cas_only_obj_2 l γe V es uf :
@{V} append_only_loc l γe uf swriter -∗ swriter_token l γe es -∗ @{V} append_only_loc l γe uf cas_only.
Proof.
iIntros "omo↦ SW". iDestruct (view_at_intro with "SW") as (?) "[_ SW]".
iApply (swriter_to_cas_only_obj_1 with "omo↦ SW").
Qed.
Lemma swriter_to_cas_only l γe es uf :
append_only_loc l γe uf swriter -∗ swriter_token l γe es -∗ append_only_loc l γe uf cas_only.
Proof.
iIntros "omo↦ SW". iCombine "omo↦ SW" as "RES".
iDestruct (view_at_intro with "RES") as (V) "[#⊒V [omo↦ SW]]".
iDestruct (swriter_to_cas_only_obj_1 with "omo↦ SW") as "omo↦".
iDestruct (view_at_elim with "⊒V omo↦") as "omo↦". done.
Qed.
Lemma cas_only_to_swriter_obj l γe γs q mo E omo M e eidx V uf :
e ∈ M →
lookup_omo omo eidx = Some e →
gen_of eidx = (length omo - 1)%nat →
OmoAuth γe γs q E omo mo _ -∗
OmoEview γe M -∗
@{V} append_only_loc l γe uf cas_only -∗
OmoAuth γe γs q E omo mo _ ∗
@{V} append_only_loc l γe uf swriter ∗
swriter_token l γe (omo_write_op omo).
Proof.
iIntros "%IN %Heidx %EQgen M● #⊒M omo↦".
iDestruct (OmoAuth_wf with "M●") as %[OMO_GOOD _].
iDestruct (OmoAuth_omo_nonempty with "M●") as %Nomo.
have NZomo : length omo ≠ 0 by destruct omo.
have [[e' es'] Hlast] : is_Some (omo !! (length omo - 1)) by rewrite lookup_lt_is_Some; lia.
have He' : lookup_omo omo (wr_event (length omo - 1)) = Some e' by rewrite lookup_omo_wr_event /omo_write_op list_lookup_fmap Hlast.
eapply lookup_omo_event_valid in Heidx as HeV; [|done]. destruct HeV as [eV HeV].
iDestruct (OmoEinfo_get with "M●") as "#e✓eV"; [done|].
iDestruct (OmoEq_get with "M●") as "#e=e'".
{ exact Heidx. } { exact He'. } { done. }
rewrite append_only_loc_eq.
iDestruct "omo↦" as (??????????) "(%& %Hγx & #Hγx & M●' & ES● & ML● & l↦ & #ML✓ & (%ML_t_valid & %ζ_comp & %ζ_ML_valid & %ζ_uf_valid & %Hty))".
subst q0. rewrite !view_at_objective_iff.
iDestruct (OmoAuth_agree with "M● M●'") as %(<- & <- & <- & <-).
iDestruct "ES●" as "[ES●1 [ES●2 ES●3]]". iCombine "ES●1 ES●3" as "ES●1".
iDestruct "ML●" as "[ML●1 [ML●2 ML●3]]". iCombine "ML●1 ML●3" as "ML●1".
iDestruct (big_sepL2_length with "ML✓") as %EQlenML.
have [minfo Hminfo] : is_Some (ML !! (length omo - 1)) by rewrite lookup_lt_is_Some -EQlenML; lia.
iDestruct (big_sepL2_lookup with "ML✓") as (?? eV' ?? V') "((%EQ1 & %eV'EV & %EQ2) & e'✓eV' & _ & l⊒@SYNC & BIG)"; [done|done|].
inversion EQ1. subst e0 es minfo. clear EQ1.
iAssert (l sn⊒{γl} {[t := (v, V')]})%I with "[-]" as "#l⊒".
{ destruct eidx.
- simpl in EQgen. subst gen. rewrite lookup_omo_ro_event /omo_read_op list_lookup_fmap Hlast /= in Heidx.
iDestruct (big_sepL_lookup with "BIG") as (?) "(%eVEV & #e✓eV' & _ & l⊒@SYNC')"; [done|].
iDestruct (OmoEinfo_agree with "e✓eV e✓eV'") as %<-.
iDestruct (OmoEinfo_OmoEview with "e✓eV ⊒M") as "#⊒SYNC"; [done|].
iDestruct (view_at_elim with "⊒SYNC l⊒@SYNC'") as "?". done.
- simpl in EQgen. subst gen. rewrite lookup_omo_wr_event /omo_write_op list_lookup_fmap Hlast /= in Heidx.
inversion Heidx. subst e'.
iDestruct (OmoEinfo_agree with "e✓eV e'✓eV'") as %<-.
iDestruct (OmoEinfo_OmoEview with "e✓eV ⊒M") as "#⊒SYNC"; [done|].
iDestruct (view_at_elim with "⊒SYNC l⊒@SYNC") as "?". done. }
iFrame "M●". iSplitR "ES●1 ML●1".
- iExists γx,γl,γw,γm,γs,E,omo,mo. iExists (1/2/2)%Qp,ML,ζ. iFrame "∗#%". done.
- rewrite swriter_token_eq. iExists γx,γl,γw,γm,ML,t,v,V'. iFrame "∗#". iPureIntro. split; try done.
rewrite last_lookup -EQlenML. replace (Init.Nat.pred (length omo)) with (length omo - 1) by lia. done.
Qed.
Lemma cas_only_to_swriter l γe γs q mo E omo uf :
OmoAuth γe γs q E omo mo _ -∗
append_only_loc l γe uf cas_only -∗
OmoAuth γe γs q E omo mo _ ∗
append_only_loc l γe uf swriter ∗
swriter_token l γe (omo_write_op omo).
Proof.
iIntros "M● omo↦". rewrite append_only_loc_eq.
iDestruct (OmoAuth_wf with "M●") as %[OMO_GOOD _].
iDestruct (OmoAuth_omo_nonempty with "M●") as %Nomo.
have NZomo : length omo ≠ 0 by destruct omo.
have [[e es] Hlast] : is_Some (omo !! (length omo - 1)) by rewrite lookup_lt_is_Some; lia.
have He : lookup_omo omo (wr_event (length omo - 1)) = Some e by rewrite lookup_omo_wr_event /omo_write_op list_lookup_fmap Hlast.
eapply lookup_omo_event_valid in He as HeV; [|done]. destruct HeV as [eV HeV].
iDestruct (OmoEinfo_get with "M●") as "#e✓eV"; [done|].
iDestruct (OmoEq_get with "M●") as "#e=e"; try done.
iDestruct "omo↦" as (??????????) "(%& %Hγx & #Hγx & M●' & ES● & ML● & l↦ & #ML✓ & (%ML_t_valid & %ζ_comp & %ζ_ML_valid & %ζ_uf_valid & %Hty))".
subst q0.
iDestruct (OmoAuth_agree with "M● M●'") as %(<- & <- & <- & <-).
iDestruct "ES●" as "[ES●1 [ES●2 ES●3]]". iCombine "ES●1 ES●3" as "ES●1".
iDestruct "ML●" as "[ML●1 [ML●2 ML●3]]". iCombine "ML●1 ML●3" as "ML●1".
iDestruct (AtomicPtsTo_AtomicSync with "l↦") as "#SY".
iDestruct (AtomicSync_AtomicSeen with "SY") as "l⊒".
iDestruct (big_sepL2_length with "ML✓") as %EQlenML.
have [[[t v] V] MLlast] : is_Some (last ML).
{ rewrite last_is_Some. unfold not. intros. subst ML. by destruct omo. }
iFrame "M●". iSplitR "ES●1 ML●1".
- iExists γx,γl,γw,γm,γs,E,omo,mo. iExists (1/2/2)%Qp,ML,ζ. iFrame "∗#%". done.
- rewrite swriter_token_eq. iExists γx,γl,γw,γm,ML,t,v,V. iFrame "∗#". iSplitR; [done|].
iApply AtomicSeen_mono_lookup_singleton; try done.
unfold Hist_ML_valid in *. specialize (ζ_ML_valid t v V). rewrite ζ_ML_valid elem_of_list_lookup.
rewrite last_lookup in MLlast. eexists. done.
Qed.
Lemma append_only_loc_swriter_from_na_rel l (vl : lit) (P : vProp) :
vl ≠ LitPoison →
P -∗ l ↦ #vl -∗
|==> ∃ γe γs V eV (omo := omo_append_w [] 0%nat []),
⊒V ∗
OmoAuth γe γs (1/2)%Qp [eV] omo [(0%nat, (#vl, V))] _ ∗
@{V} (OmoEview γe {[0%nat]} ∗ P ∗ swriter_token l γe (omo_write_op omo)) ∗
append_only_loc l γe ∅ swriter ∗
OmoTokenW γe 0%nat ∗
OmoEinfo γe 0%nat eV ∗
⌜ eV.(type) = WriteE (#vl, V) ∧ eV.(sync) = V ⌝.
Proof.
iIntros "%NPoison P l↦".
iMod (AtomicPtsToX_from_na_cofinite_rel_view _ _ ∅ with "P l↦") as (γl t V) "(_ & #⊒V & P@V & lsw & l↦)".
iAssert (@{V} l sw↦{γl} {[t := (#vl, V)]})%I with "[l↦]" as "l↦".
{ rewrite AtomicPtsTo_eq. iExists t. done. }
iAssert (@{V} (l at↦{γl} {[t := (#vl, V)]} ∗ l sn⊒{γl} {[t := (#vl, V)]}))%I with "[l↦ lsw]" as "[l↦ #l⊒]".
{ iCombine "l↦ lsw" as "RES". iApply (view_at_mono with "RES"); [done|]. iIntros "[l↦ lsw]".
iDestruct (AtomicPtsTo_SW_to_CON_1 with "l↦ lsw") as "[l↦ sync]".
rewrite AtomicSync_AtomicSeen. iFrame. }
iDestruct (view_at_elim with "⊒V l↦") as "l↦".
set einit := 0.
set M := {[einit]}.
set eVinit := mkOmoEvent (WriteE (#vl, V)) V M.
set stinit := (einit, (#vl, V)).
set ML := [(t, #vl, V)].
iMod (@mono_list_own_alloc event_id _ _ [einit]) as (γw) "[ES● #ES◯]".
iMod (mono_list_own_alloc ML) as (γm) "[ML● #ML◯]".
remember (encode (γl,γw,γm)) as γx eqn:Hγx.
iMod (OmoAuth_alloc_Gname_no_Token eVinit stinit γx) as (γe γs) "(M● & #⊒M & #einit✓eVinit & #einit↪stinit & #Hγx & WCOMMIT)".
{ by apply loc_step_WriteE. } { done. }
iDestruct (OmoHbToken_finish with "M●") as "[M● M●']".
iModIntro. iExists γe,γs,V,eVinit. iFrame "⊒V M● P@V ⊒M WCOMMIT einit✓eVinit".
iDestruct "ES●" as "[ES●1 [ES●2 ES●3]]". iDestruct "ML●" as "[ML●1 [ML●2 ML●3]]".
iCombine "ES●1 ES●3" as "ES●1". iCombine "ML●1 ML●3" as "ML●1".
iSplitL "ES●1 ML●1"; last iSplitL; try done.
- rewrite swriter_token_eq. iExists γx,γl,γw,γm,ML,t,#vl,V. iFrame "∗#%". done.
- rewrite append_only_loc_eq. iExists γx,γl,γw,γm,γs,_,_,_. iExists _,[(t,#vl,V)],_. iFrame "∗#%". iSplit.
+ rewrite /OMO_ML_valid big_sepL2_singleton. iExists einit,[],eVinit,t,#vl,V. iFrame "#". rewrite big_sepL_nil. done.
+ iPureIntro. split_and!; try done.
* rewrite /ML_time_mono. intros. rewrite !list_lookup_fmap in H,H0. destruct i1, i2; try done. lia.
* rewrite /Hist_comparable. intros. rewrite lookup_singleton_Some in H. destruct H as [<- EQ].
inversion EQ. subst v V0. exists vl. done.
* rewrite /Hist_ML_valid. intros. split; intros.
-- rewrite lookup_singleton_Some in H. destruct H as [<- EQ]. inversion EQ. subst v V0.
rewrite elem_of_list_lookup. exists 0. done.
-- rewrite elem_of_list_lookup in H. destruct H as [i Hi]. destruct i; try done. inversion Hi. subst t0 v V0.
rewrite lookup_singleton_Some. done.
* rewrite /uf_valid. intros. rewrite lookup_singleton_Some in H. destruct H as [<- EQ]. inversion EQ. subst v V0. clear EQ.
right. rewrite /no_earlier_time. intros. destruct H as [[v' V'] Ht'].
rewrite lookup_singleton_Some in Ht'. destruct Ht' as [<- EQ]. inversion EQ. subst v' V'. clear EQ. done.
Qed.
Lemma append_only_loc_swriter_from_na l (vl : lit) :
vl ≠ LitPoison →
l ↦ #vl -∗
|==> ∃ γe γs V eV (omo := omo_append_w [] 0%nat []),
⊒V ∗
OmoAuth γe γs (1/2)%Qp [eV] omo [(0%nat, (#vl, V))] _ ∗
@{V} (OmoEview γe {[0%nat]} ∗ swriter_token l γe (omo_write_op omo)) ∗
append_only_loc l γe ∅ swriter ∗
OmoTokenW γe 0%nat ∗
OmoEinfo γe 0%nat eV ∗
⌜ eV.(type) = WriteE (#vl, V) ∧ eV.(sync) = V ⌝.
Proof.
iIntros "%NPoison l↦".
iMod (append_only_loc_swriter_from_na_rel _ _ emp with "[] l↦") as (????) "(H1 & H2 & (H3 & _ & H4) & H5)"; try done.
iModIntro. repeat iExists _. iFrame.
Qed.
Lemma append_only_loc_cas_only_from_na_rel l (vl : lit) (P : vProp) :
vl ≠ LitPoison →
P -∗ l ↦ #vl -∗
|==> ∃ γe γs V eV (omo := omo_append_w [] 0%nat []),
⊒V ∗
OmoAuth γe γs (1/2)%Qp [eV] omo [(0%nat, (#vl, V))] _ ∗
@{V} (OmoEview γe {[0%nat]} ∗ P) ∗
append_only_loc l γe ∅ cas_only ∗
OmoTokenW γe 0%nat ∗
OmoEinfo γe 0%nat eV ∗
⌜ eV.(type) = WriteE (#vl, V) ∧ eV.(sync) = V ⌝.
Proof.
iIntros "%NPoison P l↦".
iMod (append_only_loc_swriter_from_na_rel with "P l↦") as (????) "(#⊒V & M● & (#⊒M & P@V & SW) & omo↦ & WCOMMIT & #elem & Pures)"; [done|].
iDestruct (view_at_elim with "⊒V SW") as "SW".
iDestruct (swriter_to_cas_only with "omo↦ SW") as "omo↦".
iModIntro. iExists γe,γs,V,eV. iFrame "∗#%".
Qed.
Lemma append_only_loc_cas_only_from_na l (vl : lit) :
vl ≠ LitPoison →
l ↦ #vl -∗
|==> ∃ γe γs V eV (omo := omo_append_w [] 0%nat []),
⊒V ∗
OmoAuth γe γs (1/2)%Qp [eV] omo [(0%nat, (#vl, V))] _ ∗
@{V} OmoEview γe {[0%nat]} ∗
append_only_loc l γe ∅ cas_only ∗
OmoTokenW γe 0%nat ∗
OmoEinfo γe 0%nat eV ∗
⌜ eV.(type) = WriteE (#vl, V) ∧ eV.(sync) = V ⌝.
Proof.
iIntros "%NPoison l↦".
iMod (append_only_loc_cas_only_from_na_rel _ _ emp with "[] l↦") as (????) "(H1 & H2 & [H3 _] & H4)"; try done.
iModIntro. repeat iExists _. iFrame.
Qed.
Lemma append_only_loc_to_na Ec l γe γs q E omo mo uf ty :
↑histN ⊆ Ec →
⎡ hist_inv ⎤ -∗ OmoAuth γe γs q E omo mo _ -∗ append_only_loc l γe uf ty ={Ec}=∗
∃ v e eV, l ↦ v ∗ OmoAuth γe γs (q + 1/2)%Qp E omo mo _ ∗ OmoEinfo γe e eV ∗
⌜ last (omo_write_op omo) = Some e ∧ (loc_event_msg eV.(type)).1 = v ⌝.
Proof.
iIntros "%INCL #HInv M● omo↦". rewrite append_only_loc_eq.
iDestruct "omo↦" as (??????????) "(%& %Hγx & #Hγx & M●' & ES● & ML● & l↦ & #ML✓ & (%ML_t_valid & %ζ_comp & %ζ_ML_valid & %ζ_uf_valid & %Hty))".
iDestruct (OmoAuth_agree with "M● M●'") as %(<- & <- & <- & <-).
iCombine "M● M●'" as "M●".
iMod (AtomicPtsTo_to_na with "HInv l↦") as (t v) "[l↦ [%VAL %LATEST]]"; [done|].
iDestruct (OmoAuth_wf with "M●") as %[OMO_GOOD _].
iDestruct (OmoAuth_omo_nonempty with "M●") as %Nomo.
have NZomo : length omo ≠ 0 by destruct omo.
iDestruct (big_sepL2_length with "ML✓") as %EQlenML.
have [[[t' v'] V'] Hlast] : is_Some (last ML).
{ rewrite last_is_Some. unfold not. intros. subst ML. done. }
unfold Hist_ML_valid in *.
have Ht' : (t', v', V') ∈ ML.
{ rewrite elem_of_list_lookup. rewrite last_lookup in Hlast. eexists. done. }
rewrite -ζ_ML_valid in Ht'.
have EQ : t = t'.
{ have CASE : (t < t' ∨ t = t' ∨ t' < t)%positive by lia.
destruct CASE as [COMP|[COMP|COMP]]; try done.
- unfold no_earlier_time in *.
have Ht'' : is_Some (ζ !! t') by done.
specialize (LATEST t' Ht'').
have COMP' : (t' ≤ t)%positive by done.
lia.
- destruct (ζ !! t) eqn:Heq; try done. destruct p as [v'' V]. inversion VAL. subst v''. clear VAL.
rewrite ζ_ML_valid elem_of_list_lookup in Heq. destruct Heq as [i Hi].
rewrite last_lookup in Hlast.
replace (Init.Nat.pred (length ML)) with (length ML - 1) in Hlast by lia.
unfold ML_time_mono in *.
have CONDLT : i < length ML - 1.
{ have LE : i ≤ length ML - 1 by apply lookup_lt_Some in Hi; lia.
destruct (decide (i = length ML - 1)) as [->|NEQ]; try lia.
rewrite Hi in Hlast. inversion Hlast. subst t' v' V'. lia. }
have COND1 : ML.*1.*1 !! i = Some t by rewrite !list_lookup_fmap Hi.
have COND2 : ML.*1.*1 !! (length ML - 1) = Some t' by rewrite !list_lookup_fmap Hlast.
specialize (ML_t_valid _ _ _ _ COND1 COND2 CONDLT). lia. }
subst t'.
rewrite Ht' in VAL. inversion VAL. subst v'. clear VAL.
have [[e es] He] : is_Some (last omo) by rewrite last_is_Some.
rewrite !last_lookup in Hlast,He. rewrite -EQlenML in Hlast.
iDestruct (big_sepL2_lookup with "ML✓") as (??????) "((%EQ1 & %eVEV & %EQ2) & #e✓eV & _)"; [done|done|].
inversion EQ1. inversion EQ2. subst e0 es0 t0 v0 V'. clear EQ1 EQ2.
iModIntro. iExists v,e,eV. iFrame "∗#%". iPureIntro. split.
- rewrite last_lookup -omo_write_op_length /omo_write_op list_lookup_fmap He. done.
- rewrite eVEV. done.
Qed.
Lemma append_only_loc_own_loc_prim l γe uf ty :
append_only_loc l γe uf ty ⊢ ∃ C : cell, l p↦{1} C.
Proof.
iIntros "omo↦". rewrite append_only_loc_eq.
iDestruct "omo↦" as (??????????) "(%& %Hγx & #Hγx & M●' & ES● & ML● & l↦ & #ML✓ & (%ML_t_valid & %ζ_comp & %ζ_ML_valid & %ζ_uf_valid & %Hty))".
rewrite AtomicPtsTo_own_loc_prim. done.
Qed.
Lemma append_only_loc_read l γe γs mo E omo M uf ty o tid V Vb (Ec : coPset) :
Relaxed ⊑ o → ↑histN ⊆ Ec →
{{{ OmoAuth γe γs (1/2)%Qp E omo mo _ ∗ OmoEview γe M ∗ @{Vb} append_only_loc l γe uf ty ∗ ⊒V }}}
Read o #l @ tid; Ec
{{{ e gen v' V' V'' eV eV', RET v';
let E' := E ++ [eV'] in
let e' := length E in
let omo' := omo_insert_r omo gen e' in
let M' := {[e']} ∪ M in
⌜ omo_write_op omo !! gen = Some e
∧ loc_event_msg eV.(type) = (v', V')
∧ V ⊑ V''
∧ eV'.(type) = ReadE (v', V')
∧ eV'.(sync) = V'' ⌝ ∗
OmoAuth γe γs (1/2)%Qp E' omo' mo _ ∗
OmoTokenR γe e' ∗ (* use this to commit the event and update [OmoAuth] *)
OmoUB γe M e ∗
OmoEinfo γe e eV ∗
OmoEq γe e e' ∗
OmoEinfo γe e' eV' ∗
⊒V'' ∗
(if decide (AcqRel ⊑ o) then ⌜V' ⊑ V''⌝ else ▽{tid} ⊒V') ∗
@{V''} OmoEview γe M' ∗
@{Vb ⊔ V''} append_only_loc l γe uf ty }}}.
Proof.
iIntros "%MOMORD %INCL" (Φ) "(M● & #⊒M & omo↦ & #⊒V) Post". rewrite append_only_loc_eq.
iDestruct "omo↦" as (??????????) "(%& %Hγx & #Hγx & M●' & ES● & ML● & l↦ & #ML✓ & (%ML_t_valid & %ζ_comp & %ζ_ML_valid & %ζ_uf_valid & %Hty))".
rewrite !view_at_objective_iff.
iDestruct (OmoAuth_agree with "M● M●'") as %(<- & <- & <- & <-).
iDestruct (OmoAuth_wf with "M●") as %[OMO_GOOD _].
iDestruct (OmoEview_nonempty with "⊒M") as %NEmp.
iDestruct (OmoAuth_OmoEview with "M● ⊒M") as %MIncl.
iDestruct (big_sepL2_length with "ML✓") as %EQlenML.
iCombine "M● M●'" as "M●".
iDestruct (view_at_intro_incl with "⊒M ⊒V") as (V') "(#⊒V' & %LeVV' & #⊒M@V')".
(* Extract latest observed message *)
iAssert (∃ e ew eidx tw vw Vw,
⌜ e ∈ M ∧ lookup_omo omo eidx = Some e ∧ ML !! (gen_of eidx) = Some (tw, vw, Vw) ∧ OmoUBgen omo M (gen_of eidx) ⌝ ∗
l sn⊒{γl} {[tw := (vw, Vw)]} ∗ OmoSnap γe γs e (ew, (vw, Vw)))%I
with "[-]" as "(%&%&%&%&%&%& (%eIn & %Heidx & %MLgen & %MAXgen) & #l⊒ & #e↪st)".
{ iClear "Post ⊒M@V'". iInduction M as [|e M NotIn] "IH" using set_ind_L; [done|].
destruct (decide (M = ∅)) as [Memp|NEmp'].
- have EQ : {[e]} ∪ M = {[e]} by set_solver. rewrite !EQ. clear EQ.
have HeV : e ∈ ({[e]} ∪ M) by set_solver-. apply MIncl in HeV.
eapply lookup_omo_surjective in HeV as Heidx; [|done]. destruct Heidx as [eidx Heidx]. destruct HeV as [eV HeV].
have [[e' es'] Hgen] : is_Some (omo !! (gen_of eidx)).
{ rewrite lookup_lt_is_Some. apply lookup_omo_lt_Some in Heidx. done. }
have [minfo Hminfo] : is_Some (ML !! (gen_of eidx)).
{ rewrite lookup_lt_is_Some -EQlenML. apply lookup_lt_Some in Hgen. done. }
iDestruct (big_sepL2_lookup with "ML✓") as (?? eV' tw vw Vw) "((%EQ1 & %eV'EV & %EQ2) & #e'✓eV' & #e'↪st' & l⊒@SYNC' & BIG)"; [done|done|].
inversion EQ1. subst e0 es minfo. clear EQ1.
destruct eidx.
+ simpl in Hgen. rewrite lookup_omo_ro_event /omo_read_op list_lookup_fmap Hgen /= in Heidx.
iDestruct (big_sepL_lookup with "BIG") as (?) "(%eVEV & e✓eV & e↪st & l⊒@SYNC)"; [done|].
iDestruct (OmoEinfo_get with "M●") as "#e✓eV'"; [done|].
iDestruct (OmoEinfo_agree with "e✓eV e✓eV'") as %->.
iDestruct (OmoEinfo_OmoEview _ e with "e✓eV ⊒M") as "⊒SYNC"; [set_solver-|].
iDestruct (view_at_elim with "⊒SYNC l⊒@SYNC") as "l⊒".
iExists e,e',(ro_event gen i'),tw,vw,Vw. iFrame "l⊒ e↪st". iPureIntro. split_and!; try done.
* set_solver-.
* rewrite lookup_omo_ro_event /omo_read_op list_lookup_fmap Hgen. done.
* rewrite /OmoUBgen. intros.
have EQ : e0 = e by set_solver. subst e0. exists (ro_event gen i'). split.
-- rewrite lookup_omo_ro_event /omo_read_op list_lookup_fmap Hgen. done.
-- done.
+ simpl in Hgen. rewrite lookup_omo_wr_event /omo_write_op list_lookup_fmap Hgen /= in Heidx. inversion Heidx. subst e'. clear Heidx.
iDestruct (OmoEinfo_get with "M●") as "#e✓eV"; [done|].
iDestruct (OmoEinfo_agree with "e✓eV e'✓eV'") as %<-.
iDestruct (OmoEinfo_OmoEview _ e with "e✓eV ⊒M") as "⊒SYNC"; [set_solver-|].
iDestruct (view_at_elim with "⊒SYNC l⊒@SYNC'") as "l⊒".
iExists e,e,(wr_event gen),tw,vw,Vw. iFrame "l⊒ e'↪st'". iPureIntro. split_and!; try done.
* set_solver-.
* rewrite lookup_omo_wr_event /omo_write_op list_lookup_fmap Hgen. done.
* rewrite /OmoUBgen. intros.
have EQ : e0 = e by set_solver. subst e0. exists (wr_event gen). split; [|done].
rewrite lookup_omo_wr_event /omo_write_op list_lookup_fmap Hgen. done.
- iDestruct (OmoEview_split with "⊒M") as "[⊒e ⊒M']"; [set_solver-|done|].
iDestruct ("IH" with "[] [] ⊒M' ES● ML● l↦ M●") as "#H"; [done|..].
{ iPureIntro. intros. apply MIncl. set_solver. }
iDestruct "H" as (e' ew' eidx' tw' vw' Vw') "((%e'IN & %Heidx' & %MLgen' & %MAXgen) & l⊒' & e'↪st')".
have HeV : e ∈ ({[e]} ∪ M) by set_solver-. apply MIncl in HeV.
eapply lookup_omo_surjective in HeV as Heidx; [|done]. destruct Heidx as [eidx Heidx]. destruct HeV as [eV HeV].
destruct (le_lt_dec (gen_of eidx) (gen_of eidx')) as [LE|LT].
{ (* [e] is non-latest event -> induction hypothesis is the answer *)
iExists e',ew',eidx',tw',vw',Vw'. iFrame "l⊒' e'↪st'". iPureIntro. split_and!; try done.
- set_solver.
- rewrite /OmoUBgen. intros.
have CASE : e0 = e ∨ e0 ∈ M by set_solver.
destruct CASE as [->|IN].
+ exists eidx. done.
+ apply MAXgen. done. }
(* [e] is the latest event *)
have [[e'' es''] Hgen] : is_Some (omo !! (gen_of eidx)).
{ rewrite lookup_lt_is_Some. apply lookup_omo_lt_Some in Heidx. done. }
have [minfo Hminfo] : is_Some (ML !! (gen_of eidx)).
{ rewrite lookup_lt_is_Some -EQlenML. apply lookup_lt_Some in Hgen. done. }
iDestruct (big_sepL2_lookup with "ML✓") as (?? eV'' tw vw Vw) "((%EQ1 & %eV''EV & %EQ2) & e''✓eV'' & e''↪st'' & l⊒@SYNC' & BIG)"; [done|done|].
inversion EQ1. subst e0 es minfo. clear EQ1. destruct eidx.
+ simpl in Hgen. rewrite lookup_omo_ro_event /omo_read_op list_lookup_fmap Hgen /= in Heidx.
iDestruct (big_sepL_lookup with "BIG") as (?) "(%eVEV & e✓eV & e↪st & l⊒@SYNC)"; [done|].
iDestruct (OmoEinfo_get with "M●") as "#e✓eV'"; [done|].
iDestruct (OmoEinfo_agree with "e✓eV e✓eV'") as %->.
iDestruct (OmoEinfo_OmoEview _ e with "e✓eV ⊒M") as "⊒SYNC"; [set_solver-|].
iDestruct (view_at_elim with "⊒SYNC l⊒@SYNC") as "l⊒".
iExists e,e'',(ro_event gen i'),tw,vw,Vw. iFrame "l⊒ e↪st". iPureIntro. split_and!; try done.
* set_solver-.
* rewrite lookup_omo_ro_event /omo_read_op list_lookup_fmap Hgen. done.
* rewrite /OmoUBgen. intros.
have CASE : e0 = e ∨ e0 ∈ M by set_solver. destruct CASE as [->|IN].
-- exists (ro_event gen i'). split; [|done]. rewrite lookup_omo_ro_event /omo_read_op list_lookup_fmap Hgen. done.
-- unfold OmoUBgen in *. specialize (MAXgen _ IN) as (eidx'' & Heidx'' & LE).
exists eidx''. split; [done|]. simpl in *. lia.
+ simpl in Hgen. rewrite lookup_omo_wr_event /omo_write_op list_lookup_fmap Hgen /= in Heidx. inversion Heidx. subst e''. clear Heidx.
iDestruct (OmoEinfo_get with "M●") as "#e✓eV"; [done|].
iDestruct (OmoEinfo_agree with "e✓eV e''✓eV''") as %<-.
iDestruct (OmoEinfo_OmoEview _ e with "e✓eV ⊒M") as "⊒SYNC"; [set_solver-|].
iDestruct (view_at_elim with "⊒SYNC l⊒@SYNC'") as "l⊒".
iExists e,e,(wr_event gen),tw,vw,Vw. iFrame "l⊒ e''↪st''". iPureIntro. split_and!; try done.
* set_solver-.
* rewrite lookup_omo_wr_event /omo_write_op list_lookup_fmap Hgen. done.
* rewrite /OmoUBgen. intros.
have CASE : e0 = e ∨ e0 ∈ M by set_solver. destruct CASE as [->|IN].
-- exists (wr_event gen). split; [|done]. rewrite lookup_omo_wr_event /omo_write_op list_lookup_fmap Hgen. done.
-- unfold OmoUBgen in *. specialize (MAXgen _ IN) as (eidx'' & Heidx'' & LE).
exists eidx''. split; [done|]. simpl in *. lia. }
wp_apply wp_fupd. wp_apply (AtomicSeen_read with "[$l⊒ $l↦ $⊒V']"); [done|done|].
iIntros (tr vr Vr V'' ζ'') "(Pures & #⊒V'' & H1 & #l⊒@V'' & l↦)".
iDestruct "Pures" as %([Subζ1 Subζ2] & Htr & MAXtr & LeV'V'').
iAssert (∃ ir, ⌜ ML !! ir = Some (tr, vr, Vr) ∧ gen_of eidx ≤ ir ⌝)%I with "[-]" as %(ir & MLir & LEir).
{ unfold Hist_ML_valid in *. unfold no_earlier_time in *. unfold ML_time_mono in *.
have Htr' : ζ !! tr = Some (vr, Vr) by eapply lookup_weaken.
rewrite ζ_ML_valid elem_of_list_lookup in Htr'. destruct Htr' as [ir MLir].
have Letwtr : (tw ≤ tr)%positive by apply MAXtr; rewrite lookup_singleton.
iExists ir. iPureIntro. split; [done|].
destruct (le_lt_dec (gen_of eidx) ir) as [LE|LT]; try done.
have COND1 : ML.*1.*1 !! ir = Some tr by rewrite !list_lookup_fmap MLir.
have COND2 : ML.*1.*1 !! (gen_of eidx) = Some tw by rewrite !list_lookup_fmap MLgen.
specialize (ML_t_valid _ _ _ _ COND1 COND2 LT). lia. }
have [[er esr] OMOer] : is_Some (omo !! ir).
{ rewrite lookup_lt_is_Some EQlenML. apply lookup_lt_Some in MLir. done. }
iDestruct (big_sepL2_lookup with "ML✓") as (?? eVr ???) "((%EQ1 & %eVrEV & %EQ2) & #er✓eVr & #er↪str & _)"; [done|done|].
inversion EQ1. inversion EQ2. subst e0 es t v V0. clear EQ1 EQ2.
iDestruct (OmoLe_get _ _ _ _ _ _ eidx (wr_event ir) with "M●") as "#e≤er".
{ done. } { rewrite lookup_omo_wr_event /omo_write_op list_lookup_fmap OMOer. done. } { simpl. done. }
set en := (length E).
set M' := {[en]} ∪ M.
set st := (er, (vr, Vr)).
set eVn := mkOmoEvent (ReadE (vr, Vr)) V'' M'.
iDestruct (OmoUB_from_gen with "M●") as "#MAXgen"; [exact Heidx|exact MAXgen|done|].
iDestruct (OmoUB_mono with "MAXgen e≤er") as "MAXgen'". simpl.
iDestruct (view_at_mono_2 _ V'' with "⊒M@V'") as "⊒M@V''"; [solve_lat|].
iMod (OmoAuth_insert_ro_no_Token with "M● ⊒M@V'' er↪str MAXgen' []") as (?) "(M● & #⊒M'@V'' & #er=en & #en✓eVn & RCOMMIT & Pures)".
{ have ? : step en eVn st st.
{ apply loc_step_ReadE; try done. set_solver. }
iPureIntro. split_and!; try done. }
iDestruct "Pures" as %(eidx' & Heidx' & EQgen).
iDestruct (OmoHbToken_finish with "M●") as "[M● M●']".
apply lookup_omo_lt_Some in Heidx' as LT. rewrite omo_insert_r_length -EQgen in LT.
have [es Hes] : is_Some (omo_read_op omo !! gen) by rewrite lookup_lt_is_Some -omo_read_op_length.
erewrite lookup_omo_before_insert_r in Heidx'; [|done].
destruct (decide (eidx' = ro_event gen (length es))) as [->|NEQ]; last first.
{ eapply lookup_omo_event_valid in Heidx'; [|done]. rewrite lookup_lt_is_Some in Heidx'. lia. }
set omo' := omo_insert_r omo gen (length E).
have Heidx'' : lookup_omo omo' (wr_event ir) = Some er.
{ subst omo'. erewrite lookup_omo_before_insert_r; [|done]. rewrite decide_False; [|done].
rewrite lookup_omo_wr_event /omo_write_op list_lookup_fmap OMOer. done. }
iDestruct (OmoEq_Eq with "M● er=en") as %EQgen'; [done|done|].
simpl in EQgen'. clear EQgen. subst ir.
iDestruct ("Post" $! er gen vr Vr V'' eVr eVn with "[-]") as "HΦ".
{ iFrame "H1 M●' RCOMMIT ⊒V'' en✓eVn er✓eVr er=en MAXgen' ⊒M'@V''". iSplitR.
- iPureIntro. split_and!; try done; [|solve_lat]. rewrite /omo_write_op list_lookup_fmap OMOer. done.
- iExists γx,γl,γw,γm,γs. iExists _,omo',mo,q,ML,ζ. subst omo'. rewrite omo_insert_r_write_op. iFrame "l↦ M● ES● ML● Hγx".
iSplit; [done|]. iSplit; [|done]. rewrite view_at_objective_iff.
rewrite /OMO_ML_valid /omo_insert_r -{2}(take_drop gen omo) (drop_S _ (er, esr)); [|done].
rewrite alter_app_r_alt; [|by rewrite take_length; lia].
replace (gen - length (take gen omo)) with 0; last first.
{ rewrite take_length Nat.min_l; [lia|]. apply lookup_lt_Some in OMOer. lia. }
simpl. rewrite -{2}(take_drop gen ML) (drop_S _ (tr, vr, Vr)); [|done].
rewrite -{1}(take_drop gen omo) (drop_S _ (er, esr)); [|done].
rewrite -{1}(take_drop gen ML) (drop_S _ (tr, vr, Vr)); [|done].
iDestruct (big_sepL2_app_inv with "ML✓") as "[ML✓1 ML✓2]".
{ left. rewrite !take_length EQlenML. done. }
rewrite big_sepL2_cons. iDestruct "ML✓2" as "[ML✓2' ML✓3]".
iApply big_sepL2_app; [done|].
iApply big_sepL2_cons. iFrame "ML✓3".
iDestruct "ML✓2'" as (??????) "((%EQ1 & %EQ2 & %EQ3) & H1 & H2 & H3 & H4)".
inversion EQ1. inversion EQ3. subst e0 es0 t v V0. clear EQ1 EQ3.
iExists er,(esr ++ [en]),eVr,tr,vr,Vr. rewrite big_sepL_snoc.
iDestruct (OmoEinfo_agree with "er✓eVr H1") as %<-.
iFrame "H1 H2 H3 H4". iSplit; [done|]. iExists eVn.
iDestruct (OmoSnap_get_from_Eq with "er↪str er=en") as "en↪st".
iFrame "en✓eVn en↪st". iSplit; [done|].
rewrite (AtomicSeen_mono_lookup_singleton _ _ ζ'' tr vr Vr); [done|].
eapply lookup_weaken; try done. }
iModIntro. by iApply "HΦ".
Qed.
Lemma append_only_loc_read_with_swriter_token l γe γs mo E omo es M uf o tid V Vb (Ec : coPset) :
Relaxed ⊑ o → ↑histN ⊆ Ec →
{{{ OmoAuth γe γs (1/2)%Qp E omo mo _ ∗ OmoEview γe M ∗
swriter_token l γe es ∗ @{Vb} append_only_loc l γe uf swriter ∗ ⊒V }}}
Read o #l @ tid; Ec
{{{ e v' V' V'' eV eV', RET v';
let E' := E ++ [eV'] in
let e' := length E in
let omo' := omo_insert_r omo (length omo - 1)%nat e' in
let M' := {[e']} ∪ M in
⌜ last (omo_write_op omo) = Some e
∧ loc_event_msg eV.(type) = (v', V')
∧ V ⊑ V''
∧ eV'.(type) = ReadE (v', V')
∧ eV'.(sync) = V'' ⌝ ∗
OmoAuth γe γs (1/2)%Qp E' omo' mo _ ∗
OmoTokenR γe e' ∗ (* use this to commit the event and update [OmoAuth] *)
OmoUB γe M e ∗
OmoEinfo γe e eV ∗
OmoEinfo γe e' eV' ∗
OmoEq γe e e' ∗
⊒V'' ∗
(if decide (AcqRel ⊑ o) then ⌜V' ⊑ V''⌝ else ▽{tid} ⊒V') ∗
@{V''} (swriter_token l γe es ∗ OmoEview γe M') ∗
@{Vb ⊔ V''} append_only_loc l γe uf swriter }}}.
Proof.
iIntros "%MOMORD %INCL" (Φ) "(M● & #⊒M & SW & omo↦ & #⊒V) Post". rewrite append_only_loc_eq swriter_token_eq.
iDestruct "omo↦" as (??????????) "(%& %Hγx & #Hγx & M●' & ES● & ML● & l↦ & #ML✓ & (%ML_t_valid & %ζ_comp & %ζ_ML_valid & %ζ_uf_valid & %Hty))".
iDestruct "SW" as (????? tw vw Vw) "([%Hγx' %LASTML] & #Hγx' & ES●' & ML●' & #l⊒)".
rewrite !view_at_objective_iff.
iDestruct (OmoGname_agree with "Hγx Hγx'") as %<-. encode_agree Hγx.
iDestruct (OmoAuth_agree with "M● M●'") as %(<- & <- & <- & <-).
iDestruct (OmoAuth_wf with "M●") as %[OMO_GOOD _].
iDestruct (OmoEview_nonempty with "⊒M") as %NEmp.
iDestruct (OmoAuth_OmoEview with "M● ⊒M") as %MIncl.
iDestruct (big_sepL2_length with "ML✓") as %EQlenML.
iCombine "M● M●'" as "M●".
iDestruct (mono_list_auth_own_agree with "ML● ML●'") as %[_ <-].
iDestruct (view_at_intro_incl with "⊒M ⊒V") as (V') "(#⊒V' & %LeVV' & #⊒M@V')".
wp_apply wp_fupd. wp_apply (AtomicSeen_read with "[$l⊒ $l↦ $⊒V']"); [done|done|].
iIntros (tr vr Vr V'' ζ'') "(Pures & #⊒V'' & H1 & #l⊒@V'' & l↦)".
iDestruct "Pures" as %([Subζ1 Subζ2] & Htr & MAXtr & LeV'V'').
iAssert (⌜ tw = tr ∧ vw = vr ∧ Vw = Vr ⌝)%I with "[-]" as %(-> & -> & ->).
{ have Htr' : ζ !! tr = Some (vr, Vr) by eapply lookup_weaken.
rewrite ζ_ML_valid elem_of_list_lookup in Htr'. destruct Htr' as [ir Hir].
rewrite last_lookup in LASTML. replace (Init.Nat.pred (length ML)) with (length ML - 1) in LASTML by lia.
have NZML : length ML ≠ 0 by destruct ML.
apply lookup_lt_Some in Hir as LT.
destruct (decide (ir = length ML - 1)) as [->|NEQ].
{ rewrite LASTML in Hir. inversion Hir. done. }
have LT' : ir < length ML - 1 by lia.
have COND1 : ML.*1.*1 !! ir = Some tr by rewrite !list_lookup_fmap Hir.
have COND2 : ML.*1.*1 !! (length ML - 1) = Some tw by rewrite !list_lookup_fmap LASTML.
specialize (ML_t_valid _ _ _ _ COND1 COND2 LT').
have LE : (tw ≤ tr)%positive.
{ apply MAXtr. rewrite lookup_singleton. done. }
lia. }
iDestruct (OmoAuth_omo_nonempty with "M●") as %Nomo.
have [[er esr] Her] : is_Some (last omo) by rewrite last_is_Some.
iDestruct (big_sepL2_lookup with "ML✓") as (?? eVr ???) "((%EQ1 & %eVrEV & %EQ2) & er✓eVr & er↪str & _ & BIG)".
{ rewrite last_lookup in Her. done. } { rewrite last_lookup -EQlenML in LASTML. done. }
inversion EQ1. inversion EQ2. subst e es0 t v V0. clear EQ1 EQ2.
set en := (length E).
set M' := {[en]} ∪ M.
set st := (er, (vr, Vr)).
set eVn := mkOmoEvent (ReadE (vr, Vr)) V'' M'.
have MAXgen : OmoUBgen omo M (length omo - 1).
{ rewrite /OmoUBgen. intros.
apply MIncl in H. eapply lookup_omo_surjective in H as Heidx; [|done]. destruct Heidx as [eidx Heidx].
exists eidx. split; [done|]. apply lookup_omo_lt_Some in Heidx. lia. }
iDestruct (OmoUB_from_gen _ _ _ _ _ _ _ _ _ (wr_event (length omo - 1)) with "M●") as "#MAXgen".
{ rewrite lookup_omo_wr_event /omo_write_op list_lookup_fmap.
rewrite last_lookup in Her. replace (Init.Nat.pred (length omo)) with (length omo - 1) in Her by lia.
rewrite Her. done. } { done. } { done. }
iDestruct (view_at_mono_2 _ V'' with "⊒M@V'") as "⊒M@V''"; [solve_lat|].
iMod (OmoAuth_insert_ro_no_Token with "M● ⊒M@V'' er↪str MAXgen []") as (?) "(M● & #⊒M'@V'' & #er=en & #en✓eVn & RCOMMIT & Pures)".
{ have ? : step en eVn st st.
{ apply loc_step_ReadE; try done. set_solver. }
iPureIntro. split_and!; try done. }
iDestruct "Pures" as %(eidx' & Heidx' & EQgen).
iDestruct (OmoHbToken_finish with "M●") as "[M● M●']".
apply lookup_omo_lt_Some in Heidx' as LT. rewrite omo_insert_r_length -EQgen in LT.
have [es' Hes'] : is_Some (omo_read_op omo !! gen) by rewrite lookup_lt_is_Some -omo_read_op_length.
erewrite lookup_omo_before_insert_r in Heidx'; [|done].
destruct (decide (eidx' = ro_event gen (length es'))) as [->|NEQ]; last first.
{ eapply lookup_omo_event_valid in Heidx'; [|done]. rewrite lookup_lt_is_Some in Heidx'. lia. }
set omo' := omo_insert_r omo gen (length E).
have Heidx'' : lookup_omo omo' (wr_event (length omo - 1)) = Some er.
{ subst omo'. erewrite lookup_omo_before_insert_r; [|done]. rewrite decide_False; [|done].
rewrite lookup_omo_wr_event /omo_write_op list_lookup_fmap.
rewrite last_lookup in Her. replace (Init.Nat.pred (length omo)) with (length omo - 1) in Her by lia. rewrite Her. done. }
iDestruct (OmoEq_Eq with "M● er=en") as %EQgen'; [done|done|].
simpl in EQgen'. clear EQgen. subst gen.
iDestruct ("Post" $! er vr Vr V'' eVr eVn with "[-]") as "HΦ".
{ iFrame "H1 M●' RCOMMIT ⊒V'' en✓eVn er✓eVr er=en MAXgen ⊒M'@V''". iSplitR; last iSplitL "ML●' ES●'".
- iPureIntro. split_and!; try done; [|solve_lat]. rewrite last_lookup -omo_write_op_length /omo_write_op list_lookup_fmap.
rewrite last_lookup in Her. rewrite Her. done.
- iExists γx,γl,γw,γm,ML,tr,vr,Vr. iFrame "Hγx ML●' ES●'". iSplitR; [done|].
rewrite (AtomicSeen_mono_lookup_singleton _ _ ζ'' tr vr Vr); [done|]. done.
- iExists γx,γl,γw,γm,γs. iExists _,omo',mo,q,ML,ζ. subst omo'. rewrite omo_insert_r_write_op. iFrame "l↦ M● ES● ML● Hγx".
iSplit; [done|]. iSplit; [|done]. rewrite view_at_objective_iff.
rewrite /OMO_ML_valid /omo_insert_r -{3}(take_drop (length omo - 1) omo) (drop_S _ (er, esr)); last first.
{ rewrite last_lookup in Her. replace (Init.Nat.pred (length omo)) with (length omo - 1) in Her by lia. done. }
rewrite alter_app_r_alt; [|by rewrite take_length; lia].
replace ((length omo - 1) - length (take (length omo - 1) omo)) with 0; last first.
{ rewrite take_length Nat.min_l; [lia|]. lia. }
simpl. rewrite -{2}(take_drop (length ML - 1) ML) (drop_S _ (tr, vr, Vr)); last first.
{ rewrite last_lookup in LASTML. replace (Init.Nat.pred (length ML)) with (length ML - 1) in LASTML by lia. done. }
rewrite -{1}(take_drop (length omo - 1) omo) (drop_S _ (er, esr)); last first.
{ rewrite last_lookup in Her. replace (Init.Nat.pred (length omo)) with (length omo - 1) in Her by lia. done. }
rewrite -{1}(take_drop (length ML - 1) ML) (drop_S _ (tr, vr, Vr)); last first.
{ rewrite last_lookup in LASTML. replace (Init.Nat.pred (length ML)) with (length ML - 1) in LASTML by lia. done. }
iDestruct (big_sepL2_app_inv with "ML✓") as "[ML✓1 ML✓2]".
{ left. rewrite !take_length EQlenML. done. }
rewrite big_sepL2_cons. iDestruct "ML✓2" as "[ML✓2' ML✓3]".
iApply big_sepL2_app; [done|].
iApply big_sepL2_cons. iFrame "ML✓3".
iDestruct "ML✓2'" as (??????) "((%EQ1 & %EQ2 & %EQ3) & H1 & H2 & H3 & H4)".
inversion EQ1. inversion EQ3. subst e es0 t v V0. clear EQ1 EQ3.
iExists er,(esr ++ [en]),eVr,tr,vr,Vr. rewrite big_sepL_snoc.
iDestruct (OmoEinfo_agree with "er✓eVr H1") as %<-.
iFrame "H1 H2 H3 H4". iSplit; [done|]. iExists eVn.
iDestruct (OmoSnap_get_from_Eq with "er↪str er=en") as "en↪st".
iFrame "en✓eVn en↪st". iSplit; [done|].
rewrite (AtomicSeen_mono_lookup_singleton _ _ ζ'' tr vr Vr); [done|].
eapply lookup_weaken; try done. }
iModIntro. by iApply "HΦ".
Qed.
Lemma append_only_loc_acquire_read l γe γs mo E omo M uf ty tid V Vb (Ec : coPset) :
↑histN ⊆ Ec →
{{{ OmoAuth γe γs (1/2)%Qp E omo mo _ ∗ OmoEview γe M ∗ @{Vb} append_only_loc l γe uf ty ∗ ⊒V }}}
!ᵃᶜ#l @ tid; Ec
{{{ e (gen : nat) v' V' V'' eV eV', RET v';
let E' := E ++ [eV'] in
let e' := length E in
let omo' := omo_insert_r omo gen e' in
let M' := {[e']} ∪ M in
⌜ omo_write_op omo !! gen = Some e
∧ loc_event_msg eV.(type) = (v', V')
∧ V ⊔ V' ⊑ V''
∧ eV'.(type) = ReadE (v', V')
∧ eV'.(sync) = V'' ⌝ ∗
OmoAuth γe γs (1/2)%Qp E' omo' mo _ ∗
OmoTokenR γe e' ∗ (* use this to commit the event and update [OmoAuth] *)
OmoUB γe M e ∗
OmoEinfo γe e eV ∗
OmoEinfo γe e' eV' ∗
OmoEq γe e e' ∗
⊒V'' ∗
@{V''} OmoEview γe M' ∗
@{Vb ⊔ V''} append_only_loc l γe uf ty }}}.
Proof.
iIntros "%" (Φ) "(M● & #⊒M & omo↦ & #⊒V) Post".
wp_apply (append_only_loc_read with "[$M● $⊒M $omo↦ $⊒V]"); try done.
iIntros (???????) "(Pures & M● & RCoMMIT & #MAXgen & #e✓eV & #e=en & #en✓eVn & #⊒V'' & Pure & #⊒M' & omo↦)".
iDestruct ("Post" $! e gen v' V' V'' eV eV' with "[-]") as "HΦ".
{ iFrame "∗#%". iDestruct "Pures" as %(H1 & H2 & H3 & H4 & H5).
iDestruct "Pure" as %H6. iPureIntro.
split_and!; try done. solve_lat. }
by iApply "HΦ".
Qed.
Lemma append_only_loc_relaxed_read l γe γs mo E omo M uf ty tid V Vb (Ec : coPset) :
↑histN ⊆ Ec →
{{{ OmoAuth γe γs (1/2)%Qp E omo mo _ ∗ OmoEview γe M ∗ @{Vb} append_only_loc l γe uf ty ∗ ⊒V }}}
!ʳˡˣ#l @ tid; Ec
{{{ e (gen : nat) v' V' V'' eV eV', RET v';
let E' := E ++ [eV'] in
let e' := length E in
let omo' := omo_insert_r omo gen e' in
let M' := {[e']} ∪ M in
⌜ omo_write_op omo !! gen = Some e
∧ loc_event_msg eV.(type) = (v', V')
∧ V ⊑ V''
∧ eV'.(type) = ReadE (v', V')
∧ eV'.(sync) = V'' ⌝ ∗
OmoAuth γe γs (1/2)%Qp E' omo' mo _ ∗