open Atomic_deadlock open MachineDefTypes open MachineDefValue type p_thread_id = MachineDefTypes.thread_id type p_value = MachineDefValue.value type fence = | Lwsync | Hwsync | Ctrlisync (* Nop gives fences something to stick to. * An RMW represents a load-reserve and it's partnered succeeding * store-conditional. * A block represents an infinite sequence of failing store-conditionals *) type action = | Read of action_id * p_thread_id * address * p_value | Write of action_id * p_thread_id * address * p_value | RMW of action_id * p_thread_id * address * p_value * p_value | Nop of action_id * p_thread_id | Block of action_id * p_thread_id * address val is_read : action -> bool let is_read a = match a with | Read _ _ _ _ -> true | RMW _ _ _ _ _ -> true | _ -> false end val is_write : action -> bool let is_write a = match a with | Write _ _ _ _ -> true | RMW _ _ _ _ _ -> true | _ -> false end val get_thread : action -> p_thread_id let get_thread a = match a with | Read _ tid _ _ -> tid | Write _ tid _ _ -> tid | RMW _ tid _ _ _ -> tid | Nop _ tid -> tid | Block _ tid _ -> tid end val get_address : action -> address option let get_address a = match a with | Read _ _ a _ -> Some a | Write _ _ a _ -> Some a | RMW _ _ a _ _ -> Some a | Nop _ _ -> None | Block _ _ a -> Some a end (* val get_value : action -> p_value let get_value a = match a with | Read _ _ _ v -> v | Write _ _ _ v -> v end *)