-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathbasic.v
executable file
·4224 lines (3716 loc) · 151 KB
/
basic.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
(*********************************************************************)
(* Stability in Weak Memory Models *)
(* *)
(* Jade Alglave INRIA Paris-Rocquencourt, France *)
(* University of Oxford, UK *)
(* *)
(* Copyright 2010 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed *)
(* under the terms of the Lesser GNU General Public License. *)
(*********************************************************************)
Require Import Ensembles.
Require Import Arith.
From CoqCat Require Import util.
From CoqCat Require Import wmm.
Require Import Classical_Prop.
Import OEEvt.
Set Implicit Arguments.
(** * Basics about memory models
Lemmas about weak memory models. The Basic module takes an architecture and a
dependency module as parameters and assume a weak memory model based on them.
The facts stated in this module are thus independent of the memory model
considered
*)
Module Basic (A : Archi) (dp: Dp).
Import A.
Import dp.
Module AWmm := Wmm A dp.
Import AWmm.
Section Ax.
(** ** Events *)
(** An event can't be a write and a read at the same time *)
Lemma read_write_contrad :
forall x l1 l2,
~(write_to x l1 /\ read_from x l2).
Proof.
unfold write_to; unfold read_from;
intros x l1 l2 [[v1 Hw ] [v2 Hr]].
rewrite Hw in Hr; inversion Hr.
Qed.
(** If an event writes to a location, it must be a write event *)
Lemma write_to_implies_writes: (*basic*)
forall E x l,
(events E) x ->
write_to x l ->
(writes E) x.
Proof.
intros E x l He (*[v*) Hw(*]*); unfold writes; split; auto.
exists l; (*exists v;*) auto.
Qed.
(** If an event reads from a location, it must a read event *)
Lemma read_from_implies_reads: (*basic*)
forall E x l,
(events E) x ->
read_from x l ->
(reads E) x.
Proof.
intros E x l He (*[v*) Hw(*]*); unfold reads; split; auto.
exists l; (*exists v;*) auto.
Qed.
(** If an event reads from two locations, these locations are identical *)
Lemma read_from_implies_same_loc :
forall x l1 l2,
read_from x l1 ->
read_from x l2 ->
l1 = l2.
Proof.
unfold read_from;
intros x l1 l2 [v1 H1] [v2 H2].
rewrite H1 in H2; inversion H2; auto.
Qed.
(** In a valid execution, if a two events are related by the read-from relation,
then the first event is a write and the second is a read *)
Lemma rf_implies_same_loc :
forall E X w y l,
valid_execution E X ->
rf X w y ->
read_from y l ->
write_to w l.
Proof.
intros E X w y l Hv Hrf Hr.
destruct_valid Hv.
generalize (Hrf_cands w y Hrf); intros [? [? [l' [Hw [Hr' ?]]]]].
generalize (read_from_implies_same_loc Hr Hr'); intro Heq; subst; auto.
Qed.
(** In a well-formed execution witness, two events related by the read-from
relation affect the same location *)
Lemma rf_implies_same_loc2 :
forall E X w y,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
rf X w y ->
loc w = loc y.
Proof.
intros E X w y [Hwswf Hrfwf] Hrf.
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (Hrf_cands w y Hrf); intros [? [? [l [[v1 Hw] [[v2 Hr] ?]]]]].
unfold loc; rewrite Hw; rewrite Hr; auto.
Qed.
(** A write event is writing at its location *)
Lemma write_to_implies_this_loc :
forall y l,
write_to y l ->
loc y = (*Some*) l.
Proof.
intros x l [v Hw]; unfold loc; rewrite Hw; auto.
Qed.
(** In a well-formed execution witness, two events related by the write
serialization relation affect the same location *)
Lemma ws_implies_same_loc :
forall E X w y,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
ws X w y ->
loc w = loc y.
Proof.
intros E X w y [Hwswf Hrfwf] Hws.
destruct Hwswf as [? Hl].
generalize (Hl w y Hws); intros [l [[? Hw] [? Hy]]].
rewrite (write_to_implies_this_loc Hw);
rewrite (write_to_implies_this_loc Hy); trivial.
Qed.
(** In a well-formed execution witness, two events related by the from-read
relation affect the same location *)
Lemma fr_implies_same_loc :
forall E X w y,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
fr E X w y ->
loc w = loc y.
Proof.
intros E X w y Hs [Hw [Hy [wr [Hrf Hws]]]].
rewrite <- (ws_implies_same_loc X wr y Hs); auto.
eapply sym_eq.
eapply rf_implies_same_loc2; [apply Hs | apply Hrf].
Qed.
(** In a valid execution, the from-read relation relates some read events to
some write events *)
Lemma fr_implies_same_loc2 :
forall E X x y l,
valid_execution E X ->
fr E X x y ->
read_from x l ->
write_to y l.
Proof.
intros E X x y l Hv [Hew [Hey [z [Hrf Hws]]]] Hr.
destruct_valid Hv.
generalize (Hws_cands z y Hws); intros [ly [[? Hwz] [? Hwy]]].
assert (write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X)) as Hand.
split; split; auto.
generalize (rf_implies_same_loc2 X z x Hand Hrf); intro Heq.
unfold read_from in Hr; unfold write_to in Hwz.
destruct Hr as [Hvx Hax]; destruct Hwz as [Hvz Haz].
unfold loc in Heq; rewrite Hax in Heq; rewrite Haz in Heq;
inversion Heq as [Hl]; rewrite <- Hl; auto.
Qed.
(** A read event reads from its location *)
Lemma read_from_implies_this_loc :
forall y l,
read_from y l ->
loc y = (*Some*) l.
Proof.
intros x l [v Hw].
unfold loc; rewrite Hw; auto.
Qed.
(** If a write event writes to two locations, these locations are identical *)
Lemma write_to_implies_same_loc :
forall y l1 l2 v,
action y = Access W l1 v ->
write_to y l2 ->
l1 = l2.
Proof.
unfold write_to;
intros x l1 l2 v H1 [v2 H2 ].
rewrite H1 in H2; inversion H2.
trivial.
Qed.
(** If an event has the shape [Access W _ _], then it is a write event *)
Lemma write_implies_write_to :
forall x l v,
action x = Access W l v ->
write_to x l.
Proof.
intros x l v Hx; unfold write_to; exists v; auto.
Qed.
(** ** Program Order *)
(** Program order (without [iico]) is a transitive relation *)
Lemma pos_trans :
forall E x y z,
(po_strict E) x y ->
(po_strict E) y z ->
(po_strict E) x z.
Proof.
unfold po_strict;
intros E x y z [Hpxy [Hinf_xy [Hex Hey]]] [Hpyz [Hinf_yz [Heyb Hez]]].
split; [rewrite Hpxy; rewrite Hpyz; trivial |
split; [ | split; [apply Hex | apply Hez]]].
eapply lt_trans; [apply Hinf_xy | apply Hinf_yz].
Qed.
(** If two events are related by the sequence of program order and
intra-instruction order, they are related by the program order *)
Lemma po_iico_trans :
forall E x y z,
well_formed_event_structure E ->
(po_strict E) x y ->
(iico E) y z ->
(po_strict E) x z.
Proof.
unfold po_strict;
intros E x y z Hwf [Hpxy [Hinf_xy [Hex Hey]]] Hyz.
unfold well_formed_event_structure in Hwf.
destruct Hwf as [? [? [? [? [? [? [Heq ?]]]]]]].
generalize (Heq y z Hyz); intro Heqi.
rewrite <- Heqi.
split; [apply Hpxy | split; [apply Hinf_xy |
split; [apply Hex | ]]].
apply H2; exists y; apply Hyz.
Qed.
(** If two events are related by the sequence of intra-instruction order and
program order, they are related by the program order *)
Lemma iico_po_trans :
forall E x y z,
well_formed_event_structure E ->
(iico E) x y ->
(po_strict E) y z ->
(po_strict E) x z.
Proof.
unfold po_strict;
intros E x y z Hwf Hxy [Hpyz [Hinf_yz [Hey Hez]]].
unfold well_formed_event_structure in Hwf.
destruct Hwf as [? [? [? [? [? [? [Heq ?]]]]]]].
generalize (Heq x y Hxy); intro Heqi.
rewrite Heqi.
split; [apply Hpyz | split; [apply Hinf_yz |
split; [ | apply Hez]]].
apply H1; exists y; apply Hxy.
Qed.
(** Intra-instruction order is a transitive relation *)
Lemma iico_trans :
forall E x y z,
well_formed_event_structure E ->
(iico E) x y ->
(iico E) y z ->
(iico E) x z.
Proof.
intros E x y z Hwf Hxy Hyz.
destruct Hwf as [? [? [? [? [? [? [? Htrans]]]]]]].
unfold trans in Htrans; apply (Htrans x y z Hxy Hyz).
Qed.
(** In a well-formed event structure, program order is a transitive relation *)
Lemma po_trans :
forall E x y z,
well_formed_event_structure E ->
(po_iico E) x y ->
(po_iico E) y z ->
(po_iico E) x z.
Proof.
unfold po_iico;
intros E x y z Hwf Hxy Hyz.
inversion Hxy as [Hpo_xy | Hiico_xy];
inversion Hyz as [Hpo_yz | Hiico_yz].
left; eapply pos_trans; eauto.
left; eapply po_iico_trans; eauto.
left; eapply iico_po_trans; eauto.
right; eapply iico_trans; eauto.
Qed.
(** In a well-formed event structure, program order is irreflexive, and since
it is a transitive relation, it is also acyclic. *)
Lemma po_ac :
forall E x,
well_formed_event_structure E ->
~((po_iico E) x x).
Proof.
unfold not;
intros E x Hwf Hpo_iico.
unfold well_formed_event_structure in Hwf.
destruct Hwf as [? [? [? [? [Hac ?]]]]].
inversion Hpo_iico as [Hpo | Hiico].
unfold po_strict in Hpo.
destruct Hpo as [? [Hinf [? ?]]].
generalize (gt_irrefl (poi (iiid x))); intro Hc.
contradiction.
unfold acyclic in Hac; apply (Hac x);
apply trc_step; apply Hiico.
Qed.
(** In a well-formed event structure, two events executed on different threads
are not ordered by program order *)
Lemma diff_proc_implies_not_po :
forall E x y,
well_formed_event_structure E ->
proc_of x <> proc_of y ->
~(po_iico E x y).
Proof.
intros E x y Hwf Hdiff Hxy.
inversion Hxy as [Hpo | Hiico].
destruct Hpo as [Hpr ?].
unfold not in Hdiff; unfold proc_of in Hdiff.
apply (Hdiff Hpr).
destruct Hwf as [? [? [? [? [? [? [Heq ?]]]]]]].
generalize (Heq x y Hiico); intro Heqi.
unfold proc_of in Hdiff; unfold not in Hdiff; rewrite Heqi in Hdiff;
apply Hdiff; auto.
Qed.
(** In a well-formed event structure, two events executed on the same thread
are ordered by program order *)
Lemma same_proc_implies_po :
forall E x y,
well_formed_event_structure E ->
proc_of x = proc_of y ->
In _ (events E) x -> In _ (events E) y ->
po_iico E x y \/ po_iico E y x.
Proof.
intros E x y Hwf Heqp Hex Hey.
destruct (lt_eq_lt_dec x.(iiid).(poi) y.(iiid).(poi)) as [Horb | Hsup].
inversion Horb as [Hinf | Heq].
left; left; split; auto.
left; right.
destruct Hwf as [? [? [? [? [? [Hii ?]]]]]].
assert (events E x /\ events E y /\ poi (iiid x) = poi (iiid y)) as Hand.
split; [|split]; auto.
apply (Hii x y Hand).
right; left; split; auto.
Qed.
(** In a well-formed event structure, two events ordered by program order are
executed on the same processor *)
Lemma po_implies_same_proc :
forall E x y,
well_formed_event_structure E ->
In _ (events E) x -> In _ (events E) y ->
po_iico E x y -> proc_of x = proc_of y.
Proof.
intros E x y Hwf Hex Hey Hpo_xy.
destruct Hwf as [Ht ?].
apply Ht; auto.
Qed.
(** ** Write serialization *)
(** If a write serialization relation is well-formed, events related by it write
to the same location *)
Lemma ws_cands :
forall E X x e,
write_serialization_well_formed (events E) (ws X) ->
ws X x e ->
exists l : Location,
In _ (writes_to_same_loc_l (events E) l) x /\
In _ (writes_to_same_loc_l (events E) l) e.
Proof.
intros E X x e Hv Hws.
destruct Hv as [? Hws_cands]; apply (Hws_cands x e Hws).
Qed.
(** For any location, if:
- write serialization is a strict linear (i.e. total) order on the writes to
this location
- events related by write serialization write to the same location
Then, write serialization is an irreflexive relation
*)
Lemma ws_cy :
forall E X x,
(forall l : Location,
linear_strict_order
(rrestrict (ws X) (writes_to_same_loc_l (events E) l))
(writes_to_same_loc_l (events E) l)) ->
(forall x e, ws X x e ->
(exists l : Location,
In _ (writes_to_same_loc_l (events E) l) x /\
In _ (writes_to_same_loc_l (events E) l) e)) ->
~(ws X x x).
Proof.
intros E X x Hl Hcands.
unfold not; intro Hws;
generalize (Hcands x x Hws); intros [lx [[Hex Hwx] ?]].
destruct (Hl lx) as [Hdr [Htrans [Hac Htot]]].
generalize (Hac x); intro Hn.
unfold not in Hn; apply Hn; split;
[apply Hws | unfold In; unfold writes_to_same_loc_l].
split; [split; [apply Hex | apply Hwx] |
split; [apply Hex | apply Hwx]].
Qed.
(** For any location, if:
- write serialization is a strict linear (i.e. total) order on the writes to
this location
- events related by write serialization write to the same location
Then any events related by write serialization belong to the events of the
event structure
*)
Lemma ws_evt_right :
forall E X x y,
(forall l : Location,
linear_strict_order
(rrestrict (ws X) (writes_to_same_loc_l (events E) l))
(writes_to_same_loc_l (events E) l)) ->
(forall x e, ws X x e ->
(exists l : Location,
In _ (writes_to_same_loc_l (events E) l) x /\
In _ (writes_to_same_loc_l (events E) l) e)) ->
ws X x y ->
In _ (events E) y.
Proof.
intros E X x y Hlin Hcands Hws.
generalize (Hcands x y Hws); intros [l [[Hex Hwx] [Hey Hwy]]];
apply Hey.
Qed.
Lemma ws_evt_left :
forall E X x y,
(forall l : Location,
linear_strict_order
(rrestrict (ws X) (writes_to_same_loc_l (events E) l))
(writes_to_same_loc_l (events E) l)) ->
(forall x e, ws X x e ->
(exists l : Location,
In _ (writes_to_same_loc_l (events E) l) x /\
In _ (writes_to_same_loc_l (events E) l) e)) ->
ws X x y ->
In _ (events E) x.
Proof.
intros E X x y Hlin Hcands Hws.
generalize (Hcands x y Hws); intros [l [[Hex Hwx] [Hey Hwy]]];
apply Hex.
Qed.
(** For any location, if:
- write serialization is a strict linear (i.e. total) order on the writes to
this location
- events related by write serialization write to the same location
Then write serialization always relates an event to a write
*)
Lemma ws_right :
forall E X x y,
(forall l : Location,
linear_strict_order
(rrestrict (ws X) (writes_to_same_loc_l (events E) l))
(writes_to_same_loc_l (events E) l)) ->
(forall x e, ws X x e ->
(exists l : Location,
In _ (writes_to_same_loc_l (events E) l) x /\
In _ (writes_to_same_loc_l (events E) l) e)) ->
ws X x y ->
exists v, exists l, action y = Access W l v.
Proof.
intros E X x y Hlin Hcands Hws.
generalize (Hcands x y Hws); intros [l [[Hex Hwx] [Hey Hwy]]].
case_eq (action y).
intros d ly v Hy.
case_eq d.
intro Hr; unfold write_to in Hwy; rewrite Hy in Hwy; rewrite Hr in Hwy;
destruct Hwy as [vy Hwy]; inversion Hwy.
intro Hw; exists v; exists ly; trivial.
Qed.
(** The domain and the range of a well-formed write serialization relation
contains only write events *)
Lemma dom_ws_is_write :
forall E X x y,
write_serialization_well_formed (events E) (ws X) ->
ws X x y ->
exists l, exists v, action x = Access W l v.
Proof.
intros E X x y [? Hws_cands] Hws.
generalize (Hws_cands x y Hws); intros [l [[Hex Hwx] [Hey Hwy]]].
case_eq (action x).
intros d lx v Hx.
case_eq d.
intro Hr; unfold write_to in Hwx; rewrite Hx in Hwx; rewrite Hr in Hwx;
destruct Hwx as [vx Hwx]; inversion Hwx.
intro Hw; exists lx; exists v; trivial.
Qed.
Lemma ran_ws_is_write :
forall E X x y,
write_serialization_well_formed (events E) (ws X) ->
ws X x y ->
exists v, exists l, action y = Access W l v.
Proof.
intros E X x y [Hws_tot Hws_cands] Hws.
apply (ws_right E X x y Hws_tot Hws_cands Hws).
Qed.
(** A well-formed write serialization relation is transitive *)
Lemma ws_trans :
forall E X x y z,
write_serialization_well_formed (events E) (ws X) ->
ws X x y -> ws X y z ->
ws X x z.
Proof.
intros E X x y z [Hws_tot Hws_cands] Hxy Hyz.
generalize (ws_right E X x y Hws_tot Hws_cands Hxy); intros [v [l Hy]].
generalize (Hws_tot l); intros [Hdr [Htrans [Hac Htot]]].
assert (rrestrict (ws X) (writes_to_same_loc_l (events E) l) x y) as Hxyb.
split; [apply Hxy |].
generalize (Hws_cands x y Hxy); intros [lx [Hlx Hlxy]].
generalize Hlxy; intro Hlxyb.
destruct Hlxy as [? Hwlxy].
generalize (write_to_implies_same_loc Hy Hwlxy); intro Heq.
rewrite Heq; split; auto.
assert (rrestrict (ws X) (writes_to_same_loc_l (events E) l) y z) as Hyzb.
split; [apply Hyz |].
destruct Hxyb as [? [? Hly]].
split; [apply Hly |].
generalize (Hws_cands y z Hyz); intros [ly [Hlyy Hlyz]].
destruct Hlyy as [? Hwlyy].
generalize (write_to_implies_same_loc Hy Hwlyy); intro Heq.
rewrite Heq; auto.
assert (rrestrict (ws X) (writes_to_same_loc_l (events E) l) x y /\
rrestrict (ws X) (writes_to_same_loc_l (events E) l) y z) as Hand.
split; auto.
generalize (Htrans x y z Hand); intros [Hxz ?].
auto.
Qed.
(** ** Read-from *)
(** The domain of a read-from relation contains only write events *)
Lemma dom_rf_is_write :
forall E X x y,
(forall e1 e2 : Event, rf X e1 e2 -> rfmaps (events E) e1 e2) ->
rf X x y ->
exists l, exists v, action x = Access W l v.
Proof.
intros E X x y Hrf_cands Hxy.
case_eq (action x).
intros dx lx vx Hx.
case_eq dx.
intro Hr.
generalize (Hrf_cands x y Hxy); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold write_to in Hwx; rewrite Hx in Hwx; rewrite Hr in Hwx;
destruct Hwx as [v Hwx]; inversion Hwx.
intro Hw; rewrite Hw in Hx.
exists lx; exists vx; trivial.
Qed.
(** The range of a read-from relation contains only read events *)
Lemma ran_rf_is_read :
forall E X x y,
(forall e1 e2 : Event, rf X e1 e2 -> rfmaps (events E) e1 e2) ->
rf X x y ->
exists l, exists v, action y = Access R l v.
Proof.
intros E X x y Hrf_cands Hxy.
case_eq (action y).
intros dy ly vy Hy.
case_eq dy.
intro Hr; rewrite Hr in Hy.
exists ly; exists vy; trivial.
intro Hw.
generalize (Hrf_cands x y Hxy); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold read_from in Hry; rewrite Hy in Hry; rewrite Hw in Hry;
destruct Hry as [[v Hry] ?]; inversion Hry.
Qed.
(** If two events are related to a read event by a well-formed read-from
relation, these two events are identical *)
Lemma rf_uni :
forall E X x w1 w2,
rfmaps_well_formed E (events E) (rf X) ->
rf X w1 x -> rf X w2 x ->
w1 = w2.
Proof.
intros E X x w1 w2 Hrfwf Hxy.
destruct Hrfwf as [? [? Hrf_uni]].
apply Hrf_uni; [apply Hxy].
Qed.
(** In a well-formed event structure, both the domain and the range of a
well-formed read-from relation belong to the events of the event structure *)
Lemma dom_rf_in_events :
forall E X x e,
well_formed_event_structure E ->
rfmaps_well_formed E (events E) (rf X) ->
(rf X) x e ->
In _ (events E) x.
Proof.
intros E X x e Hwf Hrfwf Hrf.
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (Hrf_cands x e Hrf); unfold rfmaps; intro Hrfmap.
destruct Hrfmap as [Hevt_x Hrest]; exact Hevt_x.
Qed.
Lemma ran_rf_in_events :
forall E X x e,
well_formed_event_structure E ->
rfmaps_well_formed E (events E) (rf X) ->
(rf X) x e ->
In _ (events E) e.
Proof.
intros E X x e Hwf Hrfwf Hrf.
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (Hrf_cands x e Hrf); unfold rfmaps; intro Hrfmap.
destruct Hrfmap as [Hevt_x [Hevt_e Hrest]]; exact Hevt_e.
Qed.
(** ** [mrf] Read-from *)
(** The domain of [mrf] contains only writes *)
Lemma dom_mrf_is_write :
forall E X x y,
(forall e1 e2 : Event, rf X e1 e2 -> rfmaps (events E) e1 e2) ->
mrf X x y ->
exists l, exists v, action x = Access W l v.
Proof.
case_eq inter; case_eq intra; intros Hinter Hintra; unfold mrf;
unfold mrfi; unfold mrfe; rewrite Hinter; rewrite Hintra;
intros E X x y Hrf_cands Hxy; simpl in Hxy; inversion Hxy as [Hrfi | Hrfe].
case_eq (action x).
intros dx lx vx Hx.
case_eq dx.
intro Hr.
destruct Hrfi as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold write_to in Hwx; rewrite Hx in Hwx; rewrite Hr in Hwx;
destruct Hwx as [v Hwx]; inversion Hwx.
intro Hw; rewrite Hw in Hx.
exists lx; exists vx; trivial.
case_eq (action x).
intros dx lx vx Hx.
case_eq dx.
intro Hr.
destruct Hrfe as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold write_to in Hwx; rewrite Hx in Hwx; rewrite Hr in Hwx;
destruct Hwx as [v Hwx]; inversion Hwx.
intro Hw; rewrite Hw in Hx.
exists lx; exists vx; trivial.
inversion Hrfi.
case_eq (action x).
intros dx lx vx Hx.
case_eq dx.
intro Hr.
destruct Hrfe as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold write_to in Hwx; rewrite Hx in Hwx; rewrite Hr in Hwx;
destruct Hwx as [v Hwx]; inversion Hwx.
intro Hw; rewrite Hw in Hx.
exists lx; exists vx; trivial.
case_eq (action x).
intros dx lx vx Hx.
case_eq dx.
intro Hr.
destruct Hrfi as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold write_to in Hwx; rewrite Hx in Hwx; rewrite Hr in Hwx;
destruct Hwx as [v Hwx]; inversion Hwx.
intro Hw; rewrite Hw in Hx.
exists lx; exists vx; trivial.
inversion Hrfe.
inversion Hrfi.
inversion Hrfe.
Qed.
(** The range of [mrf] contains only reads *)
Lemma ran_mrf_is_read :
forall E X x y,
(forall e1 e2 : Event, rf X e1 e2 -> rfmaps (events E) e1 e2) ->
mrf X x y ->
exists l, exists v, action y = Access R l v.
Proof.
case_eq inter; case_eq intra; intros Hinter Hintra; unfold mrf;
unfold mrfi; unfold mrfe; rewrite Hinter; rewrite Hintra;
intros E X x y Hrf_cands Hxy; simpl in Hxy; inversion Hxy as [Hrfi | Hrfe].
case_eq (action y).
intros dy ly vy Hy.
case_eq dy.
intro Hr; rewrite Hr in Hy.
exists ly; exists vy; trivial.
intro Hw.
destruct Hrfi as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold read_from in Hry; rewrite Hy in Hry; rewrite Hw in Hry;
destruct Hry as [[v Hry] ?]; inversion Hry.
case_eq (action y).
intros dy ly vy Hy.
case_eq dy.
intro Hr; rewrite Hr in Hy.
exists ly; exists vy; trivial.
intro Hw.
destruct Hrfe as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold read_from in Hry; rewrite Hy in Hry; rewrite Hw in Hry;
destruct Hry as [[v Hry] ?]; inversion Hry.
inversion Hrfi.
case_eq (action y).
intros dy ly vy Hy.
case_eq dy.
intro Hr; rewrite Hr in Hy.
exists ly; exists vy; trivial.
intro Hw.
destruct Hrfe as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold read_from in Hry; rewrite Hy in Hry; rewrite Hw in Hry;
destruct Hry as [[v Hry] ?]; inversion Hry.
case_eq (action y).
intros dy ly vy Hy.
case_eq dy.
intro Hr; rewrite Hr in Hy.
exists ly; exists vy; trivial.
intro Hw.
destruct Hrfi as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold read_from in Hry; rewrite Hy in Hry; rewrite Hw in Hry;
destruct Hry as [[v Hry] ?]; inversion Hry.
inversion Hrfe.
inversion Hrfi.
inversion Hrfe.
Qed.
(** If [mrf] relates two events to a single event, these two events are
identical *)
Lemma mrf_uni :
forall E X x w1 w2,
rfmaps_well_formed E (events E) (rf X) ->
mrf X w1 x -> mrf X w2 x ->
w1 = w2.
Proof.
case_eq inter; case_eq intra; intros Hinter Hintra; unfold mrf;
unfold mrfi; unfold mrfe; rewrite Hinter; rewrite Hintra; simpl;
intros E X x w1 w2 Hrfwf H1 H2; destruct Hrfwf as [? [? Hrf_uni]];
inversion H1 as [Hrfi1 | Hrfe1]; inversion H2 as [Hrfi2 | Hrfe2].
destruct Hrfi1 as [Hrf1 ?]; destruct Hrfi2 as [Hrf2 ?];
apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
destruct Hrfi1 as [Hrf1 ?]; destruct Hrfe2 as [Hrf2 ?];
apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
destruct Hrfe1 as [Hrf1 ?]; destruct Hrfi2 as [Hrf2 ?];
apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
destruct Hrfe1 as [Hrf1 ?]; destruct Hrfe2 as [Hrf2 ?];
apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
inversion Hrfi1.
inversion Hrfi1.
inversion Hrfi2.
destruct Hrfe1 as [Hrf1 ?]; destruct Hrfe2 as [Hrf2 ?];
apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
destruct Hrfi1 as [Hrf1 ?]; destruct Hrfi2 as [Hrf2 ?];
apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
inversion Hrfe2.
inversion Hrfe1.
inversion Hrfe2.
inversion Hrfi2.
inversion Hrfe2.
inversion Hrfi2.
inversion Hrfe2.
Qed.
(** If [mrf] and read-from relate two writes to a single event, these two
writes are identical *)
Lemma mrf_rf_uni :
forall E X x w1 w2,
rfmaps_well_formed E (events E) (rf X) ->
mrf X w1 x -> rf X w2 x ->
w1 = w2.
Proof.
case_eq inter; case_eq intra; intros Hinter Hintra; unfold mrf;
unfold mrfi; unfold mrfe; rewrite Hinter; rewrite Hintra; simpl;
intros E X x w1 w2 Hrfwf H1 Hrf2; destruct Hrfwf as [? [? Hrf_uni]];
inversion H1 as [Hrfi1 | Hrfe1].
destruct Hrfi1 as [Hrf1 ?]; apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
destruct Hrfe1 as [Hrf1 ?]; apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
inversion Hrfi1.
destruct Hrfe1 as [Hrf1 ?]; apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
destruct Hrfi1 as [Hrf1 ?]; apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
inversion Hrfe1.
inversion Hrfi1.
inversion Hrfe1.
Qed.
(** From-read *)
(** If from-read relates two events, then there is a third event such that:
- Read-from relates the third and first event;
- Write serialization relate the third and second event
*)
Lemma fr_ax1 :
forall E X x y,
fr E X x y ->
exists wr, rf X wr x /\ ws X wr y.
Proof.
intros E X x y Hxy.
destruct Hxy as [? [? Hxy]]; auto.
Qed.
(**
In a well-formed event structure, with a well-formed execution witness, if there
exists an event related to x by read-from and to y by write serialization,
then from-read relate x and y
*)
Lemma fr_ax2 :
forall E X x y,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(exists wr, rf X wr x /\ ws X wr y) ->
fr E X x y.
Proof.
intros E X x y Hwf Hvalid Hxy.
generalize Hvalid; intro Hv.
destruct Hvalid as [Hwswf Hrfwf].
destruct Hxy as [? [Hrf Hws]]; split; [| split].
eapply ran_rf_in_events; [apply Hwf | apply Hrfwf | apply Hrf].
destruct Hwswf as [Hws_tot Hws_cands].
eapply ws_evt_right; [apply Hws_tot | apply Hws_cands | apply Hws].
exists x0; auto.
Qed.
(** In an execution witness with a well-formed read-from relation, the domain
of the from-read relation is composed entirely of reads *)
Lemma dom_fr_is_read :
forall E X x y,
rfmaps_well_formed E (events E) (rf X) ->
fr E X x y ->
exists l, exists v, action x = Access R l v.
Proof.
intros E X x y Hvalid Hxy.
generalize (fr_ax1 Hxy); intros [? [Hrf Hws]].
destruct Hvalid as [? [Hrf_cands ?]].
eapply ran_rf_is_read; [apply Hrf_cands | apply Hrf].
Qed.
(** In an execution witness with a well-formed write serialization relation, the
range of the from-read relation is composed entirely of writes *)
Lemma ran_fr_is_write :
forall E X x y,
write_serialization_well_formed (events E) (ws X) ->
fr E X x y ->
exists v, exists l, action y = Access W l v.
Proof.
intros E X x y Hvalid Hxy.
generalize (fr_ax1 Hxy); intros [? [Hrf Hws]].
eapply ran_ws_is_write; [apply Hvalid | apply Hws].
Qed.
End Ax.
(** ** Domain and Ranges *)
Section DomRan.
(** *** Program order *)
(** Two events related by the program order (without [iico]) of an event struct
belong to the events of this event structure *)
Lemma po_strict_domain_in_events (E:Event_struct) (e e0:Event) :
(po_strict E) e e0 ->
In _ (events E) e.
Proof.
unfold po_strict; unfold In; intros Hin.
destruct Hin as [Hproc [Hpoi [He He0]]].
exact He.
Qed.
Lemma po_strict_range_in_events (E:Event_struct) (e e0:Event) :
(po_strict E) e e0 ->
In _ (events E) e0.
Proof.
unfold po_strict; unfold In; intros Hin.
destruct Hin as [Hproc [Hpoi [He He0]]].
exact He0.
Qed.
(** *** Intra-instruction order *)
(** In a well-formed event structure, the domain and the range of the
intra-instruction order contain only events of the event structure *)
Lemma iico_domain_incl_in_events (E:Event_struct) (e e0: Event) :
(well_formed_event_structure E) ->
iico E e e0 -> In _ (events E) e.
Proof.
unfold well_formed_event_structure.
intros Hwf.
destruct Hwf as [? Hwf].
destruct Hwf as [Hsame_eiid_iiid Hwf].
destruct Hwf as [Hdomain_intra Hwf].
destruct Hwf as [Hrange_intra Hwf].
intros He_in_range_intra.
assert (In _ (dom (iico E)) e).
unfold ran; unfold In; exists e0; exact He_in_range_intra.
unfold Included in Hdomain_intra; apply Hdomain_intra; exact H0.
Qed.
Lemma iico_range_incl_in_events (E:Event_struct) (e e0: Event) : (* basic *)
(well_formed_event_structure E) ->
iico E e e0 -> In _ (events E) e0.
Proof.
unfold well_formed_event_structure.
intros Hwf.
destruct Hwf as [? Hwf].
destruct Hwf as [Hsame_eiid_iiid Hwf].
destruct Hwf as [Hdomain_intra Hwf].
destruct Hwf as [Hrange_intra Hwf].
intros He0_in_domain_intra.
assert (In _ (ran (iico E)) e0).
unfold range; unfold In; exists e; exact He0_in_domain_intra.
unfold Included in Hrange_intra; apply Hrange_intra; exact H0.
Qed.
(** In a well-formed event structure, the domain and the range of the