added the exmem effect for AArch64 store-exclusive

22 files changed, 88 insertions, 41 deletions

diff --git a/src/ast.ml b/src/ast.ml
index 5eb45554..186d7f9a 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -119,6 +119,7 @@ base_effect_aux =  (* effect *)
  | BE_rmem (* read memory *)
  | BE_wmem (* write memory *)
  | BE_eamem (* signal effective address for writing memory *)
+ | BE_exmem (* determine if a store-exclusive (ARM) is going to succeed *)
  | BE_wmv (* write memory, sending only value *)
  | BE_barr (* memory barrier *)
  | BE_depend (* dynamic footprint *)
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index dd97541f..426b0811 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -11,6 +11,7 @@ let rec bind m f = match m with
   | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
   | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
   | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (bind o f,opt))
+  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (bind o f,opt))
   | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (bind o f,opt))
   | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (bind o f,opt))
   | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (bind o f,opt))
@@ -40,6 +41,11 @@ let read_mem dir rk addr sz =
     (Done bitv,Nothing) in
   Read_mem (rk,addr,sz) k
 
+val excl_result : unit -> M bool
+let excl_result () =
+  let k successful = (return successful,Nothing) in
+  Excl_res k
+
 val write_mem_ea : write_kind -> vector bitU -> integer -> M unit
 let write_mem_ea wk addr sz =
   let addr = address_lifted_of_bitv addr in
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 0dfd10d7..ddd30eda 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -66,7 +66,11 @@ let read_mem dir read_kind addr sz state =
   then [(Left value, <| state with last_exclusive_operation_was_load = true |>)]
   else [(Left value, state)]
   
-
+val excl_result : unit -> M bool
+let excl_result () state =
+  let success =
+    (Left true,  <| state with last_exclusive_operation_was_load = false |>) in
+  (Left false, state) :: if state.last_exclusive_operation_was_load then [success] else []
 
 val write_mem_ea : write_kind -> vector bitU -> integer -> M unit
 let write_mem_ea write_kind addr sz state = 
@@ -83,29 +87,7 @@ let write_mem_val v state =
   let addresses_with_value = List.zip addrs v in
   let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
                             state.memstate addresses_with_value in
-
-  let is_exclusive = match write_kind with
-    | Sail_impl_base.Write_plain -> false
-    | Sail_impl_base.Write_tag -> failwith "Write_tag not implemented"
-    | Sail_impl_base.Write_tag_conditional -> failwith "Write_tag_conditional not implemented"
-    | Sail_impl_base.Write_conditional -> true
-    | Sail_impl_base.Write_release -> false
-    | Sail_impl_base.Write_exclusive -> true
-    | Sail_impl_base.Write_exclusive_release -> true
-  end in
-
-  if is_exclusive 
-  then
-    let success =
-      (Left true,  <| state with memstate = memstate; 
-                                 last_exclusive_operation_was_load = false |>) in
-    let failure =
-      (Left false, <| state with last_exclusive_operation_was_load = false |>) in
-    if state.last_exclusive_operation_was_load
-    then [failure;success]
-    else [failure]
-  else [(Left true, <| state with memstate = memstate |>)]
-
+  [(Left true,  <| state with memstate = memstate |>)]
 
 
 val read_reg : register -> M (vector bitU)
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 82cc6b7c..a0d4d312 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -280,6 +280,7 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect =
                                | Parse_ast.BE_wmem   -> BE_wmem
 			       | Parse_ast.BE_wmv    -> BE_wmv
 			       | Parse_ast.BE_eamem  -> BE_eamem
+			       | Parse_ast.BE_exmem  -> BE_exmem
 			       | Parse_ast.BE_depend -> BE_depend
                                | Parse_ast.BE_undef  -> BE_undef
                                | Parse_ast.BE_unspec -> BE_unspec
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 24f624e3..4de1e869 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -359,6 +359,7 @@ type action =
  | Write_mem of id * value * maybe (nat * nat) * value
  | Write_ea of id * value
  | Write_memv of id * value * value
