[gen] Limit value checks to communication-adjacent events by ShaleXIONG · Pull Request #1845 · herd/herdtools7

ShaleXIONG · 2026-05-29T15:20:16Z

This change narrows generated final-condition value checks so they focus on events that are adjacent to communication edges. A node is considered adjacent if (1) its incoming edge (node.prev.edge) or (2) outgoing edge (node.edge) is communication edge, or (3) both the read or write side of an RMW is adjacent to a communication edge.

For reads, check_value when building the cycle in cycle.ml is now only enabled when the read is adjacent to a communication edge and the location already requires value checking. This avoids emitting final-condition checks for plain program-order reads that do not witness communication. For example: diyone7 -arch AArch64 PodWW Rfe PodRR PosRR Amo.Swp Coe, now generates:

AArch64 S+po+poR-pos-amo.swp
Generator=diyone7 (version 7.58+1)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Rf Co
Orig=PodWW Rfe PodRR PosRR Amo.Swp Coe
"PodWW Rfe PodRR PosRR Amo.Swp Coe"
{
 0:X1=x; 0:X3=y;
 1:X1=x; 1:X3=y;
}
 P0          | P1             ;
 MOV W0,#2   | LDR W0,[X3]    ;
 STR W0,[X1] | LDR W2,[X1]    ; (* <- this read from `PosRR` is no longer checked *)
 MOV W2,#1   | MOV W5,#1      ;
 STR W2,[X3] | SWP W5,W4,[X1] ;

exists ([x]=2 /\ 1:X0=1 /\ 1:X4=0) (* <- drop `1:X2=0` from previous version *)

For writes, coherence write collection in cycle.ml now trims trailing local writes until it reaches either:

a write adjacent to a communication edge
an inserted store. Note the store edge always add an extra write to the beginning of the thread hence it should be considered adjacent to communication edge.
This means the final write checks will ignore local writes inside a thread but only focus on those adjacent to communication edges. For example, diyone7 -arch AArch64 PosWW PosWW Coi -oneloc -obs oo

AArch64 CoWW+posW-pos-coi
Generator=diyone7 (version 7.58+1)
Com=Co
Orig=PosWW PosWW Coi
"PosWW PosWW Coi"
{
 0:X1=x;
}
 P0          ;
 MOV W0,#2   ;
 STR W0,[X1] ;
 MOV W2,#3   ;
 STR W2,[X1] ;
 MOV W3,#1   ;
 STR W3,[X1] ;

exists ([x]=2) (* <-- it was [x]=3 previously, while now it checks 
                                  the write associated with communication edges. *)

This technical change also leads to more tests in diy7, because diy7 by default only generates tests with up to 2 writes per locations, while now they are writes only adjacent to communication edges. All the new tests are forbidden.

Only mark read values for final-condition checking when the event is adjacent to a communication edge and the location already requires value checking.

relokin · 2026-06-05T17:42:30Z

+    let adjacent_with_communication_edge_or_store m =
+      adjacent_with_communication_edge m || E.is_insert_store m.edge.E.edge in
+    (* Remove the tail until we reach a write adjacent to a communication
+     edge or an inserted store. This `coherence` function works together with `check` in
+     `top_gen.ml` to decide coherence/write value check.
+     Especially when there are two or more writes, the last value
+     will be checked. Here we remove the tail which means a local,
+     non-communication write will be ignored. *)
+    List.fold_right ( fun (loc,n) (new_list,have_seen_communication) ->
+      match have_seen_communication,adjacent_with_communication_edge_or_store n with
+      | true,_ | _,true -> (loc,n) :: new_list,true
+      | false, false -> new_list,false
+    ) (do_rec n) ([],false)
+    |> fst


Suggested change

let adjacent_with_communication_edge_or_store m =

adjacent_with_communication_edge m || E.is_insert_store m.edge.E.edge in

(* Remove the tail until we reach a write adjacent to a communication

edge or an inserted store. This `coherence` function works together with `check` in

`top_gen.ml` to decide coherence/write value check.

Especially when there are two or more writes, the last value

will be checked. Here we remove the tail which means a local,

non-communication write will be ignored. *)

List.fold_right ( fun (loc,n) (new_list,have_seen_communication) ->

match have_seen_communication,adjacent_with_communication_edge_or_store n with

| true,_ | _,true -> (loc,n) :: new_list,true

| false, false -> new_list,false

) (do_rec n) ([],false)

|> fst

do_rec n

I have changed back here as you suggested here too.
This means to rule out a particular situation diyone7 -arch AArch64 PosWW PosWW Coi -oneloc -obs oo, which previously generates a test as below:

