Merge of the "volatile" branch:

- native treatment of volatile accesses in CompCert C's semantics
- translation of volatile accesses to built-ins in SimplExpr
- native treatment of struct assignment and passing struct parameter by value
- only passing struct result by value remains emulated
- in cparser, remove emulations that are no longer used
- added C99's type _Bool and used it to express || and && more efficiently.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 698 insertions, 259 deletions

diff --git a/common/Behaviors.v b/common/Behaviors.v
index ccb5749..454ea34 100644
--- a/common/Behaviors.v
+++ b/common/Behaviors.v
@@ -530,6 +530,156 @@ Qed.
 
 End BACKWARD_SIMULATIONS.
 
+(** * Program behaviors for the "atomic" construction *)
+
+Section ATOMIC.
+
+Variable L: semantics.
+Hypothesis Lwb: well_behaved_traces L.
+
+Remark atomic_finish: forall s t, output_trace t -> Star (atomic L) (t, s) t (E0, s).
+Proof.
+  induction t; intros.
+  apply star_refl.
+  simpl in H; destruct H. eapply star_left; eauto.
+  simpl. apply atomic_step_continue; auto. simpl; auto. auto.
+Qed.
+
+Lemma step_atomic_plus:
+  forall s1 t s2, Step L s1 t s2 -> Plus (atomic L) (E0,s1) t (E0,s2).
+Proof.
+  intros.  destruct t.
+  apply plus_one. simpl; apply atomic_step_silent; auto.
+  exploit Lwb; eauto. simpl; intros. 
+  eapply plus_left. eapply atomic_step_start; eauto. eapply atomic_finish; eauto. auto.
+Qed.
+
+Lemma star_atomic_star:
+  forall s1 t s2, Star L s1 t s2 -> Star (atomic L) (E0,s1) t (E0,s2).
+Proof.
+  induction 1. apply star_refl. eapply star_trans with (s2 := (E0,s2)).
+  apply plus_star. eapply step_atomic_plus; eauto. eauto. auto.
+Qed.
+ 
+Lemma atomic_forward_simulation: forward_simulation L (atomic L).
+Proof.
+  set (ms := fun (s: state L) (ts: state (atomic L)) => ts = (E0,s)).
+  apply forward_simulation_plus with ms; intros.
+  auto.
+  exists (E0,s1); split. simpl; auto. red; auto. 
+  red in H. subst s2. simpl; auto. 
+  red in H0. subst s2. exists (E0,s1'); split.
+  apply step_atomic_plus; auto. red; auto.
+Qed.
+
+Lemma atomic_star_star_gen:
+  forall ts1 t ts2, Star (atomic L) ts1 t ts2 ->
+  exists t', Star L (snd ts1) t' (snd ts2) /\ fst ts1 ** t' = t ** fst ts2.
+Proof.
+  induction 1. 
+  exists E0; split. apply star_refl. traceEq.
+  destruct IHstar as [t' [A B]].
+  simpl in H; inv H; simpl in *.
+  exists t'; split. eapply star_left; eauto. auto.
+  exists (ev :: t0 ** t'); split. eapply star_left; eauto. rewrite B; auto. 
+  exists t'; split. auto. rewrite B; auto.
+Qed.
+
+Lemma atomic_star_star:
+  forall s1 t s2, Star (atomic L) (E0,s1) t (E0,s2) -> Star L s1 t s2.
+Proof.
+  intros. exploit atomic_star_star_gen; eauto. intros [t' [A B]]. 
+  simpl in *. replace t with t'. auto. subst; traceEq. 
+Qed.
+
+Lemma atomic_forever_silent_forever_silent:
+  forall s, Forever_silent (atomic L) s -> Forever_silent L (snd s).
+Proof.
+  cofix COINDHYP; intros. inv H. inv H0. 
+  apply forever_silent_intro with (snd (E0, s')). auto. apply COINDHYP; auto. 
+Qed.
+
+Remark star_atomic_output_trace:
+  forall s t t' s',
+  Star (atomic L) (E0, s) t (t', s') -> output_trace t'.
+Proof.
+  assert (forall ts1 t ts2, Star (atomic L) ts1 t ts2 ->
+          output_trace (fst ts1) -> output_trace (fst ts2)).
+  induction 1; intros. auto. inv H; simpl in *.
+  apply IHstar. auto.
+  apply IHstar. exploit Lwb; eauto.
+  destruct H2. apply IHstar. auto.
+  intros. change t' with (fst (t',s')). eapply H; eauto. simpl; auto. 
+Qed.
+
+Lemma atomic_forever_reactive_forever_reactive:
+  forall s T, Forever_reactive (atomic L) (E0,s) T -> Forever_reactive L s T.
+Proof.
+  assert (forall t s T, Forever_reactive (atomic L) (t,s) T ->
+          exists T', Forever_reactive (atomic L) (E0,s) T' /\ T = t *** T').
+  induction t; intros. exists T; auto.
+  inv H. inv H0. congruence. simpl in H; inv H. 
+  destruct (IHt s (t2***T0)) as [T' [A B]]. eapply star_forever_reactive; eauto.
+  exists T'; split; auto. simpl. congruence. 
+
+  cofix COINDHYP; intros. inv H0. destruct s2 as [t2 s2]. 
+  destruct (H _ _ _ H3) as [T' [A B]].  
+  assert (Star (atomic L) (E0, s) (t**t2) (E0, s2)).
+    eapply star_trans. eauto. apply atomic_finish. eapply star_atomic_output_trace; eauto. auto. 
+  replace (t *** T0) with ((t ** t2) *** T'). apply forever_reactive_intro with s2. 
+  apply atomic_star_star; auto. destruct t; simpl in *; unfold E0 in *; congruence.
+  apply COINDHYP. auto.
+  subst T0; traceEq.
+Qed.
+
+Theorem atomic_behaviors:
+  forall beh, program_behaves L beh <-> program_behaves (atomic L) beh.
+Proof.
+  intros; split; intros.
+  (* L -> atomic L *)
+  exploit forward_simulation_behavior_improves. eapply atomic_forward_simulation. eauto. 
+  intros [beh2 [A B]]. red in B. destruct B as [EQ | [t [C D]]].
+  congruence.
+  subst beh. inv H. inv H1.
+  apply program_runs with (E0,s). simpl; auto. 
+  apply state_goes_wrong with (E0,s'). apply star_atomic_star; auto. 
+  red; intros; red; intros. inv H. eelim H3; eauto. eelim H3; eauto. 
+  intros; red; intros. simpl in H. destruct H. eelim H4; eauto. 
+  apply program_goes_initially_wrong. 
+  intros; red; intros. simpl in H; destruct H. eelim H1; eauto. 
+  (* atomic L -> L *)
+  inv H.
+  (* initial state defined *)
+  destruct s as [t s]. simpl in H0. destruct H0; subst t. 
+  apply program_runs with s; auto. 
+  inv H1.
+  (* termination *)
+  destruct s' as [t' s']. simpl in H2; destruct H2; subst t'. 
+  econstructor. eapply atomic_star_star; eauto. auto. 
+  (* silent divergence *)
+  destruct s' as [t' s'].
+  assert (t' = E0). inv H2. inv H1; auto. subst t'. 
+  econstructor. eapply atomic_star_star; eauto. 
+  change s' with (snd (E0,s')). apply atomic_forever_silent_forever_silent. auto.
+  (* reactive divergence *)
+  econstructor. apply atomic_forever_reactive_forever_reactive. auto. 
+  (* going wrong *)
+  destruct s' as [t' s'].
+  assert (t' = E0).
+    destruct t'; auto. eelim H2. simpl. apply atomic_step_continue.
+    eapply star_atomic_output_trace; eauto.
+  subst t'. econstructor. apply atomic_star_star; eauto. 
+  red; intros; red; intros. destruct t0.
+  elim (H2 E0 (E0,s'0)). constructor; auto. 
+  elim (H2 (e::nil) (t0,s'0)). constructor; auto.
+  intros; red; intros. elim (H3 r). simpl; auto. 
+  (* initial state undefined *)
+  apply program_goes_initially_wrong. 
+  intros; red; intros. elim (H0 (E0,s)); simpl; auto.
+Qed.
+
+End ATOMIC.
+
 (** * Additional results about infinite reduction sequences *)
 
 (** We now show that any infinite sequence of reductions is either of
diff --git a/common/Events.v b/common/Events.v
index 018314e..3d082a7 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -490,6 +490,59 @@ Qed.
 
 End MATCH_TRACES_INV.
 
+(** An output trace is a trace composed only of output events,
+  that is, events that do not take any result from the outside world. *)
+
+Definition output_event (ev: event) : Prop :=
+  match ev with
+  | Event_syscall _ _ _ => False
+  | Event_vload _ _ _ _ => False
+  | Event_vstore _ _ _ _ => True
+  | Event_annot _ _ => True
+  end.
+  
+Fixpoint output_trace (t: trace) : Prop :=
+  match t with
+  | nil => True
+  | ev :: t' => output_event ev /\ output_trace t'
+  end.
+
+(** * Semantics of volatile memory accesses *)
+
+Definition block_is_volatile (F V: Type) (ge: Genv.t F V) (b: block) : bool :=
+  match Genv.find_var_info ge b with
+  | None => false
+  | Some gv => gv.(gvar_volatile)
+  end.
+
+Inductive volatile_load (F V: Type) (ge: Genv.t F V):
+                   memory_chunk -> mem -> block -> int -> trace -> val -> Prop :=
+  | volatile_load_vol: forall chunk m b ofs id ev v,
+      block_is_volatile ge b = true ->
+      Genv.find_symbol ge id = Some b ->
+      eventval_match ge ev (type_of_chunk chunk) v ->
+      volatile_load ge chunk m b ofs
+                      (Event_vload chunk id ofs ev :: nil)
+                      (Val.load_result chunk v)
+  | volatile_load_nonvol: forall chunk m b ofs v,
+      block_is_volatile ge b = false ->
+      Mem.load chunk m b (Int.unsigned ofs) = Some v ->
+      volatile_load ge chunk m b ofs E0 v.
+
+Inductive volatile_store (F V: Type) (ge: Genv.t F V):
+                  memory_chunk -> mem -> block -> int -> val -> trace -> mem -> Prop :=
+  | volatile_store_vol: forall chunk m b ofs id ev v,
+      block_is_volatile ge b = true ->
+      Genv.find_symbol ge id = Some b ->
+      eventval_match ge ev (type_of_chunk chunk) v ->
+      volatile_store ge chunk m b ofs v
+                      (Event_vstore chunk id ofs ev :: nil)
+                      m
+  | volatile_store_nonvol: forall chunk m b ofs v m',
+      block_is_volatile ge b = false ->
+      Mem.store chunk m b (Int.unsigned ofs) v = Some m' ->
+      volatile_store ge chunk m b ofs v E0 m'.
+
 (** * Semantics of external functions *)
 
 (** For each external function, its behavior is defined by a predicate relating:
@@ -530,12 +583,6 @@ Definition inject_separated (f f': meminj) (m1 m2: mem): Prop :=
   f b1 = None -> f' b1 = Some(b2, delta) ->
   ~Mem.valid_block m1 b1 /\ ~Mem.valid_block m2 b2.
 
-Definition block_is_volatile (F V: Type) (ge: Genv.t F V) (b: block) : bool :=
-  match Genv.find_var_info ge b with
-  | None => false
-  | Some gv => gv.(gvar_volatile)
-  end.
-
 Record extcall_properties (sem: extcall_sem)
                           (sg: signature) : Prop := mk_extcall_properties {
 
@@ -624,20 +671,34 @@ Record extcall_properties (sem: extcall_sem)
 
 Inductive volatile_load_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V):
               list val -> mem -> trace -> val -> mem -> Prop :=
-  | volatile_load_sem_vol: forall b ofs m id ev v,
-      Genv.find_symbol ge id = Some b -> block_is_volatile ge b = true ->
-      eventval_match ge ev (type_of_chunk chunk) v ->
-      volatile_load_sem chunk ge
-          (Vptr b ofs :: nil) m
-          (Event_vload chunk id ofs ev :: nil)
-          (Val.load_result chunk v) m
-  | volatile_load_sem_nonvol: forall b ofs m v,
-      block_is_volatile ge b = false ->
-      Mem.load chunk m b (Int.unsigned ofs) = Some v ->
-      volatile_load_sem chunk ge
-          (Vptr b ofs :: nil) m
-          E0
-          v m.
+  | volatile_load_sem_intro: forall b ofs m t v,
+      volatile_load ge chunk m b ofs t v ->
+      volatile_load_sem chunk ge (Vptr b ofs :: nil) m t v m.
+
+Lemma volatile_load_preserved:
+  forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) chunk m b ofs t v,
+  (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) ->
+  (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) ->
+  volatile_load ge1 chunk m b ofs t v ->
+  volatile_load ge2 chunk m b ofs t v.
+Proof.
+  intros. inv H1; constructor; auto.
+  rewrite H0; auto.
+  rewrite H; auto.
+  eapply eventval_match_preserved; eauto.
+  rewrite H0; auto.
+Qed.
+
+Lemma volatile_load_extends:
+  forall F V (ge: Genv.t F V) chunk m b ofs t v m',
+  volatile_load ge chunk m b ofs t v ->
+  Mem.extends m m' ->
+  exists v', volatile_load ge chunk m' b ofs t v' /\ Val.lessdef v v'.
+Proof.
+  intros. inv H.
+  econstructor; split; eauto. econstructor; eauto.
+  exploit Mem.load_extends; eauto. intros [v' [A B]]. exists v'; split; auto. constructor; auto.
+Qed.
 
 Remark meminj_preserves_block_is_volatile:
   forall F V (ge: Genv.t F V) f b1 b2 delta,
@@ -653,6 +714,35 @@ Proof.
   auto.
 Qed.
 
+Lemma volatile_load_inject:
+  forall F V (ge: Genv.t F V) f chunk m b ofs t v b' ofs' m',
+  meminj_preserves_globals ge f ->
+  volatile_load ge chunk m b ofs t v ->
+  val_inject f (Vptr b ofs) (Vptr b' ofs') ->
+  Mem.inject f m m' ->
+  exists v', volatile_load ge chunk m' b' ofs' t v' /\ val_inject f v v'.
+Proof.
+  intros. inv H0.
+  inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H8 in EQ; inv EQ.
+  rewrite Int.add_zero. exists (Val.load_result chunk v0); split.
+  constructor; auto. 
+  apply val_load_result_inject. eapply eventval_match_inject_2; eauto.
+  exploit Mem.loadv_inject; eauto. simpl; eauto. simpl; intros [v' [A B]]. exists v'; split; auto. 
+  constructor; auto. rewrite <- H3. inv H1. eapply meminj_preserves_block_is_volatile; eauto. 
+Qed.
+
+Lemma volatile_load_receptive:
+  forall F V (ge: Genv.t F V) chunk m b ofs t1 t2 v1,
+  volatile_load ge chunk m b ofs t1 v1 -> match_traces ge t1 t2 ->
+  exists v2, volatile_load ge chunk m b ofs t2 v2.
+Proof.
+  intros. inv H; inv H0.
+  exploit eventval_match_valid; eauto. intros [A B]. 
+  exploit eventval_valid_match. eexact H9. rewrite <- H10; eauto. 
+  intros [v' EVM]. exists (Val.load_result chunk v'). constructor; auto.
+  exists v1; constructor; auto.
+Qed.
+
 Lemma volatile_load_ok:
   forall chunk,
   extcall_properties (volatile_load_sem chunk) 
@@ -660,64 +750,36 @@ Lemma volatile_load_ok:
 Proof.
   intros; constructor; intros.
 (* well typed *)
-  unfold proj_sig_res; simpl. destruct H.
+  unfold proj_sig_res; simpl. inv H. inv H0.
   destruct chunk; destruct v; simpl; constructor.
   eapply Mem.load_type; eauto. 
 (* arity *)
-  destruct H; simpl; auto.
+  inv H; inv H0; auto.
 (* symbols *)
-  destruct H1. 
-  econstructor; eauto. rewrite H; auto. eapply eventval_match_preserved; eauto. 
-  econstructor; eauto.
+  inv H1. constructor. eapply volatile_load_preserved; eauto. 
 (* valid blocks *)
-  destruct H; auto.
+  inv H; auto.
 (* bounds *)
-  destruct H; auto.
+  inv H; auto.
 (* mem extends *)
-  destruct H. 
-  inv H1. inv H8. inv H6. 
-  exists (Val.load_result chunk v); exists m1'; intuition.
-  constructor; auto.
-  red; auto.
-  inv H1. inv H7. inv H5. 
-  exploit Mem.load_extends; eauto. intros [v' [A B]]. 
-  exists v'; exists m1'; intuition.
-  econstructor; eauto.
-  red; auto.
+  inv H. inv H1. inv H6. inv H4. 
+  exploit volatile_load_extends; eauto. intros [v' [A B]].
+  exists v'; exists m1'; intuition. constructor; auto. red; auto.
 (* mem injects *)
-  destruct H0.
-  inv H2. inv H9. inv H7.
-  generalize H; intros [P [Q R]].
-  exploit P; eauto. intro EQ; rewrite H6 in EQ; inv EQ.
-  exists f; exists (Val.load_result chunk v); exists m1'; intuition.
-  rewrite Int.add_zero. constructor; auto.
-  apply val_load_result_inject. eapply eventval_match_inject_2; eauto.
-  red; auto.
-  red; auto.
-  red; intros. congruence.
-  inv H2. inv H8.
-  exploit Mem.loadv_inject; eauto. simpl. eauto. intros [v1 [A B]].
-  inv H6; simpl in *.
-  exists f; exists v1; exists m1'; intuition.
-  econstructor; eauto.
-  rewrite <- H0. eapply meminj_preserves_block_is_volatile; eauto.
-  red; auto.
-  red; auto.
-  red; intros. congruence.
+  inv H0. inv H2. inv H7. inversion H5; subst. 
+  exploit volatile_load_inject; eauto. intros [v' [A B]]. 
+  exists f; exists v'; exists m1'; intuition. constructor; auto.
+  red; auto. red; auto. red; intros. congruence.
 (* trace length *)
-  inv H; simpl; omega.
+  inv H; inv H0; simpl; omega.
 (* receptive *)
-  inv H; inv H0.
-  exploit eventval_match_valid; eauto. intros [A B]. 
-  exploit eventval_valid_match. eexact H9. rewrite <- H10; eauto. 
-  intros [v' EVM]. exists (Val.load_result chunk v'); exists m1.
-  eapply volatile_load_sem_vol; eauto. 
-  exists vres1; exists m1; eapply volatile_load_sem_nonvol; eauto.
+  inv H. exploit volatile_load_receptive; eauto. intros [v2 A].
+  exists v2; exists m1; constructor; auto.
 (* determ *)
-  inv H; inv H0; try congruence.
+  inv H; inv H0. inv H1; inv H7; try congruence.
   assert (id = id0) by (eapply Genv.genv_vars_inj; eauto). subst id0.
-  exploit eventval_match_valid. eexact H3. intros [V1 T1].
-  exploit eventval_match_valid. eexact H11. intros [V2 T2].
+  exploit eventval_match_valid. eexact H2. intros [V1 T1].
+  exploit eventval_match_valid. eexact H4. intros [V2 T2].
   split. constructor; auto. congruence.
   intros EQ; inv EQ. 
   assert (v = v0) by (eapply eventval_match_determ_1; eauto). subst v0.
@@ -728,31 +790,19 @@ Qed.
 Inductive volatile_load_global_sem (chunk: memory_chunk) (id: ident) (ofs: int)
                                    (F V: Type) (ge: Genv.t F V):
               list val -> mem -> trace -> val -> mem -> Prop :=
-  | volatile_load_global_sem_vol: forall b m ev v,
-      Genv.find_symbol ge id = Some b -> block_is_volatile ge b = true ->
-      eventval_match ge ev (type_of_chunk chunk) v ->
-      volatile_load_global_sem chunk id ofs ge
-          nil m
-          (Event_vload chunk id ofs ev :: nil)
-          (Val.load_result chunk v) m
-  | volatile_load_global_sem_nonvol: forall b m v,
-      Genv.find_symbol ge id = Some b -> block_is_volatile ge b = false ->
-      Mem.load chunk m b (Int.unsigned ofs) = Some v ->
-      volatile_load_global_sem chunk id ofs ge
-          nil m
-          E0
-          v m.
+  | volatile_load_global_sem_intro: forall b t v m,
+      Genv.find_symbol ge id = Some b ->
+      volatile_load ge chunk m b ofs t v ->
+      volatile_load_global_sem chunk id ofs ge nil m t v m.
 
 Remark volatile_load_global_charact:
   forall chunk id ofs (F V: Type) (ge: Genv.t F V) vargs m t vres m',
   volatile_load_global_sem chunk id ofs ge vargs m t vres m' <->
   exists b, Genv.find_symbol ge id = Some b /\ volatile_load_sem chunk ge (Vptr b ofs :: vargs) m t vres m'.
 Proof.
-  intros; split. 
-  intros. inv H; exists b; split; auto; constructor; auto. 
-  intros [b [P Q]]. inv Q. 
-  assert (id0 = id) by (eapply Genv.genv_vars_inj; eauto). subst id0. econstructor; eauto.
-  econstructor; eauto.
+  intros; split.
+  intros. inv H. exists b; split; auto. constructor; auto. 
+  intros [b [P Q]]. inv Q. econstructor; eauto.
 Qed.
 
 Lemma volatile_load_global_ok:
@@ -762,117 +812,79 @@ Lemma volatile_load_global_ok:
 Proof.
   intros; constructor; intros.
 (* well typed *)
-  unfold proj_sig_res; simpl. destruct H.
+  unfold proj_sig_res; simpl. inv H. inv H1.
   destruct chunk; destruct v; simpl; constructor.
   eapply Mem.load_type; eauto. 
 (* arity *)
-  destruct H; simpl; auto.
+  inv H; inv H1; auto.
 (* symbols *)
-  destruct H1. 
-  econstructor; eauto. rewrite H; auto. eapply eventval_match_preserved; eauto.
-  econstructor; eauto. rewrite H; auto.
+  inv H1. econstructor. rewrite H; eauto. eapply volatile_load_preserved; eauto. 
 (* valid blocks *)
-  destruct H; auto.
+  inv H; auto.
 (* bounds *)
-  destruct H; auto.
-(* mem extends *)
-  destruct H. 
-  inv H1. 
-  exists (Val.load_result chunk v); exists m1'; intuition.
-  econstructor; eauto.
-  red; auto.
-  inv H1. 
-  exploit Mem.load_extends; eauto. intros [v' [A B]]. 
-  exists v'; exists m1'; intuition.
-  econstructor; eauto.
-  red; auto.
-(* mem injects *)
-  destruct H0.
-  inv H2.
-  exists f; exists (Val.load_result chunk v); exists m1'; intuition.
-  econstructor; eauto.
-  apply val_load_result_inject. eapply eventval_match_inject_2; eauto.
-  red; auto.
-  red; auto.
-  red; intros. congruence.
-  inv H2. destruct H as [P [Q R]]. exploit P; eauto. intros EQ. 
-  exploit Mem.load_inject; eauto. rewrite Zplus_0_r. intros [v1 [A B]].
-  exists f; exists v1; exists m1'; intuition.
-  econstructor; eauto.
-  red; auto.
-  red; auto.
-  red; intros. congruence.
+  inv H; auto.
+(* extends *)
+  inv H. inv H1. exploit volatile_load_extends; eauto. intros [v' [A B]].
+  exists v'; exists m1'; intuition. econstructor; eauto. red; auto.
+(* inject *)
+  inv H0. inv H2.
+  assert (val_inject f (Vptr b ofs) (Vptr b ofs)). 
+    exploit (proj1 H); eauto. intros EQ. econstructor. eauto. rewrite Int.add_zero; auto.
+  exploit volatile_load_inject; eauto. intros [v' [A B]].
+  exists f; exists v'; exists m1'; intuition. econstructor; eauto. 
+  red; auto. red; auto. red; intros; congruence. 
 (* trace length *)
-  inv H; simpl; omega.
+  inv H; inv H1; simpl; omega.
 (* receptive *)
-  inv H; inv H0.
-  exploit eventval_match_valid; eauto. intros [A B]. 
-  exploit eventval_valid_match. eexact H9. rewrite <- H10; eauto. 
-  intros [v' EVM]. exists (Val.load_result chunk v'); exists m1.
-  eapply volatile_load_global_sem_vol; eauto. 
-  exists vres1; exists m1; eapply volatile_load_global_sem_nonvol; eauto.
+  inv H. exploit volatile_load_receptive; eauto. intros [v2 A].
+  exists v2; exists m1; econstructor; eauto.
 (* determ *)
-  inv H; inv H0; try congruence.
-  assert (b = b0) by congruence. subst b0. 
-  exploit eventval_match_valid. eexact H3. intros [V1 T1].
-  exploit eventval_match_valid. eexact H5. intros [V2 T2].
-  split. constructor; auto. congruence.
-  intros EQ; inv EQ. 
-  assert (v = v0) by (eapply eventval_match_determ_1; eauto). subst v0.
-  auto.
-  split. constructor. intuition congruence.
+  rewrite volatile_load_global_charact in *. 
+  destruct H as [b1 [A1 B1]]. destruct H0 as [b2 [A2 B2]].
+  rewrite A1 in A2; inv A2.
+  eapply ec_determ. eapply volatile_load_ok. eauto. eauto. 
 Qed.
 
 (** ** Semantics of volatile stores *)
 
 Inductive volatile_store_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V):
               list val -> mem -> trace -> val -> mem -> Prop :=
-  | volatile_store_sem_vol: forall b ofs m id ev v,
-      Genv.find_symbol ge id = Some b -> block_is_volatile ge b = true ->
-      eventval_match ge ev (type_of_chunk chunk) v ->
-      volatile_store_sem chunk ge
-          (Vptr b ofs :: v :: nil) m
-          (Event_vstore chunk id ofs ev :: nil)
-          Vundef m
-  | volatile_store_sem_nonvol: forall b ofs m v m',
-      block_is_volatile ge b = false ->
-      Mem.store chunk m b (Int.unsigned ofs) v = Some m' ->
-      volatile_store_sem chunk ge
-          (Vptr b ofs :: v :: nil) m
-          E0
-          Vundef m'.
+  | volatile_store_sem_intro: forall b ofs m1 v t m2,
+      volatile_store ge chunk m1 b ofs v t m2 ->
+      volatile_store_sem chunk ge (Vptr b ofs :: v :: nil) m1 t Vundef m2.
 
-Lemma volatile_store_ok:
-  forall chunk,
-  extcall_properties (volatile_store_sem chunk) 
-                     (mksignature (Tint :: type_of_chunk chunk :: nil) None).
+Lemma volatile_store_preserved:
+  forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) chunk m1 b ofs v t m2,
+  (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) ->
+  (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) ->
+  volatile_store ge1 chunk m1 b ofs v t m2 ->
+  volatile_store ge2 chunk m1 b ofs v t m2.
 Proof.
-  intros; constructor; intros.
-(* well typed *)
-  unfold proj_sig_res; simpl. inv H; constructor.
-(* arity *)
-  inv H; simpl; auto.
-(* symbols preserved *)
-  inv H1. 
-  constructor. rewrite H; auto. rewrite H0; auto. eapply eventval_match_preserved; eauto.
-  constructor; auto. rewrite H0; auto.
-(* valid block *)
-  inv H. auto. eauto with mem.
-(* bounds *)
-  inv H. auto. eapply Mem.bounds_store; eauto.
-(* mem extends*)
-  inv H.
-  inv H1. inv H6. inv H8. inv H7.
-  exists Vundef; exists m1'; intuition.
-  constructor; auto. eapply eventval_match_lessdef; eauto.
-  red; auto.
-  inv H1. inv H5. inv H7. inv H6.
-  exploit Mem.store_within_extends; eauto. intros [m' [A B]].
-  exists Vundef; exists m'; intuition.
-  constructor; auto.
+  intros. inv H1; constructor; auto.
+  rewrite H0; auto.
+  rewrite H; auto.
+  eapply eventval_match_preserved; eauto.
+  rewrite H0; auto.
+Qed.
+
+Lemma volatile_store_extends:
+  forall F V (ge: Genv.t F V) chunk m1 b ofs v t m2 m1' v',
+  volatile_store ge chunk m1 b ofs v t m2 ->
+  Mem.extends m1 m1' ->
+  Val.lessdef v v' ->
+  exists m2', 
+     volatile_store ge chunk m1' b ofs v' t m2'
+  /\ Mem.extends m2 m2'
+  /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2'.
+Proof.
+  intros. inv H.
+  econstructor; split. econstructor; eauto. eapply eventval_match_lessdef; eauto.
+  split. auto. red; auto.
+  exploit Mem.store_within_extends; eauto. intros [m2' [A B]].
+  exists m2'; intuition. econstructor; eauto. 
   red; split; intros.
   eapply Mem.perm_store_1; eauto.
-  rewrite <- H1. eapply Mem.load_store_other; eauto.
+  rewrite <- H4. eapply Mem.load_store_other; eauto.
   destruct (eq_block b0 b); auto. subst b0; right. 
   exploit Mem.valid_access_in_bounds. 
   eapply Mem.store_valid_access_3. eexact H3.
@@ -883,30 +895,37 @@ Proof.
                               (Int.unsigned ofs, Int.unsigned ofs + size_chunk chunk)).
   red; intros. generalize (H x H5). unfold loc_out_of_bounds, Intv.In; simpl. omega.
   simpl; omega. simpl; omega.
-(* mem injects *)
-  inv H0.
-  inv H2. inv H7. inv H9. inv H10.
-  generalize H; intros [P [Q R]].
-  exploit P; eauto. intro EQ; rewrite H6 in EQ; inv EQ.
-  exists f; exists Vundef; exists m1'; intuition.
-  rewrite Int.add_zero. constructor; auto. 
-  eapply eventval_match_inject; eauto. 
-  red; auto.
-  red; auto.
-  red; intros; congruence.
-  inv H2. inv H8. inv H9. inv H6.
+Qed.
+
+Lemma volatile_store_inject:
+  forall F V (ge: Genv.t F V) f chunk m1 b ofs v t m2 m1' b' ofs' v',
+  meminj_preserves_globals ge f ->
+  volatile_store ge chunk m1 b ofs v t m2 ->
+  val_inject f (Vptr b ofs) (Vptr b' ofs') ->
+  val_inject f v v' ->
+  Mem.inject f m1 m1' ->
+  exists m2',
+       volatile_store ge chunk m1' b' ofs' v' t m2'
+    /\ Mem.inject f m2 m2'
+    /\ mem_unchanged_on (loc_unmapped f) m1 m2
+    /\ mem_unchanged_on (loc_out_of_reach f m1) m1' m2'.
+Proof.
+  intros. inv H0.
+  inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H9 in EQ; inv EQ.
+  rewrite Int.add_zero. exists m1'.
+  split. constructor; auto.  eapply eventval_match_inject; eauto.
+  split. auto. split. red; auto. red; auto. 
   assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto.
   exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]].
-  inv H4. 
-  exists f; exists Vundef; exists m2'; intuition.
-  constructor; auto. rewrite <- H3. eapply meminj_preserves_block_is_volatile; eauto.  
+  inv H1. exists m2'; intuition. 
+  constructor; auto. rewrite <- H4. eapply meminj_preserves_block_is_volatile; eauto.  
   split; intros. eapply Mem.perm_store_1; eauto.
-  rewrite <- H4. eapply Mem.load_store_other; eauto. 
-  left. exploit (H2 ofs0). generalize (size_chunk_pos chunk0). omega. 
+  rewrite <- H6. eapply Mem.load_store_other; eauto. 
+  left. exploit (H1 ofs0). generalize (size_chunk_pos chunk0). omega. 
   unfold loc_unmapped. congruence.
   split; intros. eapply Mem.perm_store_1; eauto.
-  rewrite <- H4. eapply Mem.load_store_other; eauto.
-  destruct (eq_block b0 b2); auto. subst b0; right.
+  rewrite <- H6. eapply Mem.load_store_other; eauto.
+  destruct (eq_block b0 b'); auto. subst b0; right.
   assert (EQ: Int.unsigned (Int.add ofs (Int.repr delta)) = Int.unsigned ofs + delta).
     eapply Mem.address_inject; eauto with mem.
   unfold Mem.storev in A. rewrite EQ in A. rewrite EQ.
@@ -917,16 +936,48 @@ Proof.
   generalize (size_chunk_pos chunk). intro G.
   apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0)
                               (Int.unsigned ofs + delta, Int.unsigned ofs + delta + size_chunk chunk)).
-  red; intros. exploit (H2 x H8). eauto. unfold Intv.In; simpl. omega.
+  red; intros. exploit (H1 x H7). eauto. unfold Intv.In; simpl. omega.
   simpl; omega. simpl; omega.
-  red; intros; congruence.
+Qed.
+
+Lemma volatile_store_receptive:
+  forall F V (ge: Genv.t F V) chunk m b ofs v t1 m1 t2,
+  volatile_store ge chunk m b ofs v t1 m1 -> match_traces ge t1 t2 -> t1 = t2.
+Proof.
+  intros. inv H; inv H0; auto.  
+Qed.
+
+Lemma volatile_store_ok:
+  forall chunk,
+  extcall_properties (volatile_store_sem chunk) 
+                     (mksignature (Tint :: type_of_chunk chunk :: nil) None).
+Proof.
+  intros; constructor; intros.
+(* well typed *)
+  unfold proj_sig_res; simpl. inv H; constructor.
+(* arity *)
+  inv H; simpl; auto.
+(* symbols preserved *)
+  inv H1. constructor. eapply volatile_store_preserved; eauto. 
+(* valid block *)
+  inv H. inv H1. auto. eauto with mem.
+(* bounds *)
+  inv H. inv H1. auto. eapply Mem.bounds_store; eauto.
+(* mem extends*)
+  inv H. inv H1. inv H6. inv H7. inv H4.
+  exploit volatile_store_extends; eauto. intros [m2' [A [B C]]]. 
+  exists Vundef; exists m2'; intuition. constructor; auto. 
+(* mem inject *)
+  inv H0. inv H2. inv H7. inv H8. inversion H5; subst.
+  exploit volatile_store_inject; eauto. intros [m2' [A [B [C D]]]].
+  exists f; exists Vundef; exists m2'; intuition. constructor; auto. red; intros; congruence.
 (* trace length *)
-  inv H; simpl; omega.
+  inv H; inv H0; simpl; omega.
 (* receptive *)
-  assert (t1 = t2). inv H; inv H0; auto. 
-  exists vres1; exists m1; congruence.
+  assert (t1 = t2). inv H. eapply volatile_store_receptive; eauto.
+  subst t2; exists vres1; exists m1; auto.
 (* determ *)
-  inv H; inv H0; try congruence.
+  inv H; inv H0. inv H1; inv H8; try congruence.
   assert (id = id0) by (eapply Genv.genv_vars_inj; eauto). subst id0.
   assert (ev = ev0) by (eapply eventval_match_determ_2; eauto). subst ev0.
   split. constructor. auto.
@@ -936,20 +987,10 @@ Qed.
 Inductive volatile_store_global_sem (chunk: memory_chunk) (id: ident) (ofs: int)
                                    (F V: Type) (ge: Genv.t F V):
               list val -> mem -> trace -> val -> mem -> Prop :=
-  | volatile_store_global_sem_vol: forall b m ev v,
-      Genv.find_symbol ge id = Some b -> block_is_volatile ge b = true ->
-      eventval_match ge ev (type_of_chunk chunk) v ->
-      volatile_store_global_sem chunk id ofs ge
-          (v :: nil) m
-          (Event_vstore chunk id ofs ev :: nil)
-          Vundef m
-  | volatile_store_global_sem_nonvol: forall b m v m',
-      Genv.find_symbol ge id = Some b -> block_is_volatile ge b = false ->
-      Mem.store chunk m b (Int.unsigned ofs) v = Some m' ->
-      volatile_store_global_sem chunk id ofs ge
-          (v :: nil) m
-          E0
-          Vundef m'.
+  | volatile_store_global_sem_intro: forall b m1 v t m2,
+      Genv.find_symbol ge id = Some b ->
+      volatile_store ge chunk m1 b ofs v t m2 ->
+      volatile_store_global_sem chunk id ofs ge (v :: nil) m1 t Vundef m2.
 
 Remark volatile_store_global_charact:
   forall chunk id ofs (F V: Type) (ge: Genv.t F V) vargs m t vres m',
@@ -958,9 +999,7 @@ Remark volatile_store_global_charact:
 Proof.
   intros; split. 
   intros. inv H; exists b; split; auto; econstructor; eauto.
-  intros [b [P Q]]. inv Q. 
-  assert (id0 = id) by (eapply Genv.genv_vars_inj; eauto). subst id0. econstructor; eauto.
-  econstructor; eauto.
+  intros [b [P Q]]. inv Q. econstructor; eauto. 
 Qed.
 
 Lemma volatile_store_global_ok:
@@ -974,13 +1013,11 @@ Proof.
 (* arity *)
   inv H; simpl; auto.
 (* symbols preserved *)
-  inv H1. 
-  econstructor. rewrite H; eauto. rewrite H0; auto. eapply eventval_match_preserved; eauto.
-  econstructor; eauto. rewrite H; auto.
+  inv H1. econstructor. rewrite H; eauto. eapply volatile_store_preserved; eauto. 
 (* valid block *)
-  inv H. auto. eauto with mem.
+  inv H. inv H2. auto. eauto with mem.
 (* bounds *)
-  inv H. auto. eapply Mem.bounds_store; eauto.
+  inv H. inv H2. auto. eapply Mem.bounds_store; eauto.
 (* mem extends*)
   rewrite volatile_store_global_charact in H. destruct H as [b [P Q]]. 
   exploit ec_mem_extends. eapply volatile_store_ok. eexact Q. eauto. eauto. 
@@ -995,16 +1032,14 @@ Proof.
   exists f'; exists vres'; exists m2'; intuition.
   rewrite volatile_store_global_charact. exists b; auto. 
 (* trace length *)
-  inv H; simpl; omega.
+  inv H. inv H1; simpl; omega.
 (* receptive *)
-  assert (t1 = t2). inv H; inv H0; auto. 
+  assert (t1 = t2). inv H. eapply volatile_store_receptive; eauto. subst t2. 
   exists vres1; exists m1; congruence.
 (* determ *)
-  inv H; inv H0; try congruence.
-  assert (b = b0) by congruence. subst b0.
-  assert (ev = ev0) by (eapply eventval_match_determ_2; eauto). subst ev0.
-  split. constructor. auto.
-  split. constructor. intuition congruence.
+  rewrite volatile_store_global_charact in *. 
+  destruct H as [b1 [A1 B1]]. destruct H0 as [b2 [A2 B2]]. rewrite A1 in A2; inv A2. 
+  eapply ec_determ. eapply volatile_store_ok. eauto. eauto. 
 Qed.
 
 (** ** Semantics of dynamic memory allocation (malloc) *)
diff --git a/common/Smallstep.v b/common/Smallstep.v
index 63ab5ea..458e8c6 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -817,12 +817,15 @@ End COMPOSE_SIMULATIONS.
 
 (** * Receptiveness and determinacy *)
 
+Definition single_events (L: semantics) : Prop :=
+  forall s t s', Step L s t s' -> (length t <= 1)%nat.
+
 Record receptive (L: semantics) : Prop :=
   Receptive {
     sr_receptive: forall s t1 s1 t2,
       Step L s t1 s1 -> match_traces (globalenv L) t1 t2 -> exists s2, Step L s t2 s2;
-    sr_traces: forall s t s',
-      Step L s t s' -> (length t <= 1)%nat
+    sr_traces:
+      single_events L
   }.
 
 Record determinate (L: semantics) : Prop :=
@@ -830,8 +833,8 @@ Record determinate (L: semantics) : Prop :=
     sd_determ: forall s t1 s1 t2 s2,
       Step L s t1 s1 -> Step L s t2 s2 ->
       match_traces (globalenv L) t1 t2 /\ (t1 = t2 -> s1 = s2);
-    sd_traces: forall s t s',
-      Step L s t s' -> (length t <= 1)%nat;
+    sd_traces:
+      single_events L;
     sd_initial_determ: forall s1 s2,
       initial_state L s1 -> initial_state L s2 -> s1 = s2;
     sd_final_nostep: forall s r,
@@ -925,8 +928,6 @@ Record backward_simulation (L1 L2: semantics) : Type :=
       exists i', exists s1',
          (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order i' i))
       /\ bsim_match_states i' s1' s2';
-    bsim_traces:
-      forall s2 t s2', Step L2 s2 t s2' -> (length t <= 1)%nat;
     bsim_symbols_preserved:
       forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id
   }.
@@ -960,9 +961,6 @@ Variable L2: semantics.
 Hypothesis symbols_preserved:
   forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id.
 
-Hypothesis length_traces:
-  forall s2 t s2', Step L2 s2 t s2' -> (length t <= 1)%nat.
-
 Variable match_states: state L1 -> state L2 -> Prop.
 
 Hypothesis initial_states_exist:
@@ -1085,6 +1083,7 @@ Section COMPOSE_BACKWARD_SIMULATIONS.
 Variable L1: semantics.
 Variable L2: semantics.
 Variable L3: semantics.
+Hypothesis L3_single_events: single_events L3.
 Variable S12: backward_simulation L1 L2.
 Variable S23: backward_simulation L2 L3.
 
@@ -1117,7 +1116,7 @@ Proof.
   intros [ [i2' [s2' [PLUS2 MATCH2]]] | [i2' [ORD2 [EQ MATCH2]]]].
   (* 1 L2 makes one or several transitions *)
   assert (EITHER: t = E0 \/ (length t = 1)%nat).
-    exploit bsim_traces; eauto. 
+    exploit L3_single_events; eauto. 
     destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction.
   destruct EITHER.
   (* 1.1 these are silent transitions *)
@@ -1202,8 +1201,6 @@ Proof.
   eapply (bsim_progress S23). eauto. eapply star_safe; eauto. eapply bsim_safe; eauto. 
 (* simulation *)
   exact bb_simulation.
-(* trace length *)
-  exact (bsim_traces S23). 
 (* symbols *)
   intros. transitivity (Genv.find_symbol (globalenv L2) id); apply bsim_symbols_preserved; auto.
 Qed.
@@ -1217,9 +1214,8 @@ Section FORWARD_TO_BACKWARD.
 Variable L1: semantics.
 Variable L2: semantics.
 Variable FS: forward_simulation L1 L2.
-
-Hypothesis receptive: receptive L1.
-Hypothesis determinate: determinate L2.
+Hypothesis L1_receptive: receptive L1.
+Hypothesis L2_determinate: determinate L2.
 
 (** Exploiting forward simulation *)
 
@@ -1391,7 +1387,7 @@ Proof.
 (* 1. At matching states *)
   exploit f2b_progress; eauto. intros TRANS; inv TRANS.
   (* 1.1  L1 can reach final state and L2 is at final state: impossible! *)
-  exploit (sd_final_nostep determinate); eauto. contradiction.
+  exploit (sd_final_nostep L2_determinate); eauto. contradiction.
   (* 1.2  L1 can make 0 or several steps; L2 can make 1 or several matching steps. *)
   inv H2. 
   exploit f2b_determinacy_inv. eexact H5. eexact STEP2.
@@ -1409,15 +1405,15 @@ Proof.
   right; split. auto. constructor.
   econstructor. eauto. auto. apply star_one; eauto. eauto. eauto. 
   (* 1.2.2 L2 makes a non-silent transition, and so does L1 *)
-  exploit not_silent_length. eapply (sr_traces receptive); eauto. intros [EQ | EQ].
+  exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ].
   congruence.
   subst t2. rewrite E0_right in H1. 
   (* Use receptiveness to equate the traces *)
-  exploit (sr_receptive receptive); eauto. intros [s1''' STEP1].
+  exploit (sr_receptive L1_receptive); eauto. intros [s1''' STEP1].
   exploit fsim_simulation_not_E0. eexact STEP1. auto. eauto. 
   intros [i''' [s2''' [P Q]]]. inv P.
   (* Exploit determinacy *)
-  exploit not_silent_length. eapply (sr_traces receptive); eauto. intros [EQ | EQ].
+  exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ].
   subst t0. simpl in *. exploit sd_determ_1. eauto. eexact STEP2. eexact H2. 
   intros. elim NOT2. inv H8. auto.
   subst t2. rewrite E0_right in *. 
@@ -1436,17 +1432,17 @@ Proof.
   right; split. apply star_refl. constructor. omega.
   econstructor; eauto. eapply star_right; eauto. 
   (* 2.2 L2 make a non-silent transition *)
-  exploit not_silent_length. eapply (sr_traces receptive); eauto. intros [EQ | EQ].
+  exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ].
   congruence.
   subst. rewrite E0_right in *.
   (* Use receptiveness to equate the traces *)
-  exploit (sr_receptive receptive); eauto. intros [s1''' STEP1].
+  exploit (sr_receptive L1_receptive); eauto. intros [s1''' STEP1].
   exploit fsim_simulation_not_E0. eexact STEP1. auto. eauto. 
   intros [i''' [s2''' [P Q]]].
   (* Exploit determinacy *)
   exploit f2b_determinacy_star. eauto. eexact STEP2. auto. apply plus_star; eauto. 
   intro R. inv R. congruence. 
-  exploit not_silent_length. eapply (sr_traces receptive); eauto. intros [EQ | EQ].
+  exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ].
   subst. simpl in *. exploit sd_determ_1. eauto. eexact STEP2. eexact H2. 
   intros. elim NOT2. inv H7; auto.  
   subst. rewrite E0_right in *. 
@@ -1482,11 +1478,11 @@ Proof.
 (* final states *)
   intros. inv H.
   exploit f2b_progress; eauto. intros TRANS; inv TRANS.
-  assert (r0 = r) by (eapply (sd_final_determ determinate); eauto). subst r0.
+  assert (r0 = r) by (eapply (sd_final_determ L2_determinate); eauto). subst r0.
   exists s1'; auto.
-  inv H4. exploit (sd_final_nostep determinate); eauto. contradiction.
-  inv H5. congruence. exploit (sd_final_nostep determinate); eauto. contradiction.
-  inv H2. exploit (sd_final_nostep determinate); eauto. contradiction.
+  inv H4. exploit (sd_final_nostep L2_determinate); eauto. contradiction.
+  inv H5. congruence. exploit (sd_final_nostep L2_determinate); eauto. contradiction.
+  inv H2. exploit (sd_final_nostep L2_determinate); eauto. contradiction.
 (* progress *)
   intros. inv H. 
   exploit f2b_progress; eauto. intros TRANS; inv TRANS. 
@@ -1496,14 +1492,265 @@ Proof.
   inv H1. right; econstructor; econstructor; eauto.
 (* simulation *)
   exact f2b_simulation_step.
-(* trace length *)
-  exact (sd_traces determinate).
 (* symbols preserved *)
   exact (fsim_symbols_preserved FS).
 Qed.
 
 End FORWARD_TO_BACKWARD.
 
+(** * Transforming a semantics into a single-event, equivalent semantics *)
+
+Definition well_behaved_traces (L: semantics) : Prop :=
+  forall s t s', Step L s t s' ->
+  match t with nil => True | ev :: t' => output_trace t' end.
+
+Section ATOMIC.
+
+Variable L: semantics.
+
+Hypothesis Lwb: well_behaved_traces L.
+
+Inductive atomic_step (ge: Genv.t (funtype L) (vartype L)): (trace * state L) -> trace -> (trace * state L) -> Prop :=
+  | atomic_step_silent: forall s s',
+      Step L s E0 s' ->
+      atomic_step ge (E0, s) E0 (E0, s')
+  | atomic_step_start: forall s ev t s',
+      Step L s (ev :: t) s' ->
+      atomic_step ge (E0, s) (ev :: nil) (t, s')
+  | atomic_step_continue: forall ev t s,
+      output_trace (ev :: t) ->
+      atomic_step ge (ev :: t, s) (ev :: nil) (t, s).
+
+Definition atomic : semantics := {|
+  state := (trace * state L)%type;
+  funtype := funtype L;
+  vartype := vartype L;
+  step := atomic_step;
+  initial_state := fun s => initial_state L (snd s) /\ fst s = E0;
+  final_state := fun s r => final_state L (snd s) r /\ fst s = E0;
+  globalenv := globalenv L
+|}.
+
+End ATOMIC.
+
+(** A forward simulation from a semantics [L1] to a single-event semantics [L2]
+  can be "factored" into a forward simulation from [atomic L1] to [L2]. *)
+
+Section FACTOR_FORWARD_SIMULATION.
+
+Variable L1: semantics.
+Variable L2: semantics.
+Variable sim: forward_simulation L1 L2.
+Hypothesis L2single: single_events L2.
+
+Inductive ffs_match: fsim_index sim -> (trace * state L1) -> state L2 -> Prop :=
+  | ffs_match_at: forall i s1 s2,
+      sim i s1 s2 ->
+      ffs_match i (E0, s1) s2
+  | ffs_match_buffer: forall i ev t s1 s2 s2',
+      Star L2 s2 (ev :: t) s2' -> sim i s1 s2' ->
+      ffs_match i (ev :: t, s1) s2.
+
+Lemma star_non_E0_split':
+  forall s2 t s2', Star L2 s2 t s2' -> 
+  match t with
+  | nil => True
+  | ev :: t' => exists s2x, Plus L2 s2 (ev :: nil) s2x /\ Star L2 s2x t' s2'
+  end.
+Proof.
+  induction 1. simpl. auto.
+  exploit L2single; eauto. intros LEN. 
+  destruct t1. simpl in *. subst. destruct t2. auto. 
+  destruct IHstar as [s2x [A B]]. exists s2x; split; auto.
+  eapply plus_left. eauto. apply plus_star; eauto. auto. 
+  destruct t1. simpl in *. subst t. exists s2; split; auto. apply plus_one; auto.
+  simpl in LEN. omegaContradiction.
+Qed.  
+
+Lemma ffs_simulation:
+  forall s1 t s1', Step (atomic L1) s1 t s1' ->
+  forall i s2, ffs_match i s1 s2 ->
+  exists i', exists s2',
+     (Plus L2 s2 t s2' \/ (Star L2 s2 t s2') /\ fsim_order sim i' i)
+  /\ ffs_match i' s1' s2'.
+Proof.
+  induction 1; intros.
+(* silent step *)
+  inv H0. 
+  exploit (fsim_simulation sim); eauto. 
+  intros [i' [s2' [A B]]]. 
+  exists i'; exists s2'; split. auto. constructor; auto.
+(* start step *)
+  inv H0. 
+  exploit (fsim_simulation sim); eauto. 
+  intros [i' [s2' [A B]]].
+  destruct t as [ | ev' t]. 
+  (* single event *)
+  exists i'; exists s2'; split. auto. constructor; auto.
+  (* multiple events *)
+  assert (C: Star L2 s2 (ev :: ev' :: t) s2'). intuition. apply plus_star; auto. 
+  exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]]. 
+  exists i'; exists s2x; split. auto. econstructor; eauto.
+(* continue step *)
+  inv H0. 
+  exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]]. 
+  destruct t. 
+  exists i; exists s2'; split. left. eapply plus_star_trans; eauto. constructor; auto. 
+  exists i; exists s2x; split. auto. econstructor; eauto. 
+Qed.
+
+Theorem factor_forward_simulation:
+  forward_simulation (atomic L1) L2.
+Proof.
+  apply Forward_simulation with (fsim_match_states := ffs_match) (fsim_order := fsim_order sim).
+(* wf *)
+  apply fsim_order_wf.
+(* initial states *)
+  intros. destruct s1 as [t1 s1]. simpl in H. destruct H. subst. 
+  exploit (fsim_match_initial_states sim); eauto. intros [i [s2 [A B]]]. 
+  exists i; exists s2; split; auto. constructor; auto.
+(* final states *)
+  intros. destruct s1 as [t1 s1]. simpl in H0; destruct H0; subst. inv H. 
+  eapply (fsim_match_final_states sim); eauto.
+(* simulation *)
+  exact ffs_simulation.
+(* symbols preserved *)
+  simpl. exact (fsim_symbols_preserved sim).
+Qed.
+
+End FACTOR_FORWARD_SIMULATION.
+
+(** Likewise, a backward simulation from a single-event semantics [L1] to a semantics [L2]
+  can be "factored" as a backward simulation from [L1] to [atomic L2]. *)
+
+Section FACTOR_BACKWARD_SIMULATION.
+
+Variable L1: semantics.
+Variable L2: semantics.
+Variable sim: backward_simulation L1 L2.
+Hypothesis L1single: single_events L1.
+Hypothesis L2wb: well_behaved_traces L2.
+
+Inductive fbs_match: bsim_index sim -> state L1 -> (trace * state L2) -> Prop :=
+  | fbs_match_intro: forall i s1 t s2 s1',
+      Star L1 s1 t s1' -> sim i s1' s2 ->
+      t = E0 \/ output_trace t ->
+      fbs_match i s1 (t, s2).
+
+Lemma fbs_simulation:
+  forall s2 t s2', Step (atomic L2) s2 t s2' ->
+  forall i s1, fbs_match i s1 s2 -> safe L1 s1 ->
+  exists i', exists s1',
+     (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order sim i' i))
+     /\ fbs_match i' s1' s2'.
+Proof.
+  induction 1; intros.
+(* silent step *)
+  inv H0.
+  exploit (bsim_simulation sim); eauto. eapply star_safe; eauto. 
+  intros [i' [s1'' [A B]]].
+  exists i'; exists s1''; split.
+  destruct A as [P | [P Q]]. left. eapply star_plus_trans; eauto. right; split; auto. eapply star_trans; eauto. 
+  econstructor. apply star_refl. auto. auto.
+(* start step *)
+  inv H0.
+  exploit (bsim_simulation sim); eauto. eapply star_safe; eauto. 
+  intros [i' [s1'' [A B]]].
+  assert (C: Star L1 s1 (ev :: t) s1'').
+    eapply star_trans. eauto. destruct A as [P | [P Q]]. apply plus_star; eauto. eauto. auto. 
+  exploit star_non_E0_split'; eauto. simpl. intros [s1x [P Q]].
+  exists i'; exists s1x; split.
+  left; auto.
+  econstructor; eauto.
+  exploit L2wb; eauto. 
+(* continue step *)
+  inv H0. unfold E0 in H8; destruct H8; try congruence.
+  exploit star_non_E0_split'; eauto. simpl. intros [s1x [P Q]].
+  exists i; exists s1x; split. left; auto. econstructor; eauto. simpl in H0; tauto. 
+Qed.
+
+Lemma fbs_progress:
+  forall i s1 s2, 
+  fbs_match i s1 s2 -> safe L1 s1 ->
+  (exists r, final_state (atomic L2) s2 r) \/
+  (exists t, exists s2', Step (atomic L2) s2 t s2').
+Proof.
+  intros. inv H. destruct t.  
+(* 1. no buffered events *)
+  exploit (bsim_progress sim); eauto. eapply star_safe; eauto.
+  intros [[r A] | [t [s2' A]]]. 
+(* final state *)
+  left; exists r; simpl; auto.
+(* L2 can step *) 
+  destruct t. 
+  right; exists E0; exists (nil, s2'). constructor. auto.
+  right; exists (e :: nil); exists (t, s2'). constructor. auto.
+(* 2. some buffered events *)
+  unfold E0 in H3; destruct H3. congruence. 
+  right; exists (e :: nil); exists (t, s3). constructor. auto. 
+Qed.
+
+Theorem factor_backward_simulation:
+  backward_simulation L1 (atomic L2).
+Proof.
+  apply Backward_simulation with (bsim_match_states := fbs_match) (bsim_order := bsim_order sim).
+(* wf *)
+  apply bsim_order_wf.
+(* initial states exist *)
+  intros. exploit (bsim_initial_states_exist sim); eauto. intros [s2 A].
+  exists (E0, s2). simpl; auto. 
+(* initial states match *)
+  intros. destruct s2 as [t s2]; simpl in H0; destruct H0; subst.
+  exploit (bsim_match_initial_states sim); eauto. intros [i [s1' [A B]]]. 
+  exists i; exists s1'; split. auto. econstructor. apply star_refl. auto. auto.
+(* final states match *)
+  intros. destruct s2 as [t s2]; simpl in H1; destruct H1; subst.
+  inv H. exploit (bsim_match_final_states sim); eauto. eapply star_safe; eauto. 
+  intros [s1'' [A B]]. exists s1''; split; auto. eapply star_trans; eauto.
+(* progress *)
+  exact fbs_progress.
+(* simulation *)
+  exact fbs_simulation.
+(* symbols *)
+  simpl. exact (bsim_symbols_preserved sim).
+Qed.
+
+End FACTOR_BACKWARD_SIMULATION.
+
+(** Receptiveness of [atomic L]. *)
+
+Record strongly_receptive (L: semantics) : Prop :=
+  Strongly_receptive {
+    ssr_receptive: forall s ev1 t1 s1 ev2,
+      Step L s (ev1 :: t1) s1 ->
+      match_traces (globalenv L) (ev1 :: nil) (ev2 :: nil) ->
+      exists s2, exists t2, Step L s (ev2 :: t2) s2;
+    ssr_well_behaved:
+      well_behaved_traces L
+  }.
+
+Theorem atomic_receptive:
+  forall L, strongly_receptive L -> receptive (atomic L).
+Proof.
+  intros. constructor; intros.
+(* receptive *)
+  inv H0. 
+  (* silent step *)
+  inv H1. exists (E0, s'). constructor; auto.
+  (* start step *)
+  assert (exists ev2, t2 = ev2 :: nil). inv H1; econstructor; eauto. 
+  destruct H0 as [ev2 EQ]; subst t2.
+  exploit ssr_receptive; eauto. intros [s2 [t2 P]].
+  exploit ssr_well_behaved. eauto. eexact P. simpl; intros Q. 
+  exists (t2, s2). constructor; auto.
+  (* continue step *)
+  simpl in H2; destruct H2. 
+  assert (t2 = ev :: nil). inv H1; simpl in H0; tauto.
+  subst t2. exists (t, s0). constructor; auto. simpl; auto.  
+(* single-event *)
+  red. intros. inv H0; simpl; omega.
+Qed.
+
 (** * Connections with big-step semantics *)
 
 (** The general form of a big-step semantics *)
diff --git a/common/Values.v b/common/Values.v
index 7fae3b7..54eac86 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -160,6 +160,13 @@ Definition notint (v: val) : val :=
 
 Definition of_bool (b: bool): val := if b then Vtrue else Vfalse.
 
+Definition boolval (v: val) : val :=
+  match v with
+  | Vint n => of_bool (negb (Int.eq n Int.zero))
+  | Vptr b ofs => Vtrue
+  | _ => Vundef
+  end.
+
 Definition notbool (v: val) : val :=
   match v with
   | Vint n => of_bool (Int.eq n Int.zero)