+ | Excl_res of id * value
  | Barrier of id * value
  | Footprint of id * value
  | Nondet of list (exp tannot) * tag
@@ -2242,6 +2243,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                 mk_hole_frame (Write_mem (id_of_string name_ext) v Nothing wv)
           else if has_eamem_effect effects
           then mk_thunk_frame (Write_ea (id_of_string name_ext) v)
+          else if has_exmem_effect effects
+          then mk_thunk_frame (Excl_res (id_of_string name_ext) v)
           else if has_wmv_effect effects
           then let (wv,v) =
                  match v with
diff --git a/src/lem_interp/interp_ast.lem b/src/lem_interp/interp_ast.lem
index 64fb14b2..6091e8b1 100644
--- a/src/lem_interp/interp_ast.lem
+++ b/src/lem_interp/interp_ast.lem
@@ -121,6 +121,7 @@ type base_effect_aux =  (* effect *)
  | BE_rmem (* read memory *)
  | BE_wmem (* write memory *)
  | BE_eamem (* signal effective address for writing memory *)
+ | BE_exmem (* determine if a store-exclusive (ARM) is going to succeed *)
  | BE_wmv (* write memory, sending only value *)
  | BE_barr (* memory barrier *)
  | BE_depend (* dynamic footprint *)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 72bf0bcc..3e71ba37 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -430,6 +430,8 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
       (Ivh_error (Interp_interface.Internal_error ("Write memory request in a " ^ errk_str)), events_out)
     | (Interp.Action (Interp.Write_ea _ _) _,_,_) ->
       (Ivh_error (Interp_interface.Internal_error ("Write ea request in a " ^ errk_str)), events_out)
+    | (Interp.Action (Interp.Excl_res _ _) _,_,_) ->
+      (Ivh_error (Interp_interface.Internal_error ("Exclusive result request in a " ^ errk_str)), events_out)
     | (Interp.Action (Interp.Write_memv _ _ _) _,_,_) ->
       (Ivh_error (Interp_interface.Internal_error ("Write memory value request in a " ^ errk_str)), events_out)
     | _ -> (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str)), events_out)
@@ -443,19 +445,19 @@ let call_external_functions direction outcome =
         | Just f -> Just (f value) end
     | _ -> Nothing end
 
-let build_context defs reads writes write_eas write_vals barriers externs = 
+let build_context defs reads writes write_eas write_vals barriers excl_res externs =
   (*TODO add externs to to_top_env*)
   match Interp.to_top_env call_external_functions defs with 
     | (_,((Interp.Env _ _ dir _ _ _ _ _) as context)) -> 
       Context context (if Interp.is_inc(dir) then D_increasing else D_decreasing)
-        reads writes write_eas write_vals barriers externs end
+        reads writes write_eas write_vals barriers excl_res externs end
 
 
 let translate_address top_level end_flag thunk_name registers address =
   let (Address bytes i) = address in
   let mode = make_mode true false in
   let int_mode = mode.internal_mode in
-  let (Context top_env direction _ _ _ _ _ _) = top_level in
+  let (Context top_env direction _ _ _ _ _ _ _) = top_level in
   let intern_val = intern_mem_value mode direction (memory_value_of_address end_flag address) in
   let val_str = Interp.string_of_value intern_val in
   let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
@@ -499,7 +501,7 @@ let intern_instruction direction (name,parms) =
 let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers instruction =
   let mode = make_mode true false in
   let int_mode = mode.internal_mode in
-  let (Context top_env direction _ _ _ _ _ _) = top_level in
+  let (Context top_env direction _ _ _ _ _ _ _) = top_level in
   let intern_val = intern_instruction direction instruction in
   let val_str = Interp.string_of_value intern_val in
   let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
@@ -641,7 +643,7 @@ end
 
 
 let interp_value_to_instr_external top_level instr = 
