Arm DependenciesArm Architecture Formal Team |
There are several types of dependencies in the Arm memory model: address, data and control dependencies.
They provide order from one instruction to another, following the rules listed in the Arm Architecture Reference Manual, Section B2.3.6 (specifically the Dependency-ordered-before relation).
Here is an example of address dependency. Consider the test MP+rel+addr:
AArch64 MP+rel+addr
{
0:X1=x; 0:X3=y;
1:X0=y; 1:X4=x;
}
P0 | P1 ;
MOV W0,#1 | LDR W1,[X0] ;
STR W0,[X1] | EOR W2,W1,W1 ;
MOV W2,#1 | LDR W3,[X4,W2,SXTW] ;
STLR W2,[X3] | ;
exists (1:X1=1 /\ 1:X3=0)
This test is forbidden by the Arm memory model. This can be seen using the following command:
% herd7 MP+rel+addr.litmus
which gives the following response:
Test MP+rel+addr Allowed States 3 1:X1=0; 1:X3=0; 1:X1=0; 1:X3=1; 1:X1=1; 1:X3=1; No
The reason for this test being forbidden is two-fold:
This can be seen by asking herd7 to display the forbidden execution, as follows:
% herd7 -conf show.cfg -show prop -skipchecks external -preview MP+rel+addr.litmus
This produces the following diagram:
Here is an example of data dependency. Consider the test S+rel+data.litmus:
AArch64 S+rel+data
{
0:X1=x; 0:X3=y;
1:X0=y; 1:X3=x;
}
P0 | P1 ;
MOV W0,#2 | LDR W1,[X0] ;
STR W0,[X1] | EOR W2,W1,W1 ;
MOV W2,#1 | ADD W2,W2,#1 ;
STLR W2,[X3] | STR W2,[X3] ;
exists ([x]=2 /\ 1:X1=1)
This test is forbidden by the Arm memory model. This can be seen using the following command:
% herd7 S+rel+data.litmus
which gives the following response:
Test S+rel+data Allowed States 3 1:X1=0; [x]=1; 1:X1=0; [x]=2; 1:X1=1; [x]=1; No
The reason for this test being forbidden is two-fold:
This can be seen by asking herd7 to display the forbidden execution, as follows:
% herd7 -conf show.cfg -show prop -skipchecks external -preview S+rel+data.litmus
This produces the following diagram:
Here is an example of control dependency. Consider the test LB+rel+ctrl.litmus:
AArch64 LB+rel+ctrl
{
0:X0=x; 0:X3=y;
1:X0=y; 1:X3=x;
}
P0 | P1 ;
LDR W1,[X0] | LDR W1,[X0] ;
MOV W2,#1 | CBNZ W1,LC00 ;
STLR W2,[X3] | LC00: ;
| MOV W2,#1 ;
| STR W2,[X3] ;
exists (0:X1=1 /\ 1:X1=1)
This test is forbidden by the Arm memory model. This can be seen using the following command:
% herd7 LB+rel+data.litmus
which gives the following response:
Test LB+rel+ctrl Allowed States 3 0:X1=0; 1:X1=0; 0:X1=0; 1:X1=1; 0:X1=1; 1:X1=0; No
The reason for this test being forbidden is two-fold:
This can be seen by asking herd7 to display the forbidden execution, as follows:
% herd7 -conf show.cfg -show prop -skipchecks external -preview LB+rel+ctrl.litmus
This produces the following diagram:
At a high level, Intrinsic dependencies convey the order(s) in which a given instruction should perform its Effects.
There are several types of Intrinsic dependencies, for example an Intrinsic Data Dependency from an Effect E1 to an Effect E2 means that E1 hands over some data to E2. Those are the iico_data arrows in our diagrams.
Intrinsic dependencies contribute to building AArch64 dependencies in the memory model, such as Address dependencies. This is what we are going to look at next.
But first, let’s look into Intrinsic dependencies for an LDR (load instruction).
Consider the test LDR:
AArch64 LDR
{
0:X2=x;
0:X1=0;
int64_t x=1;
}
P0 ;
LDR X1,[X2] ;
exists(0:X1=1)
At user-level, the Effects generated by the LDR instruction are as follows:
This can be seen using the following command (Unix)
% herd7 -conf show.cfg -showevents all -show prop -gv LDR.litmus
Or (MacOS):
% herd7 -conf show.cfg -showevents all -show prop -preview LDR.litmus
By contrast, an STR instruction is not required to order its Effects linearly. To see this, consider the test STR:
AArch64 STR
{
0:X1=0;
0:X2=x;
}
P0 ;
MOV X1,#1 ;
STR X1,[X2];
exists(x=1)
At user-level, the Effects generated by the STR instruction are as follows:
This can be seen using the following command (Unix)
% herd7 -conf show.cfg -showevents all -show prop -gv STR.litmus
Or (MacOS):
% herd7 -conf show.cfg -showevents all -show prop -preview STR.litmus
The following cat file aarch64deps.cat: https://github.com/herd/herdtools7/blob/master/herd/libdir/aarch64deps.cat is where we build AArch64 dependencies from Intrinsic dependencies.
To illustrate this, let’s have a look at what is happening on P1 of MP+rel+addr from an Intrinsic dependencies point of view:
% herd7 -conf show.cfg -showevents all -show prop -skipchecks external -preview MP+rel+addr.litmus
This produces the following diagram:
As you can see, there is a path from the Memory Read Effect c: R[y]=1 generated by the first load on P1 to the Memory Read Effect d: R[x]=0 generated by the second load on P1. This path is made of iico_data (Intrinsic data) and rf-reg (Reads-from-register) arrows.
This path constitutes a “Dependency through Registers and Memory”. A dependency through registers and memory which starts with an Explicit Memory Read Effect such as the Effect c: R[y]=1 constitutes a “Basic dependency”.
Basic dependencies are a building block of AArch64 dependencies. More precisely, Address, Data and Control dependencies all start with an initial step of Basic dependencies.
To determine whether this path constitutes an Address dependency (as opposed to a Data say) we need to examine if this step lands on an Effect which affects the address calculation of the target instruction (e.g. the Register Read Effect r: R1:X2q=0 of the LDR W3,[X4,W2,SXTW] on P1 in MP+rel+addr).
Finally, we need to check if there is one or several further steps of Intrinsic Data Dependency (reaching the Memory Effects of the target instruction, e.g. d: R[x]=0 for LDR W3,[X4,W2,SXTW] on P1 in MP+rel+addr).
To illustrate this, let’s have a look at what is happening on P1 of S+rel+data from an Intrinsic dependencies point of view:
% herd7 -conf show.cfg -showevents all -show prop -skipchecks external -preview S+rel+data.litmus
This produces the following diagram:
As you can see, there is a path from the Memory Read Effect c: R[y]=1 generated by the load on P1 to the Memory Write Effect d: W[x]=1 generated by the store on P1. This path is made of iico_data (Intrinsic data) and rf-reg (Reads-from-register) arrows.
This path constitutes a “Dependency through Registers and Memory”. A dependency through registers and memory which starts with an Explicit Memory Read Effect such as the Effect c: R[y]=1 constitutes a “Basic dependency”.
To determine whether this path constitutes a Data dependency we need to examine if this step lands on an Effect which affects the data used by the target instruction (e.g. the Register Read Effect t: R1:X2q=1 of the STR W2,[X3] on P1 in S+rel+data).
Finally, we need to check if there is one or several further steps of Intrinsic Data Dependency (reaching the Memory Effects of the target instruction, e.g. d: W[x]=1 for STR W2,[X3] on P1 in S+rel+data).
To illustrate this, let’s have a look at what is happening on P1 of LB+rel+ctrl from an Intrinsic dependencies point of view:
% herd7 -conf show.cfg -showevents all -show prop -skipchecks external -preview LB+rel+ctrl.litmus
This produces the following diagram:
As you can see, there is a path from the Memory Read Effect c: R[y]=1 generated by the load on P1 to the Branching Effect o: Branching (bcc) generated by the branch on P1. This path is made of iico_data (Intrinsic data) and rf-reg (Reads-from-register) arrows.
This path constitutes a “Dependency through Registers and Memory”. A dependency through registers and memory which starts with an Explicit Memory Read Effect such as the Effect c: R[y]=1 constitutes a “Basic dependency”.
To determine whether this path constitutes a Control dependency we need to check if there is one or several further steps of program order (reaching the Memory Effects of the target instruction, e.g. d: W[x]=1 for STR W2,[X3] on P1 in LB+rel+ctrl).
This document was translated from LATEX by HEVEA.