Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -715,7 +715,7 @@ diy-test:: diyone-basic-test
diyone-basic-test:
@ echo
dune test gen/tests
@ echo "diyone7 basic test: OK"
@ echo "diy* basic test: OK"
diy-test:: diy-baseline-cycleonly
diy-baseline-cycleonly::
@ echo
Expand Down
8 changes: 4 additions & 4 deletions gen/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,13 +12,13 @@ To summarise, given two primitive relaxations, `lhs` and `rhs`, the following ca
|-------|-------|
| internal communication edge or insert edge | dependency edge or program order edge between different locations such as `PodWR` |
| dependency edge or program order edge between different locations such as `PodWR` | internal communication edge or insert edge |
| dependency edge between different locations such as `DpAddrdW` | program order edge between different locations such as `PodWR` |
| dependency edge between different locations such as `DpAddrdW` | program order edge between different locations such as `PodWR`, or same-location write-write edge such as `PosWW`, treated like `Coi` |
| dependency edge between different locations such as `DpAddrdR` | same-location read-write edge such as `PosRW`, treated like `Fri` |
| program order edge between different locations such as `PodWR` | dependency edge between different locations such as `DpAddrdW` |
| internal read-from edge `Rfi` | program order edge between the same location such as `PosWR` |
| program order edge between the same location such as `PosWR` | internal read-from edge `Rfi` |
| same-location write-read edge such as `PosWR`, treated like `Rfi` | dependency edge between different locations such as `DpAddrdW` |
| RMW edge | any edge |
| any edge | RMW edge |
| external edge | any edge |
| any edge | external edge |

The command `diy7 -filter <lhs> <rhs>` provides the filter result between `<lhs>` and `<rhs>`.
The command `diy7 -filter-check <lhs> <rhs>` provides the filter result between `<lhs>` and `<rhs>`.
18 changes: 12 additions & 6 deletions gen/alt.ml
Original file line number Diff line number Diff line change
Expand Up @@ -68,8 +68,9 @@ struct
Also notice that we are more tolerant for Rfi.
*)
(* Assuming Dp is safe *)
| Rf Int,Dp _ | Dp _,Rf Int -> true
| Dp (_,sd,_),Ws Int | Dp (_,sd,_),Fr Int ->
| (Rf Int|Po(Same,Dir W,Dir R)),Dp _
| Dp _,(Rf Int|Po(Same,Dir W,Dir R)) -> true
| Dp (_,sd,_),(Ws Int|Po(Same,Dir W,Dir W)|Fr Int|Po(Same,Dir R,Dir W)) ->
not (po_safe sd (dir_src e1) (dir_tgt e2))
| Po (sd1,_,_), Dp (_,sd2,_) ->
not (po_safe sd1 (dir_src e1) (dir_tgt e1)) &&
Expand Down Expand Up @@ -103,12 +104,17 @@ struct
(*
Now accept some internal with internal composition
*)
| (Ws Int|Rf Int|Fr Int|Insert _),(Dp (_,_,_)|Po (Diff,_,_))
| (Dp (_,_,_)|Po (Diff,_,_)),(Ws Int|Rf Int|Fr Int|Insert _)
| (Ws Int|Po(Same,Dir W,Dir W)
|Rf Int|Po(Same,Dir W,Dir R)
|Fr Int|Po(Same,Dir R,Dir W)|Insert _),(Dp (_,_,_)|Po (Diff,_,_))
| (Dp (_,_,_)|Po (Diff,_,_)),
(Ws Int|Po(Same,Dir W,Dir W)
|Rf Int|Po(Same,Dir W,Dir R)
|Fr Int|Po(Same,Dir R,Dir W)|Insert _)
| Dp (_,Diff,_),Po (Diff,_,_)
| Po (Diff,_,_),Dp (_,Diff,_)
| Rf Int,Po (Same,_,_)
| Po (Same,_,_),Rf Int
| (Rf Int|Po(Same,Dir W,Dir R)),Po (Same,_,_)
| Po (Same,_,_),(Rf Int|Po(Same,Dir W,Dir R))
| (Rmw _,_)|(_,Rmw _) -> true
| _,_ ->
(* Reject other internal followed by internal sequences *)
Expand Down
Loading
Loading