-  let (Context (Interp.Env _ instructions _ _ _ _ _ _) _ _ _ _ _ _ _) = top_level in
+  let (Context (Interp.Env _ instructions _ _ _ _ _ _) _ _ _ _ _ _ _ _) = top_level in
   match instr with
   | Interp.V_ctor (Id_aux (Id i) _) _ _ parm ->
      match (find_instruction i instructions) with
@@ -666,7 +668,7 @@ let interp_value_to_instr_external top_level instr =
 
 let decode_to_instruction top_level registers value : instruction_or_decode_error = 
   let mode = make_interpreter_mode true false in
-  let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _) = top_level in
+  let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _ _) = top_level in
   let intern_val = intern_opcode direction value in
   let val_str = Interp.string_of_value intern_val in
   let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in
@@ -703,7 +705,7 @@ end
 
 
 let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_error = 
-  let (Context top_env _ _ _ _ _ _ _) = top_level in
+  let (Context top_env _ _ _ _ _ _ _ _) = top_level in
   match decode_to_instruction top_level registers value with
   | IDE_instr instr instrv ->
      let mode = make_interpreter_mode true false in
@@ -718,7 +720,7 @@ let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_e
 
 
 let instr_external_to_interp_value top_level instr =
-  let (Context _ direction _ _ _ _ _ _) = top_level in
+  let (Context _ direction _ _ _ _ _ _ _) = top_level in
   let (name,parms) = instr in
 
   let get_value (_,typ,v) = 
@@ -745,7 +747,7 @@ let instr_external_to_interp_value top_level instr =
 val instruction_to_istate : context -> instruction -> instruction_state 
 let instruction_to_istate (top_level:context) (((name, parms) as instr):instruction) : instruction_state  = 
   let mode = make_interpreter_mode true false in
