-
Notifications
You must be signed in to change notification settings - Fork 0
/
numbering.v
1198 lines (1027 loc) · 37.4 KB
/
numbering.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
(*
This project is an attempt at formalising the proof of DRF-SC for the repaired
C11 memory model presented in the article (Repairing Sequential Consistency in
C/C++11; Lahav, Vafeiadis, Kang et al., PLDI 2017)
Author: Quentin Ladeveze, Inria Paris, France
*)
From RelationAlgebra Require Import
lattice prop monoid rel kat_tac normalisation kleene kat rewriting.
Require Import Ensembles.
Require Import Lia.
Require Import Classical_Prop.
From RC11 Require Import util.
From RC11 Require Import exec.
From RC11 Require Import proprel_classic.
From RC11 Require Import prefix.
From RC11 Require Import rc11.
From RC11 Require Import conflict.
(** This file defines the notion of numbering on the events of an execution. *)
(** ** Definition *)
(** A valid numbering on an execution assigns to each event of the execution a
distinct number such that, if two events are related by the transitive closure
of the union of the sequenced-before and read-from relations of the execution,
then the numbering of the first event is smaller than the numbering of the
second event *)
Definition numbering event : nat :=
match event with
| Read eid _ _ _ => eid
| Write eid _ _ _ => eid
| Fence eid _ => eid
end.
(** Two different events can't have the same numbering *)
Definition numbering_injective (ex: Execution) := forall x y,
x <> y <-> numbering x <> numbering y.
(** Two identical events have the same numbering *)
Lemma numbering_injective_eq (ex: Execution) (x y: Event):
numbering_injective ex ->
x = y <-> numbering x = numbering y.
Proof.
intros Hinj.
split; intros H.
- rewrite H; auto.
- destruct (classic (x = y)) as [Hxy | Hxy].
+ auto.
+ rewrite (Hinj _ _) in Hxy.
destruct (Hxy H).
Qed.
(** If an event is equal to a read whose numbering is the numbering of a second
event, the two events are equal *)
Lemma eq_num_read {ex: Execution} {x y: Event} {m: Mode} {l: Loc} {v: Val}:
numbering_injective ex ->
Read (numbering y) m l v = x ->
x = y.
Proof.
intros Hnuminj Heq.
eapply numbering_injective_eq. eauto.
rewrite <-Heq. auto.
Qed.
Lemma eq_num_read2 {ex: Execution} {x y: Event} {m: Mode} {l: Loc} {v: Val}:
numbering_injective ex ->
x = Read (numbering y) m l v ->
x = y.
Proof.
intros Hnuminj Heq.
eapply numbering_injective_eq. eauto.
rewrite Heq. auto.
Qed.
(** If a numbering of the events of an execution is injective, the numbering of
the events of its prefixes is also injective *)
Lemma numbering_injective_pre (ex pre: Execution):
numbering_injective ex ->
prefix pre ex ->
numbering_injective pre.
Proof.
intros Hnuminj Hpre. destruct_prefix Hpre.
intros x y. apply Hnuminj; apply Hevts; auto.
Qed.
(** If an first event is related to a second event by the union of the sequenced
before relation and reads-from relation, the numbering of the first event is
strictly inferior to the numbering of the second event *)
Definition numbering_coherent ex :=
forall x y, ((sb ex) ⊔ (rf ex)) x y ->
numbering x < numbering y.
(** If a first event is related to a second event by the reflexive transitive
closure of the union of the sequenced-before relation and reads-from relation,
the numbering of the second event is greater or equal to the numbering of the
first event *)
Lemma numbering_coherent_rtc (ex: Execution) (x y: Event):
numbering_coherent ex ->
((sb ex) ⊔ (rf ex))^* x y ->
numbering y >= numbering x.
Proof.
intros Hnumco.
generalize dependent y.
generalize dependent x.
apply rtc_ind.
- intros z1 z2 Hstep.
apply Hnumco in Hstep. lia.
- intuition auto.
- intros z1 z2 z3 _ IH1 _ IH2.
lia.
Qed.
(** If a first event is related to a second event by the transitive closure of
the union of the sequenced-before relation and reads-from relation, the
numbering of the second event is greater than the numbering of the first
event *)
Lemma numbering_coherent_tc (ex: Execution) (x y: Event):
numbering_coherent ex ->
((sb ex) ⊔ (rf ex))^+ x y ->
numbering y > numbering x.
Proof.
intros Hnumco [z Hstep Hrtc].
apply Hnumco in Hstep.
apply (numbering_coherent_rtc _ _ _ Hnumco) in Hrtc.
lia.
Qed.
(** If a first event is related by the sequenced-before relation to a second
event, the numbering of the second event is strictly greater than the numbering
of the first event *)
Lemma sb_num_ord (ex: Execution) (x y: Event):
numbering_coherent ex ->
sb ex x y ->
(numbering y) > (numbering x).
Proof.
intros Hnumco Hsb.
eapply numbering_coherent_tc, tc_incl_itself. eauto.
left; auto.
Qed.
(** If a first event is related by the read-modify-write relation to a second
event, the numbering of the second event is strictly greater than the numbering
of the first event *)
Lemma rmw_num_ord (ex: Execution) (x y: Event):
valid_exec ex ->
numbering_coherent ex ->
rmw ex x y ->
(numbering y) > (numbering x).
Proof.
intros Hval Hnumco Hrmw.
eapply (rmw_incl_sb _ Hval) in Hrmw.
eapply sb_num_ord; eauto.
Qed.
(** If a first event is related by the reads-from relation to a second event,
the numbering of the second event is strictly greater than the numbering of the
first event *)
Lemma rf_num_ord (ex: Execution) (x y: Event):
numbering_coherent ex ->
rf ex x y ->
(numbering y) > (numbering x).
Proof.
intros Hnumco Hsb.
eapply numbering_coherent_tc, tc_incl_itself; eauto.
right; auto.
Qed.
(** If the numbering of the events of an execution is coherent, the numbering of
the events of its prefixes is also coherent *)
Lemma numbering_coherent_pre (ex pre: Execution):
numbering_coherent ex ->
prefix pre ex ->
numbering_coherent pre.
Proof.
intros Hnumco Hpre. destruct_prefix Hpre.
intros x y Hsbrf.
apply Hnumco.
apply (incl_rel_thm Hsbrf). rewrite Hsb, Hrf. kat.
Qed.
(** In every execution, there is a last event whose numbering is greater than
the one of all the other events *)
Axiom numbering_bounded:
exists e, forall e', numbering e >= numbering e'.
(** Tests if the numbering of an event is Less or Equal to a bound *)
Definition NLE (b: nat) : prop_set Event :=
fun e => b >= (numbering e).
(** Being in the set of events whose numbering is less or equal to a bound is
equivalent to satisfying the NLE test with this bound *)
Lemma NLE_I_evts (bound: nat):
[I (fun x => bound >= numbering x)] = [NLE bound].
Proof. unfold NLE. kat_eq. Qed.
(** If an event's numbering is less or equal to a bound minus one, it is less
or equal to the bound *)
Lemma NLE_bound_min_one (bound: nat):
[NLE (bound-1)] ≦ [NLE bound].
Proof.
intros x y [H1 H2].
split; auto.
unfold NLE in *. lia.
Qed.
(** If we test that an event's numbering is less or equal to two bounds, one of
which is strictly inferior to the other, we can replace these two tests by the
test of the event's numbering being less or equal to the smaller bound *)
Lemma nle_double (k1 k2: nat):
k1 < k2 ->
[NLE k1]⋅[NLE k2] = [NLE k1].
Proof.
intros Hord. apply ext_rel, antisym.
- intros x y [z [Heq1 Hr1] [Heq2 Hr2]].
rewrite Heq2 in Heq1, Hr2. split; auto.
- intros x y [Heq Hr].
exists x; split; auto.
unfold NLE in Hr. unfold NLE. lia.
Qed.
(** An bounded execution is a restriction of the events and relations of an
execution to the events whose numbering is less or equal to a given bound. *)
Definition bounded_exec (ex: Execution) (n: nat) : Execution :=
{|
exec.evts := Intersection _ (evts ex) (fun x => n >= numbering x);
exec.sb := [NLE n] ⋅ (sb ex) ⋅ [NLE n];
exec.rmw := [NLE n] ⋅ (rmw ex) ⋅ [NLE n];
exec.rf := [NLE n] ⋅ (rf ex) ⋅ [NLE n];
exec.mo := [NLE n] ⋅ (mo ex) ⋅ [NLE n];
|}.
(** Simplifications of the different getters applied over bounded executions *)
Lemma simpl_evts_be (ex: Execution) (n:nat):
evts (bounded_exec ex n) = Intersection _ (evts ex) (fun x => n >= numbering x).
Proof. compute; auto. Qed.
Lemma simpl_sb_be (ex: Execution) (n:nat):
sb (bounded_exec ex n) = [NLE n] ⋅ (sb ex) ⋅ [NLE n].
Proof. compute; auto. Qed.
Lemma simpl_rmw_be (ex: Execution) (n:nat):
rmw (bounded_exec ex n) = [NLE n] ⋅ (rmw ex) ⋅ [NLE n].
Proof. compute; auto. Qed.
Lemma simpl_rf_be (ex: Execution) (n:nat):
rf (bounded_exec ex n) = [NLE n] ⋅ (rf ex) ⋅ [NLE n].
Proof. compute; auto. Qed.
Lemma simpl_mo_be (ex: Execution) (n:nat):
mo (bounded_exec ex n) = [NLE n] ⋅ (mo ex) ⋅ [NLE n].
Proof. compute; auto. Qed.
Lemma simpl_rb_be (ex: Execution) (n:nat):
rb (bounded_exec ex n) ≦ [NLE n] ⋅ (rb ex) ⋅ [NLE n].
Proof.
unfold rb. rewrite simpl_mo_be, simpl_rf_be.
rewrite 2dot_cnv, injcnv.
kat.
Qed.
Create HintDb bounded_exec_db.
Hint Rewrite simpl_sb_be simpl_rmw_be simpl_rf_be simpl_mo_be : bounded_exec_db.
Tactic Notation "rew" "bounded" := autorewrite with bounded_exec_db.
Tactic Notation "rew" "bounded" "in" hyp(H) := autorewrite with bounded_exec_db in H.
(** Extract the information about the numbering of events from relations in
bounded executions *)
Lemma bounded_sb_l (ex: Execution) (n: nat) (x y: Event):
sb (bounded_exec ex n) x y ->
numbering x <= n.
Proof.
intros H. rew bounded in H.
apply simpl_trt_hyp in H as [H1 [_ H2]].
unfold NLE in *. lia.
Qed.
Lemma bounded_sb_r (ex: Execution) (n: nat) (x y: Event):
sb (bounded_exec ex n) x y ->
numbering y <= n.
Proof.
intros H. rew bounded in H.
apply simpl_trt_hyp in H as [H1 [_ H2]].
unfold NLE in *. lia.
Qed.
Lemma bounded_rf_l (ex: Execution) (n: nat) (x y: Event):
rf (bounded_exec ex n) x y ->
numbering x <= n.
Proof.
intros H. rew bounded in H.
apply simpl_trt_hyp in H as [H1 [_ H2]].
unfold NLE in *. lia.
Qed.
Lemma bounded_rf_r (ex: Execution) (n: nat) (x y: Event):
rf (bounded_exec ex n) x y ->
numbering y <= n.
Proof.
intros H. rew bounded in H.
apply simpl_trt_hyp in H as [H1 [_ H2]].
unfold NLE in *. lia.
Qed.
Lemma bounded_mo_l (ex: Execution) (n: nat) (x y: Event):
mo (bounded_exec ex n) x y ->
numbering x <= n.
Proof.
intros H. rew bounded in H.
apply simpl_trt_hyp in H as [H1 [_ H2]].
unfold NLE in *. lia.
Qed.
Lemma bounded_mo_r (ex: Execution) (n: nat) (x y: Event):
mo (bounded_exec ex n) x y ->
numbering y <= n.
Proof.
intros H. rew bounded in H.
apply simpl_trt_hyp in H as [H1 [_ H2]].
unfold NLE in *. lia.
Qed.
Lemma bounded_rb_l (ex: Execution) (n: nat) (x y: Event):
rb (bounded_exec ex n) x y ->
numbering x <= n.
Proof.
intros H. unfold rb in H. destruct H as [z H _].
rewrite <-cnv_rev in H.
rew bounded in H.
apply simpl_trt_hyp in H as [H1 [_ H2]].
unfold NLE in *. lia.
Qed.
Lemma bounded_rb_r (ex: Execution) (n: nat) (x y: Event):
rb (bounded_exec ex n) x y ->
numbering y <= n.
Proof.
intros H. unfold rb in H. destruct H as [z _ H].
rew bounded in H.
apply simpl_trt_hyp in H as [H1 [_ H2]].
unfold NLE in *. lia.
Qed.
(** An event belonging to the events of a bounded executions belong to the events
of the execution *)
Lemma bounding_evts_in (ex: Execution) (x: Event) (bound: nat):
In _ (evts (bounded_exec ex bound)) x ->
In _ (evts ex) x.
Proof.
intros [y Hin _]. auto.
Qed.
(** Bounding two executions by the same bound maintains the prefix relationship
between them *)
Lemma bounding_of_prefix (pre ex: Execution) (bound: nat):
prefix pre ex ->
prefix (bounded_exec pre bound) (bounded_exec ex bound).
Proof.
intros Hpre.
inverse_prefix Hpre.
repeat (apply conj).
- rewrite simpl_evts_be. intros x H.
apply in_intersection in H as [H1 H2].
split.
+ apply Hevts in H1. auto.
+ unfold In in *. auto.
- intros a b Hsbrf Hinb. specialize (Hclosed a b).
split.
+ apply Hclosed.
* destruct Hsbrf as [Hsbrf|Hsbrf];
rew bounded in Hsbrf;
apply simpl_trt_rel in Hsbrf; [left|right]; auto.
* rewrite simpl_evts_be in Hinb. apply in_intersection in Hinb as [Hinb _].
auto.
+ unfold In.
destruct Hsbrf as [Hsbrf|Hsbrf];
apply simpl_trt_hyp in Hsbrf as [Hsbrf _];
unfold NLE in Hsbrf; auto.
- rew bounded. rewrite simpl_evts_be.
rewrite I_inter. rewrite NLE_I_evts.
rewrite Hsb. kat_eq.
- rew bounded. rewrite simpl_evts_be.
rewrite I_inter. rewrite NLE_I_evts.
rewrite Hrf. kat_eq.
- rew bounded. rewrite simpl_evts_be.
rewrite I_inter. rewrite NLE_I_evts.
rewrite Hmo. kat_eq.
- rew bounded. rewrite simpl_evts_be.
rewrite I_inter. rewrite NLE_I_evts.
rewrite Hrmw. kat_eq.
Qed.
(** The union of all the relations of an execution bounded by [n] is included in
the union of all the relations of the execution bounded by [n] restricted to the
events whose numbering is less or equal to [n] *)
Lemma sc_cycle_be_incl_be_sc_cycle (ex: Execution) (n: nat):
sb (bounded_exec ex n) ⊔
rf (bounded_exec ex n) ⊔
mo (bounded_exec ex n) ⊔
rb (bounded_exec ex n) ≦
[NLE n] ⋅
(sb (bounded_exec ex n) ⊔
rf (bounded_exec ex n) ⊔
mo (bounded_exec ex n) ⊔
rb (bounded_exec ex n) ) ⋅ [NLE n].
Proof.
unfold rb.
rew bounded.
rewrite 2dot_cnv, injcnv.
kat.
Qed.
(** The union of all the relations of a bounded execution is included in the
union of all the relations of the execution *)
Lemma cycle_be_incl_cycle_ex (ex: Execution) (bound:nat):
sb (bounded_exec ex bound) ⊔ rf (bounded_exec ex bound) ⊔
mo (bounded_exec ex bound) ⊔ rb (bounded_exec ex bound) ≦
sb ex ⊔ rf ex ⊔ mo ex ⊔ rb ex.
Proof.
unfold rb. rew bounded. rewrite 2dot_cnv, injcnv. kat.
Qed.
(** In a valid execution, if two events are related by [sb ex ⊔ rf ex], they
belong to the events of [ex] *)
Lemma sbrf_in_events (ex: Execution) (x y : Event) :
valid_exec ex ->
((sb ex) ⊔ (rf ex)) x y ->
In _ (evts ex) x /\ In _ (evts ex) y.
Proof.
intros Hval [Hsb | Hrf]; split;
eauto using sb_orig_evts, sb_dest_evts, rf_orig_evts, rf_dest_evts.
Qed.
(** If an event belongs to the events of an execution bounded by [n], its
numbering is less or equal to [n] and it belongs to the events of the execution *)
Lemma I_evts_bounded_le_bnd (ex: Execution) (n: nat):
[I (evts (bounded_exec ex n))] = [NLE n] ⋅ [I (evts ex)].
Proof.
apply ext_rel, antisym.
- intros x y [Heq Hinter]. destruct Hinter.
exists x; split; auto.
- intros x y [z [Heq Hr] [Heq1 Hr1]].
rewrite <- Heq in Hr1. rewrite Heq1 in Heq.
split; [|split]; auto.
Qed.
(** Any bounding of a valid execution is a prefix of this execution *)
Lemma bounded_exec_is_prefix (ex: Execution) (n: nat):
valid_exec ex ->
numbering_coherent ex ->
prefix (bounded_exec ex n) ex.
Proof.
intros Hval Hnumco.
split; [|split].
- apply intersection_included_itself.
- intros x y Hnum.
generalize (sbrf_in_events _ _ _ Hval Hnum); intros [Hx Hy].
apply (Hnumco _ _) in Hnum.
intros H. destruct H as [y Hevts Hbound]; split.
+ auto.
+ unfold_in; lia.
- rew bounded.
repeat (apply conj);
destruct_val_exec Hval.
+ destruct_sb_v Hsb_v.
destruct Hsb_lso as [Hsb_in_e _].
rewrite Hsb_in_e, I_evts_bounded_le_bnd. kat_eq.
+ destruct_rf_v Hrf_v. rewrite Hrf_in_e, I_evts_bounded_le_bnd. kat_eq.
+ destruct_mo_v Hmo_v. destruct Hmopo as [Hmo_in_e _].
rewrite Hmo_in_e, I_evts_bounded_le_bnd. kat_eq.
+ destruct_rmw_v Hrmw_v. rewrite Hrmw_in_e, I_evts_bounded_le_bnd. kat_eq.
Qed.
(** If an execution is valid, any of its boundings is valid *)
Lemma bounded_is_valid (ex: Execution) (bound: nat):
valid_exec ex ->
numbering_coherent ex ->
valid_exec (bounded_exec ex bound).
Proof.
intros Hval Hnumco.
eapply prefix_valid.
eauto.
eapply bounded_exec_is_prefix;
eauto.
Qed.
(** If an execution is complete, any of its boundings is complete *)
Lemma bounded_is_complete (ex: Execution) (bound: nat):
complete_exec ex ->
numbering_coherent ex ->
complete_exec (bounded_exec ex bound).
Proof.
intros Hcomp Hnumco.
eapply prefix_complete.
eauto.
eapply bounded_exec_is_prefix; auto.
destruct Hcomp as [Hval _]. auto.
Qed.
(** If an execution is consistent in the RC11 model, any of its boundings is
consistent in the RC11 model *)
Lemma bounded_is_rc11 (ex: Execution) (bound: nat):
valid_exec ex ->
numbering_coherent ex ->
rc11_consistent ex ->
rc11_consistent (bounded_exec ex bound).
Proof.
intros Hval Hnumco Hrc11.
eapply prefix_rc11_consistent.
eauto.
eapply bounded_exec_is_prefix;
eauto.
Qed.
(** If we have two boundings of an execution, the bounding bounded by the
smallest bound is a prefix of the bounding bounded by the biggest bound *)
Lemma two_ord_bounds_pre (ex: Execution) (k1 k2: nat):
valid_exec ex ->
numbering_coherent ex ->
k1 < k2 ->
prefix (bounded_exec ex k1) (bounded_exec ex k2).
Proof.
intros Hval Hnumco Hord.
inverse_val_exec Hval.
repeat (apply conj).
- destruct ex. apply inter_incl. intros x.
unfold In. intros H. lia.
- intros a b [Hsb|Hrf] Hin;
apply in_intersection in Hin as [Hevts Hbord]; unfold_in.
+ rew bounded in Hsb. apply simpl_trt_hyp in Hsb as [_ [Hr _]].
apply sb_num_ord in Hr as Habord; auto. split.
* eapply sb_orig_evts; eauto.
* unfold_in; lia.
+ rew bounded in Hrf. apply simpl_trt_hyp in Hrf as [_ [Hr _]].
apply rf_num_ord in Hr as Habord; auto. split.
* eapply rf_orig_evts; eauto.
* unfold_in; lia.
- rew bounded. rewrite I_evts_bounded_le_bnd.
rewrite <- (nle_double _ _ Hord) at 1.
rewrite <- (nle_double _ _ Hord) at 2.
destruct_sb_v Hsb_v.
destruct Hsb_lso as [Hsb_in_e _].
rewrite Hsb_in_e. kat_eq.
- rew bounded. rewrite I_evts_bounded_le_bnd.
rewrite <- (nle_double _ _ Hord) at 1.
rewrite <- (nle_double _ _ Hord) at 2.
destruct_rf_v Hrf_v. rewrite Hrf_in_e. kat_eq.
- rew bounded. rewrite I_evts_bounded_le_bnd.
rewrite <- (nle_double _ _ Hord) at 1.
rewrite <- (nle_double _ _ Hord) at 2.
destruct_mo_v Hmo_v. destruct Hmopo as [Hmo_in_e _].
rewrite Hmo_in_e. kat_eq.
- rew bounded. rewrite I_evts_bounded_le_bnd.
rewrite <- (nle_double _ _ Hord) at 1.
rewrite <- (nle_double _ _ Hord) at 2.
destruct_rmw_v Hrmw_v. rewrite Hrmw_in_e. kat_eq.
Qed.
(** There is a bound high enough so that the bounding of the execution is equal
to the execution *)
Lemma bounded_execution_itself_exists (ex: Execution):
valid_exec ex ->
exists k, ex = (bounded_exec ex k).
Proof.
destruct (numbering_bounded) as [k Hsup].
intros Hval.
exists (numbering k).
apply tautology_makes_fullset in Hsup. destruct ex.
unfold bounded_exec. rew bounded.
unfold NLE. rewrite Hsup. f_equal.
- simpl. erewrite inter_fullset. auto.
- unfold exec.sb. rewrite fullset_one. kat_eq.
- unfold exec.rmw. rewrite fullset_one. kat_eq.
- unfold exec.rf. rewrite fullset_one. kat_eq.
- unfold exec.mo. rewrite fullset_one. kat_eq.
Qed.
(** ** Smallest conflicting prefix *)
(** A bound encodes the smallest possible conflicting prefix if all the other
conflicting boundings are bounded by a bigger bound *)
Definition smallest_conflicting_bounding (ex: Execution) (bound: nat) :=
expi (bounded_exec ex bound) /\
(forall n, expi (bounded_exec ex n) ->
n >= bound).
Axiom smallest_conflicting_bounding_exists:
forall ex, expi ex ->
(exists bound, smallest_conflicting_bounding ex bound).
(** The boundings smaller than the smallest conflicting bounding are not
conflicting *)
Lemma smaller_than_smallest_not_conflicting (ex: Execution) (bound: nat):
(smallest_conflicting_bounding ex bound) ->
forall smaller, smaller < bound ->
~(expi (bounded_exec ex smaller)).
Proof.
intros [_ Hsmallest] smaller Hsmaller Hnot.
apply Hsmallest in Hnot.
lia.
Qed.
Theorem smaller_than_smallest_sc (ex: Execution) (bound: nat):
valid_exec ex ->
numbering_coherent ex ->
rc11_consistent ex ->
(smallest_conflicting_bounding ex bound) ->
forall smaller, smaller < bound ->
sc_consistent (bounded_exec ex smaller).
Proof.
intros Hval Hnumco Hrc11 Hscb smaller Hsmaller.
eapply no_conflict_prefix_sc; eauto.
- eauto using bounded_exec_is_prefix.
- eapply smaller_than_smallest_not_conflicting; eauto.
Qed.
(** ** Minimal conflicting pair *)
(** If an execution contains conflicts, there is a unique pair of events that
are in conflict and belong to the smallest conflicting prefix of the execution *)
Definition minimal_conflicting_pair (ex: Execution) (bound: nat) (j k: Event) :=
(smallest_conflicting_bounding ex bound) /\
(pi (bounded_exec ex bound) j k).
(** Two events forming a minimal conflicting pair can be equal *)
Lemma mcp_irr (ex: Execution) (bound: nat) (k: Event):
~(minimal_conflicting_pair ex bound k k).
Proof.
intros Hnot.
destruct Hnot as [_ Hnot].
apply pi_diff in Hnot.
intuition auto.
Qed.
(** The minimal conflicting pair of given execution and bound is a symmetric
relation *)
Lemma mcp_is_sym (ex: Execution) (bound: nat) (j k: Event):
(minimal_conflicting_pair ex bound j k) <->
(minimal_conflicting_pair ex bound k j).
Proof. compute; intuition eauto. Qed.
(** The two events and the bound forming the minimal conflicting pair of an
execution are such that the two events are pi-conflicting in the bounding of
the execution by the bound *)
Lemma mcp_is_pi (ex: Execution) (bound:nat) (j k: Event):
minimal_conflicting_pair ex bound j k ->
pi (bounded_exec ex bound) j k.
Proof. intros [_ ?]. auto. Qed.
(** The two events and the bound forming the minimal conflicting pair of an
execution are such that the two events belong to the events of the bounding of
the execution by the bound *)
Lemma mcp_in_evts_left (ex: Execution) (x y: Event) (bound:nat):
minimal_conflicting_pair ex bound x y ->
In _ (evts (bounded_exec ex bound)) x.
Proof. intros. eauto using pi_in_evts_left, mcp_is_pi. Qed.
Lemma mcp_in_evts_right (ex: Execution) (x y: Event) (bound:nat):
minimal_conflicting_pair ex bound x y ->
In _ (evts (bounded_exec ex bound)) y.
Proof. intros. eauto using pi_in_evts_right, mcp_is_pi. Qed.
Lemma mcp_in_evts_left2 (ex: Execution) (x y: Event) (bound: nat):
minimal_conflicting_pair ex bound x y ->
In _ (evts ex) x.
Proof.
intros Hmcp. apply mcp_in_evts_left in Hmcp.
destruct Hmcp; auto.
Qed.
Lemma mcp_in_evts_right2 (ex: Execution) (x y: Event) (bound: nat):
minimal_conflicting_pair ex bound x y ->
In _ (evts ex) y.
Proof.
intros Hmcp. apply mcp_in_evts_right in Hmcp.
destruct Hmcp; auto.
Qed.
(** One of the two events forming a minimal conflicting pair must be a write
event *)
Lemma mcp_one_is_write (ex: Execution) (x y: Event) (bound:nat):
minimal_conflicting_pair ex bound x y ->
is_write x \/ is_write y.
Proof. intros. eauto using pi_one_is_write, mcp_is_pi. Qed.
(** Two events forming a minimal conflicting pair are different *)
Lemma mcp_diff (ex: Execution) (x y: Event) (bound:nat):
minimal_conflicting_pair ex bound x y ->
x <> y.
Proof. intros. eauto using pi_diff, mcp_is_pi. Qed.
(** Two events forming a minimal conflicting pair affect the same location *)
Lemma mcp_same_loc (ex: Execution) (x y: Event) (bound:nat):
minimal_conflicting_pair ex bound x y ->
get_loc x = get_loc y.
Proof. intros. eauto using pi_same_loc, mcp_is_pi. Qed.
(** At least one of the two events forming a conflicting pair must be a SC
event *)
Lemma mcp_at_least_one_not_sc (ex: Execution) (x y: Event) (bound:nat):
minimal_conflicting_pair ex bound x y ->
at_least_one_not_sc x y.
Proof. intros. eauto using pi_at_least_one_not_sc, mcp_is_pi. Qed.
(** Two events forming a minimal conflicting pair must each be either a read or
a write *)
Lemma mcp_readwrite_l (ex: Execution) (x y: Event) (bound: nat):
minimal_conflicting_pair ex bound x y ->
(is_write x) \/ (is_read x).
Proof. intros. eauto using pi_readwrite_l, mcp_is_pi. Qed.
Lemma mcp_readwrite_r (ex: Execution) (x y: Event) (bound: nat):
minimal_conflicting_pair ex bound x y ->
(is_write y) \/ (is_read y).
Proof. intros. eauto using pi_readwrite_r, mcp_is_pi. Qed.
(** Two events forming a minimal conflicting pair are not ordered by the
transitive closure of the union of the sequenced-before relation and of the
restriction of the reads-from relation to SC events, in the execution bounded
by the minimal bound in either direction *)
Lemma mcp_not_sbrfsc (ex: Execution) (x y: Event) (bound:nat):
minimal_conflicting_pair ex bound x y ->
~((sb (bounded_exec ex bound) ⊔ (res_mode Sc (rf (bounded_exec ex bound))))^+ x y).
Proof. intros. eauto using pi_not_sbrfsc, mcp_is_pi. Qed.
Lemma mcp_not_cnv_sbrfsc (ex: Execution) (x y: Event) (bound:nat):
minimal_conflicting_pair ex bound x y ->
~((sb (bounded_exec ex bound) ⊔ (res_mode Sc (rf (bounded_exec ex bound))))^+ y x).
Proof. intros. eauto using pi_not_cnv_sbrfsc, mcp_is_pi. Qed.
(** The events forming a minimal conflicting pair have a numbering less or equal
to the minimal bound *)
Lemma mcp_left_le_bound (ex: Execution) (x y: Event) (bound:nat):
minimal_conflicting_pair ex bound x y ->
(numbering x) <= bound.
Proof.
intros Hmcp. eapply mcp_in_evts_left in Hmcp.
destruct Hmcp as [? _ Hxord]. unfold In in Hxord.
auto.
Qed.
Lemma mcp_right_le_bound (ex: Execution) (x y: Event) (bound:nat):
minimal_conflicting_pair ex bound x y ->
(numbering y) <= bound.
Proof.
intros Hmcp. eapply mcp_in_evts_right in Hmcp.
destruct Hmcp as [? _ Hxord]. unfold In in Hxord.
auto.
Qed.
(** The numbering of one of the two events forming a minimal conflicting pair
is equal to the minimal bound and the numbering of the other event is strictly
inferior to the minmal bound *)
Lemma mcp_left_eq_lt_bound (ex: Execution) (bound: nat) (x y: Event):
minimal_conflicting_pair ex bound x y ->
(numbering x) = bound \/ (numbering x) < bound.
Proof.
intros Hmcp.
destruct (Compare_dec.lt_eq_lt_dec (numbering x) bound) as [[Hord|Hord]|Hord];
[right;auto|left;auto|].
apply mcp_left_le_bound in Hmcp. lia.
Qed.
Lemma mcp_right_eq_lt_bound (ex: Execution) (bound: nat) (x y: Event):
minimal_conflicting_pair ex bound x y ->
(numbering y) = bound \/ (numbering y) < bound.
Proof.
intros Hmcp.
destruct (Compare_dec.lt_eq_lt_dec (numbering y) bound) as [[Hord|Hord]|Hord];
[right;auto|left;auto|].
apply mcp_right_le_bound in Hmcp. lia.
Qed.
(** Every execution containing pi-conflicting events has a minimal conflicting
pair *)
Lemma mcp_exists (ex: Execution):
expi ex ->
(exists bound j k, minimal_conflicting_pair ex bound j k).
Proof.
intros Hconf.
destruct (smallest_conflicting_bounding_exists _ Hconf) as [bound Hsmallest].
exists bound.
destruct Hsmallest as [[j [k Hpreconf]] Hsmallest].
exists j, k. split; [split|]; auto.
exists j, k. auto.
Qed.
(** Every execution containing pi-conflicting events has a minimal conflicting
pair with one of the events having the biggest numbering *)
Lemma mcp_exists_ord (ex: Execution):
expi ex ->
numbering_injective ex ->
(exists bound j k, minimal_conflicting_pair ex bound j k /\
(numbering j) < (numbering k)).
Proof.
intros Hexpi Hnuminj.
destruct (mcp_exists _ Hexpi) as [b [j [k Hmcp]]].
destruct (Compare_dec.lt_eq_lt_dec (numbering j) (numbering k)) as
[[Hcomp|Hcomp]|Hcomp].
- exists b, j, k. intuition auto.
- exfalso. eapply mcp_irr.
eapply numbering_injective_eq in Hcomp; eauto.
rewrite Hcomp in Hmcp. eauto.
- exists b, k, j. intuition auto.
eapply mcp_is_sym. auto.
Qed.
(** In a minimal conflicting pair, at least one of the two events is not SC *)
Lemma mcp_not_sc (ex: Execution) (bound: nat) (j k: Event):
(minimal_conflicting_pair ex bound j k) ->
~((get_mode j) = Sc /\ (get_mode k) = Sc).
Proof.
intros [_ [[_ H] _]].
auto.
Qed.
(** In a minimal conflicting pair, the two conflicting events cannot be related
by sb *)
Lemma mcp_not_sb_jk (ex: Execution) (bound: nat) (j k: Event):
minimal_conflicting_pair ex bound j k ->
~(sb ex j k).
Proof.
intros Hmcp Hsb.
inversion Hmcp as [_ [_ Hnot]].
apply Hnot. left. apply tc_incl_itself. left.
rew bounded. simpl_trt.
- eapply mcp_left_le_bound. eauto.
- auto.
- eapply mcp_right_le_bound. eauto.
Qed.
(*
(** In a valid execution, the set of events whose numbering in an execution
bounded by [n] is less or equal to a bound, is the same as the set of events
whose numbering in the execution is less or equal to the same bound *)
Lemma NLE_set_in_bound_ex_rew (ex: Execution) (b1 b2: nat):
valid_exec ex ->
(fun x => b2 >= (numbering x)) =
(fun x => b2 >= (numbering x)).
Proof.
intuition auto.
intros Hval.
pose proof (bounded_exec_is_prefix _ b1 Hval) as Hpre.
pose proof (numbering_pre_stable _ _ Hpre) as Hnumeq.
apply ext_set. split; intros H.
- rewrite Hnumeq in H. auto.
- rewrite Hnumeq. auto.
Qed.
Lemma NLE_in_bound_ex_rew (ex: Execution) (b1 b2: nat):
valid_exec ex ->
[NLE (bounded_exec ex b1) b2] = [NLE ex b2].
Proof.
intros Hval.
pose proof (bounded_exec_is_prefix _ b1 Hval) as Hpre.
pose proof (numbering_pre_stable _ _ Hpre) as Hnumeq.
apply ext_rel, antisym; intros x y H;
destruct H as [Heq Hord];
split; auto; unfold NLE in *.
- rewrite Hnumeq in Hord; auto.
- rewrite Hnumeq; auto.
Qed.
*)
(** Bounding an execution already bounded by a smaller bound has no effect *)
Lemma double_bounding_rew (ex: Execution) (b1 b2: nat):
valid_exec ex ->
b1 < b2 ->
bounded_exec (bounded_exec ex b1) b2 = bounded_exec ex b1.
Proof.
intros Hval Hord.
unfold bounded_exec at 1.
(*
rewrite (NLE_in_bound_ex_rew _ b1 b2 Hval).
rewrite (NLE_set_in_bound_ex_rew _ b1 b2 Hval).
*)
rew bounded. unfold bounded_exec at 2.
f_equal.
- apply ext_set. intros x; split; intros H.
+ destruct H as [y Hevtsb1 Hordb2].
unfold bounded_exec in Hevtsb1.
simpl in Hevtsb1. unfold In in Hevtsb1. auto.
+ split.
* unfold bounded_exec. simpl. unfold In. auto.
* destruct H as [y _ Hb1]. unfold_in. lia.
- rewrite <- (nle_double _ _ Hord) at 4.
rewrite <- (nle_double _ _ Hord) at 3.
kat_eq.
- rewrite <- (nle_double _ _ Hord) at 4.
rewrite <- (nle_double _ _ Hord) at 3.
kat_eq.
- rewrite <- (nle_double _ _ Hord) at 4.
rewrite <- (nle_double _ _ Hord) at 3.
kat_eq.
- rewrite <- (nle_double _ _ Hord) at 4.
rewrite <- (nle_double _ _ Hord) at 3.
kat_eq.
Qed.
(** Bounding an execution already bounded with a greater bound is the same as
directly bounding the execution with the smaller bound *)
Lemma double_bounding_rew' (ex: Execution) (b1 b2: nat):
valid_exec ex ->
b1 < b2 ->
bounded_exec (bounded_exec ex b2) b1 = bounded_exec ex b1.
Proof.
intros Hval Hord.
unfold bounded_exec at 1.
(*
rewrite (NLE_in_bound_ex_rew _ b2 b1 Hval).
rewrite (NLE_set_in_bound_ex_rew _ b2 b1 Hval).
*)
rew bounded. unfold bounded_exec at 2.
f_equal.
- apply ext_set. intros x; split; intros H.
+ destruct H as [y Hevtsb2 Hb1].
split; auto.
destruct Hevtsb2; auto.
+ destruct H as [y Hevts Hb1].
split; auto.
split; auto.
unfold_in; lia.
- rewrite <- (nle_double _ _ Hord) at 4.
rewrite <- (nle_double _ _ Hord) at 3.
kat_eq.
- rewrite <- (nle_double _ _ Hord) at 4.
rewrite <- (nle_double _ _ Hord) at 3.
kat_eq.
- rewrite <- (nle_double _ _ Hord) at 4.
rewrite <- (nle_double _ _ Hord) at 3.
kat_eq.
- rewrite <- (nle_double _ _ Hord) at 4.
rewrite <- (nle_double _ _ Hord) at 3.
kat_eq.
Qed.
(** Bouding an execution twice with the same bound is the same as bounding it
once *)
Lemma double_same_bounding_rew (ex: Execution) (b: nat):
valid_exec ex ->
bounded_exec (bounded_exec ex b) b = bounded_exec ex b.