herd · ShaleXIONG · Mar 3, 2026 · Mar 4, 2026 · Mar 11, 2026
diff --git a/gen/alt.ml b/gen/alt.ml
@@ -223,7 +223,18 @@ struct
     | (None,_)|(_,(Irr|NoDir)) -> true
     | Some a,(Dir d) -> C.A.applies_atom a d
 
-    let pair_ok safes po_safe xs ys e1 e2 = match e1.edge,e2.edge with
+    let rec hd_non_insert = function
+      | [] -> assert false
+      | [x] -> x
+      | x::xs ->
+          if C.E.is_insert_store x.C.E.edge then hd_non_insert xs
+          else x
+    let last_non_insert xs = hd_non_insert (List.rev xs)
+
+    let pair_ok safes po_safe xs ys =
+      let e1 = last_non_insert xs in
+      let e2 = hd_non_insert ys in
+      match e1.edge,e2.edge with
 (*
   First reject some of hb' ; hb'
  *)
@@ -278,24 +289,16 @@ module Make(C:Builder.S)
         | _,_ -> false
       else fun _ _ -> true
 
-    let rec hd_non_insert = function
-      | [] -> assert false
-      | [x] -> x
-      | x::xs ->
-          if C.E.is_insert_store x.C.E.edge then hd_non_insert xs
-          else x
-    let last_non_insert xs = hd_non_insert (List.rev xs)
-
     let do_compat safes po_safe xs ys =
       let x = Misc.last xs and y = List.hd ys in
       let r =
         C.E.can_precede x y
         && check_mixed x y
-        && FilterImpl.pair_ok safes po_safe xs ys x y
+        && FilterImpl.pair_ok safes po_safe xs ys
         &&
           begin
             if do_kvm then
-              C.E.can_precede (hd_non_insert xs) (last_non_insert ys)
+              C.E.can_precede (FilterImpl.hd_non_insert xs) (FilterImpl.last_non_insert ys)
             else true
           end in
       if O.verbose > 2 then begin
@@ -798,7 +801,5 @@ module Make(C:Builder.S)
       let safe,_,_ = parse_input ~relax ~safe ~reject:[] in
       let safe_set = C.R.Set.of_list safe in
       let po_safe = edges_ofs safe |> extract_po in
-      let last = Misc.last lhs in
-      let first = List.hd rhs in
-      FilterImpl.pair_ok safe_set po_safe lhs rhs last first
+      FilterImpl.pair_ok safe_set po_safe lhs rhs
   end
diff --git a/gen/cycle.ml b/gen/cycle.ml
@@ -761,13 +761,7 @@ let remove_store n0 =
       m.evt <- { m.evt with dir=Some d; atom=a; rmw=rmw}
     end else
     begin
-      let p = find_non_pseudo_prev m.prev
-      and n = find_non_pseudo m.next in
-(*      eprintf "[%a] in [%a]..[%a]\n" debug_node m debug_node p debug_node n ; *)
-      if not (E.is_ext p.edge || E.is_ext n.edge) then begin
-        Warn.fatal "Insert pseudo edge %s appears in-between  %s..%s (at least one neighbour must be an external edge)"
-          (E.pp_edge m.edge)  (E.pp_edge p.edge)  (E.pp_edge n.edge)
-      end;
+      let p = find_non_pseudo_prev m.prev in
       match p.edge.E.edge with
       | (E.Rf Ext | E.Fr Ext) ->
         Warn.fatal "Insert pseudo edge %s appears after external communication edge %s"

