|
| 1 | +A online tutorial can be found in this [link](https://diy.inria.fr) that covers `diy7`, `diycross7` and `diyone7`. |
| 2 | +We document some extra information here. |
| 3 | + |
| 4 | +# Tool `diy7` internal filter |
| 5 | +Tool `diy7` enforce some filter by default, that is, function `choice_default` in source code file [gen/alt.ml](alt.ml). |
| 6 | +Given an unfinished cycle $[r_1, r_2, r_3, ..., r_n]$, the function defines next allowed primitive relaxation $r_{n+1}$. |
| 7 | +In the case of compound relaxation, it checks against the first primitive relaxation, e.g. $[r_{n+1}, r_{n+2}, ..., r_k]$. |
| 8 | +If the filter `choice_default` passes, returning `true`, the new unfinished/finished cycle will be, $[r_1, r_2, r_3, ..., r_n, r_{n+1}]$ or $[r_1, r_2, r_3, ..., r_n, r_{n+1}, r_{n+2}, ..., r_k]$. |
| 9 | +Before expaining the filter, let introduce some terminology on relaxations, or specifically, edges, where concrete examples are from `-arch AArch64`: |
| 10 | + |
| 11 | +- internal communication edge, namely `Coi`, `Fri` and `Rfi` |
| 12 | +- external (communication) edge, namely `Coe`, `Fre`, `Rfe` and `Hat` |
| 13 | +- insert edge, that is, fence without memory events, e.g., `DMB.SY` and `DMB.LD` |
| 14 | +- dependency edge, e.g. `DpAddrdW` and `DpCtrlsR` |
| 15 | +- program order edge that connects two memory events without any extra restrict, e.g. `PosRW` and `PodWR` |
| 16 | +- read-modify-write (RMW) edge, e.g. `LxSx` and `Amo.Cas`. |
| 17 | + |
| 18 | +Given two primitive relaxations, `lhs` and `rhs`, the following cases pass the filter `choice_default lhs rhs`: |
| 19 | + |
| 20 | +| `lhs` | `rhs` | |
| 21 | +|-------|-------| |
| 22 | +| internal communication edge or insert edge | dependency edge or program order edge between different loations such as `PodWR` | |
| 23 | +| dependency edge or program order edge between different loations such as `PodWR` | internal communication edge or insert edge | |
| 24 | +| dependency edge between different locations such as `DpAddrdW` | program order edge between different loations such as `PodWR` | |
| 25 | +| program order edge between different loations such as `PodWR` | dependency edge between different locations such as `DpAddrdW` | |
| 26 | +| internal read-from edge `Rfi` | program order edge between the same location such as `PosWR` | |
| 27 | +| program order edge between the same location such as `PosWR` | internal read-from edge `Rfi` | |
| 28 | +| RMW edge | any edge | |
| 29 | +| any edge | RMW edge | |
| 30 | +| external edge | any edge | |
| 31 | +| any edge | external edge | |
0 commit comments