fix the step_internal of Asmvliw

- Actually, we want to show that the outcome is the same
  for any order of "writes" in the parallel execution.
  (ie we ask that bundles have a deterministic semantics for parallel execution)
- we relax the condition that the outcome should be given for sequential execution
  instead, we ask that the it is given for the "in order" writes.

In theory, the semantics would also accept bundles like "R1 := R2  R2 := R1"
which are deterministic for parallel execution

But, of course, in practice, we will also prove the sequential execution.

1 files changed, 23 insertions, 19 deletions

diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 2c88673b..5b58118b 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -233,23 +233,27 @@ Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rs: regset) (m:
   | Stuck => Stuck
   end.
 
-(* utile ? *)
 Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome :=
   parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs m.
 
-
 Require Import Sorting.Permutation.
 
-Inductive parexec_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome -> Prop :=
-   parexec_bblock_Next bdy1 bdy2 rsw mw:
-      Permutation (bdy1++bdy2) (body b) ->
-      parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m = Next rsw mw ->
-      parexec_bblock f b rs m (parexec_wio_body bdy2 rs rsw m mw)
- | parexec_bblock_Stuck bdy1 bdy2:
-      Permutation (bdy1++bdy2) (body b) ->
-      parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m = Stuck ->
-      parexec_bblock f b rs m Stuck.
+Definition parexec_bblock (f: function) (b: bblock) (rs: regset) (m: mem) (o: outcome): Prop :=
+   exists bdy1 bdy2, Permutation (bdy1++bdy2) (body b) /\ 
+      o=match parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m with
+      | Next rsw mw => parexec_wio_body bdy2 rs rsw m mw
+      | Stuck => Stuck
+      end.
 
+Lemma parexec_bblock_write_in_order f b rs m:
+   parexec_bblock f b rs m (parexec_wio_bblock f b rs m).
+Proof.
+   exists (body b). exists nil.
+   constructor 1.
+   - rewrite app_nil_r; auto.
+   - unfold parexec_wio_bblock.
+     destruct (parexec_wio_bblock_aux f _ _ _ _ _); simpl; auto.
+Qed.
 
 Inductive step: state -> trace -> state -> Prop :=
   | exec_step_internal:
@@ -257,8 +261,8 @@ Inductive step: state -> trace -> state -> Prop :=
       rs PC = Vptr b ofs ->
       Genv.find_funct_ptr ge b = Some (Internal f) ->
       find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bi ->
-      exec_bblock ge f bi rs m = Next rs' m' ->
-      parexec_bblock f bi rs m (Next rs' m') ->
+      parexec_wio_bblock f bi rs m = Next rs' m' ->
+      (forall o, parexec_bblock f bi rs m o -> o=(Next rs' m')) ->
       step (State rs m) E0 (State rs' m')
   | exec_step_builtin:
       forall b ofs f ef args res rs m vargs t vres rs' m' bi,
@@ -301,11 +305,11 @@ Ltac Equalities :=
   intros; constructor; simpl; intros.
 - (* determ *)
   inv H; inv H0; Equalities.
-  + split. constructor. auto.
-  + unfold exec_bblock in H4. destruct (exec_body _ _ _ _); try discriminate.
+  + split. constructor. auto. 
+  + unfold parexec_wio_bblock, parexec_wio_bblock_aux in H4. destruct (parexec_wio_body _ _ _ _ _ _); try discriminate.
     rewrite H10 in H4. discriminate.
-  + unfold exec_bblock in H14. (* FIXME: destruct (exec_body _ _ _ _); try discriminate.
-    rewrite H4 in H13. discriminate.
+  + unfold parexec_wio_bblock, parexec_wio_bblock_aux in H11. destruct (parexec_wio_body _ _ _ _ _ _); try discriminate.
+    rewrite H4 in H11. discriminate.
   + assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.
     exploit external_call_determ. eexact H6. eexact H13. intros [A B].
     split. auto. intros. destruct B; auto. subst. auto.
@@ -325,5 +329,5 @@ Ltac Equalities :=
   inv H. unfold Vzero in H0. red; intros; red; intros.
   inv H; rewrite H0 in *; eelim NOTNULL; eauto.
 - (* final states *)
-  inv H; inv H0. congruence. *)
-Admitted.
\ No newline at end of file
+  inv H; inv H0. congruence.
+Qed.
\ No newline at end of file