diff --git a/gen/tests/AArch64/RR+RW+ctrl-[isb]+amo.cas-po.litmus.expected b/gen/tests/AArch64/RR+RW+ctrl-[isb]+amo.cas-po.litmus.expected
@@ -0,0 +1,13 @@
+Test RR+RW+ctrl-[isb]+amo.cas-po Allowed
+States 4
+0:X1=0; 0:X3=0; 1:X1=0;
+0:X1=0; 0:X3=1; 1:X1=0;
+0:X1=1; 0:X3=0; 1:X1=0;
+0:X1=1; 0:X3=1; 1:X1=0;
+Ok
+Witnesses
+Positive: 2 Negative: 6
+Condition exists (0:X1=1 /\ 0:X3=0 /\ 1:X1=0)
+Observation RR+RW+ctrl-[isb]+amo.cas-po Sometimes 2 6
+Hash=d0d2d3f73c71578091cc7e349e382cc1
+
diff --git a/gen/tests/AArch64/RR+RW+ctrl-[isb]+amo.casap-po.litmus.expected b/gen/tests/AArch64/RR+RW+ctrl-[isb]+amo.casap-po.litmus.expected
@@ -0,0 +1,13 @@
+Test RR+RW+ctrl-[isb]+amo.casap-po Allowed
+States 4
+0:X1=0; 0:X3=0; 1:X1=0;
+0:X1=0; 0:X3=1; 1:X1=0;
+0:X1=1; 0:X3=0; 1:X1=0;
+0:X1=1; 0:X3=1; 1:X1=0;
+Ok
+Witnesses
+Positive: 2 Negative: 6
+Condition exists (0:X1=1 /\ 0:X3=0 /\ 1:X1=0)
+Observation RR+RW+ctrl-[isb]+amo.casap-po Sometimes 2 6
+Hash=4f09cd61fca7d2a114ec56ff62bd8cb4
+
diff --git a/gen/tests/AArch64/RR+RW+ctrl-[isb]+amo.stadd-po.litmus.expected b/gen/tests/AArch64/RR+RW+ctrl-[isb]+amo.stadd-po.litmus.expected
@@ -0,0 +1,13 @@
+Test RR+RW+ctrl-[isb]+amo.stadd-po Allowed
+States 4
+0:X1=0; 0:X3=0;
+0:X1=0; 0:X3=1;
+0:X1=1; 0:X3=0;
+0:X1=1; 0:X3=1;
+Ok
+Witnesses
+Positive: 1 Negative: 3
+Condition exists (0:X1=1 /\ 0:X3=0)
+Observation RR+RW+ctrl-[isb]+amo.stadd-po Sometimes 1 3
+Hash=c3d1e1e7f3c65ac36cfa23768118f582
+
diff --git a/gen/tests/AArch64/RR+RW+ctrl-[isb]+amo.swp-po.litmus.expected b/gen/tests/AArch64/RR+RW+ctrl-[isb]+amo.swp-po.litmus.expected
@@ -0,0 +1,13 @@
+Test RR+RW+ctrl-[isb]+amo.swp-po Allowed
+States 4
+0:X1=0; 0:X3=0; 1:X1=0;
+0:X1=0; 0:X3=1; 1:X1=0;
+0:X1=1; 0:X3=0; 1:X1=0;
+0:X1=1; 0:X3=1; 1:X1=0;
+Ok
+Witnesses
+Positive: 1 Negative: 3
+Condition exists (0:X1=1 /\ 0:X3=0 /\ 1:X1=0)
+Observation RR+RW+ctrl-[isb]+amo.swp-po Sometimes 1 3
+Hash=96e8c4056af6c3e374129f510dae1ee4
+
diff --git a/gen/tests/AArch64/RR+RW+ctrl-[isb]+amo.swpap-po.litmus.expected b/gen/tests/AArch64/RR+RW+ctrl-[isb]+amo.swpap-po.litmus.expected
@@ -0,0 +1,13 @@
+Test RR+RW+ctrl-[isb]+amo.swpap-po Allowed
+States 4
+0:X1=0; 0:X3=0; 1:X1=0;
+0:X1=0; 0:X3=1; 1:X1=0;
+0:X1=1; 0:X3=0; 1:X1=0;
+0:X1=1; 0:X3=1; 1:X1=0;
+Ok
+Witnesses
+Positive: 1 Negative: 3
+Condition exists (0:X1=1 /\ 0:X3=0 /\ 1:X1=0)
+Observation RR+RW+ctrl-[isb]+amo.swpap-po Sometimes 1 3
+Hash=37b4b4d028cd03e03a575d3f902723f2
+
diff --git a/gen/tests/AArch64/RR+RW+ctrl-[isb]+rmw-po.litmus.expected b/gen/tests/AArch64/RR+RW+ctrl-[isb]+rmw-po.litmus.expected
@@ -0,0 +1,13 @@
+Test RR+RW+ctrl-[isb]+rmw-po Allowed
+States 4
+0:X1=0; 0:X3=0; 1:X1=0;
+0:X1=0; 0:X3=1; 1:X1=0;
+0:X1=1; 0:X3=0; 1:X1=0;
+0:X1=1; 0:X3=1; 1:X1=0;
+Loop Ok
+Witnesses
+Positive: 3 Negative: 9
+Condition exists (0:X1=1 /\ 0:X3=0 /\ 1:X1=0)
+Observation RR+RW+ctrl-[isb]+rmw-po Sometimes 3 9
+Hash=284f54dcc5611963126ca77d79c846ad
+
diff --git a/gen/tests/AArch64/RR+RW+ctrl-[isb]+rmw-po.litmus.expected-warn b/gen/tests/AArch64/RR+RW+ctrl-[isb]+rmw-po.litmus.expected-warn
@@ -0,0 +1 @@
+Warning: File "/var/folders/ys/4k4qj5qs0ns030sn0kptsmgr0000gn/T/tmp.b1hSMIuz59/RR+RW+ctrl-[isb]+rmw-po.litmus": unrolling limit exceeded at Loop01, legal outcomes may be missing.
diff --git a/gen/tests/AArch64/RR+RW+ctrl-[isb]+rmwap-po.litmus.expected b/gen/tests/AArch64/RR+RW+ctrl-[isb]+rmwap-po.litmus.expected
@@ -0,0 +1,13 @@
+Test RR+RW+ctrl-[isb]+rmwap-po Allowed
+States 4
+0:X1=0; 0:X3=0; 1:X1=0;
+0:X1=0; 0:X3=1; 1:X1=0;
+0:X1=1; 0:X3=0; 1:X1=0;
+0:X1=1; 0:X3=1; 1:X1=0;
+Loop Ok
+Witnesses
+Positive: 3 Negative: 9
+Condition exists (0:X1=1 /\ 0:X3=0 /\ 1:X1=0)
+Observation RR+RW+ctrl-[isb]+rmwap-po Sometimes 3 9
+Hash=0b62775ee6462aa6f776b02c4e4e99cf
+
diff --git a/gen/tests/AArch64/RR+RW+ctrl-[isb]+rmwap-po.litmus.expected-warn b/gen/tests/AArch64/RR+RW+ctrl-[isb]+rmwap-po.litmus.expected-warn
@@ -0,0 +1 @@
+Warning: File "/var/folders/ys/4k4qj5qs0ns030sn0kptsmgr0000gn/T/tmp.b1hSMIuz59/RR+RW+ctrl-[isb]+rmwap-po.litmus": unrolling limit exceeded at Loop01, legal outcomes may be missing.
diff --git a/gen/tests/baseline-size-4.cycle.expected b/gen/tests/baseline-size-4.cycle.expected
@@ -7888,6 +7888,30 @@ DpAddrsW PodWWPL PosWRLA HatAP DpAddrdW Rfe
 DpAddrsW PodWWPL PosWRLA HatAP DpCtrldW Rfe
 DpAddrsW PodWWPL PosWRLA HatAP DpDatadW Rfe
 DpAddrsW PodWWPL PosWRLA HatAQ PodRWQP Rfe
