Contents
Part I Running tests with
litmus
1 A tour of
litmus
1.1 A simple run
1.2 Cross compilation
1.3 Running several tests at once
2 Controlling test parameters
2.1 Architecture of tests
2.2 Affinity
2.2.1 Introduction to affinity
2.2.2 Study of affinity
2.2.3 Advanced control
2.2.4 Custom control
2.3 Controlling executable files
3 Advanced control of test parameters
3.1 Timebase synchronisation mode
3.2 Advanced prefetch control
3.2.1 Custom prefetch
3.2.2 Prefetch metadata
3.2.3 “Static” prefetch control
4 Usage of
litmus
Part II Generating tests
5 Preamble
5.1 Relaxation of Sequential Consistency
5.2 Introduction to candidate relaxations
5.3 More candidate relaxations
5.4 Summary of simple candidate relaxations
5.4.1 Communication candidate relaxations
5.4.2 Program order candidate relaxations
5.4.3 Fence candidate relaxations
6 Testing candidate relaxations with
diy
6.1 Principle
6.2 Testing x86
7 Additional relaxations
7.1 Intra-processor dependencies
7.2 Composite relaxations and cumulativity
7.3 Detour candidate relaxations
8 Test variations with
diycross
9 Identifying coherence orders with observers
9.1 Simple observers
9.2 More observers
9.2.1 Fences and loops in observers
9.2.2 Local observers
9.2.3 Performance of observers
9.3 Three stores or more
10 Command usage
10.1 A note on test names
10.1.1 Family names
10.1.2 Descriptive names for variants
10.2 Common options
10.3 Usage of
diyone
10.4 Usage of
diycross
10.5 Usage of
diy
10.6 Usage of
readRelax
11 Additional tools: extracting cycles and classification
11.1 Usage of
mcycles
11.2 Usage of
classify
Part III Simulating memory models with
herd
12 Writing simple models
12.1 Sequential consistency
12.2 Total Store Order (TSO)
13 Producing pictures of executions
13.1 Graph modes
13.2 Showing forbidden executions
14 Model definitions
14.1 Identifiers
14.2 Expressions
14.3 Instructions
14.4 Models
15 Usage of
herd
15.1 Arguments
15.2 Options
15.3 Configuration files
15.4 File searching
16 Extensions to Herd
16.1 Additional command line options
16.2 Curried function application
16.3 Expressions over sets
16.4 Provided conditions and undefined-unless conditions
16.5 Additional identifiers
Part IV Some examples
17 Running several tests at once, changing critical parameters
18 Cross compiling, affinity experiment
19 Cross running, testing low-end devices
20 Finding and showing invalid executions
20.1 Running tests on hardware
20.1.1 Trimslice computer (a machine that runs linux)
20.1.2 APQ8060 (a development board that runs Android)
20.1.3 Other machines
Part V Automating the testing process
21 Preamble
22 A tour of
dont
22.1 Checking conformance
22.2 Checking non-conformance
22.3 Automatically exploring the memory model exhibited by a machine
23 Usage of
dont
23.1 Command-line options
23.2 Configuration files