From 5ddf4523acc8e85fc6ac1467ff0aaeb6c888fd4d Mon Sep 17 00:00:00 2001 From: Jeehoon Kang Date: Wed, 1 Feb 2017 12:17:27 +0100 Subject: [PATCH 1/4] Apply Ori's diff --- src/axiomatic/Gstep.v | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/src/axiomatic/Gstep.v b/src/axiomatic/Gstep.v index d8645c0..1b4d223 100644 --- a/src/axiomatic/Gstep.v +++ b/src/axiomatic/Gstep.v @@ -393,17 +393,14 @@ Section GstepLemmas. cdes WF'; cdes WF_SB0. specialize (SB_TID0 x y H). desf; try by exploit SB_INIT; eauto. - exploit sb_actb; eauto. - exploit sb_acta; eauto. - ins; desf; try subst x; try subst y. - by exfalso; auto. - by exfalso; auto. + forward eapply SB_ACTa0; eauto. + ins; desf; try subst x. + by exfalso; eapply SB_IRR0; eapply SB_T0; eauto. + assert (sb x y \/ sb y x). + eapply SB_TOT; eauto. + by intro; subst x; eauto. + desf; auto. by exfalso; eapply SB_IRR0; eapply SB_T0; eauto. - exploit SB_TOT; eauto. - ins; desf; eauto. - intro; subst x; eauto. - intro; desf; eauto. - exfalso; eauto. Qed. Lemma gstep_rmw_a : gstep_a rmw rmw'. @@ -525,7 +522,8 @@ Proof. desf; ins. cdes WF_RF; cdes WF_MO; cdes INC. exploit (RF_TOT a). by left; eauto. eauto with acts. - intros; desc. exploit rf_lv; try edone; intro; desc. + intros; desc. + forward eapply rf_lv with (rf:=rf'); try edone; intro; desc. eexists; splits; eauto. apply RF_ACTa in x0; destruct x0; eauto. exfalso; subst; destruct (lab a0); ins. @@ -631,9 +629,10 @@ Proof. exists y; splits; eauto. desf. - left; splits. congruence. - - right; splits; try done. eapply init_events_wf2; eauto. - intro. eapply init_proper_thread; eauto. + - right; splits; try done. - right; splits; eauto. + eapply init_events_wf2; eauto. + intro. eapply init_proper_thread; eauto. - exfalso. eapply init_not_proper with (a:=z0); eauto. Qed. From 07c94b7c91d9db89155d5c7ffd90b76c3a96e09e Mon Sep 17 00:00:00 2001 From: Jeehoon Kang Date: Tue, 14 Feb 2017 13:03:43 +0900 Subject: [PATCH 2/4] Fix compilation errors for Coq 8.6 --- lib/hahn | 2 +- src/invariant/Invariant.v | 2 +- src/lang/MemoryFacts.v | 2 +- src/opt/Merge.v | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/hahn b/lib/hahn index 27b20af..68c36c3 160000 --- a/lib/hahn +++ b/lib/hahn @@ -1 +1 @@ -Subproject commit 27b20afb50abf6222821077825b3d2058b09bf1e +Subproject commit 68c36c3698312132ee1adebdba5f8d62dd243634 diff --git a/src/invariant/Invariant.v b/src/invariant/Invariant.v index 8b4aa40..42452ca 100644 --- a/src/invariant/Invariant.v +++ b/src/invariant/Invariant.v @@ -172,7 +172,7 @@ Section Invariant. { i. des. inv SEM. congr. } condtac; ss. { guardH o. i. des. inv SEM. - exploit Memory.split_get0; eauto. i. des. + exploit Memory.split_get0; try exact MEM; eauto. i. des. esplits; eauto. } i. esplits; eauto. diff --git a/src/lang/MemoryFacts.v b/src/lang/MemoryFacts.v index 98ba8c2..17935bd 100644 --- a/src/lang/MemoryFacts.v +++ b/src/lang/MemoryFacts.v @@ -75,7 +75,7 @@ Module MemoryFacts. - erewrite Memory.split_o; eauto. repeat condtac; ss. + des. subst. congr. + guardH o. des. subst. i. inv GET. - exploit Memory.split_get0; eauto. i. des. esplits; eauto. + exploit Memory.split_get0; try exact MEM; eauto. i. des. esplits; eauto. + i. esplits; eauto. - erewrite Memory.lower_o; eauto. condtac; ss. + des. subst. congr. diff --git a/src/opt/Merge.v b/src/opt/Merge.v index df67547..1f5df54 100644 --- a/src/opt/Merge.v +++ b/src/opt/Merge.v @@ -300,7 +300,7 @@ Proof. { auto. } * econs 2. econs 2. econs; [|econs 4]; eauto. { econs. econs. s. rewrite ? Const.add_0_r. eauto. } - { eapply merge_write_read1; try apply STEP_SRC; eauto. } + { eapply merge_write_read1; try apply STEP2; eauto. } * auto. * etrans; eauto. * etrans; eauto. From 6ff7ed6a99c170027cf8c2750b1a914a4bf4e68e Mon Sep 17 00:00:00 2001 From: Jeehoon Kang Date: Wed, 15 Feb 2017 21:33:54 +0900 Subject: [PATCH 3/4] Fix compilation errors in the DRF proof --- src/drf/PIStep.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/drf/PIStep.v b/src/drf/PIStep.v index 4f9ef93..59417c8 100644 --- a/src/drf/PIStep.v +++ b/src/drf/PIStep.v @@ -685,7 +685,7 @@ Proof. { inv WF. auto. } { ii. destruct (ThreadEvent.is_promising e0) eqn:E0; [by destruct e0|]. ii; hexploit pi_wf_small_step_is_reading; try exact WF2; eauto. - i. hexploit pi_wf_small_step_is_promising; eauto. + i. hexploit pi_wf_small_step_is_promising; try exact STEPT; eauto. } { apply rtcn_rtc in A23. inv A12. exploit pi_step_except_small_step; eauto. i. destruct cST3. ss. @@ -698,7 +698,7 @@ Proof. } i. destruct cST3. subst. des. { destruct (ThreadEvent.is_promising e0) eqn:E0; subst. - - exploit IH; try exact A23; eauto. + - exploit IH; try exact A23; try exact WF; eauto. { econs; econs; eauto; ii; by des; destruct e2', e0. } i. des. esplits; try exact STEPS; eauto. - assert (EQ: e2' = e0). @@ -749,7 +749,7 @@ Proof. } exploit IH; try exact STEP2'; eauto. - { eapply pi_step_future; eauto. } + { eapply pi_step_future; try exact WF; eauto. } i. des. esplits; [|econs; try exact STEPS0|]; eauto; omega. Qed. From 99bd7e1ba871907584544ab573974fe78498c119 Mon Sep 17 00:00:00 2001 From: orilahav Date: Wed, 15 Feb 2017 17:41:56 +0100 Subject: [PATCH 4/4] 8.6 --- src/axiomatic/GsimM.v | 2 +- src/axiomatic/GstepWrite.v | 10 +++++----- src/axiomatic/MsimG.v | 2 +- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/axiomatic/GsimM.v b/src/axiomatic/GsimM.v index fe91c15..c3ac04b 100644 --- a/src/axiomatic/GsimM.v +++ b/src/axiomatic/GsimM.v @@ -1054,7 +1054,7 @@ red; splits; try done. red; splits; eauto. eby eapply no_rmw_from_init. eby eapply rmw_acta. - + unfold singl_rel, sb_ext, eqv_rel, seq in *; desf; eauto; subst z0 z b a; left. + + unfold singl_rel, sb_ext, eqv_rel, seq in *; desf; eauto; left. eapply SB_AT_END; eauto. by left; congr. eby destruct SB3; subst. diff --git a/src/axiomatic/GstepWrite.v b/src/axiomatic/GstepWrite.v index 11c2afa..1fdd54c 100644 --- a/src/axiomatic/GstepWrite.v +++ b/src/axiomatic/GstepWrite.v @@ -399,10 +399,10 @@ Proof. rewrite gstep_urr_write; try edone; relsimp. rewrite gstep_sb_ext_helper_w2; ins. split; repeat apply inclusion_union_l; eauto 12 with rel. - red; unfold seq, eqv_rel; ins; desf; try (by destruct a as [??[]]); + red; unfold seq, eqv_rel; ins; desf; try (by destruct y as [??[]]); by right; eauto. - rewrite <- inclusion_union_r2, !eqv_join; unfold eqv_rel; red; ins; desf. - subst y; splits; ins; tauto. + rewrite <- inclusion_union_r2, !eqv_join; unfold eqv_rel; red; + ins; desf; splits; auto. Qed. Lemma gstep_c_rel_rwr_write l l' : @@ -416,10 +416,10 @@ Proof. rewrite gstep_rwr_write; try edone; relsimp. rewrite gstep_sb_ext_helper_w2; ins. split; repeat apply inclusion_union_l; eauto 12 with rel. - red; unfold seq, eqv_rel; ins; desf; try (by destruct a as [??[]]); + red; unfold seq, eqv_rel; ins; desf; try (by destruct y as [??[]]); by right; eauto. rewrite <- inclusion_union_r2, !eqv_join; unfold eqv_rel; red; ins; desf. - subst y; splits; ins; tauto. + splits; auto. Qed. Lemma gstep_t_rel_urr_write l' l x : diff --git a/src/axiomatic/MsimG.v b/src/axiomatic/MsimG.v index f8d4471..d8db1ea 100644 --- a/src/axiomatic/MsimG.v +++ b/src/axiomatic/MsimG.v @@ -341,7 +341,7 @@ Proof. intros K K'; cdes GSTEP; desf; ins; desf. by cdes WF'; exfalso; eapply WF_MO; eauto. assert (P: is_proper y). - by eapply no_mo_to_init; eauto. + by eapply no_mo_to_init with (mo:=mo0); eauto. destruct (classic (exists x : event, (rf;; rmw) x y)) as [C|]; desc; eauto. assert (INx: In x acts). by eapply seq_doma in C; [|eapply rf_acta]; eauto.