[gen] Add pair-cell offset annotation for AArch64.

Makefile

@@ -380,6 +380,48 @@ diy-test-aarch64:
 		$(REGRESSION_TEST_MODE)
 	@ echo "herd7 AArch64 diycross7 tests: OK"
 
+diy-test:: diy-test-aarch64-pair
+diy-test-aarch64-pair:
+	@ echo
+	$(HERD_DIYCROSS_REGRESSION_TEST) \
+		-herd-path $(HERD) \
+		-diycross-path $(DIYCROSS) \
+		-libdir-path ./herd/libdir \
+		-expected-dir ./gen/tests/AArch64.pair \
+		-diycross-arg -arch \
+		-diycross-arg AArch64 \
+		-diycross-arg PodWW \
+		-diycross-arg P,Pa,w4 \
+		-diycross-arg Coe \
+		-diycross-arg P,Pa,w4 \
+		-diycross-arg PodWR \
+		-diycross-arg P,Pa,w4 \
+		-diycross-arg Fre \
+		$(REGRESSION_TEST_MODE)
+	@ echo "herd7 AArch64 pair diycross7 tests: OK"
+
+diy-test:: diy-test-aarch64-pair-local
+diy-test-aarch64-pair-local:
+	@ echo
+	$(HERD_DIYCROSS_REGRESSION_TEST) \
+		-herd-path $(HERD) \
+		-diycross-path $(DIYCROSS) \
+		-libdir-path ./herd/libdir \
+		-expected-dir ./gen/tests/AArch64.pair.local \
+		-diycross-arg -obs \
+		-diycross-arg local \
+		-diycross-arg -arch \
+		-diycross-arg AArch64 \
+		-diycross-arg PodWW \
+		-diycross-arg P,Pa,w4 \
+		-diycross-arg Coe \
+		-diycross-arg P,Pa,w4 \
+		-diycross-arg PodWR \
+		-diycross-arg P,Pa,w4 \
+		-diycross-arg Fre \
+		$(REGRESSION_TEST_MODE)
+	@ echo "herd7 AArch64 pair local-observer diycross7 tests: OK"
+
 diy-test:: diy-test-mixed
 diy-test-mixed::
 	@ echo

gen/AArch64Compile_gen.ml

@@ -1619,7 +1619,8 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
 
     let emit_ldp_reg opt st init rA =
       let r1,r2,st = next_reg2 st in
-      r1,init,pseudo [do_ldp opt r1 r2 rA;add vloc r1 r1 r2;],st
+      let st = A.set_friends r1 [r2] st in
+      r1,init,pseudo [do_ldp opt r1 r2 rA;],st
 
     let emit_ldp_reg opt idx st _p init rA =
       match opt,idx with
@@ -1672,7 +1673,11 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
 
 
     let emit_obs t = match t with
-    | Code.Ord | Code.Instr-> emit_load_mixed naturalsize 0
+    | Code.Ord | Code.Instr->
+        fun st p init loc ->
+        let r,init,cs,st = emit_load_mixed naturalsize 0 st p init loc in
+        let st = A.add_type (A.of_reg p r) Cfg.typ st in
+        r,init,cs,st
     | Code.Pte->
         fun st p init loc ->
         let r,init,cs,st = LDR.emit_load_var A64.V64 st p init (Misc.add_pte loc) in

gen/common/AArch64Arch_gen.ml

@@ -629,7 +629,11 @@ let is_tthm fields =
      let r = fold_atom_rw (fun rw -> f (Atomic rw)) r in
      r
 
-   let fold_non_mixed f r = fold_acc false (fun acc r -> f (acc,None) r) r
+   let fold_non_mixed f r =
+     let r = fold_acc false (fun acc r -> f (acc,None) r) r in
+     if do_mixed then r
+     (* Add an annotation to access the second cell of a pair. *)
+     else f (Plain None,Some (C.naturalsize,MachSize.nbytes C.naturalsize)) r
 
    let fold_atom f r =
      let r = fold_non_mixed f r in