-  let (Context top_env _ _ _ _ _ _ _) = top_level in
+  let (Context top_env _ _ _ _ _ _ _ _) = top_level in
   let ast_node = fst (Interp.to_exp mode Interp.eenv (instr_external_to_interp_value top_level instr)) in
   (IState
      (Interp.Thunk_frame
@@ -755,7 +757,7 @@ let instruction_to_istate (top_level:context) (((name, parms) as instr):instruct
      top_level)
 
 let rec interp_to_outcome mode context thunk = 
-  let (Context _ direction mem_reads mem_writes mem_write_eas mem_write_vals barriers spec_externs) = context in
+  let (Context _ direction mem_reads mem_writes mem_write_eas mem_write_vals barriers excl_res spec_externs) = context in
   let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
   match thunk () with
   | (Interp.Value _,lm,le) -> (Done,lm)
@@ -813,7 +815,15 @@ let rec interp_to_outcome mode context thunk =
               Write_ea write_k (Address_lifted location address_int) length tracking (IState next_state context)
             else Error "Memory address for write is not 64 bits"
           | _ -> Error ("Memory function " ^ i ^ " to signal impending write, not found") end, lm)
-        | Interp.Write_memv (Id_aux (Id i) _) address_val write_val ->
+      | Interp.Excl_res (Id_aux (Id i) _) loc_val ->
+        (match excl_res with
+          | (Just (i', ER return)) ->
+              Excl_res (fun b ->
+                          match return with
+                          | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context)
+                          | Just return_bool -> return_bool (IState next_state context) b end)
+          | _ -> Error ("Exclusive result function, not provided") end, lm)
+      | Interp.Write_memv (Id_aux (Id i) _) address_val write_val ->
            (match List.lookup i mem_write_vals with
             | (Just (MV parmf return)) -> 
               let (value, v_tracking) = 
@@ -899,7 +909,7 @@ end
 
 (*ie_loop returns a tuple of event list, and a tuple ofinternal interpreter memory, bool to indicate normal or exceptional termination*)
 let rec ie_loop mode register_values (IState interp_state context) = 
-  let (Context _ direction externs reads writes write_eas write_vals barriers) = context in
+  let (Context _ direction externs reads writes write_eas write_vals barriers excl_res) = context in
   let unknown_reg size =  
     <| rv_bits = (List.replicate size Bitl_unknown);
        rv_start = 0;
@@ -935,6 +945,11 @@ let rec ie_loop mode register_values (IState interp_state context) =
     | (Write_ea write_k loc length tracking i_state, _) ->
       let (events,analysis_data) = ie_loop mode register_values i_state in
       ((E_write_ea write_k loc length tracking)::events,analysis_data)
+    | (Excl_res i_state_fun, _) ->
+      let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in
+      let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in
+      (*TODO: consider if lm and lm should be merged*)
+      (E_excl_res :: (events ++ events'), analysis_data)
     | (Write_memv opt_address value tracking i_state_fun, _) ->
       let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in
       let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in
@@ -995,6 +1010,8 @@ let rec outcome_to_outcome pp_instruction_state mode =
      failwith "Write_mem not supported anymore"
   | Interp_interface.Write_ea wk addr size _ state ->
      Sail_impl_base.Write_ea (wk,addr,size) (state_to_outcome_s mode state)
+  | Interp_interface.Excl_res k ->
+     Sail_impl_base.Excl_res (fun v -> state_to_outcome_s mode (k v))
   | Interp_interface.Write_memv _ mv _ k ->
      Sail_impl_base.Write_memv mv (fun v -> state_to_outcome_s mode (k v))
   | Interp_interface.Barrier bk state ->
@@ -1078,6 +1095,7 @@ let instruction_kind_of_event : event -> maybe instruction_kind = function
   | E_read_mem rk _ _ _ -> Just (IK_mem_read rk)
   | E_write_mem wk _ _ _ _ _  -> Just (IK_mem_write wk)
   | E_write_ea wk _ _ _ -> Just (IK_mem_write wk)
+  | E_excl_res -> Nothing
   | E_write_memv _ _ _ -> Nothing
   | E_barrier bk -> Just (IK_barrier bk)
   | E_footprint -> Nothing
@@ -1093,6 +1111,7 @@ let regs_in_of_event : event -> list reg_name = function
   | E_read_mem _ _ _ _ -> []
   | E_write_mem _ _ _ _ _ _  -> []
   | E_write_ea _ _ _ _ -> []
+  | E_excl_res -> []
   | E_write_memv _ _ _ -> []
   | E_barrier _ -> []
   | E_footprint -> []
@@ -1106,6 +1125,7 @@ let regs_out_of_event : event -> list reg_name = function
   | E_read_mem _ _ _ _ -> []
   | E_write_mem _ _ _ _ _ _  -> []
   | E_write_ea _ _ _ _ -> []
+  | E_excl_res -> []
   | E_write_memv _ _ _ -> []
   | E_barrier _ -> []
   | E_footprint -> []
@@ -1123,6 +1143,7 @@ let regs_feeding_memory_access_address_of_event : event -> list reg_name = funct
   | E_write_mem _ _ _ None _ _       -> []
   | E_write_ea wk _ _ (Just rs)      -> rs
   | E_write_ea wk _ _ None           -> []
+  | E_excl_res                       -> []
   | E_write_memv _ _ _               -> []
   | E_barrier bk                     -> []
   | E_footprint                      -> []
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 3ef6abb8..77572de9 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -185,11 +185,13 @@ type memory_write = MW of write_kind * memory_parameter_transformer * (maybe (in
 and memory_writes = list (string * memory_write)
 and memory_write_val = MV of optional_memory_transformer * (maybe (instruction_state -> bool -> instruction_state))
 and memory_write_vals = list (string * memory_write_val)
+and excl_res_t = ER of maybe (instruction_state -> bool -> instruction_state)
+and excl_res = maybe (string * excl_res_t)
 
 (* Definition information needed to run an instruction *)
 and context =
     Context of Interp.top_level * direction * 
-	memory_reads * memory_writes * memory_write_eas * memory_write_vals * barriers * external_functions
+	memory_reads * memory_writes * memory_write_eas * memory_write_vals * barriers * excl_res * external_functions
 
 (* An instruction in flight *)
 and instruction_state = IState of interpreter_state * context
@@ -204,6 +206,9 @@ type outcome =
 | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name)
   * memory_value * maybe (list reg_name)  * (bool -> instruction_state)
 
+(* Request the result of store-exclusive *)
+| Excl_res of (bool -> instruction_state)
+
 (* Tell the system a write is imminent, at address lifted tainted by register list, of size nat *)
 | Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * instruction_state
 
@@ -248,7 +253,7 @@ type outcome =
 
 
 (* Functions to build up the initial state for interpretation *)
-val build_context : specification -> memory_reads -> memory_writes -> memory_write_eas -> memory_write_vals -> barriers -> external_functions -> context 
+val build_context : specification -> memory_reads -> memory_writes -> memory_write_eas -> memory_write_vals -> barriers -> excl_res -> external_functions -> context
 val initial_instruction_state : context -> string -> list register_value -> instruction_state 
   (* string is a function name, list of value are the parameters to that function *)
 
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
index 86042d61..2c338ff7 100644
--- a/src/lem_interp/interp_utilities.lem
+++ b/src/lem_interp/interp_utilities.lem
@@ -119,6 +119,7 @@ let rec has_effect which efcts =
     | (BE_wmem,BE_wmem)     -> true 
     | (BE_wmv,BE_wmv)       -> true
     | (BE_eamem,BE_eamem)   -> true
+    | (BE_exmem,BE_exmem)   -> true
     | (BE_barr,BE_barr)     -> true 
     | (BE_undef,BE_undef)   -> true 
     | (BE_unspec,BE_unspec) -> true 
@@ -131,6 +132,7 @@ let has_rmem_effect = has_effect BE_rmem
 let has_barr_effect = has_effect BE_barr
 let has_wmem_effect = has_effect BE_wmem
 let has_eamem_effect = has_effect BE_eamem
+let has_exmem_effect = has_effect BE_exmem
 let has_wmv_effect = has_effect BE_wmv
 let has_depend_effect = has_effect BE_depend
 
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 7d182258..855658b4 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -125,6 +125,7 @@ let doc_effect (BE_aux (e,_)) =
   | BE_wmem -> "wmem"
   | BE_wmv  -> "wmv"
   | BE_eamem -> "eamem"
+  | BE_exmem -> "exmem"
   | BE_barr -> "barr"
   | BE_depend -> "depend"
   | BE_undef -> "undef"
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 4922a59a..01c828dd 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -434,6 +434,8 @@ let rec format_events = function
     "     Write_ea at " ^ (memory_value_to_string E_big_endian location) ^ ", based on registers " ^
       format_tracking tracking ^ " across " ^ (string_of_int length) ^ " bytes\n" ^ 
       (format_events events)
+  | E_excl_res::events ->
+    "     Excl_res\n" ^ (format_events events)
   | (E_write_memv(_, value, v_tracking))::events ->
     "     Write_memv of " ^ (memory_value_to_string E_big_endian value) ^ ", based on registers " ^
       format_tracking v_tracking ^ "\n" ^
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 8be5354a..600699ec 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -377,6 +377,10 @@ let run
         | Write_ea1(_,(Address_lifted(location,_)), size,_,next) ->
           show "write_announce" (memory_value_to_string !default_endian location) left ((string_of_int size) ^ " bytes");
           (step next, env, next)
+        | Excl_res1(next_thunk) ->
+          show "exclusive_result" "" "" "";
+          let next = next_thunk true in
+          (step next,env',next)
         | Barrier1(bkind,next) ->
           show "mem_barrier" "" "" "";
           (step next, env, next)
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 02d53896..fad04a51 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -780,6 +780,7 @@ type event =
 | E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
 | E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name)
 | E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name)
+| E_excl_res
 | E_write_memv of maybe address_lifted * memory_value * maybe (list reg_name)
 | E_barrier of barrier_kind
 | E_footprint 
@@ -797,6 +798,7 @@ let eventCompare e1 e2 =
     compare ((wk1,v1,i1),(tr1,v1',tr1'))  ((wk2,v2,i2),(tr2,v2',tr2')) 
   | (E_write_ea wk1 a1 i1 tr1, E_write_ea wk2 a2 i2 tr2) ->
     compare (wk1, (a1, i1, tr1)) (wk2, (a2, i2, tr2))
+  | (E_excl_res, E_excl_res) -> EQ
   | (E_write_memv _ mv1 tr1, E_write_memv _ mv2 tr2) -> compare (mv1,tr1) (mv2,tr2)
   | (E_barrier bk1, E_barrier bk2) -> compare bk1 bk2
   | (E_read_reg r1, E_read_reg r2) -> compare r1 r2
@@ -806,6 +808,7 @@ let eventCompare e1 e2 =
   | (E_read_mem _ _ _ _, _) -> LT
   | (E_write_mem _ _ _ _ _ _, _) -> LT
   | (E_write_ea _ _ _ _, _) -> LT
+  | (E_excl_res, _) -> LT
   | (E_write_memv _ _ _, _) -> LT
   | (E_barrier _, _) -> LT
   | (E_read_reg _, _) -> LT
@@ -839,6 +842,8 @@ type outcome 'a =
   | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome 'a))
   (* Tell the system a write is imminent, at address lifted, of size nat *)
   | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome 'a))
+  (* Request the result of store-exclusive *)
+  | Excl_res of (bool -> with_aux (outcome 'a))
   (* Request to write memory at last signalled address. Memory value should be 8
      times the size given in ea signal *)
   | Write_memv of memory_value * (bool -> with_aux (outcome 'a))
diff --git a/src/lexer.mll b/src/lexer.mll
index 98c9098d..921be112 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -120,6 +120,7 @@ let kw_table =
      ("wmem",                    (fun x -> Wmem));
      ("wmv",                     (fun x -> Wmv));
      ("eamem",                   (fun x -> Eamem));
+     ("exmem",                   (fun x -> Exmem));
      ("undef",                   (fun x -> Undef));
      ("unspec",                  (fun x -> Unspec));
      ("nondet",                  (fun x -> Nondet));
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 2e72761e..68ebbf9b 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -80,6 +80,7 @@ base_effect_aux =  (* effect *)
  | BE_wmem (* write memory *)
  | BE_wmv (* write memory value *)
  | BE_eamem (* address for write signaled *)
+ | BE_exmem (* determine if a store-exclusive (ARM) is going to succeed *)
  | BE_barr (* memory barrier *)
  | BE_depend (* dynmically dependent footprint *)
  | BE_undef (* undefined-instruction exception *)
diff --git a/src/parser.mly b/src/parser.mly
index d172f61b..fce6ff9d 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -132,7 +132,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %token Enumerate Else Exit Extern False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order 
 %token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef 
 %token Undefined Union With Val
-%token Barr Depend Rreg Wreg Rmem Wmem Wmv Eamem Undef Unspec Nondet Escape
+%token Barr Depend Rreg Wreg Rmem Wmem Wmv Eamem Exmem Undef Unspec Nondet Escape
 
 
 /* Avoid shift/reduce conflict - see right_atomic_exp rule */
@@ -315,6 +315,8 @@ effect:
     { efl BE_wmv }
   | Eamem
     { efl BE_eamem }
+  | Exmem
+    { efl BE_exmem }
   | Undef
     { efl BE_undef }
   | Unspec
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index e90d9cf1..51cf070b 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -91,6 +91,7 @@ let doc_effect (BE_aux (e,_)) =
   | BE_wmem -> "wmem"
   | BE_wmv  -> "wmv"
   | BE_eamem -> "eamem"
+  | BE_exmem -> "exmem"
   | BE_barr -> "barr"
   | BE_depend -> "depend"
   | BE_escape -> "escape"
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index b55685f4..a436cf90 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -125,8 +125,8 @@ let effectful (Effect_aux (eff,_)) =
      List.exists
        (fun (BE_aux (eff,_)) ->
          match eff with
-         | BE_rreg | BE_wreg | BE_rmem | BE_wmem | BE_eamem | BE_wmv
-         | BE_barr | BE_depend | BE_nondet | BE_escape -> true
+         | BE_rreg | BE_wreg | BE_rmem | BE_wmem | BE_eamem | BE_exmem
+         | BE_wmv | BE_barr | BE_depend | BE_nondet | BE_escape -> true
          | _ -> false)
        effs
 
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 03b8bdf5..268aeb2f 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -184,6 +184,7 @@ and pp_format_base_effect_lem (BE_aux(e,l)) =
     | BE_wmem -> "BE_wmem"
     | BE_wmv  -> "BE_wmv"
     | BE_eamem -> "BE_eamem"
+    | BE_exmem -> "BE_exmem"
     | BE_barr -> "BE_barr"
     | BE_depend -> "BE_depend"
     | BE_undef -> "BE_undef"
diff --git a/src/pretty_print_t_ascii.ml b/src/pretty_print_t_ascii.ml
index 79897f4b..1494ca0a 100644
--- a/src/pretty_print_t_ascii.ml
+++ b/src/pretty_print_t_ascii.ml
@@ -99,6 +99,7 @@ and pp_format_base_effect_ascii (BE_aux(e,l)) =
     | BE_wmem -> "wmem"
     | BE_wmv  -> "wmv"
     | BE_eamem -> "eamem"
+    | BE_exmem -> "exmem"
     | BE_barr -> "barr"
     | BE_depend -> "depend"
     | BE_undef -> "undef"
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 2eaef407..45630d3e 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -385,6 +385,7 @@ and ef_to_string (Ast.BE_aux(b,l)) =
       | Ast.BE_wmem  -> "wmem"
       | Ast.BE_wmv   -> "wmv"
       | Ast.BE_eamem -> "eamem"
+      | Ast.BE_exmem -> "exmem"
       | Ast.BE_barr  -> "barr"
       | Ast.BE_undef -> "undef"
       | Ast.BE_depend -> "depend"
@@ -3084,6 +3085,9 @@ let compare_effect (BE_aux(e1,_)) (BE_aux(e2,_)) =
   | (BE_eamem,BE_eamem) -> 0
   | (BE_eamem,_) -> -1
   | (_,BE_eamem) -> 1
+  | (BE_exmem,BE_exmem) -> 0
+  | (BE_exmem,_) -> -1
+  | (_,BE_exmem) -> 1
   | (BE_barr,BE_barr) -> 0
   | (BE_barr,_) -> 1
   | (_,BE_barr) -> -1
@@ -3141,6 +3145,7 @@ let has_wreg_effect = has_effect (BE_aux(BE_wreg, Parse_ast.Unknown))
 let has_rmem_effect = has_effect (BE_aux(BE_rmem, Parse_ast.Unknown))
 let has_wmem_effect = has_effect (BE_aux(BE_wmem, Parse_ast.Unknown))
 let has_eamem_effect = has_effect (BE_aux(BE_eamem, Parse_ast.Unknown))
+let has_exmem_effect = has_effect (BE_aux(BE_exmem, Parse_ast.Unknown))
 let has_memv_effect = has_effect (BE_aux(BE_wmv, Parse_ast.Unknown))
 let has_lret_effect = has_effect (BE_aux(BE_lret, Parse_ast.Unknown))
 
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 4912585a..f6f196a9 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -250,6 +250,7 @@ val has_wreg_effect : effect -> bool
 val has_rmem_effect : effect -> bool
 val has_wmem_effect : effect -> bool
 val has_eamem_effect : effect -> bool
+val has_exmem_effect : effect -> bool
 val has_memv_effect : effect -> bool
 val has_lret_effect : effect -> bool