AArch64 a Generator=diyone7 (version 7.58+1) Com=Co Orig=PosWW PosWW Coi "PosWW PosWW Coi" { 0:X1=x; } P0 ; MOV W0,#2 ; STR W0,[X1] ; MOV W2,#3 ; STR W2,[X1] ; MOV W3,#1 ; STR W3,[X1] ; exists ([x]=3) (* <- this should be [x]=2 *)

Yet this is a very uncommon or event uninteresting litmus tests. So maybe we should just leave it for the current check [x]=3. I will need to investigate if there are better way to fix this problem possible another PR?

relokin

I think the case of writes needs more work.

Prior to this PR, I get:

$> diyone7 -metadata false -arch AArch64  PosWW PodWW Rfe PodRR Fre
AArch64 MP+posW-po+po
{
 0:X1=x; 0:X4=y;
 1:X1=x; 1:X4=y;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W0,[X4] ;
 STR W0,[X1] | LDR W2,[X1] ;
 MOV W2,#2   |             ;
 STR W2,[X1] |             ;
 MOV W3,#1   |             ;
 STR W3,[X4] |             ;

exists ([x]=2 /\ 1:X0=1 /\ 1:X2=0)

This post-condition is not ideal and I don't think it should check the value of [x], but it is acceptable.

After this PR:

$> diyone7 -metadata false -arch AArch64  PosWW PodWW Rfe PodRR Fre
AArch64 MP+posW-po+po
{
 0:X1=x; 0:X4=y;
 1:X1=x; 1:X4=y;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W0,[X4] ;
 STR W0,[X1] | LDR W2,[X1] ;
 MOV W2,#2   |             ;
 STR W2,[X1] |             ;
 MOV W3,#1   |             ;
 STR W3,[X4] |             ;

exists ([x]=1 /\ 1:X0=1 /\ 1:X2=0)

We haven't removed the check on [x]. What is worse is that the new check means the post-condition is focusing of the write after write ordering rather than the whole cycle.

relokin · 2026-07-03T15:49:52Z

+      | _ ->
+          C.E.is_com n.C.C.prev.C.C.edge
+          || C.E.is_com n.C.C.edge
+          || n.C.C.evt.C.C.rmw


Why are we adding checks for writes generated by atomics?

In short, the best fix here is to remove both (1) the write check if it is followed by Rfe event and (2) remove the universal write check in rmw (which is your question here).

let consider diyone7 -arch AArch64 DpAddrdW Rfe Amo.Cas PodWW Rfe

AArch64 LB+addr+amo.cas-po Generator=diyone7 (version 7.58+1) Prefetch=0:x=F,0:y=W,1:y=F,1:x=W Com=Rf Rf Orig=DpAddrdW Rfe Amo.Cas PodWW Rfe "DpAddrdW Rfe Amo.Cas PodWW Rfe" { 0:X0=x; 0:X4=y; 1:X0=x; 1:X4=y; } P0 | P1 ; LDR W1,[X0] | MOV W1,#1 ; EOR W2,W1,W1 | MOV W2,#2 ; MOV W3,#1 | CAS W1,W2,[X4] ; STR W3,[X4,W2,SXTW] | MOV W3,#1 ; | STR W3,[X0] ; exists ([y]=2 /\ 0:X1=1 /\ 1:X1=1) (* The current `master`, OR if we keep the universal write check on rmw here *) exists ([y]=1 /\ 0:X1=1 /\ 1:X1=1) (* If we only remove the universal write check on rmw, which I think is incorrect *) exists (0:X1=1 /\ 1:X1=1) (* remove write check if it is followed by `Rfe` and remove universal write check in `rmw` *)

ShaleXIONG · 2026-07-06T13:04:46Z

I think the case of writes needs more work.

Prior to this PR, I get:
$> diyone7 -metadata false -arch AArch64  PosWW PodWW Rfe PodRR Fre
AArch64 MP+posW-po+po
{
 0:X1=x; 0:X4=y;
 1:X1=x; 1:X4=y;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W0,[X4] ;
 STR W0,[X1] | LDR W2,[X1] ;
 MOV W2,#2   |             ;
 STR W2,[X1] |             ;
 MOV W3,#1   |             ;
 STR W3,[X4] |             ;

exists ([x]=2 /\ 1:X0=1 /\ 1:X2=0)
This post-condition is not ideal and I don't think it should check the value of [x], but it is acceptable.

After this PR:
$> diyone7 -metadata false -arch AArch64  PosWW PodWW Rfe PodRR Fre
AArch64 MP+posW-po+po
{
 0:X1=x; 0:X4=y;
 1:X1=x; 1:X4=y;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W0,[X4] ;
 STR W0,[X1] | LDR W2,[X1] ;
 MOV W2,#2   |             ;
 STR W2,[X1] |             ;
 MOV W3,#1   |             ;
 STR W3,[X4] |             ;

exists ([x]=1 /\ 1:X0=1 /\ 1:X2=0)
We haven't removed the check on [x]. What is worse is that the new check means the post-condition is focusing of the write after write ordering rather than the whole cycle.

I think the best fix here is ignore the write event in Rfe and Fre edge since the read event already check the value. Let me explore the current forbidden.conf whether this change will introduce unexpected allowed tests.

… rfe.

TiberiuBucur · 2026-07-06T15:52:39Z

Jumping in here as I've spent some time last week familiarising myself with the patch to help with the review process.

After the current changes, the problem highlighted above still persists (at least for me, hopefully I haven't done something wrong):

> diyone7 -metadata false -arch AArch64  PosWW PodWW Rfe PodRR Fre
AArch64 MP+posW-po+po
{
 0:X1=x; 0:X4=y;
 1:X1=x; 1:X4=y;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W0,[X4] ;
 STR W0,[X1] | LDR W2,[X1] ;
 MOV W2,#2   |             ;
 STR W2,[X1] |             ;
 MOV W3,#1   |             ;
 STR W3,[X4] |             ;

exists ([x]=1 /\ 1:X0=1 /\ 1:X2=0)

To me it seems like the issue is more to do with this write that is checked being on the receiving end of that final Fre edge, but also being unobservable in the final state due to the internal visibility requirement:
irreflexive [Exp & W]; (po & same-loc); [Exp & W]; (ca & int); [Exp & W] as coWW-Exp
So that one check already invalidates the postcondition, therefore not showcasing the underlying forbidden cycle that is of interest here.

Have I missed anything @ShaleXIONG ? If not, then perhaps another check on top of what you're already doing, to verify the checked write can be last in coherence order for that location, might be enough?

I'm also wondering if it's worth distinguishing further between PosWW and Coi and only check that location in the case of Coi? For refererence, this is what using Coi currently generates:

>diyone7 -metadata false -arch AArch64  Coi PodWW Rfe PodRR Fre
AArch64 MP+coi-po+po
{
 0:X1=x; 0:X4=y;
 1:X1=x; 1:X4=y;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W0,[X4] ;
 STR W0,[X1] | LDR W2,[X1] ;
 MOV W2,#2   |             ;
 STR W2,[X1] |             ;
 MOV W3,#1   |             ;
 STR W3,[X4] |             ;

exists ([x]=2 /\ 1:X0=1 /\ 1:X2=0)

What do you think?

ShaleXIONG · 2026-07-06T16:04:54Z

Jumping in here as I've spent some time last week familiarising myself with the patch to help with the review process.

After the current changes, the problem highlighted above still persists (at least for me, hopefully I haven't done something wrong):
> diyone7 -metadata false -arch AArch64  PosWW PodWW Rfe PodRR Fre
AArch64 MP+posW-po+po
{
 0:X1=x; 0:X4=y;
 1:X1=x; 1:X4=y;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W0,[X4] ;
 STR W0,[X1] | LDR W2,[X1] ;
 MOV W2,#2   |             ;
 STR W2,[X1] |             ;
 MOV W3,#1   |             ;
 STR W3,[X4] |             ;

exists ([x]=1 /\ 1:X0=1 /\ 1:X2=0)
To me it seems like the issue is more to do with this write that is checked being on the receiving end of that final Fre edge, but also being unobservable in the final state due to the internal visibility requirement: irreflexive [Exp & W]; (po & same-loc); [Exp & W]; (ca & int); [Exp & W] as coWW-Exp So that one check already invalidates the postcondition, therefore not showcasing the underlying forbidden cycle that is of interest here.

Have I missed anything @ShaleXIONG ? If not, then perhaps another check on top of what you're already doing, to verify the checked write can be last in coherence order for that location, might be enough?

I'm also wondering if it's worth distinguishing further between PosWW and Coi and only check that location in the case of Coi? For refererence, this is what using Coi currently generates:
>diyone7 -metadata false -arch AArch64  Coi PodWW Rfe PodRR Fre
AArch64 MP+coi-po+po
{
 0:X1=x; 0:X4=y;
 1:X1=x; 1:X4=y;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W0,[X4] ;
 STR W0,[X1] | LDR W2,[X1] ;
 MOV W2,#2   |             ;
 STR W2,[X1] |             ;
 MOV W3,#1   |             ;
 STR W3,[X4] |             ;

exists ([x]=2 /\ 1:X0=1 /\ 1:X2=0)
What do you think?

Yes you are right here. I am experiencing on the check on Fre. If we remove them all together. I need to ensure all the currently forbidden tests remain forbidden. Regarding the different between PosWW and Coi. I will check after I find a solution on Fre and Rfe edges first.

TiberiuBucur · 2026-07-06T16:09:27Z

Yes you are right here. I am experiencing on the check on Fre. If we remove them all together. I need to ensure all the currently forbidden tests remain forbidden.

Ah, didn't know if the last update was targeting this or not, apologies. :)

ShaleXIONG · 2026-07-06T16:11:55Z

Yes you are right here. I am experiencing on the check on Fre. If we remove them all together. I need to ensure all the currently forbidden tests remain forbidden.

Ah, didn't know if the last update was targeting this or not, apologies. :)

Ah unfortunately no. I am still exploring what I can do. Removing the write check associated to Fre gives us some unwanted allowed tests for example:

AArch64 Armv8-ext-forbidden00011008
Generator=diy7 (version 7.58+1)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
Com=Rf Fr
Orig=DMB.STdWW Rfe DpAddrCseldW ISBsWR Fre
Cycle=Rfe DpAddrCseldW ISBsWR Fre DMB.STdWW
Relax=
Safe=Rfe Fre DMB.STdWW [DpAddrCseldW,ISBsWR]
"DMB.STdWW Rfe DpAddrCseldW ISBsWR Fre"
{
 0:X1=x; 0:X3=y;
 1:X1=x; 1:X3=y;
}
 P0          | P1                  ;
 MOV W0,#2   | LDR W0,[X3]         ;
 STR W0,[X1] | MOV W4,#1           ;
 DMB ST      | CMP W0,#0           ;
 MOV W2,#1   | CSEL W2,W4,W5,EQ    ;
 STR W2,[X3] | AND W2,W2,#2        ;
             | MOV W6,#1           ;
             | STR W6,[X1,W2,SXTW] ;
             | ISB                 ;
             | LDR W7,[X1]         ;

exists (1:X0=1 /\ 1:X7=1)

We only check the write event associated with `Fre` when there is other writes in different processes. This is done by examine the process observation set, `obs` in `compute_cos`.

ShaleXIONG requested a review from relokin May 29, 2026 15:21

ShaleXIONG marked this pull request as ready for review May 29, 2026 15:21

ShaleXIONG force-pushed the cycle-rework-rf-poswr branch from a64b4fc to e7aa846 Compare May 29, 2026 15:33

[gen] restrict read value checks to communication-adjacent events

b38c444

Only mark read values for final-condition checking when the event is adjacent to a communication edge and the location already requires value checking.

ShaleXIONG changed the title ~~[gen] only check read values near communication~~ [gen] Limit value checks to communication-adjacent events Jun 5, 2026

ShaleXIONG force-pushed the cycle-rework-rf-poswr branch from e7aa846 to b38c444 Compare June 5, 2026 08:53

relokin reviewed Jun 5, 2026

View reviewed changes

[MERGE] Address comment on simplifying the communication edge check.

30b5c92

relokin reviewed Jun 17, 2026

View reviewed changes

Comment thread gen/cycle.ml Outdated

ShaleXIONG and others added 2 commits June 17, 2026 18:31

[MERGE] check read value for rmw and revert change on written value.

9ed4518

[MERGE] another try on disitinguish PosWW and Coi.

1a83b72

relokin reviewed Jul 3, 2026

View reviewed changes

[MERGE] address minor comments.

555c570

[gen] Remove the universal write check in rmw or if it is followed by…

3c7342d

… rfe.

ShaleXIONG force-pushed the cycle-rework-rf-poswr branch from ea7126f to 3c7342d Compare July 6, 2026 14:49

[gen] Filter Fre write checks

350e730

We only check the write event associated with `Fre` when there is other writes in different processes. This is done by examine the process observation set, `obs` in `compute_cos`.

Uh oh!

Conversation

ShaleXIONG commented May 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

relokin Jun 5, 2026

Choose a reason for hiding this comment

Uh oh!

ShaleXIONG Jun 17, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

relokin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

relokin Jul 3, 2026

Choose a reason for hiding this comment

Uh oh!

ShaleXIONG Jul 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

ShaleXIONG commented Jul 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

TiberiuBucur commented Jul 6, 2026

Uh oh!

ShaleXIONG commented Jul 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

TiberiuBucur commented Jul 6, 2026

Uh oh!

ShaleXIONG commented Jul 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

ShaleXIONG commented May 29, 2026 •

edited

Loading

ShaleXIONG Jul 6, 2026 •

edited

Loading

ShaleXIONG commented Jul 6, 2026 •

edited

Loading

ShaleXIONG commented Jul 6, 2026 •

edited

Loading

ShaleXIONG commented Jul 6, 2026 •

edited

Loading