@@ -805,13 +809,17 @@ let overwrite_value v ao w = match ao with
 
 (* Wide accesses *)
 
+   (* Return the number of cells required by size-access `atom`. *)
    let as_integers a =
      Misc.seq_opt
        (function
         | Neon n,_ -> (match neon_as_integers n with
                        | 1 -> None
                        | n -> Some n)
         | Pair _,_ -> Some 2
+        | (Plain _|Acq _|AcqPc _|Rel _|Atomic _),Some (_,o) ->
+            let n = o / MachSize.nbytes C.naturalsize + 1 in
+            if n > 1 then Some n else None
         | _ -> None)
        a
 

gen/cycle.ml

@@ -443,9 +443,26 @@ let find_non_pseudo_prev m = find_edge_prev non_pseudo m
         | None-> k)
     m StringMap.empty
 
+  (* Map a size annotation to the cell index.
+     Return the residual annotation after selecting the cell,
+     - `w4` over `int32_t` selects cell 1, (1, None)
+     - `w4` over `int64_t` and `fullmixed` selects cell 0, but keep the atom
+        for the mixed access (0, Some `w4`) *)
+  let split_access_atom atom =
+    match E.get_access_atom atom with
+    | Some (_,o) ->
+        let cell_idx = o / MachSize.nbytes O.naturalsize in
+        let atom = if cell_idx = 0 then atom else None in
+        cell_idx,atom
+    | None -> 0,atom
+
   let is_pair n = match n.evt.loc with
       | Data loc ->
-         if E.is_pair n.edge then Some loc
+         if E.is_pair n.edge ||
+            match E.get_access_atom n.evt.atom with
+            | Some (sz,_) -> sz = O.naturalsize
+            | None -> false
+         then Some loc
          else None
       | Code _ -> None
 
@@ -535,7 +552,8 @@ module CoSt = struct
   let update_cell_on_write st n =
     let e = n.evt in match e.bank with
     | Ord|Pair -> begin
-       let old = st.co_cell.(0) in
+       let idx,atom = split_access_atom e.atom in
+       let old = st.co_cell.(idx) in
        let co_cell = Array.copy st.co_cell in
        let cell2 =
          match n.prev.edge.E.edge with
@@ -546,7 +564,7 @@ module CoSt = struct
        begin
          match e.bank with
          | Ord ->
-            co_cell.(0) <- E.overwrite_value old e.atom cell2
+            co_cell.(idx) <- E.overwrite_value old atom cell2
          | Pair -> (* No Rmw for pairs *)
             let width = Value.from_int ((Value.to_int e.v) - 1) in
             co_cell.(0) <- E.overwrite_value old e.atom width;
@@ -913,7 +931,9 @@ let check_cycle c =
     if v = n.evt.v then
       Warn.fatal "Updated value remains the same. An issue should be reported.";
     let st = CoSt.implicit_pte_update st W in
-    n.evt <- { n.evt with v = tr_value n.evt v; } ;
+    let idx,_ = split_access_atom n.evt.atom in
+    let v = if idx = 0 then tr_value n.evt v else v in
+    n.evt <- { n.evt with v; } ;
     (* Writing Ord resets morello tag *)
     let st = CoSt.set_co st CapaTag evt_null.ctag in
     let e,st = CoSt.update_cell_on_write st n in