+DpCtrlCseldR ISB Hat Amo.Cas DMB.STdWW Rfe
+DpCtrlCseldR ISB Hat Amo.Cas DMB.SYdWW Rfe
+DpCtrlCseldR ISB Hat Amo.Cas DSB.STdWW Rfe
+DpCtrlCseldR ISB Hat Amo.Cas DSB.SYdWW Rfe
+DpCtrlCseldR ISB Hat Amo.Cas PodWR Amo.CasPL RfeLP
+DpCtrlCseldR ISB Hat Amo.Cas PodWR Amo.SwpPL RfeLP
+DpCtrlCseldR ISB Hat Amo.Cas PodWR LxSxPL RfeLP
+DpCtrlCseldR ISB Hat Amo.Cas PodWWPL RfeLP
+DpCtrlCseldR ISB Hat Amo.Swp DMB.STdWW Rfe
+DpCtrlCseldR ISB Hat Amo.Swp DMB.SYdWW Rfe
+DpCtrlCseldR ISB Hat Amo.Swp DSB.STdWW Rfe
+DpCtrlCseldR ISB Hat Amo.Swp DSB.SYdWW Rfe
+DpCtrlCseldR ISB Hat Amo.Swp PodWR Amo.CasPL RfeLP
+DpCtrlCseldR ISB Hat Amo.Swp PodWR Amo.SwpPL RfeLP
+DpCtrlCseldR ISB Hat Amo.Swp PodWR LxSxPL RfeLP
+DpCtrlCseldR ISB Hat Amo.Swp PodWWPL RfeLP
+DpCtrlCseldR ISB Hat LxSx DMB.STdWW Rfe
+DpCtrlCseldR ISB Hat LxSx DMB.SYdWW Rfe
+DpCtrlCseldR ISB Hat LxSx DSB.STdWW Rfe
+DpCtrlCseldR ISB Hat LxSx DSB.SYdWW Rfe
+DpCtrlCseldR ISB Hat LxSx PodWR Amo.CasPL RfeLP
+DpCtrlCseldR ISB Hat LxSx PodWR Amo.SwpPL RfeLP
+DpCtrlCseldR ISB Hat LxSx PodWR LxSxPL RfeLP
+DpCtrlCseldR ISB Hat LxSx PodWWPL RfeLP
 DpCtrlCseldW ISB Rfe DpCtrlCseldW ISB Rfe
 DpCtrlCseldW ISB Rfe DpCtrldW ISB Rfe
 DpCtrlCseldW ISB Rfe PodRR Amo.CasPL RfeLP
