-
Notifications
You must be signed in to change notification settings - Fork 0
/
sc.v
executable file
·1638 lines (1378 loc) · 60.3 KB
/
sc.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.
Require Import Bool.
From CoqCat Require Import util.
From CoqCat Require Import wmm.
From CoqCat Require Import basic.
From CoqCat Require Import hierarchy.
Set Implicit Arguments.
(** * Sequentially consistent execution
In this module, we define
- A notion of sequential execution
- A way to extract an SC execution witness from a sequential execution
- Two different possible implementation of a sequentially consistant memory models
- Lemmas that relate these three notions together *)
Module Sc (dp : Dp).
Import dp.
(** ** Definition *)
(** Create a relation that relates the event [er] to all the write events of
the event structure E that precede [er] in a relation [r] *)
Definition previous_writes (E:Event_struct) (r : Rln Event) (er:Event) :=
fun ew => writes E ew /\ r ew er /\ loc ew = loc er.
(* begin hide *)
Set Implicit Arguments.
(* end hide *)
(** Given a set [xs] and a relation [r] on this set, the set of maximum elements
is such that :
- all its elements belong to [xs]
- for any element [x] of the set of maximum elements, if there is an element [x'] belonging to [xs], then [x = x']
Simply put, all the elements of [xs] that are related to no elements or to themselves.
*)
Definition maximal_elements (A:Set) (xs:set A) (r:Rln A) : set A :=
fun x => In _ xs x /\ forall x', In _ xs x'/\ r x x' -> (x = x').
(* begin hide *)
Unset Implicit Arguments.
(* end hide *)
(** A sequential execution on an event structure is an order on the events of this structure such that:
- this order is a strict linear order (i.e. it is total)
- the program order is included in this order *)
Definition seq_exec (E:Event_struct) (so:Rln Event) : Prop :=
linear_strict_order so (events E) /\
rel_incl (po_iico E) so.
(** ** Building a SC execution witness
We show how to build an execution witness (a read-from relation and a write serialization from a sequential execution *)
(** *** read-from of SC execution *)
(** Two events are related by the read-from relation extracted from the sequential execution if:
- they are events from the domain or the range of the sequential execution
- the first one is a write event and the second one is a read event
- they access the same location
- they read/write the same value
- the first event belongs to the maximal elements of the previous writes (w.r.t. to the sequential execution) of the second event. Simply put, the first event
is the most recent write before the second event in the sequential execution *)
Definition so_rfm (E:Event_struct) (so : Rln Event) :=
fun ew => fun er =>
(rfmaps (udr so)) ew er /\
(maximal_elements
(previous_writes E so er) so) ew.
(** For any sequential execution on a event structure, for every read event in this structure, there is a write such that the read-from extracted from the sequential execution relates the write event to the read event *)
Hypothesis so_rfm_init :
forall E so,
forall er, In _ (reads E) er ->
exists ew, In _ (events E) ew /\ so_rfm E so ew er .
(** *** write serialization of sequential execution *)
(** Two events are related by the write serialization extracted from the sequential execution if:
- They are related by the sequential execution
- They are both writes to the same location *)
Definition so_ws (so:Rln Event) : (Rln Event) :=
fun e1 => fun e2 =>
so e1 e2 /\
exists l, In _ (writes_to_same_loc_l (udr so) l) e1 /\
In _ (writes_to_same_loc_l (udr so) l) e2.
(** ** Definition of a SC witness
A SC witness associated to an event structure and a sequential execution is composed of the read-from relation and write serialization extracted from the sequential execution.
*)
Definition sc_witness (E:Event_struct) (so:Rln Event) : Execution_witness :=
mkew (so_ws so) (so_rfm E so).
(** ** An SC-compatible architecture
The definition of [AiSc] is exactly the same as the one of its module type [Archi], but it adds an extra hypothesis [ab_sc_compat]. The goal of this extra-hypothesis is to ensure that the barrier relation will not enforce an ordering on events that would be incoherent with an SC architecture *)
Module AiSc <: Archi.
(** The preserved program order of the architecture is arbitrary but it respect the properties defined in [Archi] *)
Parameter ppo : Event_struct -> Rln Event.
Hypothesis ppo_valid : forall E, rel_incl (ppo E) (po_iico E).
Hypothesis ppo_fun :
forall E s x y,
ppo E x y /\ s x /\ s y <->
ppo (mkes (Intersection Event (events E) s) (rrestrict (iico E) s)) x y.
(** The global read-from relation is arbitrary *)
Parameter inter : bool.
Parameter intra : bool.
(** The barrier relation is arbitrary but it respects the properties defined in [Archi] and the extra hypothesis [ab_sc_compat] *)
Parameter abc : Event_struct -> Execution_witness -> Rln Event.
(** The barrier relation must be included in the sequence of:
- The reflexive closure of read-from
- The sequence of the program order and of the reflexive closure of read-from
This condition disallows the three following scenarios:
- An event [e1] must occur before an event [e2] according to the barrier, but [e2] must occur before [e1] according to the program order. Since we are on a
SC architecture, all the program order is preserved an this situation creates
a conflict.
- An event [e] must occur before a write [w] according to the barrier, and a read [r] that reads the value written by [w] must occur before [e] according to the program order.
- An read [r] must occur before an event [e] according to the barrier and reads a value written by a write [w], but [w] must occur after [e] according to program order.
*)
Parameter ab_sc_compat :
forall E X, rel_incl (abc E X) (rel_seq (maybe (rf X)) (rel_seq (po_iico E) (maybe (rf X)))).
Hypothesis ab_evts : forall (E:Event_struct) (X:Execution_witness),
forall x y, well_formed_event_structure E ->
rfmaps_well_formed E (events E) (rf X) ->
abc E X x y -> In _ (events E) x /\ In _ (events E) y.
Hypothesis ab_incl :
forall E X, rel_incl (abc E X) (tc (rel_union (com E X) (po_iico E))).
Hypothesis ab_fun :
forall E X s x y,
well_formed_event_structure E ->
rfmaps_well_formed E (events E) (rf X) ->
(abc E X x y /\ s x /\ s y <->
abc (mkes (Intersection Event (events E) s) (rrestrict (iico E) s))
(mkew (rrestrict (ws X) s) (rrestrict (rf X) s)) x y).
Parameter stars : Event_struct -> set Event.
End AiSc.
Import AiSc.
(** ** Lemmas about SC executions
The module [ScAx] takes an architecture as a parameter, and contains lemmas about SC executions *)
Module ScAx (A:Archi).
Definition bimpl (b1 b2:bool) : Prop:=
if (negb b1) || b2 then True else False.
(** This is an alias of boolean implication, aimed at the comparison of the global read-from relation of two architectures *)
Definition rf_impl (rf1 rf2 : bool) :=
bimpl rf1 rf2.
(** This is an alias of relation inclusion for any possible event structure, aimed at the comparison of the preserved program order of two architectures *)
Definition ppo_incl (ppo1 ppo2 : Event_struct -> Rln Event) :=
forall E, rel_incl (ppo1 E) (ppo2 E).
(** This is an alias of relation inclusion for any possible event structure and any possible execution witness, aimed at the comparison of the barrier relation of two architectures *)
Definition ab_incl (ab1 ab2 : Event_struct -> Execution_witness -> Rln Event) :=
forall E X, rel_incl (ab1 E X) (ab2 E X).
(** We suppose that:
- The preserved program order of [A] is included in the preserved program order of [AiSc] in any event structure
- If the intra-threads read-froms are global on [A], they are global on [AiSc]
- If the inter-threads read-froms are global on [A], they are global on [AiSc]
- The barrier relation of [A] is include in the barrier relation of [AiSc] in any event structure and for any execution witness
I.e. we suppose that [A] is weaker than [AiSc] *)
Hypothesis AwkAiSc :
ppo_incl (A.ppo) (AiSc.ppo) /\
bimpl (A.intra) (AiSc.intra) /\
bimpl (A.inter) (AiSc.inter) /\
ab_incl (A.abc) (AiSc.abc).
(** We immport the basic facts about A and we build a weak memory model on it *)
Module ABasic := Basic A dp.
Import ABasic.
Module AWmm := Wmm A dp.
Import AWmm.
Import A.
(** We define the SC check condition, which is the acyclicity of the program order and of the communication relation. This corresponds to the ghb acyclicity part of the condition of the generic condition of validity. Indeed, on an SC architectures, there are no barriers, all the program order is preserved and the whole read-from relation is global *)
Definition sc_check (E:Event_struct) (X:Execution_witness) : Prop :=
acyclic (rel_union (po_iico E) (com E X)).
(** *** Validy of SC execution
We show that an SC execution is valid on any architecture *)
Section sc_valid.
(** The domain and the range of a write serialization extracted from a sequential execution are included in the events of the event structure of this sequential execution *)
Lemma so_ws_dom_ran_wf :
forall E so l,
seq_exec E so ->
Included _
(Union _
(dom (rrestrict (so_ws so) (writes_to_same_loc_l (events E) l)))
(ran (rrestrict (so_ws so) (writes_to_same_loc_l (events E) l)))) (* = *)
(writes_to_same_loc_l (events E) l).
Proof.
intros E so l Hsc.
unfold Included; intros x Hx.
inversion Hx as [e Hd | e Hr].
unfold dom in Hd; unfold In in Hd; unfold rrestrict in Hd.
destruct Hd as [y [Hso [Hmx Hmy]]]; apply Hmx.
unfold ran in Hr; unfold In in Hr; unfold rrestrict in Hr.
destruct Hr as [y [Hso [Hmy Hmx]]]; apply Hmx.
Qed.
(** The write serialization extracted from a sequential execution is a well-formed write serialization *)
Lemma sc_ws_wf :
forall E so,
seq_exec E so ->
write_serialization_well_formed (events E) (so_ws so).
Proof.
intros E so Hsc_ord; split.
(*lin*)
intro l;split.
(*dom/ran*)
eapply (so_ws_dom_ran_wf). apply Hsc_ord.
destruct Hsc_ord as [[Hdr [Htrans [Hac Htot]]] Hincl]; split.
(*trans*)
intros x1 x2 x3 H123; destruct H123 as [H12 H23].
unfold In in * |- * ; unfold rrestrict in * |- * ;
destruct H12 as [Hso12 [H1 H2]]; destruct H23 as [Hso23 [H2' H3]];
split; [| split; [exact H1 | exact H3]].
unfold In in * |- *; unfold so_ws in * |- *;
destruct Hso12 as [Hso12 Hl12]; destruct Hso23 as [Hso23 Hl23]; split;
[unfold In; eapply Htrans; split; [apply Hso12 | apply Hso23] |
exists l; split].
unfold writes_to_same_loc_l; unfold In; split.
unfold udr; apply incl_union_left_in; exists x2; apply Hso12.
destruct H1 as [Hevt1 Hw1]; apply Hw1.
unfold writes_to_same_loc_l; unfold In; split.
unfold udr; apply incl_union_right_in; exists x2; apply Hso23.
destruct H3 as [Hevt3 Hw3]; apply Hw3.
split.
(*ac*)
unfold not; intros x Hx; destruct Hx as [[Hso Hl] Hrest]; unfold not in Hac;
apply (Hac x); exact Hso.
(*tot*)
intros x1 x2 Hdiff H1 H2.
assert (In _ (events E) x1) as Hevt1.
destruct H1 as [He1 Hrest]; unfold udr in He1.
apply He1.
assert (In _ (events E) x2) as Hevt2.
destruct H2 as [He2 Hrest]; unfold udr in He2.
apply He2.
generalize (Htot x1 x2 Hdiff Hevt1 Hevt2); intro Ht.
inversion Ht as [H12 | H21]; unfold rrestrict; unfold so_ws; unfold In;
[left | right]; split.
split; [apply H12 | exists l; split].
unfold writes_to_same_loc_l; unfold In; split.
unfold udr; apply incl_union_left_in; exists x2; apply H12.
destruct H1 as [He1 Hw1]; apply Hw1.
unfold writes_to_same_loc_l; unfold In; split.
unfold udr; apply incl_union_right_in; exists x1; apply H12.
destruct H2 as [He2 Hw2]; apply Hw2.
unfold In in H1; unfold In in H2; split; [apply H1 | apply H2].
split; [apply H21 | exists l; split].
unfold writes_to_same_loc_l; unfold In; split.
unfold udr; apply incl_union_left_in; exists x1; apply H21.
destruct H2 as [He2 Hw2]; apply Hw2.
unfold writes_to_same_loc_l; unfold In; split.
unfold udr; apply incl_union_right_in; exists x2; apply H21.
destruct H1 as [He1 Hw1]; apply Hw1.
unfold In in H1; unfold In in H2; split; [apply H2 | apply H1].
(*mem*)
intros x e Hws.
destruct Hsc_ord as [[Hdr ?] ?].
destruct Hws as [Hso [l [[Hex Hwx] [Hee Hwe]]]]; exists l; split;
unfold In; unfold writes_to_same_loc_l.
split; [apply Hdr; apply Hex |apply Hwx].
split; [apply Hdr; apply Hee |apply Hwe].
Qed.
Ltac destruct_lin H :=
destruct H as [Hdr [Htrans [Hac Htot]]].
(** In the execution witness extracted from a sequential execution, no read event reads a value written by a write event that occurs later in the program order *)
Lemma sc_caus_wf :
forall E so,
seq_exec E so ->
acyclic (rel_union (so_rfm E so) (ls E)).
Proof.
intros E so Hsc.
destruct Hsc as [Hlin Hincl].
apply ac_incl with so.
generalize (lso_is_tc Hlin); intro Heq.
destruct Hlin as [Hdr [Htrans [Hac Htot]]].
rewrite <- Heq in Hac; trivial.
unfold rel_incl; unfold rel_union;
intros x y Hin.
inversion Hin as [Hrf | Hdp].
destruct Hrf as [? [[? [Hso ?]] Hmax]]; exact Hso.
apply Hincl.
unfold ls in Hdp.
destruct Hdp as [Hrx [Hwy Hpo_xy]]; apply Hpo_xy.
Qed.
(** The read-from relation extracted from a sequential execution is a well-formed read-from relation *)
Lemma sc_rf_wf :
forall E so,
seq_exec E so ->
rfmaps_well_formed E (events E) (so_rfm E so).
Proof.
intros E so (*Hdp*) Hsc_ord; unfold rfmaps_well_formed; split.
destruct Hsc_ord as [Hlin Hincl]; destruct_lin Hlin.
intros er Her; generalize (so_rfm_init E so er Her);
intros [ew [Hew Hrfw]]; exists ew.
split; auto.
split; [intros e1 e2 H12 | ].
destruct H12 as [Hso12 [Hrf12 Hno12]].
destruct Hsc_ord as [[Hdr Hrest] Hincl].
unfold rfmaps.
destruct Hrf12 as [[Hevt1 Hw1] [Hso Heq]].
destruct Hso12 as [H1 [H2 Hl]].
split; [ | split; [|apply Hl]].
apply Hevt1.
apply Hdr; apply H2.
intros x w1 w2 [Hrf_w1x [Hpw_w1x Hmax_w1x]] [Hrf_w2x [Hpw_w2x Hmax_w2x]].
destruct (eqEv_dec w1 w2) as [Hy | Hn].
apply Hy.
assert (so w1 w2 \/ so w2 w1) as Hor.
destruct Hsc_ord as [[Hdr [Htrans [Hac Htot]]] ?].
apply (Htot w1 w2 Hn).
destruct Hpw_w1x as [[Hew1 ?] ?]; apply Hew1.
destruct Hpw_w2x as [[Hew2 ?] ?]; apply Hew2.
inversion Hor as [H12 | H21].
apply (Hmax_w1x w2); split; auto.
apply sym_eq; apply (Hmax_w2x w1); split; auto.
Qed.
(** For any location, there are no contradictions between a sequential execution and the program order on the events reading from/writing to this location *)
Lemma so_ac_pio :
forall E so,
seq_exec E so ->
acyclic
(rel_union so (pio E)).
Proof.
intros E so Hsc.
apply ac_incl with (rel_union so (po_iico E)).
generalize (rel_union_refl so (po_iico E)); intro Heq; rewrite Heq.
destruct Hsc as [Hlin Hincl]; apply incl_implies_ac_union.
apply Hincl.
unfold acyclic; unfold not; intros x Htc.
generalize (lso_is_tc Hlin); intro Hso; rewrite Hso in Htc.
destruct Hlin as [Hdr [Htrans [Hac Htot]]].
unfold not in Hac; eapply Hac; apply Htc.
apply rel_incl_left.
unfold rel_incl; unfold pio;
intros x y [Hloc Hpo].
apply Hpo.
Qed.
(** For any location, there are no contradictions between a sequential execution and the program order on the events reading from/writing to the same location and to the pairs of events for which at least one of the event is a write *)
Lemma so_ac_pio_llh :
forall E so,
seq_exec E so ->
acyclic
(rel_union so (pio_llh E)).
Proof.
intros E so Hsc.
eapply incl_ac with (rel_union so (pio E)).
intros x y Hxy; inversion Hxy; [left |
right; unfold pio; destruct H as [? [? ?]]]; auto.
apply so_ac_pio; auto.
Qed.
(** The communication relation extracted from a sequential execution is included in the sequential execution itself *)
Lemma com_in_so :
forall E so,
seq_exec E so ->
rel_incl (com E (sc_witness E so)) so.
Proof.
unfold rel_incl; intros E so Hsc_ord x y Hhb.
inversion Hhb as [Hrf_fr | Hws]; unfold sc_witness in *; simpl in *.
inversion Hrf_fr as [Hrf | Hfr].
(*in rf*)
destruct Hrf as [Hrf [[? [Hso ?]] ?]]; apply Hso.
(*in fr*)
destruct Hfr as [Hx [Hy [wr [Hwrx Hwry]]]]; simpl in *.
destruct Hsc_ord as [[Hdom [Htrans [Hac Htot]]] Hincl];
destruct Hwrx as [Hso_wrx [Hrf_wrx Hno]];
destruct Hso_wrx as [Hso_wr [Hso_x [lx [Hwwr [Hr_x ?]]]]];
destruct Hwry as [Hso_wry [l2 [Hw_wr [Hevt_y [vy Hw_y]]]]].
destruct Hrf_wrx as [? [Hso ?]].
(*destruct Hw_y as [Hevt_y Hw_y].*)
destruct (eqEv_dec x y) as [Heq | Hdiff].
rewrite Heq in Hr_x.
case_eq (action y); unfold read_from in Hr_x; unfold write_to in Hw_y.
intros d l v He2; rewrite He2 in Hr_x; rewrite He2 in Hw_y; case_eq d.
intro Hr; rewrite Hr in Hw_y; (*destruct Hw_y as [? Hw_y];*) inversion Hw_y.
intro Hw; rewrite Hw in Hr_x; destruct Hr_x as [? Hr_x]; inversion Hr_x.
assert (In _ (events E) x) as He1.
apply Hdom; apply Hso_x.
assert (In _ (events E) y) as He2.
apply Hdom; apply Hevt_y.
generalize (Htot x y Hdiff He1 He2); intro Hor2.
inversion Hor2 as [H12 | H21].
exact H12.
assert (wr = y) as Heq.
apply (Hno y); split; auto.
(*destruct Hw_y as [vy Hwy]; *)
unfold In; unfold previous_writes; split; [ |split; auto].
unfold writes; split; auto; exists l2; exists vy; auto.
rewrite <- H1; destruct Hw_wr as [? [lwr Hw_wr]]; unfold write_to in *;
unfold loc; rewrite Hw_wr; rewrite Hw_y; trivial.
subst; generalize (Hac y); intro Hc.
contradiction.
(*in ws*)
destruct Hws as [Hso Hrest]; apply Hso.
Qed.
(** For any given location, there are no conflicts between the communication relation extracted from a sequential execution and the program order restricted to events reading from/writing to this location *)
Lemma sc_com_wf :
forall E so,
seq_exec E so ->
acyclic
(rel_union (com E (sc_witness E so)) (pio E)).
Proof.
intros E so Hsc_ord.
eapply ac_incl;
[apply so_ac_pio; apply Hsc_ord |
apply rel_incl_right; apply com_in_so;
apply Hsc_ord].
Qed.
(** For any given location, there are no conflicts between the communication relation extracted from a sequential execution and the program order restricted to events reading from/writing to this location, and to pairs of events for which at least one of the events is a write
This condition corresponds to the [uniproc] condition *)
Lemma sc_hb_llh_wf :
forall E so,
seq_exec E so ->
acyclic
(rel_union (com E (sc_witness E so)) (pio_llh E)).
Proof.
intros E so Hsc_ord.
eapply ac_incl;
[apply so_ac_pio_llh; apply Hsc_ord |
apply rel_incl_right; apply com_in_so;
apply Hsc_ord].
Qed.
(** The read-from relation extracted from a sequential execution is included in the sequential execution *)
Lemma sc_rf_in_so :
forall E so,
rel_incl (rf (sc_witness E so)) so.
Proof.
intros E so; unfold rel_incl; unfold sc_witness; simpl; unfold so_rfm.
intros e1 e2 Hin; destruct Hin as [? [[? [Hso ?]] Hmax]]; exact Hso.
Qed.
(** The write serialization extracted from a sequential execution is included in the sequential execution *)
Lemma sc_ws_in_so :
forall E so,
rel_incl (ws (sc_witness E so)) so.
Proof.
intros E so; unfold sc_witness; simpl; unfold so_ws.
intros e1 e2 Hin; destruct Hin as [Hso Hrest]; exact Hso.
Qed.
(** The from-read relation extracted from a sequential execution is included in the sequential execution *)
Lemma sc_fr_in_so :
forall E so,
seq_exec E so ->
rel_incl (fr E (sc_witness E so)) so.
Proof.
intros E so Hsc_ord; unfold sc_witness; unfold fr; unfold frmaps; simpl.
intros e1 e2 Hin.
destruct Hin as [Hevt1 [Hevt2 [wr [Hrf_wr1 Hws_wr2]]]];
destruct Hsc_ord as [[Hdom [Htrans [Hac Htot]]] Hincl];
destruct Hrf_wr1 as [Hrf_wr1 [Hpw_wr1 Hmax_wr1]];
destruct Hws_wr2 as [Hso_wr2 [l2 [Hw_wr Hw_e2]]].
destruct Hrf_wr1 as [Hevt_wr [Hevt_e2 [l1 [Hww_wr [Hr_e2 ?]]]]];
destruct Hw_e2 as [Hevtb_e2 Hw_e2].
destruct (eqEv_dec e1 e2) as [Heq | Hdiff].
rewrite Heq in Hr_e2.
case_eq (action e2); unfold read_from in Hr_e2; unfold write_to in Hw_e2.
intros d l v He2; rewrite He2 in Hr_e2; rewrite He2 in Hw_e2; case_eq d.
intro Hr; rewrite Hr in Hw_e2; destruct Hw_e2 as [? Hw_e2]; inversion Hw_e2.
intro Hw; rewrite Hw in Hr_e2; destruct Hr_e2 as [? Hr_e2]; inversion Hr_e2.
assert (In _ (events E) e1) as He1.
apply Hevt1.
assert (In _ (events E) e2) as He2.
apply Hevt2.
generalize (Htot e1 e2 Hdiff He1 He2); intro Hor2.
inversion Hor2 as [H12 | H21].
exact H12.
assert (wr = e2) as Heq.
apply (Hmax_wr1 e2); split; auto.
destruct Hw_e2 as [ve2 Hwe2];
unfold In; unfold previous_writes; split; [ |split; auto].
unfold writes; split; auto; exists l2; exists ve2; auto.
destruct Hw_wr as [? [v2 Hwwr]];
destruct Hpw_wr1 as [? [Hso Hlwr]]; unfold write_to in *;
rewrite <- Hlwr; unfold loc; rewrite Hwwr; rewrite Hwe2; trivial.
subst; generalize (Hac e2); intro Hc.
contradiction.
Qed.
(** In any event structure, the preserved program order of [AWmm] is included in any sequential execution over this event structure *)
Lemma sc_ppo_in_so :
forall E so,
seq_exec E so ->
rel_incl (ppo E) so.
Proof.
unfold rel_incl;
intros E so Hsc_ord e1 e2 Hin_c.
destruct Hsc_ord as [Hlin Hincl]; apply Hincl.
apply A.ppo_valid ; exact Hin_c.
Qed.
(** In any event structure, the sequence of:
- The reflexive closure of read-from
- The program order
- The reflexive closure of read-from
is included in any sequential execution over this event structure *)
Lemma rf_po_rf_in_so :
forall E so x y,
seq_exec E so ->
rel_seq (maybe (rf (sc_witness E so)))
(rel_seq (po_iico E) (maybe (rf (sc_witness E so)))) x y ->
so x y.
Proof.
intros E so x y Hse [z [Hxz [e [Hze Hey]]]].
destruct Hse as [Hlin Hincl]; destruct_lin Hlin.
inversion Hxz as [Hrfxz | Heqxz]; inversion Hey as [Hrfey | Heqey].
destruct Hrfxz as [? [[? [Hsoxz ?]] ?]] ; destruct Hrfey as [? [[? [Hsoey ?]] ?]].
apply Htrans with z; split; auto. apply Htrans with e; split; auto.
rewrite <- Heqey.
destruct Hrfxz as [? [[? [Hsoxz ?]] ?]]; apply Htrans with z; split; auto.
rewrite Heqxz.
destruct Hrfey as [? [[? [Hsoey ?]] ?]]; apply Htrans with e; split; auto.
rewrite Heqxz; rewrite <- Heqey; auto.
Qed.
(** For any event structure, the union of the barrier relation, write serialization, from-read relation, and preserved program order of the architecture [AWmm] is included in any sequential execution over this structure *)
Lemma bot_ghb_in_so :
forall E so,
seq_exec E so ->
rel_incl (rel_union (abc E (sc_witness E so))
(rel_union (rel_union (ws (sc_witness E so)) (fr E (sc_witness E so))) (ppo E))) so.
Proof.
unfold rel_incl; intros E so Hsc_ord e1 e2 Hx.
inversion Hx as [Hab | Hrest].
(*ab*)
generalize Hsc_ord; intro Hse.
destruct Hsc_ord as [Hlin ?]; destruct_lin Hlin.
generalize (AwkAiSc); intros [? [? [? Habi]]].
generalize (ab_sc_compat E (sc_witness E so) e1 e2 (Habi E (sc_witness E so) e1 e2 Hab));
intro Hin. apply (rf_po_rf_in_so E so e1 e2 Hse Hin).
inversion Hrest as [Hws_fr | Hppo].
inversion Hws_fr as [Hws | Hfr].
(*ws*)
generalize Hws; apply sc_ws_in_so.
(*fr*)
generalize Hfr; apply sc_fr_in_so; apply Hsc_ord.
(*ppo*)
generalize Hppo; apply sc_ppo_in_so; apply Hsc_ord.
Qed.
(** For any event structure, the global happens-before of the architecture [AWmm] is included in any sequential execution over this structure *)
Lemma sc_ghb_in_so :
forall E so,
seq_exec E so ->
rel_incl (ghb E (sc_witness E so)) so.
Proof.
unfold rel_incl; intros E so Hsc_ord e1 e2 Hx.
case_eq inter; case_eq intra; unfold ghb in Hx.
(*true, true*)
intros Hintra Hinter; rewrite Hintra in Hx; rewrite Hinter in Hx.
inversion Hx as [Hrf_inter | Hrest].
(*rf_inter*)
destruct Hrf_inter as [Hrf Hprocs].
generalize Hrf; apply sc_rf_in_so.
inversion Hrest as [Hrf_intra | Hres].
(*rf_intra*)
destruct Hrf_intra as [Hrf Hprocs].
generalize Hrf; apply sc_rf_in_so.
generalize Hres; apply (bot_ghb_in_so);
apply Hsc_ord.
(*true, false*)
intros Hintra Hinter; rewrite Hintra in Hx; rewrite Hinter in Hx.
inversion Hx as [Hrf_inter | Hrest].
(*rf_inter*)
destruct Hrf_inter as [Hrf Hprocs].
generalize Hrf; apply sc_rf_in_so.
generalize Hrest; apply (bot_ghb_in_so);
apply Hsc_ord.
(*false, true*)
intros Hintra Hinter; rewrite Hintra in Hx; rewrite Hinter in Hx.
inversion Hx as [Hrf_intra | Hrest].
(*rf_intra*)
destruct Hrf_intra as [Hrf Hprocs].
generalize Hrf; apply sc_rf_in_so.
generalize Hrest; apply (bot_ghb_in_so);
apply Hsc_ord.
(*false,false*)
intros Hintra Hinter; rewrite Hintra in Hx; rewrite Hinter in Hx.
generalize Hx; apply (bot_ghb_in_so);
apply Hsc_ord.
Qed.
(** For any event structure, the global happens-before on the memory model [Awmm] is always acyclic on the execution witness extracted of the sequential execution *)
Lemma sc_exec_wf:
forall E so,
seq_exec E so ->
acyclic (ghb E (sc_witness E so)).
Proof.
intros E so Hsc_ord.
eapply incl_ac.
- apply sc_ghb_in_so; auto.
- destruct Hsc_ord as [Hlin Hincl].
eapply lin_strict_ac; apply Hlin.
Qed.
(** For any event structure, the execution witness extracted from any sequential execution over the event structure respects the out-of-[thin]-air condition *)
Lemma sc_exec_thin :
forall E so,
seq_exec E so ->
acyclic (rel_union (so_rfm E so) (dp E)).
Proof.
intros E so Hsc x Hx.
assert (rel_incl (rel_union (so_rfm E so) (dp E)) so) as Hi.
intros e1 e2 H12.
inversion H12 as [Hrf | Hdp].
generalize (sc_rf_in_so E so); intros Hi.
unfold sc_witness in Hi; simpl in Hi; apply Hi; auto.
destruct Hsc as [? Hpo]; apply Hpo.
generalize (dp_valid E); intros [? ?]; auto.
assert (so x x) as Hc.
destruct Hsc as [Hlin ?].
rewrite <- (lso_is_tc Hlin).
generalize Hx; apply tc_incl; auto.
destruct Hsc as [Hlin ?].
destruct_lin Hlin.
apply (Hac x Hc).
Qed.
(** In a well-formed event structure, an execution witness extracted from any sequential execution over this structure is a valid execution on [AWmm].
I.e. an SC execution is valid on any architecture *)
Lemma sc_witness_valid:
forall E so,
well_formed_event_structure E ->
seq_exec E so ->
valid_execution E (sc_witness E so).
Proof.
intros E so Hwf Hsc_ord.
unfold valid_execution. simpl.
split.
(* write serialization is well-formed *)
{ eapply sc_ws_wf; auto. }
split.
(* read-from is well-formed *)
{ eapply sc_rf_wf; auto. }
split.
(* uniprocessor condition *)
{ eapply sc_hb_llh_wf; auto. }
split.
(* out-of-thin-air condition *)
{ eapply sc_exec_thin; auto. }
(* ghb is acyclic *)
{ apply sc_exec_wf; auto. }
Qed.
(** *** SC executions SC-check *)
(** For any event structure, the union of the communication relation and of the program order is included in any sequential execution over this structure *)
Lemma com_po_in_so :
forall E so,
seq_exec E so ->
rel_incl (rel_union (po_iico E)
(com E (sc_witness E so))) so.
Proof.
intros E so Hsc x y Hxy.
inversion Hxy.
destruct Hsc as [? Hincl]; apply Hincl; auto.
apply (com_in_so E so Hsc x y H).
Qed.
(** For any event structure, the execution witness extracted from any sequential execution over this structure satisfies the [sc_check] condition *)
Lemma sc_witness_sc :
forall E so,
seq_exec E so ->
sc_check E (sc_witness E so).
Proof.
intros E so Hsc; unfold sc_check.
eapply incl_ac.
apply com_po_in_so; auto.
destruct Hsc as [Hlin ?]; generalize Hlin; intro Hl; destruct_lin Hlin;
unfold acyclic; rewrite (lso_is_tc Hl); auto.
Qed.
End sc_valid.
(** *** Characterisation of an SC execution *)
Section sc_carac.
(** In a well-formed event structure with a well-formed execution witness, if:
- The union of the program order and of the communication relation is acyclic
- There exists a total order on the events of the event structure
- The union of the program order and of the communication relation is included in this total order
Then, the write serialization of the execution witness is the same as the one extracted from the total order after applying [sc_witness] on it *)
Lemma ac_po_com_implies_same_ws :
forall E X so,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
acyclic (rel_union (po_iico E) (com E X))->
linear_strict_order so (events E) ->
rel_incl (rel_union (po_iico E) (com E X)) so ->
ws X = ws (sc_witness E so).
Proof.
intros E X so Hwf Hs Hacy Hlin Hincl.
generalize Hs; intros [Hwswf Hrfwf].
assert (forall x y, (ws X) x y <-> (ws (sc_witness E so)) x y) as Hext.
split; intro Hin;
unfold sc_witness; unfold so_ws; simpl.
split.
apply Hincl; right; unfold com;
right; apply Hin.
destruct_lin Hlin.
generalize (ws_cands E X x y Hwswf Hin).
intros [l [Hx Hy]]; exists l; split.
split; destruct Hx as [Hudr Hwx]; auto.
unfold udr; apply incl_union_left_in; exists y; apply Hincl; right; right; auto.
split; destruct Hy as [Hudr Hwy]; auto.
unfold udr; apply incl_union_right_in; exists x; apply Hincl; right; right; auto.
unfold sc_witness in Hin; simpl in Hin.
unfold so_ws in Hin;
unfold udr in Hin.
destruct Hin as [Hin [l Hm]];
assert (In _ (writes_to_same_loc_l (events E) l) x /\
In _ (writes_to_same_loc_l (events E) l) y) as Hmem.
split; split; destruct Hm as [[Hx Hwx] [Hy Hwy]].
destruct_lin Hlin.
apply Hdr; auto.
auto.
destruct_lin Hlin.
apply Hdr; auto.
auto.
destruct Hwswf as [Hws_tot Hws_cands].
generalize (ws_tot E X (Hws_tot l) Hmem); intro Hor.
assert (x <> y) as Hneq.
destruct_lin Hlin.
unfold not; intro Heq_xe; unfold acyclic in Hac; unfold not in Hac; apply (Hac x).
rewrite <- Heq_xe in Hin; exact Hin.
generalize (Hor Hneq); intro Horb.
inversion Horb as [Hws_xe | Hws_ex].
exact Hws_xe.
assert (so y x) as Hin_ex.
apply Hincl; unfold com;
right; right; exact Hws_ex.
assert (~(acyclic so)) as Hcontrad.
unfold acyclic; unfold not; intro Hcy; apply (Hcy x).
eapply trc_ind with y; apply trc_step; [apply Hin | exact Hin_ex].
generalize Hlin; intro Hli; destruct_lin Hlin; unfold acyclic in Hcontrad.
generalize (lso_is_tc Hli); intro Heq; rewrite Heq in Hcontrad.
contradiction.
apply (ext_rel (ws X) (ws (sc_witness E so)) Hext).
Qed.
Ltac destruct_lin H :=
destruct H as [Hdr [Htrans [Hac Htot]]].
(** In well-formed event structure with an execution valid on the architecture [AWmm], if:
- There exists a total order on the events of the event structure
- The union of the program order and of the communication relation is included in this total order
- Two events are related by the read-from relation extracted from this total order
Then, these two events are related by the read-from relation of the execution.
*)
Lemma sc_rf_ax :
forall E X so x y,
well_formed_event_structure E ->
valid_execution E X ->
linear_strict_order so (events E) ->
rel_incl (rel_union (po_iico E) (com E X)) so ->
so_rfm E so x y ->
rf X x y.
Proof.
intros E X so x y Hwf Hv Hlin Hincl [Hrf [Hpw Hmax]].
generalize Hv; intro Hva.
assert (exists w, rf X w y) as Hrf_y.
assert (In _ (reads E) y) as Hey.
destruct Hrf as [? [Hey [l [? [Hry ?]]]]]; destruct_lin Hlin;
split; [apply Hdr | exists l]; auto.
destruct_valid Hv; generalize (Hrf_init y Hey); intros [w [Hor Hrfw]].
exists w; auto.
destruct Hrf_y as [w Hrf_wy].
destruct (eqEv_dec w x) as [Heq | Hdiff].
subst; trivial.
assert (ws X x w \/ ws X w x) as Hor.
destruct Hpw as [[Hex [l Hwx]] [Hsoxy Hl]].
assert (In _ (writes_to_same_loc_l (events E) l) x) as Hmx.
split; auto.
assert (In _ (writes_to_same_loc_l (events E) l) w) as Hmw.
split; auto.
destruct_lin Hlin; apply Hdr.
apply incl_union_left_in; exists y; apply Hincl; right; left; left; auto.
destruct Hrf as [? [? [ly [? [Hry ?]]]]]; destruct Hwx as [vx Hwx].
unfold loc in Hl; rewrite Hwx in Hl; generalize Hry; intro Hy;
destruct Hry as [vy Hry]; rewrite Hry in Hl; inversion Hl; auto.
apply (rf_implies_same_loc w Hv Hrf_wy Hy).
destruct_valid Hva; destruct_lin (Hws_tot l).
generalize (Htot w x Hdiff Hmw Hmx); intro Horw.
inversion Horw as [Hwswx | Hwsxw].
destruct Hwswx; auto.
destruct Hwsxw; auto.
inversion Hor as [Hxw | Hwx].
assert (so w y) as Hso_wy.
apply Hincl; right; left; left; auto.
assert (so x w) as Hso_xw.
apply Hincl; right; right; auto.
destruct_valid Hv.
generalize (Hrf_cands w y Hrf_wy); intros [Hew [Hey [l [Hww [Hry ?]]]]].
assert (exists e3 : Event, write_to e3 l /\ so x e3 /\ so e3 y) as Hcontrad.
exists w; split; auto.
assert (write_to x l) as Hwx.
destruct Hrf as [? [? [l' [Hwx' [Hry' ?]]]]].
rewrite (read_from_implies_same_loc Hry Hry'); auto.
destruct Hcontrad as [e3 [[v3 Hwe3] [Hxe3 He3y]]].
assert (x = e3) as Heq.
apply (Hmax e3); split; auto.
split; [unfold writes; split; [|exists l; exists v3; auto] |split; auto].
destruct_lin Hlin; apply Hdr; apply incl_union_left_in; exists y; auto.
destruct Hry as [vy Hry]; unfold loc; rewrite Hry; rewrite Hwe3; trivial.
subst; destruct_lin Hlin; generalize (Hac e3); intro Hc; contradiction.
assert (fr E X y x) as Hfr_yx.
unfold fr; unfold frmaps; split; [|split; [| exists w]].
assert (rfmaps_well_formed E (events E) (rf X)) as Hrfwf.
destruct_valid Hv.
split; auto.
apply (ran_rf_in_events X w y Hwf Hrfwf Hrf_wy).
assert (write_serialization_well_formed (events E) (ws X)) as Hwswf.
destruct_valid Hv.
split; auto.
apply (ran_ws_in_events X w x Hwf Hwswf Hwx).
auto.
assert (so y x) as Hso_yx.
apply Hincl; right; left; right; auto.
destruct Hpw as [? [Hso_xy ?]].
destruct_lin Hlin;
assert (so y y) as Hso_yy.
apply Htrans with x; auto.
generalize (Hac y); intro Hc; contradiction.
Qed.
(** For any execution valid on [AWmm], the read-from relation is included in the communication relation *)
Lemma rf_in_com:
forall E X x y,
valid_execution E X ->
rf X x y ->
com E X x y.
Proof.
intros E X x y Hv Hrf.
left; left; auto.
Qed.
(** In well-formed event structure with a valid execution that verifies the [sc_check] condition, if there is a total order on the events of the event structure such that the union of the program order and of the communication relation is included in it, then the read-from relation we can extract from this total order is equal to the read-from relation of the execution witness *)
Lemma so_rfm_po_com_is_rf :
forall E X so,
well_formed_event_structure E ->
valid_execution E X ->
sc_check E X ->
linear_strict_order so (events E) ->
rel_incl (rel_union (po_iico E) (com E X)) so ->
so_rfm E so = rf X.
Proof.
intros E X so Hwf Hvalid Hsc Hlin Hincl;
apply (ext_rel (so_rfm E so) (rf X)); intros x y; split; intro Hxy.
apply (sc_rf_ax E X so x y Hwf Hvalid Hlin Hincl Hxy).
unfold so_rfm; split.
split; generalize Hvalid; intro Hv; destruct_valid Hvalid.
unfold udr; apply incl_union_left_in; exists y; apply Hincl; right; left; left; auto.
split.
unfold udr; apply incl_union_right_in; exists x; apply Hincl; right; left; left; auto.
generalize (Hrf_cands x y Hxy); intros [Hex [Hey Hwxry]]; auto.
split; [split; [|split] |].
destruct_valid Hvalid; split; generalize (Hrf_cands x y Hxy);
intros [Hex [Hey [l [[v Hwx] Hry]]]]; auto; exists l; exists v; auto.
apply Hincl; right; left; left; auto.
destruct_valid Hvalid; generalize (Hrf_cands x y Hxy);
intros [Hex [Hey [l [[v Hwx] [[vy Hry] ?]]]]]; unfold loc;
rewrite Hwx; rewrite Hry; auto.
intros x' [[Hwx' [Hso_x'y Hloc]] Hso_xx'].
generalize (eqEv_dec x x'); intros [Heq | Hdiff].
exact Heq.
generalize Hvalid; intro Hv; destruct_valid Hvalid.
destruct Hwx' as [Hex' [l [v Hwx']]].
assert (In _ (writes_to_same_loc_l (events E) l) x /\
In _ (writes_to_same_loc_l (events E) l) x') as Hand.
destruct_lin Hlin.
split; split.
apply Hdr; apply incl_union_left_in; exists x'; auto. auto.
generalize (Hrf_cands x y Hxy); intros [? [? [lx [[vx Hx] [[vy Hy] ?]]]]].
exists vx; unfold write_to; rewrite Hx.
unfold loc in Hloc; rewrite Hwx' in Hloc; rewrite Hy in Hloc; inversion Hloc; trivial.
apply Hdr; apply incl_union_right_in; exists x; auto.
unfold write_to; exists v; auto.
generalize (ws_tot E X (Hws_tot l) Hand Hdiff); intro Hor.
inversion Hor.
assert (fr E X y x') as Hfr_y3.
split; [| split].
eapply ran_rf_in_events; auto.
split; auto. apply Hxy.
eapply ran_ws_in_events; auto.
split; auto. apply H.
exists x; split; auto.
assert (so y x') as Hso_y3.