@@ -1149,18 +1169,18 @@ let set_dep_v nss =
 (* TODO: this is wrong for Store CR's: consider Rfi Store PosRR *)
 let set_read_individual_v n cell check_value =
   let e = n.evt in
-  let v = E.extract_value cell.(0) e.atom in
+  let idx,atom = split_access_atom e.atom in
+  let v = E.extract_value cell.(idx) atom in
 (* eprintf "SET READ: cell=0x%x, v=0x%x\n" cell v ; *)
-  let e = { e with v=v; check_value } in
+  let e = { e with v=v; cell=[|v|]; check_value } in
   n.evt <- e
 (* eprintf "AFTER %a\n" debug_node n *)
 
 let set_read_pair_v n cell check_value =
   let e = n.evt in
-  let v0 = E.extract_value cell.(0) e.atom |> Value.to_int
-  and v1 =  E.extract_value cell.(1) e.atom |> Value.to_int in
-  let v = v0 + v1 |> Value.from_int in
-  let e = { e with v=v; check_value } in
+  let v0 = E.extract_value cell.(0) e.atom
+  and v1 = E.extract_value cell.(1) e.atom in
+  let e = { e with v=v0; cell=[|v0;v1|]; check_value } in
   n.evt <- e
 
 (* Assume all the events are for the same location,

gen/final.ml

@@ -178,11 +178,12 @@ module Make : functor (O:Config) -> functor (C:ArchRun.S) ->
             | Code.CapaTag
             | Code.CapaSeal
             | Code.Ord
-            | Code.Pair
             | Code.Instr
             | Code.Pte
               ->
                 Some (I evt.C.C.v)
+            | Code.Pair ->
+                Some (I evt.C.C.cell.(0))
             | Code.VecReg _->
                let v0 =
                  match evt.C.C.vecreg with
@@ -216,6 +217,10 @@ module Make : functor (O:Config) -> functor (C:ArchRun.S) ->
                      |> Code.add_vector O.hexa ) ) vs
                 | _ -> assert false
                 end
+             | Code.Pair ->
+                Array.to_list evt.C.C.cell
+                |> List.tl
+                |> List.map (fun v -> I v)
              | _ -> [] in
            let m = C.C.EventMap.add n.C.C.evt (C.A.of_reg p r) m in
            let fs =

gen/tests/AArch64.pair.local/R+po+popap.litmus.expected

@@ -0,0 +1,17 @@
+Test R+po+popap Allowed
+States 8
+0:X4=1; 0:X5=0; 1:X4=0;
+0:X4=1; 0:X5=0; 1:X4=1;
+0:X4=1; 0:X5=3; 1:X4=0;
+0:X4=1; 0:X5=3; 1:X4=1;
+0:X4=2; 0:X5=0; 1:X4=0;
+0:X4=2; 0:X5=0; 1:X4=1;
+0:X4=2; 0:X5=3; 1:X4=0;
+0:X4=2; 0:X5=3; 1:X4=1;
+Ok
+Witnesses
+Positive: 1 Negative: 11
+Condition exists (0:X5=3 /\ 0:X4=2 /\ 1:X4=0)
+Observation R+po+popap Sometimes 1 11
+Hash=11e571cb664b322deb7e3eb9b56f5a8f
+

gen/tests/AArch64.pair.local/R+po+popapa.litmus.expected

@@ -0,0 +1,17 @@
+Test R+po+popapa Allowed
+States 8
+0:X4=1; 0:X5=0; 1:X4=0; 1:X5=0;
+0:X4=1; 0:X5=0; 1:X4=1; 1:X5=0;
+0:X4=1; 0:X5=3; 1:X4=0; 1:X5=0;
+0:X4=1; 0:X5=3; 1:X4=1; 1:X5=0;
+0:X4=2; 0:X5=0; 1:X4=0; 1:X5=0;
+0:X4=2; 0:X5=0; 1:X4=1; 1:X5=0;
+0:X4=2; 0:X5=3; 1:X4=0; 1:X5=0;
+0:X4=2; 0:X5=3; 1:X4=1; 1:X5=0;
+Ok
+Witnesses
+Positive: 1 Negative: 11
+Condition exists (0:X5=3 /\ 0:X4=2 /\ 1:X4=0 /\ 1:X5=0)
+Observation R+po+popapa Sometimes 1 11
+Hash=fe980f021bedb9de424141da78187622
+