@@ -7936,6 +7960,15 @@ DpCtrlCseldW RfePA LxSxAL PodWWLP Rfe
 DpCtrlCseldW RfePA LxSxAP PodWW Rfe
 DpCtrlCseldW RfePA PodRWAP Rfe
 DpCtrlCseldW RfePQ PodRWQP Rfe
+DpCtrlCseldWPL ISB PosWRLA HatAA PodRWAP Rfe
+DpCtrlCseldWPL ISB PosWRLA HatAP DMB.LDdRW Rfe
+DpCtrlCseldWPL ISB PosWRLA HatAP DMB.SYdRW Rfe
+DpCtrlCseldWPL ISB PosWRLA HatAP DSB.LDdRW Rfe
+DpCtrlCseldWPL ISB PosWRLA HatAP DSB.SYdRW Rfe
+DpCtrlCseldWPL ISB PosWRLA HatAP DpAddrdW Rfe
+DpCtrlCseldWPL ISB PosWRLA HatAP DpCtrldW Rfe
+DpCtrlCseldWPL ISB PosWRLA HatAP DpDatadW Rfe
+DpCtrlCseldWPL ISB PosWRLA HatAQ PodRWQP Rfe
 DpCtrlCseldWPL PosWRLA HatAA PodRWAP Rfe
 DpCtrlCseldWPL PosWRLA HatAP DMB.LDdRW Rfe
 DpCtrlCseldWPL PosWRLA HatAP DMB.SYdRW Rfe
@@ -7945,6 +7978,30 @@ DpCtrlCseldWPL PosWRLA HatAP DpAddrdW Rfe
 DpCtrlCseldWPL PosWRLA HatAP DpCtrldW Rfe
 DpCtrlCseldWPL PosWRLA HatAP DpDatadW Rfe
 DpCtrlCseldWPL PosWRLA HatAQ PodRWQP Rfe
