Part II |
We wrote diy7 as part of our empirical approach to studying relaxed memory models: developing in tandem testing tools and models of multiprocessor behaviour. In this tutorial, we attempt an independent tool presentation. Readers interested by the companion formalism are invited to refer to our CAV 2010 publication [1].
The distribution includes additional test generators: diyone7 for generating one test and diycross7 for generating simple variations on one test.
Relaxation is one of the key concepts behind simple analysis of weak memory models. We define a candidate relaxation by reference to the most natural model of parallel execution in shared memory: Sequential Consistency (SC), as defined by L. Lamport [3]. A parallel program running on a sequentially consistent machine behaves as an interleaving of its sequential threads.
Consider once more the example SB.litmus:
X86 SB
"Fre PodWR Fre PodWR"
{ x=0; y=0; }
P0 | P1 ;
MOV [y],$1 | MOV [x],$1 ; #(a)Wy1 | (c)Wx1
MOV EAX,[x] | MOV EAX,[y] ; #(b)Rx0 | (d)Ry0
exists (0:EAX=0 /\ 1:EAX=0)
To focus on interaction through shared memory, let us consider memory accesses, or memory events. A memory event will hold a direction (write, written W, or read, written R), a memory location (written x, y) a value and a unique label. In any run of the simple example above, four memory events occur: two writes (c) Wx1 and (a) Wy1 and two reads (b) Rxv1 with a certain value v1 and (d) Ryv2 with a certain value v2.
If the program’s
behaviour is modelled by the interleaving of its events, the first event must
be a write of value 1 to location x or y and at least one
of the loads must see a 1. Thus, a SC machine would exhibit only three
possible outcomes for this test:
| Allowed: 0:EAX = 0 ∧ 1:EAX = 1 |
| Allowed: 0:EAX = 1 ∧ 1:EAX = 0 |
| Allowed: 0:EAX = 1 ∧ 1:EAX = 1 |
However, running (see Sec. 1.1) this test on a x86 machine yields an additional result:
| Allowed: 0:EAX = 0 ∧ 1:EAX = 0 |
And indeed, x86 allows each write-read pair on both processors to be reordered [2]: thus the write-read pair in program order is relaxed on each of these architectures. We cannot use SC as an accurate memory model for modern architectures. Instead we analyse memory models as relaxing the ordering constraints of the SC memory model.
Consider again our classical example, from a SC perspective. We briefly argued that the outcome “0:EAX = 0 ∧ 1:EAX = 0” is forbidden by SC. We now present a more complete reasoning:
The key idea of diy7 resides in producing programs from similar cycles. To that aim, the edges in cycles must convey additional information:
So far so good, but our x86 machine produced the outcome 0:EAX = 0 ∧ 1:EAX = 0. The Intel Memory Ordering White Paper [2] specifies: “Loads may be reordered with older stores to different locations”, which we rephrase as: PodWR is relaxed. Considering Fre to be safe, we have the graph:
And the brown sub-graph becomes acyclic.
We shall see later why we choose to relax PodWR and not Fre. At the moment, we observe that we can assume PodWR to be relaxed and Fre not to be (i.e. to be safe) and test our assumptions, by producing and running more litmus tests. The diy7 suite precisely provides tools for this approach.
As a first example, SB.litmus can be created as follows:
% diyone7 -arch X86 -name SB Fre PodWR Fre PodWR
As a second example, we can produce several similar tests as follows:
% diy7 -arch X86 -safe Fre -relax PodWR -name SB
Generator produced 2 tests
Relaxations tested: {PodWR}
diy7 produces two litmus tests, SB000.litmus and SB001.litmus, plus one index file @all. One of the litmus tests generated is the same as above, while the new test is:
% cat SB001.litmus
X86 SB001
"Fre PodWR Fre PodWR Fre PodWR"
Cycle=Fre PodWR Fre PodWR Fre PodWR
Relax=PodWR
Safe=Fre
{ }
P0 | P1 | P2 ;
MOV [z],$1 | MOV [x],$1 | MOV [y],$1 ;
MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] ;
exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0)
% cat @all
# diy -arch X86 -safe Fre -relax PodWR -name SB
# Revision: 3333
SB000.litmus
SB001.litmus
diy7 first generates cycles from the candidate relaxations given as arguments, up to a limited size, and then generates litmus tests from these cycles.
We assume the memory to be coherent. Coherence implies that, in a given execution, the writes to a given location are performed by following a sequence, or coherence order, and that all processors see the same sequence.
In diy7, the coherence orders are specified indirectly. For instance, the candidate relaxation Wse (resp. Wsi) specifies two writes, performed by different processors (resp. the same processor), to the same location ℓ, the first write preceding the second in the coherence order of ℓ. The condition of the produced test then selects the specified coherence orders. Consider for instance:
% diyone7 -arch X86 -name x86-2+2W Wse PodWW Wse PodWW
The cycle that reveals a violation of the SC memory model is:
So the coherence order is 0 (initial store, not depicted), 1, 2 for both locations x and y. While the produced test is:
X86 x86-2+2W
"Wse PodWW Wse PodWW"
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Ws Ws
Orig=Wse PodWW Wse PodWW
{
}
P0 | P1 ;
MOV [x],$2 | MOV [y],$2 ;
MOV [y],$1 | MOV [x],$1 ;
exists
(x=2 /\ y=2)
By the coherence hypothesis, checking the final value of locations suffices to characterise those two coherence orders, as expressed by the final condition of x86-2+2W:
exists (x=2 /\ y=2)
See Sec. 10 for alternative means to identify coherence orders.
Candidate relaxations Rfe and Rfi relate writes to reads that load their value. We are now equipped to generate the famous iriw test (independent reads of independent writes):
% diyone7 -arch X86 Rfe PodRR Fre Rfe PodRR Fre -name iriw
We generate its internal variation (i.e. where all Rfe are replaced by Rfi) as easily:
% diyone7 -arch X86 Rfi PodRR Fre Rfi PodRR Fre -name iriw-internal
We get the cycles of Fig. 1,
and the litmus tests of Fig. 2.
X86 iriw "Rfe PodRR Fre Rfe PodRR Fre" { } P0 | P1 | P2 | P3 ; MOV EAX,[y] | MOV [x],$1 | MOV EAX,[x] | MOV [y],$1 ; MOV EBX,[x] | | MOV EBX,[y] | ; exists (0:EAX=1 /\ 0:EBX=0 /\ 2:EAX=1 /\ 2:EBX=0)X86 iriw-internal "Rfi PodRR Fre Rfi PodRR Fre" { } P0 | P1 ; MOV [x],$1 | MOV [y],$1 ; MOV EAX,[x] | MOV EAX,[y] ; MOV EBX,[y] | MOV EBX,[x] ; exists (0:EAX=1 /\ 0:EBX=0 /\ 1:EAX=1 /\ 1:EBX=0)
Candidate relaxations given as arguments really are a “concise specification”. As an example, we get iriw for Power, simply by changing -arch X86 into -arch PPC.
% diyone7 -arch PPC Rfe PodRR Fre Rfe PodRR Fre
PPC A
"Rfe PodRR Fre Rfe PodRR Fre"
{
0:r2=y; 0:r4=x;
1:r2=x;
2:r2=x; 2:r4=y;
3:r2=y;
}
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ;
lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) | stw r1,0(r2) ;
exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0)
Also notice that without the -name option, diyone7 writes its result to standard output.
We summarise the candidate relaxations available on all architectures.
We call communication candidate relaxations the relations between two events communicating through memory, though they could belong to the same processor. Thus, these events operate on the same memory location.
| diy7 syntax | Source | Target | Processor | Additional property |
| Rfi | W | R | Same | Target reads its value from source |
| Rfe | W | R | Different | Target reads its value from source |
| Wsi | W | W | Same | Source precedes target in coherence order |
| Wse | W | W | Different | Source precedes target in coherence order |
| Fri | R | W | Same | Source reads a value from a write that precedes target in coherence order |
| Fre | R | W | Different | Source reads a value from a write that precedes target in coherence order |
We call program order candidate relaxations each relation between two events in the program order. These events are on the same processor, since they are in program order. As regards code output, diy7 interprets a program order candidate relaxation by generating two memory instructions (load or store) following one another.
Program order candidate relaxations have the following syntax:
where:
In practice, we have:
| diy7 syntax | Source | Target | Location |
| PosRR | R | R | Same |
| PodRR | R | R | Diff |
| PosRW | R | W | Same |
| PodRW | R | W | Diff |
| PosWW | W | W | Same |
| PodWW | W | W | Diff |
| PosWR | W | R | Same |
| PodWR | W | R | Diff |
It is to be noticed that PosWR, PosWW and PosRW are similar to Rfi, Wsi and Fri, respectively. More precisely, diy7 is unable to consider a PosWR (or PosWW, or PosRW) candidate relaxation as not being also a Rfi (or Wsi, or Fri) candidate relaxation. However, litmus tests conditions may be more informative in the case of Rfi and Fri.
Relaxed architectures provide specific instructions, namely barriers or fences, to enforce order of memory accesses. In diy7 the presence of a fence instruction is specified with fence candidate relaxations, similar to program order candidate relaxations, except that a fence instruction is inserted. Hence we have FencesRR, FencedRR. etc. The inserted fence is the strongest fence provided by the architecture — that is, mfence for x86 and sync for Power.
Fences can also be specified by using specific names. For instance, we have MFence for x86; while on PPC we have Sync, LwSync, Eieio and ISync. Hence, to yield two reads to different locations and separated by the lightweight PPC barrier lwsync, we specify LwSyncdRR.
The table in figure 3 lists all fence prefixes for all supported architectures:
Also notice that, for a given architecture A, recognized fence prefixes can be listed with the following command: “diyone7 -arch A -show fences”.
Most architectures, and more specifically LISA, support annotations that decorate events. The most common such annotation is “X” (or “A” depending on the architecture) for “atomic” accesses that will generate atomic accesses, i.e. load-reserve/store-conditional pairs (lr/sc) or read-modify write instructions.
As annotations apply to events, they are pseudo-candidates that appear in-between actual candidate relaxations. For instance, consider the AArch64 architecture that features primitive store release (annotation “L”) and load acquire (annotation “A”) instructions. One may specify the well known message-passing release-acquire idiom as follows:
% diyone7 -arch AArch64 PodWW L Rfe A PodRR Fre
AArch64 A
...
{
0:X1=x; 0:X3=y;
1:X1=y; 1:X3=x;
}
P0 | P1 ;
MOV W0,#1 | LDAR W0,[X1] ;
STR W0,[X1] | LDR W2,[X3] ;
MOV W2,#1 | ;
STLR W2,[X3] | ;
exists (1:X0=1 /\ 1:X2=0)
In the ARMv8 assembler code above, one notices the STLR (store release) and LDAR (load acquire) instructions.
In AArch64, the “atomic” annotation reads “X”, as “A” stands for “acquire”. This applies to both stores and loads and generate code snippets that implement “‘atomic” accesses using lr/sc pairs.
% diyone7 -arch AArch64 PodWW XL Rfe XA PodRR Fre
AArch64 A
...
{
0:X1=x; 0:X2=y;
1:X0=y; 1:X4=x;
}
P0 | P1 ;
MOV W0,#1 | Loop01: ;
STR W0,[X1] | LDAXR W1,[X0] ;
MOV W3,#1 | STXR W2,W1,[X0] ;
Loop00: | CBNZ W2,Loop01 ;
LDXR W4,[X2] | LDR W3,[X4] ;
STLXR W5,W3,[X2] | ;
CBNZ W5,Loop00 | ;
exists
(y=1 /\ 0:X4=0 /\ 1:X1=1 /\ 1:X3=0)
Observe that the “L” and “A” annotations can be combined, yielding “atomic release” store and “atomic acquire” load operations.
Loop unrolling of lr/sc idioms is controlled through the -ua <n> (abbreviation of -unrollatonic <n>) command line option. Of some interest is the setting -ua 0 that commands unrolling the loops once and testing store conditional success in the final condition:
% diyone7 -ua 0 -arch AArch64 PodWW XL Rfe XA PodRR Fre
AArch64 A
"PodWWPXL RfeXLXA PodRRXAP Fre"
Generator=diyone7 (version 7.49+01(dev))
Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
Com=Rf Fr
Orig=PodWWPXL RfeXLXA PodRRXAP Fre
{
0:X1=x; 0:X2=y;
1:X0=y; 1:X4=x;
}
P0 | P1 ;
MOV W0,#1 | LDAXR W1,[X0] ;
STR W0,[X1] | STXR W2,W1,[X0] ;
MOV W3,#1 | LDR W3,[X4] ;
LDXR W4,[X2] | ;
STLXR W5,W3,[X2] | ;
exists
(y=1 /\ 0:X5=0 /\ 0:X4=0 /\ 1:X2=0 /\ 1:X1=1 /\ 1:X3=0)
As another example of atomic accesses, the X86 architecture use atomic exchange instructions to implement atomic store operations:
% diyone7 -arch X86 A PodWR Fre A PodWR Fre
X86 A
...
{
}
P0 | P1 ;
MOV EAX,$1 | MOV EAX,$1 ;
XCHG [x],EAX | XCHG [y],EAX ;
MOV EBX,[y] | MOV EBX,[x] ;
exists
(x=1 /\ y=1 /\ 0:EBX=0 /\ 1:EBX=0)
The table in figure 4 lists all annotations for all supported architectures. Notice that all annotations do not apply to all accesses. For instance, the X86 “A” applies to stores only, while the PPC “R” (Reserve) applies to loads only, etc.
Also notice that, for a given architecture A, recognized annotation pseudo relaxations can be listed with the following command: “diyone7 -arch A -show annot.
The tool diy7 can probably be used in various, creative, ways; but the tool first stems from our technique for testing relaxed memory models. The -safe and -relax options are crucial here. We describe our technique by the means of an example: X86-TSO.
Before engaging in testing it is important to categorise candidate relaxations as safe or relaxed.
This can done by interpretation of vendor’s documentation. For instance, the iriw test of Sec. 6.3 is the example 7.7 of [2] “Stores Are Seen in a Consistent Order by Other Processors”, with a Forbid specification. Hence we deduce that Fre, Rfe and PodRR are safe. Then, from test iriw-internal of Sec. 6.3, which is Intel’s test 7.5 “Intra-Processor Forwarding Is Allowed” with an allow specification, we deduce that Rfi is relaxed. Namely, the cycle of iriw-internal is “Fre Rfi PodRR Fre Rfi PodRR”. Therefore, the only possibility is for Rfi to be relaxed.
Overall, we deduce:
Of course these remain assumptions to be tested. To do so, we perform one series of tests per relaxed candidate relaxation, and one series of tests for confirming safe candidate relaxations as much as possible. Let S be all safe candidate relaxations.
Namely, diy7 builds cycles as follows:
For the purpose of confirming relaxed candidate relaxations, S can be replaced by a subset.
Repeating command line options is painful and error prone. Besides, configuration parameters may get lost. Thus, we regroup those in configuration files that simply list the options to be passed to diy7, one option per line. For instance here is the configuration file for testing the safe relaxations of x86, x86-safe.conf.
#safe x86 conf file -arch X86 #Generate tests on four processors or less -nprocs 4 #From cycles of size at most six -size 6 #With names safe000, safe0001,... -name safe #List of safe relaxations -safe PosR* PodR* PodWW PosWW Rfe Wse Fre FencesWR FencedWR
Observe that the syntax of candidate relaxations allows one shortcut: the wildcard * stands for W and R. Thus PodR* gets expanded to the two candidate relaxations PodRR and PodRW.
We get safe tests by issuing the following command, preferably in a specific directory, say safe.
% diy7 -conf x86-safe.conf
Generator produced 38 tests
Relaxations tested: {}
Here are the configuration files for confirming that Rfi and PodWR are relaxed, x86-rfi.conf and x86-podwr.conf.
#rfi x86 conf file
-arch X86
-nprocs 4
-size 6
-name rfi
-safe PosR* PodR* PodWW PosWW Rfe Wse Fre FencesWR FencedWR
-relax Rfi
| #podrw x86 conf file
-arch X86
-nprocs 4
-size 6
-name podwr
-safe Fre
-relax PodWR
|
Notice that we used the complete safe list in x86-rfi.conf and a reduced list in x86-podwr.conf. Tests are to be generated in specific directories. To that aim, we provide a convenient archive x86.tar.
% cd rfi
% diy7 -conf x86-rfi.conf
Generator produced 11 tests
Relaxations tested: {Rfi}
% cd ../podwr
% diy7 -conf x86-podwr.conf
Generator produced 2 tests
Relaxations tested: {PodWR}
% cd ..
Now, let us run all tests at once, with the parameters of machine saumur (4 physical cores with hyper-threading):
% litmus7 -mach saumur rfi/@all > rfi/saumur.rfi.00 % litmus7 -mach saumur podwr/@all > podwr/saumur.podwr.00 % litmus7 -mach saumur safe/@all > safe/saumur.safe.00
If your machine has 2 cores only, try litmus -a 2 -limit true…
We now look for the tests that have validated their condition in the result files of litmus7. A simple tool, readRelax7, does the job:
% readRelax7 rfi/saumur.rfi.00 podwr/saumur.podwr.00 safe/saumur.safe.00
.
.
.
** Relaxation summary **
{Rfi} With {Rfe, Fre, Wse, PodRW, PodRR} {Rfe, Fre, PodRR}\
{Fre, Wse, PodWW, PodRR} {Fre, PosWW, PodRR, MFencedWR}\
{Fre, PodWW, PodRR, MFencedWR} {Fre, PodRR} {Fre, PodRR, MFencedWR}
{PodWR} With {Fre}
The tool readRelax7 first lists the result of all tests
(which is omitted above), and then dumps a summary of the
relaxations it found.
The sets of the candidate relaxations that need to be safe for the tests to
indeed reveal a relaxed candidate relaxation are also given.
Here, Rfi and PodWR are confirmed to be relaxed, while no candidate relaxation
in the safe set is found to be relaxed.
Had it been the case, a line {} With {...} would have occurred
in the relaxation summary.
The safe tests need to be run a lot of times, to increase our
confidence in the safe set.
We introduce some additional candidate relaxations that are specific to the Power architecture. We shall not detail here our experiments on Power machines. See our experience report http://diy.inria.fr/phat/ for more details.
In a very relaxed architecture such as Power, intra-processor dependencies becomes significant. Roughly, intra-processor dependencies fall into two categories:
Finally, one may control the nature of the dependency: address dependency (DpAddr(s|d)(R|W) or data dependency (DpData(s|d)W).
ARM has similar candidate relaxations, Isync being replaced by ISB.
In the produced code, diy7 expresses a data dependency by a false dependency (or dummy dependency) that operates on the address of the target memory access. For instance:
% diyone7 DpdW Rfe DpdW Rfe
PPC A
"DpAddrdW Rfe DpAddrdW Rfe"
{
0:r2=y; 0:r5=x;
1:r2=x; 1:r5=y;
}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | xor r3,r1,r1 ;
li r4,1 | li r4,1 ;
stwx r4,r3,r5 | stwx r4,r3,r5 ;
exists (0:r1=1 /\ 1:r1=1)
On P0, the effective address of the indexed store stwx r4,r3,r5
depends on the contents of the index register r3, which itself
depends on the contents of r1.
The dependency is a “false” one, since the contents of r3
always is zero, regardless of the contents of r1.
One may observe that DpdW is changed into DpAddrdW in the comment
field of the test.
As a matter of fact, DpdW is a macro for the address dependency
DpAddrW. We could have specified data dependency instead:
% diyone7 DpDatadW Rfe DpAddrdW Rfe
PPC A
"DpDatadW Rfe DpAddrdW Rfe"
{
0:r2=y; 0:r4=x;
1:r2=x; 1:r5=y;
}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | xor r3,r1,r1 ;
addi r3,r3,1 | li r4,1 ;
stw r3,0(r4) | stwx r4,r3,r5 ;
exists
(0:r1=1 /\ 1:r1=1)
On P0, the value stored by the last (store) instruction
stw r3,0(r4) is now computed from the
value read by the first (load) instruction lwz r1,0(r2).
Again, this is a “false” dependency.
A control dependency is implemented by the means of an useless compare and branch sequence, plus the isync instruction when the target event is a load. For instance
% diyone7 CtrldR Fre SyncdWW Rfe
PPC A
"DpCtrlIsyncdR Fre SyncdWW Rfe"
{
0:r2=y; 0:r4=x;
1:r2=x; 1:r4=y;
}
P0 | P1 ;
lwz r1,0(r2) | li r1,1 ;
cmpw r1,r1 | stw r1,0(r2) ;
beq LC00 | sync ;
LC00: | li r3,1 ;
isync | stw r3,0(r4) ;
lwz r3,0(r4) | ;
exists
(0:r1=1 /\ 0:r3=0)
Also notice that CtrldR is interpreted as DpCtrlIsyncR in the comment field of the test.
Of course, in all cases, we assume that “false” dependencies are not “optimised out” by the assembler or the hardware.
Users may specify a small sequence of single candidate relaxations as behaving as a single candidate relaxation to diy7. The syntax is:
The main usage of the feature is to specify cumulativity candidate relaxations, that is, the sequence of Rfe and of a fence candidate relaxation (A-cumulativity), the sequence of a fence candidate relaxation and of Rfe (B-cumulativity), or both (AB-cumulativity).
Cumulativity candidate relaxations are best expressed by the following syntactical shortcuts: let r be a fence candidate relaxation, then ACr stands for [Rfe,r], BCr stands for [r,Rfe], while ABCr stands for [Rfe,r,Rfe],
Hence, a simple way to generate iriw-like (see Sec. 6.3) litmus tests with lwsync is as follows:
% diy7 -name iriw-lwsync -nprocs 8 -size 8 -relax ACLwSyncdRR -safe Fre
Generator produced 3 tests
Relaxations tested: {ACLwSyncdRR}
where we have for instance:
% cat iriw-lwsync001.litmus
PPC iriw-lwsync001
"Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR"
Cycle=Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax=ACLwSyncdRR
Safe=Fre
{
0:r2=z; 0:r4=x; 1:r2=x;
2:r2=x; 2:r4=y; 3:r2=y;
4:r2=y; 4:r4=z; 5:r2=z;
}
P0 | P1 | P2 | P3 | P4 | P5 ;
lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ;
lwsync | stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync | stw r1,0(r2) ;
lwz r3,0(r4) | | lwz r3,0(r4) | | lwz r3,0(r4) | ;
exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0 /\ 4:r1=1 /\ 4:r3=0)
Detours combine a Pos candidate relaxation and a sequence of two external communication candidate relaxations. More precisely detours are some constrained Pos candidate relaxations: the source and target events must be related by a sequence of two communication candidate relaxations, whose target and source are a common event whose processor is new.
| diy7 syntax | Source | Target | Detour |
| DetourR | R | R | Fre; Rfe |
| DetourW | W | R | Wse; Rfe |
| DetourRW | R | W | Fre;Wse |
| DetourWW | W | W | Wse;Wse |
DetourRR and DetourWR are accepted as synonyms for DetourR and DetourW respectively.
Graphically, we have:
Finally notice that “internal” detours need no special treatement as they can be expressed by the sequences “Fri; Rfi”, “Wsi;Rfi”, etc.
The tool diycross7 has an interface similar to diyone7, except it accepts list of candidate relaxations where diyone7 accepts single candidate relaxations. The new tool produces the test resulting by “cross producing” the lists. For instance, one can generate all variations on the IRIW test (see Sec. 6.3) that involve data dependencies and the lightweight barrier lwsync as follows:
% diycross7 -arch PPC -name IRIW Rfe DpdR,LwSyncdRR Fre Rfe DpdR,LwSyncdRR Fre Generator produced 3 tests % ls @all IRIW+addrs.litmus IRIW+lwsync+addr.litmus IRIW+lwsyncs.litmus
diycross7 outputs the index file @all that lists the test source files, and three tests, with names we believe to be self-explanatory:
% cat IRIW+lwsync+addr.litmus
PPC IRIW+lwsync+addr
"Rfe LwSyncdRR Fre Rfe DpAddrdR Fre"
Cycle=Rfe LwSyncdRR Fre Rfe DpAddrdR Fre
{
0:r2=y;
1:r2=y; 1:r4=x;
2:r2=x;
3:r2=x; 3:r5=y;
}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | xor r3,r1,r1 ;
| lwz r3,0(r4) | | lwzx r4,r3,r5 ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0)
Users may use the special keywords allRR, allRW, allWR and allWW to specify the set of all existing program order candidate relaxations between the specified “R” or “W”. For instance, we get the complete variations on IRIW by:
% diycross7 -arch PPC -name IRIW Rfe allRR Fre Rfe allRR Fre Generator produced 28 tests % ls @all IRIW.litmus IRIW+addr+po.litmus IRIW+lwsync+addr.litmus ... IRIW+isyncs.litmus
We first produce the “four writes” test 2+2W for Power:
% diyone7 -name 2+2W -arch PPC PodWW Wse PodWW Wse
% cat 2+2W.litmus
PPC 2+2W
"PodWW Wse PodWW Wse"
{ 0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x; }
P0 | P1 ;
li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2)
Test 2+2W is the Power version of the x86 test
x86-2+2W of Sec. 6.3.
In that section, we argued that the final condition exists (x=2 /\ y=2)
suffices to identify the coherence orders 0, 1, 2
for locations x and y.
As a consequence, a positive final condition reveals the occurrence
of the specified cycle: Wse PodWW Wse PodWW.
Observers provide an alternative, perhaps more intuitive, means to identify coherence orders: an observer simply is an additional thread that performs several loads from the same location in sequence. Here, loading value 1 and then value 2 from location x identifies the coherence order 0, 1, 2. The command line switch -obs force commands the production of observers (test 2+2WObs):
% diyone7 -name 2+2WObs -obs force -obstype straight -arch PPC PodWW Wse PodWW Wse
% cat 2+2WObs.litmus
PPC 2+2WObs
"PodWW Wse PodWW Wse"
{ 0:r2=x; 1:r2=y; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=x; }
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | lwz r1,0(r2) | li r1,2 | li r1,2 ;
lwz r3,0(r2) | lwz r3,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
| | li r3,1 | li r3,1 ;
| | stw r3,0(r4) | stw r3,0(r4) ;
exists (0:r1=1 /\ 0:r3=2 /\ 1:r1=1 /\ 1:r3=2)
Thread P0 observes location x, while thread P1 observes location y. With respect to 2+2W, final condition has changed, the direct observation of the final contents of locations x and y being replaced by two successive observations of the contents of x and y.
It should first be noticed that the reasoning above assumes that having the same thread to read 1 from say x and then 2 implies that 1 takes place before 2 in the coherence order of x. This may not be the case in general — although it holds for Power. Moreover, running 2+2W and 2+2WObs yields contrasted results. While a positive conclusion is immediate for 2+2W, we were not able to reach a similar conclusion for 2+2WObs. As a matter of fact, 2+2WObs yielding Ok stems from the still-to-be-observed coincidence of several events: both observers threads must run at the right pace to observe the change from 1 to 2, while the cycle must indeed occur.
A simple observer consisting of loads performed in sequence is a straight observer. We define two additional sorts of observers: fenced observers, where loads are separated by the strongest fence available, and loop observers, which poll on location contents change. Those are selected by the homonymous tags given as arguments to the command line switch -obstype. For instance, we get the test 2+2WObsFenced by:
% diyone7 -name 2+2WObsFenced -obs force -obstype fenced -arch PPC PodWW Wse PodWW Wse
% cat 2+2WObsFenced.litmus
PPC 2+2WObsFenced
"PodWW Wse PodWW Wse"
{ 0:r2=x; 1:r2=y; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=x; }
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | lwz r1,0(r2) | li r1,2 | li r1,2 ;
sync | sync | stw r1,0(r2) | stw r1,0(r2) ;
lwz r3,0(r2) | lwz r3,0(r2) | li r3,1 | li r3,1 ;
| | stw r3,0(r4) | stw r3,0(r4) ;
exists (0:r1=1 /\ 0:r3=2 /\ 1:r1=1 /\ 1:r3=2)
Invoking diyone7 as “diyone -obs force -obstype loop ...”
yields the additional test 2+2WObsLoop:
PPC 2+2WObsLoop
"PodWW Wse PodWW Wse"
{ 0:r2=x; 1:r2=y;
2:r2=x; 2:r4=y; 3:r2=y; 3:r4=x; }
P0 | P1 | P2 | P3 ;
L00: | L03: | li r1,2 | li r1,2 ;
lwz r1,0(r2) | lwz r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
cmpwi r1,0 | cmpwi r1,0 | li r3,1 | li r3,1 ;
beq L00 | beq L03 | stw r3,0(r4) | stw r3,0(r4) ;
li r4,200 | li r4,200 | | ;
L01: | L04: | | ;
lwz r3,0(r2) | lwz r3,0(r2) | | ;
cmpw r3,r1 | cmpw r3,r1 | | ;
bne L02 | bne L05 | | ;
addi r4,r4,-1 | addi r4,r4,-1 | | ;
cmpwi r4,0 | cmpwi r4,0 | | ;
bne L01 | bne L04 | | ;
L02: | L05: | | ;
exists (0:r1=1 /\ 0:r3=2 /\ 1:r1=1 /\ 1:r3=2)
A loop observer first busily waits for the observed location not to hold its initial contents 0, and then busily waits for another change of location contents. The second loop is performed at most a finite number of times (here 200), in order to ensure termination.
With local observers, coherence order is observed by the test threads. This implies changing the tests, and some care must be exercised when interpreting results.
The idea is as follows: when two threads are connected by a Wse candidate relaxation, meaning that the first thread ends by writing v to some location ℓ and that the second threads starts by writing v+1 to the same location ℓ, we add an observing read of location ℓ at the end of the first thread. Then, reading v+1 means that the write by the first thread precedes the write by the second thread in ℓ coherence order. More concretely, we instruct diy7 generators to emit such local observers with option -obs local:
% diyone7 -name 2+2WLocal -obs local -obstype straight -arch PPC PodWW Wse PodWW Wse
% cat 2+2WLocal.litmus
PPC 2+2WLocal
"PodWW Wse PodWW Wse"
{
0:r2=x; 0:r4=y;
1:r2=y; 1:r4=x;
}
P0 | P1 ;
li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) ;
lwz r5,0(r4) | lwz r5,0(r4) ;
exists
(0:r5=2 /\ 1:r5=2)
With respect to 2+2W, final condition has changed, the direct observation of the final contents of locations y and x being replaced local observation of y by thread 0 and local observation of x by thread 1.
Based for instance on the test execution witness, whose only SC-violation cycle is the same as as for 2+2W,
one may argue that tests 2+2W and 2+2WLocal are equivalent, in the sense that both are allowed or both are forbidden by a model or machine.
Local observers can also be fenced or looping. For instance, one produces 2+2WLocalFenced, the fenced local observer version of 2+2W as follows:
% diyone7 -name 2+2WLocalFenced -obs local -obstype fenced -arch PPC PodWW Wse PodWW Wse
% cat 2+2WLocalFenced.litmus
PPC 2+2WLocalFenced
"PodWW Wse PodWW Wse"
{
0:r2=x; 0:r4=y;
1:r2=y; 1:r4=x;
}
P0 | P1 ;
li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) ;
sync | sync ;
lwz r5,0(r4) | lwz r5,0(r4) ;
exists
(0:r5=2 /\ 1:r5=2)
While one produces 2+2WLocalLoop, the looping local observer version of 2+2W as follows:
% diyone7 -name 2+2WLocalLoop -obs local -obstype loop -arch PPC PodWW Wse PodWW Wse
% cat 2+2WLocalLoop.litmus
PPC 2+2WLocalLoop
"PodWW Wse PodWW Wse"
{
0:r2=x; 0:r4=y;
1:r2=y; 1:r4=x;
}
P0 | P1 ;
li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) ;
li r6,200 | li r6,200 ;
L00: | L02: ;
lwz r5,0(r4) | lwz r5,0(r4) ;
cmpwi r5,1 | cmpwi r5,1 ;
bne L01 | bne L03 ;
addi r6,r6,-1 | addi r6,r6,-1 ;
cmpwi r6,0 | cmpwi r6,0 ;
bne L00 | bne L02 ;
L01: | L03: ;
exists (0:r5=2 /\ 1:r5=2)
In the code above, observing loads are attempted at most 200 time or until a value different from 1 is read.
As an indication of the performance of the various sorts of observers, the following table summarises a litmus7 experiment performed on a 8-cores 4-ways SMT Power7 machine machine— complete litmus7 log.
| 2+2W | 2+2WObs | 2+2WObsFenced | 2+2WObsLoop | 2+2WLocal | 2+2WLocalFenced | 2+2WLocalLoop | |
| Positive | 2.2M/160M | 0/80M | 326/80M | 25k/80M | 2/160M | 34k/160M | 111k/160M |
The row “Positive” shows the number of observed positive outcomes/total
number of outcomes produced.
For instance, in the case of 2+2W, we observed the positive outcome
x=2 /\ y=2
more than 2 millions times out of a total of 160 millions outcomes.
As a conclusion, all techniques achieve decent results, except straight
observers.
In test 2+2W the coherence orders sequence two writes. If there are three writes or more to the same location, it is no longer possible to identify a coherence order by observing the final contents of the memory location involved. In other words, observers are mandatory.
The argument to the -obs switch commands the production of observers. It can take four values:
With diyone7, one easily build a three writes test as for instance the following W5:
% diyone7 -obs accept -obstype fenced -arch PPC -name W5 Wse Wse PodWW Wse PodWW
% cat W5.litmus
PPC W5
"Wse Wse PodWW Wse PodWW"
{ 0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; }
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | li r1,3 | li r1,2 | li r1,2 ;
sync | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
lwz r3,0(r2) | li r3,1 | li r3,1 | ;
sync | stw r3,0(r4) | stw r3,0(r4) | ;
lwz r4,0(r2) | | | ;
exists (x=2 /\ 0:r1=1 /\ 0:r3=2 /\ 0:r4=3)
As apparent from the code above, we have a fenced observer thread
on y (P0),
while the final state of x is observed directly
(x=2).
The command line switch -obs force would yield two observers,
while -obs avoid would lead to failure.
With command line switch -obs local we get three local observations of coherence, which suffice to reconstruct the complete coherence orders:
% diyone7 -obs local -obstype fenced -arch PPC -name W5Local Wse Wse PodWW Wse PodWW
chi% cat W5Local.litmus
PPC W5Local
"Wse Wse PodWW Wse PodWW"
{
0:r2=x; 0:r4=y;
1:r2=y; 1:r4=x;
2:r2=x;
}
P0 | P1 | P2 ;
li r1,3 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
li r3,1 | li r3,1 | sync ;
stw r3,0(r4) | stw r3,0(r4) | lwz r3,0(r2) ;
sync | sync | ;
lwz r5,0(r4) | lwz r5,0(r4) | ;
exists (0:r5=2 /\ 1:r5=2 /\ 2:r3=3)
The diy7 suite consists in four main tools:
We have designed a simple naming scheme for tests. A normalised test name decomposes first as a family name, and second as a description of program order (or internal) candidate relaxations.
Cycles (and thus tests) are first grouped by families. Family names describe test structure, based upon external communication candidates relaxations. More specifically, external communication candidates relaxations suffice to settle the directions (W or R) of first and last events of threads, considering the case when those two events are the same. For instance, consider the cycle “PodWW Rfe PodRR Fre”: there are two threads in the corresponding test (as there are two external communication candidate relaxations), one thread starts and ends with a write (written WW), while the other thread starts and ends with a read (written RR). The family name is thus WW+RR, (or RR+WW, but we choose the former). For reference, a normalised family name is the minimal amongst the representations of a given cycle, following the lexical order derived from the order W < WW < RR < RW < WR < R.
The most common families have nicknames, which are defined by this document. For instance, consider the test whose cycle is “PodWR Fre PodWR Fre”. The family name is WR+WR, as this is a two-thread test, both threads starting with a write and ending with a read. The nickname for this family is, as we already know, SB (store-buffering). Here is the list of nicknames and family names for two thread tests:
| 2+2W | WW+WW | PodWW Wse PodWW Wse |
| LB | RW+RW | PodRW Rfe PodRW Rfe |
| MP | WW+RR | PodWW Rfe PodRR Fre |
| R | WW+WR | PodWW Wse PodWR Fre |
| S | WW+RW | PodWW Rfe PodRW Wse |
| SB | WR+WR | PodWR Fre PodWR Fre |
Isolated writes (and reads) originate from the combinations of communication relaxations, for instance [Fre,Rfe]. They appear as “W” (and R) in family names. For instance, “Rfe PodRR Fre Rfe PodRR Fre” contains two such isolated writes, its name is thus W+RR+W+RR and its nickname is, as we know, IRIW (Independent reads of independent writes). The test “Rfe PodRW Rfe PodRR Fre” contains one isolated write, as apparent from this diagram:
The family name is thus W+RW+RR and the nickname is WRC (Write to Read Causality).
Every family has a prototype, homonymous test where every thread code consists in one (for W or R) or two memory accesses to different locations (for WW, WR etc.). For instance, the MP test is derived from the cycle “PodWW Rfe PodRR Fre”. Variants are described by tags that illustrates the various program order relaxations: they appear after the family name, still with “+” as a separation. For instance the test derived from “LwSyncdWW Rfe DpAddrdR Fre” is named MP+lwsync+addr.
When all threads have the same tag tag, the test name is abbreviated as Family+tags. For instance, the test MP+lwsync+lwsync (“LwSyncdWW Rfe LwSyncdRR Fre”) is in fact MP+lwsyncs. Additionally, the tag pos (all po’s) is omitted, in order to yield family names for the prototype tests — cf. MP whose name would have been MP+pos otherwise.
For the sake of terseness, tags do not describe program order relaxations completely. For instance both DpAddrdR and DpAddrdW (address dependency to read and write, respectively) have the same tag, addr. It does not harm for simple tests, as the missing direction can be inferred from the family name. Consider for instance MP+lwsync+addr and LB+lwsync+addr.
The naming scheme extends to cycles with consecutive program order relaxations, by separating tags with “-” when they follow one another: for instance “LwSyncdWW Rfe DpAddrdR PodRR Fre” is named MP+lwsync+addr-po. Unfortunately, the current naming scheme falls short in supplying non-ambiguous names to all tests. For instance, “LwSyncdWW Rfe DpAddrdW PodWR Fre” is also named MP+lwsync+addr-po. In that situation tools will either fail or silently add a numeric suffix, depending on the boolean -addnum option.
% diycross7 -addnum false LwSyncdWW Rfe [DpAddrdR,PodRR],[DpAddrdW,PodWR] Fre Fatal error: Duplicate name MP+lwsync+addr-po % diycross7 -addnum true LwSyncdWW Rfe [DpAddrdR,PodRR],[DpAddrdW,PodWR] Fre Generator produced 2 tests % cat @all # diycross7 -addnum true LwSyncdWW Rfe [DpAddrdR,PodRR],[DpAddrdW,PodWR] Fre MP+lwsync+addr-po.litmus MP+lwsync+addr-po001.litmus
As a result, we get the two tests: MP+lwsync+addr-po and MP+lwsync+addr-po001.
Future versions of diy7 may solve this issue in a more satisfying manner. At the moment, users are advised not to rely too much on the automatic naming scheme. Users may name tests in a non-ambiguous fashion by (1) specifying an explicit family name (-name name) and (2) selecting the numeric scheme (-num true):
% diycross7 -name MP+X -num true LwSyncdWW Rfe [DpAddrdR,PodRR],[DpAddrdW,PodWR] Fre Generator produced 2 tests
The diycross7 generator outputs the same tests as above, with names MP+X000 and MP+X001.
All test generators accept the following documented command-line options:
If argument <dest> is an archive (extension .tar) or a compressed archive (extension .tgz), the tool builds an archive. Otherwise, <dest> is interpreted as the name of an existing directory. Default is “.”, that is tool output goes into the current directory.
The naming of tests is controlled by the following options:
The following option permits the listing for valid candidate relaxations, given the selected architecture.
The tool diyone7 has two operating modes. The selected mode depends on the presence of command-line arguments,
In the first operating mode, diyone7 takes a non-empty list of candidate relaxations as arguments and outputs a litmus test. Note that diyone7 may fail to produce the test, with a message that briefly details the failure.
% diyone7 Rfe Rfe PodRR Test a [Rfe Rfe PodRR] failed: Impossible direction PodRR Rfe
In this mode, -name <name> sets the name of the test to <name> and output it into file <name>.litmus. If absent, the test name is A and output goes to standard output.
Otherwise, i.e. when there are no command-line arguments, diyone7 reads the standard input and generates the tests described by the lines it reads. Each line starts with a test name name, followed by “:”, followed by a list of candidate relaxations RS. Then, diyone7 acts as if invoked as diyone opts -name name RS.
The tool diyone7 accepts the following documented option:
diycross7 produces several tests by “cross producing” lists of candidate relaxations given as arguments, see Sec 9. diycross7 also produces an index file @all that lists all produced litmus source files.
If option -name <name> is given, it sets the family name of generated tests, otherwise standard family names are used (cf. Sec. 11.1). By default descriptive names are used (i.e. -num false) and diycross7 will fail if two different tests have the same name (i.e. -addnum false):
% diycross7 PodWW Rfe [DpAddrdR,PodRR],[DpAddrdW,PodWR] Fre Fatal error: Duplicate name MP+po+addr-po
Should this happen users can resort either to numeric names,
%diycross7 -num true PodWW Rfe [DpAddrdR,PodRR],[DpAddrdW,PodWR] Fre Generator produced 2 tests con% ls @all MP000.litmus MP001.litmus
or to disambiguating numeric suffixes.
%diycross7 -addnum true PodWW Rfe [DpAddrdR,PodRR],[DpAddrdW,PodWR] Fre Generator produced 2 tests con% ls @all MP+po+addr-po001.litmus MP+po+addr-po.litmus
As diycross7, diy7 produce several files, hence naming issues are critical. By default, diy7 uses family names and the numeric naming scheme (-num true). Users can specify a family name family for all tests with -name family, or attempt using the descriptive names of Sec 11.1 with -num false. Moreover, diy7 produces an index file @all that lists the file names of all tests produced.
The tool diy7 also accepts the following, additional, documented options.
# are comments and are thus ignored.
The relax and safe lists command the generation of cycles as follows:
Generally speaking, diy7 generates “some” cycles and does not generate “all” cycles (up to a certain size e.g.). In (default) sc mode, diy7 performs some optimisation, most of which we leave unspecified. As an exception to this non-specification, diy7 in sc (default) mode is guaranteed not to generate redundant elementary communication relaxation in the following sense: let us call Com the union of Ws, Rf and Fr (the e|i specification is irrelevant here). Ws being transitive and by definition of Fr, one easily shows that the transitive closure Com+ of Com is the union of Com plus [Ws,Rf] (Ws followed by Rf) plus [Fr,Rf]. As a consequence, maximal subsequences of communication relaxations in diy7 cycles are limited to single relaxations (i.e. Ws, Rf and Fr) and to the above mentioned two sequences (i.e. [Ws,Rf] and [Fr,Rf]). For instance, [Ws,Ws] and [Fr,Ws] should never appear in diy7 generated cycles. However, such subsequences can be generated on an individual basis with diyone7, see the example of W5 in Sec 10.3.
In critical mode (-mode critical), cycles are strictly specified as follows:
The cycles described above are the critical cycles of [5].
In free mode (-mode free), cycles are strictly specified as follows:
Finally, the uni mode enforces the following constraints on cycles:
readRelax7 is a simple tool to extract relevant information out of litmus7 run logs of tests produced by the diy7 generator. For a given run of a given litmus test, the relevant information is:
See Sec. 7.2 for an example.
The tool readRelax7 takes file names as arguments. If no argument is present, it reads a list of file names on standard input, one name per line.
When non-standard family names or numeric names are used, it proves convenient to rename tests with the standard naming scheme. We provide two tools to do so: mcycle7 that extracts cycles from litmus source files and classify7 that normalises and renames cycles.
For instance, one can use diy7 to generate all simple, critical, tests up to three threads for X86 with the following configuration file X.conf
-arch X86 -name X -nprocs 3 -size 6 -safe Pod**,Fre,Rfe,Wse -mode critical
% diy7 -conf X.conf Generator produced 23 tests % ls @all X003.litmus X007.litmus X011.litmus X015.litmus X019.litmus X.conf X000.litmus X004.litmus X008.litmus X012.litmus X016.litmus X020.litmus X001.litmus X005.litmus X009.litmus X013.litmus X017.litmus X021.litmus X002.litmus X006.litmus X010.litmus X014.litmus X018.litmus X022.litmus
Cycles are extracted with mcycle7, which takes the index file @all as argument:
% mcycles7 @all X000: Wse PodWR Fre PodWR Fre PodWW X001: Rfe PodRR Fre PodWR Fre PodWW X002: Wse PodWR Fre PodWW X003: Wse PodWW Wse PodWR Fre PodWW X004: Rfe PodRW Wse PodWR Fre PodWW X005: Rfe PodRR Fre PodWW X006: Wse PodWW Rfe PodRR Fre PodWW X007: Rfe PodRW Rfe PodRR Fre PodWW X008: Wse Rfe PodRR Fre PodWW X009: Wse PodWW Wse PodWW ...
The output of mcycle7 can be piped into classify7 for family classification:
% mcycles7 @all | classify7 -arch X86 2+2W X009 -> 2+2W : PodWW Wse PodWW Wse 3.2W X010 -> 3.2W : PodWW Wse PodWW Wse PodWW Wse 3.LB X020 -> 3.LB : PodRW Rfe PodRW Rfe PodRW Rfe 3.SB X016 -> 3.SB : PodWR Fre PodWR Fre PodWR Fre ISA2 X007 -> ISA2 : PodWW Rfe PodRW Rfe PodRR Fre LB X019 -> LB : PodRW Rfe PodRW Rfe MP X005 -> MP : PodWW Rfe PodRR Fre ...
Notice that classify7 accepts the arch option, as it needs to parse cycles.
Finally, one can normalise tests, using normalised names by piping mcycle7 output into diyone7 with options -norm -num false:
% mkdir src % mcycles7 @all | diyone7 -arch X86 -norm -num false -o src Generator produced 23 tests % ls src 2+2W.litmus @all R.litmus WRC.litmus WRW+WR.litmus Z6.2.litmus 3.2W.litmus ISA2.litmus RWC.litmus WRR+2W.litmus WWC.litmus Z6.3.litmus 3.LB.litmus LB.litmus SB.litmus WRW+2W.litmus Z6.0.litmus Z6.4.litmus 3.SB.litmus MP.litmus S.litmus W+RWC.litmus Z6.1.litmus Z6.5.litmus
Alternatively, one may instruct classify7 to produce output for diyone7. In that case one should pass option -diyone to classify7 so as to instruct it to produce output that is parsable by diyone7:
% rm -rf src && mkdir src % mcycles7 @all | classify7 -arch X86 -diyone | diyone7 -arch X86 -o src Generator produced 23 tests % ls src 2+2W.litmus @all R.litmus WRC.litmus WRW+WR.litmus Z6.2.litmus 3.2W.litmus ISA2.litmus RWC.litmus WRR+2W.litmus WWC.litmus Z6.3.litmus 3.LB.litmus LB.litmus SB.litmus WRW+2W.litmus Z6.0.litmus Z6.4.litmus 3.SB.litmus MP.litmus S.litmus W+RWC.litmus Z6.1.litmus Z6.5.litmus
The tool mcycle7 has no options and takes litmus source files or index files as arguments. It outputs a list of lines to standard output. Each line starts with a test name, suffixed by “:”, then the cycle of the named test. Notice that this format is the input format to diyone7 in its second operating mode — see Sec. 11.3.
It is important to notice that, for mcycle7 to extract cycles, those must be present as meta-information in source files. In practice, this means that mcycle7 operates normally on sources produced by diyone7, diycross7 and diy7. Moreover only one instance of a given cycle will be output.
The tool classify7 reads its standard input, interpreting is as a list of cycles in the output format of mcycle7. It normalises and classifies those cycles. The tool classify7 accepts the following documented options:
The tool norm7 is a simplified classify7 tool: it takes a cycle on the command line and outputs a normalized cycles, with name. This output can serve as standard input to diyone7.
For instance, here is hwo one can find the systematic mane of a variation on the store-buffer “SB” test:
% norm7 -arch AArch64 Rfi DMB.LDdRR Fre Rfi DpAddrdR Fre SB+rfi-dmb.ld+rfi-addr: Rfi DMB.LDdRR Fre Rfi DpAddrdR Fre
Notice that the option -arch is mandatory (or defaults to PPC), as candidate relaxations depends on the selected architecture, as illustrated by the fence candidate DMB.LD… above.