gen/tests/AArch64.pair.local/R+po+popaw4.litmus.expected

@@ -0,0 +1,13 @@
+Test R+po+popaw4 Allowed
+States 4
+0:X4=1; 0:X5=0; 1:X4=0;
+0:X4=1; 0:X5=3; 1:X4=0;
+0:X4=2; 0:X5=0; 1:X4=0;
+0:X4=2; 0:X5=3; 1:X4=0;
+Ok
+Witnesses
+Positive: 1 Negative: 5
+Condition exists (0:X5=3 /\ 0:X4=2 /\ 1:X4=0)
+Observation R+po+popaw4 Sometimes 1 5
+Hash=ef7fb7943f3d880f57b1a6447cf489fd
+

gen/tests/AArch64.pair.local/R+po+poppa.litmus.expected

@@ -0,0 +1,13 @@
+Test R+po+poppa Allowed
+States 4
+0:X4=1; 1:X2=0; 1:X4=0;
+0:X4=1; 1:X2=1; 1:X4=0;
+0:X4=2; 1:X2=0; 1:X4=0;
+0:X4=2; 1:X2=1; 1:X4=0;
+Ok
+Witnesses
+Positive: 1 Negative: 5
+Condition exists (0:X4=2 /\ 1:X2=0 /\ 1:X4=0)
+Observation R+po+poppa Sometimes 1 5
+Hash=6ffd88bb3f103678180dfe79dabe3342
+

gen/tests/AArch64.pair.local/R+po+popw4.litmus.expected

@@ -0,0 +1,11 @@
+Test R+po+popw4 Allowed
+States 2
+0:X4=1; 1:X2=0;
+0:X4=2; 1:X2=0;
+Ok
+Witnesses
+Positive: 1 Negative: 2
+Condition exists (0:X4=2 /\ 1:X2=0)
+Observation R+po+popw4 Sometimes 1 2
+Hash=0ff1a6ae86ef333f963e1eb7f429f51a
+

gen/tests/AArch64.pair.local/R+po+pow4p.litmus.expected

@@ -0,0 +1,13 @@
+Test R+po+pow4p Allowed
+States 4
+0:X4=1; 0:X5=0; 1:X2=0;
+0:X4=1; 0:X5=0; 1:X2=1;
+0:X4=1; 0:X5=2; 1:X2=0;
+0:X4=1; 0:X5=2; 1:X2=1;
+Ok
+Witnesses
+Positive: 1 Negative: 3
+Condition exists (0:X5=2 /\ 0:X4=1 /\ 1:X2=0)
+Observation R+po+pow4p Sometimes 1 3
+Hash=39a56274fd123551bf49c94843caef13
+

gen/tests/AArch64.pair.local/R+po+pow4pa.litmus.expected

@@ -0,0 +1,13 @@
+Test R+po+pow4pa Allowed
+States 4
+0:X4=1; 0:X5=0; 1:X2=0; 1:X4=0;
+0:X4=1; 0:X5=0; 1:X2=1; 1:X4=0;
+0:X4=1; 0:X5=2; 1:X2=0; 1:X4=0;
+0:X4=1; 0:X5=2; 1:X2=1; 1:X4=0;
+Ok
+Witnesses
+Positive: 1 Negative: 3
+Condition exists (0:X5=2 /\ 0:X4=1 /\ 1:X2=0 /\ 1:X4=0)
+Observation R+po+pow4pa Sometimes 1 3
+Hash=f7894f41b2b3b7e394f7d3df4fb18275
+

gen/tests/AArch64.pair.local/R+po+pow4w4.litmus.expected