+DpCtrldR ISB Hat Amo.Cas DMB.STdWW Rfe
+DpCtrldR ISB Hat Amo.Cas DMB.SYdWW Rfe
+DpCtrldR ISB Hat Amo.Cas DSB.STdWW Rfe
+DpCtrldR ISB Hat Amo.Cas DSB.SYdWW Rfe
+DpCtrldR ISB Hat Amo.Cas PodWR Amo.CasPL RfeLP
+DpCtrldR ISB Hat Amo.Cas PodWR Amo.SwpPL RfeLP
+DpCtrldR ISB Hat Amo.Cas PodWR LxSxPL RfeLP
+DpCtrldR ISB Hat Amo.Cas PodWWPL RfeLP
+DpCtrldR ISB Hat Amo.Swp DMB.STdWW Rfe
+DpCtrldR ISB Hat Amo.Swp DMB.SYdWW Rfe
+DpCtrldR ISB Hat Amo.Swp DSB.STdWW Rfe
+DpCtrldR ISB Hat Amo.Swp DSB.SYdWW Rfe
+DpCtrldR ISB Hat Amo.Swp PodWR Amo.CasPL RfeLP
+DpCtrldR ISB Hat Amo.Swp PodWR Amo.SwpPL RfeLP
+DpCtrldR ISB Hat Amo.Swp PodWR LxSxPL RfeLP
+DpCtrldR ISB Hat Amo.Swp PodWWPL RfeLP
+DpCtrldR ISB Hat LxSx DMB.STdWW Rfe
+DpCtrldR ISB Hat LxSx DMB.SYdWW Rfe
+DpCtrldR ISB Hat LxSx DSB.STdWW Rfe
+DpCtrldR ISB Hat LxSx DSB.SYdWW Rfe
+DpCtrldR ISB Hat LxSx PodWR Amo.CasPL RfeLP
+DpCtrldR ISB Hat LxSx PodWR Amo.SwpPL RfeLP
+DpCtrldR ISB Hat LxSx PodWR LxSxPL RfeLP
+DpCtrldR ISB Hat LxSx PodWWPL RfeLP
 DpCtrldW Coe DMB.STdWWPL PosWRLA HatAP
 DpCtrldW Coe DMB.SYdWR Amo.Cas PosWRPA HatAP
 DpCtrldW Coe DMB.SYdWR Amo.Cas PosWRPQ HatQP
@@ -8068,6 +8125,15 @@ DpCtrldW RfePA LxSxAL PodWWLP Rfe
 DpCtrldW RfePA LxSxAP PodWW Rfe
 DpCtrldW RfePA PodRWAP Rfe
 DpCtrldW RfePQ PodRWQP Rfe
+DpCtrldWPL ISB PosWRLA HatAA PodRWAP Rfe
+DpCtrldWPL ISB PosWRLA HatAP DMB.LDdRW Rfe
+DpCtrldWPL ISB PosWRLA HatAP DMB.SYdRW Rfe
+DpCtrldWPL ISB PosWRLA HatAP DSB.LDdRW Rfe
+DpCtrldWPL ISB PosWRLA HatAP DSB.SYdRW Rfe
+DpCtrldWPL ISB PosWRLA HatAP DpAddrdW Rfe
+DpCtrldWPL ISB PosWRLA HatAP DpCtrldW Rfe
+DpCtrldWPL ISB PosWRLA HatAP DpDatadW Rfe
+DpCtrldWPL ISB PosWRLA HatAQ PodRWQP Rfe
 DpCtrldWPL PodWRLA FreAP PodWRPA Amo.CasAL PosWRLP Hat
 DpCtrldWPL PodWRLA FreAP PodWRPA Amo.SwpAL PosWRLP Hat
 DpCtrldWPL PodWRLA PosRRAP Fre PodWRPA Amo.CasAL PosWRLP Hat
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		Warning: File "/var/folders/ys/4k4qj5qs0ns030sn0kptsmgr0000gn/T/tmp.b1hSMIuz59/RR+RW+ctrl-[isb]+rmw-po.litmus": unrolling limit exceeded at Loop01, legal outcomes may be missing.