Skip to content

Commit 00f3aa6

Browse files
committed
[cat] Revamp the definition of dependencies
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
1 parent 37fa8ad commit 00f3aa6

File tree

3 files changed

+12
-10
lines changed

3 files changed

+12
-10
lines changed

herd/libdir/aarch64deps.cat

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -66,11 +66,9 @@ let rec dtrm =
6666

6767
(** Data, Address and Control dependencies *)
6868

69-
let basic-dep =
70-
[Exp & R | Rreg]; dtrm?
71-
let data = [Exp & R]; (basic-dep; [DATA]; iico_data+; [Exp & W]) & ~same-instance
72-
let addr = [Exp & R]; (basic-dep; [ADDR]; iico_data+; [Exp & M | Imp & Tag & R | Imp & TTD & R | HU | TLBI | DC.CVAU | IC.IVAU]) & ~same-instance
73-
let ctrl = [Exp & R]; basic-dep; [BCC]; po
69+
let data = [Exp & R]; dtrm & po; [Rreg]; iico_data & DATA; [Exp & W]
70+
let addr = [Exp & R]; dtrm & po; [Rreg]; iico_data & ADDR; [Exp & M | Imp & Tag & R | Imp & TTD & R | HU | TLBI | DC.CVAU | IC.IVAU]
71+
let ctrl = [Exp & R]; dtrm & po; [Rreg]; iico_data; [BCC]; po
7472

7573
(** Pick dependencies *)
7674
let rec pick-dtrm =
@@ -82,11 +80,11 @@ let pick-basic-dep =
8280
[Exp & R | Rreg]; pick-dtrm?
8381

8482
let pick-addr-dep =
85-
[Exp & R]; (pick-basic-dep; [ADDR]; iico_data+; [Exp & M | Imp & Tag & R | Imp & TTD & R | HU | TLBI | DC.CVAU | IC.IVAU]) & ~same-instance
83+
[Exp & R]; pick-dtrm & po; [Rreg]; iico_data & ADDR; [Exp & M | Imp & Tag & R | Imp & TTD & R | HU | TLBI | DC.CVAU | IC.IVAU]
8684
let pick-data-dep =
87-
[Exp & R]; (pick-basic-dep; [DATA]; (iico_data|iico_ctrl)+; [Exp & W]) & ~same-instance
85+
[Exp & R]; pick-dtrm & po; [Rreg]; (iico_data; iico_ctrl?) & DATA; [Exp & W]
8886
let pick-ctrl-dep =
89-
[Exp & R]; pick-basic-dep; [BCC]; po
87+
[Exp & R]; pick-dtrm & po; [Rreg]; iico_data; [BCC]; po
9088

9189
let pick-dep =
9290
( pick-basic-dep

herd/libdir/aarch64util.cat

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,10 @@
4444
* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
4545
*)
4646

47+
let iico_data = iico_data+
48+
let ADDR = [ADDR]; iico_data
49+
let DATA = [DATA]; (iico_data|iico_ctrl)+
50+
4751
(*
4852
* Include default definitions for sets that are undefined without
4953
* -variant vmsa

herd/libdir/catdefinitions.tex

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,8 +26,8 @@
2626
\newcommand{\rfi}[2]{#2 Reads-from-internal #1}
2727
\newcommand{\rfreg}[2]{#2 Reads-from-register #1}
2828
\newcommand{\rmw}[2]{#1 and #2 form a successful Read-Modify-Write pair}
29-
\newcommand{\DATA}[2]{#1 affects the data value written by #2}
30-
\newcommand{\ADDR}[2]{#1 affects the address of the Location accessed by #2}
29+
\newcommand{\DATA}[2]{the semantics of the instruction that generates #1 and #2 indicate that the value produced by #1 is consumed in the calculation of the data value written by #2}
30+
\newcommand{\ADDR}[2]{the semantics of the instruction that generates #1 and #2 indicate that the value produced by #1 is consumed in the calculation of the address of the Location of #2}
3131
\newcommand{\sameinstance}[2]{#1 and #2 are generated by the same instruction}
3232
\newcommand{\sm}[2]{\sameinstance{#1}{#2}}
3333
\newcommand{\si}[2]{\sameinstance{#1}{#2}}

0 commit comments

Comments
 (0)