@@ -0,0 +1,11 @@
+Test R+po+pow4w4 Allowed
+States 2
+0:X4=1; 0:X5=0; 1:X2=0;
+0:X4=1; 0:X5=2; 1:X2=0;
+Ok
+Witnesses
+Positive: 1 Negative: 1
+Condition exists (0:X5=2 /\ 0:X4=1 /\ 1:X2=0)
+Observation R+po+pow4w4 Sometimes 1 1
+Hash=38d04d3121cea5b827af1683952132e9
+

gen/tests/AArch64.pair.local/R+poppa+po.litmus.expected

@@ -0,0 +1,13 @@
+Test R+poppa+po Allowed
+States 4
+0:X5=1; 0:X6=2; 1:X3=0;
+0:X5=1; 0:X6=2; 1:X3=1;
+0:X5=3; 0:X6=2; 1:X3=0;
+0:X5=3; 0:X6=2; 1:X3=1;
+Ok
+Witnesses
+Positive: 1 Negative: 5
+Condition exists (0:X6=2 /\ 0:X5=3 /\ 1:X3=0)
+Observation R+poppa+po Sometimes 1 5
+Hash=e518888cd5927840471e299b1f09072a
+

gen/tests/AArch64.pair.local/R+poppa+popap.litmus.expected

@@ -0,0 +1,17 @@
+Test R+poppa+popap Allowed
+States 8
+0:X5=1; 0:X6=2; 1:X4=0;
+0:X5=1; 0:X6=2; 1:X4=1;
+0:X5=1; 0:X6=4; 1:X4=0;
+0:X5=1; 0:X6=4; 1:X4=1;
+0:X5=3; 0:X6=2; 1:X4=0;
+0:X5=3; 0:X6=2; 1:X4=1;
+0:X5=3; 0:X6=4; 1:X4=0;
+0:X5=3; 0:X6=4; 1:X4=1;
+Ok
+Witnesses
+Positive: 1 Negative: 17
+Condition exists (0:X6=4 /\ 0:X5=3 /\ 1:X4=0)
+Observation R+poppa+popap Sometimes 1 17
+Hash=30f71eada32fcf9679b9dafac04d649a
+

gen/tests/AArch64.pair.local/R+poppa+popapa.litmus.expected

@@ -0,0 +1,17 @@
+Test R+poppa+popapa Allowed
+States 8
+0:X5=1; 0:X6=2; 1:X4=0; 1:X5=0;
+0:X5=1; 0:X6=2; 1:X4=1; 1:X5=0;
+0:X5=1; 0:X6=4; 1:X4=0; 1:X5=0;
+0:X5=1; 0:X6=4; 1:X4=1; 1:X5=0;
+0:X5=3; 0:X6=2; 1:X4=0; 1:X5=0;
+0:X5=3; 0:X6=2; 1:X4=1; 1:X5=0;
+0:X5=3; 0:X6=4; 1:X4=0; 1:X5=0;
+0:X5=3; 0:X6=4; 1:X4=1; 1:X5=0;
+Ok
+Witnesses
+Positive: 1 Negative: 17
+Condition exists (0:X6=4 /\ 0:X5=3 /\ 1:X4=0 /\ 1:X5=0)
+Observation R+poppa+popapa Sometimes 1 17
+Hash=e0bdd6e8118be80cf63f571a94547058
+

gen/tests/AArch64.pair.local/R+poppa+popaw4.litmus.expected

@@ -0,0 +1,13 @@
+Test R+poppa+popaw4 Allowed
+States 4
+0:X5=1; 0:X6=2; 1:X4=0;
+0:X5=1; 0:X6=4; 1:X4=0;
+0:X5=3; 0:X6=2; 1:X4=0;
+0:X5=3; 0:X6=4; 1:X4=0;
+Ok
+Witnesses
+Positive: 1 Negative: 8
+Condition exists (0:X6=4 /\ 0:X5=3 /\ 1:X4=0)
+Observation R+poppa+popaw4 Sometimes 1 8
+Hash=c13a404c5c5388b94d69c107d43dfba2
+