[herd] Add the same-low-order-bits cat pre-defined relation.

The effective addresses of herd are pairs  symbols X offset.
Conventionally all memory locations reside at page start
and different locations reside in different pages --- litmus in
kvm mode follows that convention.

As a consequence, the ``low order bytes'' (_i.e_ the offset
from page start) are represented by the offset component of
effective addresses.

herd/AArch64Sem.ml

@@ -846,7 +846,7 @@ module Make
             let mm = mop Access.VIR (ma >>= fun a -> loc_extract a) in
             delayed_check_tags a_virt ma ii
               (mm  >>= M.ignore >>= B.next1T)
-              (lift_fault (ma >>= fun a -> mk_fault a dir an ii None) mm dir))
+              (lift_fault (mk_fault a_virt dir an ii None) mm dir))
 
       let some_ha = dirty.DirtyBit.some_ha || dirty.DirtyBit.some_hd
 

herd/event.ml

@@ -278,7 +278,8 @@ val same_instance : event -> event -> bool
   val same_location : event -> event -> bool
   val same_location_with_faults : event -> event -> bool
   val same_value : event -> event -> bool
-(*  val is_visible_location : A.location -> bool *)
+  val same_low_order_bits : event -> event -> bool
+  (*  val is_visible_location : A.location -> bool *)
 
 (********************************)
 (* Event structure output ports *)
@@ -531,6 +532,11 @@ module Make  (C:Config) (AI:Arch_herd.S) (Act:Action.S with module A = AI) :
     | Some (A.Location_global a) -> Some a
     | _ -> None
 
+    let global_index_of e =  match global_loc_of e with
+      | Some (V.Val (Constant.Symbolic sym)) ->
+         Constant.get_index sym
+      | _-> None
+
     let virtual_loc_of e = match global_loc_of e with
     | Some (A.V.Val c) -> Constant.as_virtual c
     | None|Some (A.V.Var _) -> None
@@ -556,6 +562,11 @@ module Make  (C:Config) (AI:Arch_herd.S) (Act:Action.S with module A = AI) :
     | Some v1,Some v2 -> V.compare v1 v2 = 0
     | _,_ -> false
 
+    let same_low_order_bits e1 e2 =
+      match global_index_of e1,global_index_of e2 with
+      | (None,_)|(_,None) -> false
+      | Some i1,Some i2 -> Misc.int_eq i1 i2
+
     let proc_of e = match e.iiid with
     | IdSome {A.proc=p;_} -> Some p
     | IdSpurious|IdInit -> None

herd/machModelChecker.ml

@@ -282,6 +282,11 @@ module Make
                   E.same_location_with_faults
                   (Lazy.force unv)
               end;
+              "same-low-order-bits", lazy begin
+                E.EventRel.restrict_rel
+                  E.same_low_order_bits
+                  (Lazy.force unv)
+              end;
               "int",lazy begin
                 E.EventRel.restrict_rel E.same_proc_not_init (Lazy.force unv)
               end ;

lib/constant.ml

@@ -85,6 +85,11 @@ type symbol =
   | Physical of string * int                  (* symbol, index *)
   | System of (syskind * string)              (* System memory *)
 
+let get_index = function
+  | Virtual s -> Some s.offset
+  | Physical (_,o) -> Some o
+  | System _ -> None
+
 let pp_index base o = match o with
 | 0 -> base
 | i -> sprintf "%s+%i" base i

lib/constant.mli

@@ -49,6 +49,7 @@ type symbol =
   | Physical of string * int       (* symbol, index *)
   | System of (syskind * string)   (* System memory *)
 
+val get_index : symbol -> int option
 val pp_symbol_old : symbol -> string
 val pp_symbol : symbol -> string
 val compare_symbol : symbol -> symbol -> int