The last series exercises the following result, which we also establish as a theorem about the model: when all accesses of a test are implemented with FNO or STA, then the test only has SC behaviours. We tested this on a restricted subset of our plain tests, namely the 68 that exhibit a violation of SC via a critical cycle, and that have up to 4 threads. Running those tests on hardware showed no non-SC behaviour, consistent with the model’s prediction as captured by the theorem.
In the following table, kinds are Allow for plain tests and Forbid for the tests with FNO and STA, not model output.
Kind | Model | PowerG5 | Power6 | Power7 | |
2+2W | Allow | = | Ok, 2.1M/6.3G | Ok, 251M/33G | Ok, 29G/894G |
2+2W+poaas | Forbid | = | Ok, 0/472M | Ok, 0/4.3G | Ok, 0/6.9G |
MP | Allow | = | Ok, 10M/4.9G | Ok, 6.5M/29G | Ok, 1.7G/167G |
MP+poaas | Forbid | = | Ok, 0/484M | Ok, 0/4.4G | Ok, 0/7.5G |
SB | Allow | = | Ok, 102M/4.9G | Ok, 1.9G/26G | Ok, 11G/167G |
SB+poaas | Forbid | = | Ok, 0/476M | Ok, 0/4.4G | Ok, 0/6.9G |
LB | Allow | = | No, 0/7.4G | No, 0/37G | No, 0/258G |
Allow unseen | Allow unseen | Allow unseen | |||
LB+poaas | Forbid | = | Ok, 0/476M | Ok, 0/3.3G | Ok, 0/6.9G |
R | Allow | = | Ok, 45M/1.9G | Ok, 263M/7.3G | Ok, 47M/4.5G |
R+poaas | Forbid | = | Ok, 0/476M | Ok, 0/4.3G | Ok, 0/6.9G |
S | Allow | = | Ok, 250/2.3G | Ok, 129k/8.3G | Ok, 1.7M/14G |
S+poaas | Forbid | = | Ok, 0/476M | Ok, 0/4.4G | Ok, 0/6.9G |
WRC | Allow | = | Ok, 44k/2.7G | Ok, 1.2M/13G | Ok, 25M/104G |
WRC+poaas+A | Forbid | — | Ok, 0/236M | Ok, 0/2.8G | Ok, 0/4.4G |
RWC | Allow | = | Ok, 883k/1.2G | Ok, 7.4M/4.2G | Ok, 118M/24G |
RWC+poaas+A | Forbid | — | Ok, 0/236M | Ok, 0/2.8G | Ok, 0/4.4G |
WWC | Allow | = | No, 0/1.5G | Ok, 70k/9.0G | Ok, 53k/50G |
Allow unseen | |||||
WWC+poaas+A | Forbid | — | Ok, 0/235M | Ok, 0/2.8G | Ok, 0/4.4G |
WRW+2W | Allow | = | Ok, 4/2.1G | Ok, 540k/5.6G | Ok, 7.1M/33G |
WRW+2W+poaas+A | Forbid | — | Ok, 0/235M | Ok, 0/2.8G | Ok, 0/4.4G |
WRR+2W | Allow | = | Ok, 432k/1.0G | Ok, 2.4M/4.1G | Ok, 42M/16G |
WRR+2W+poaas+A | Forbid | — | Ok, 0/235M | Ok, 0/2.8G | Ok, 0/4.4G |
WRW+WR | Allow | = | Ok, 132k/1.1G | Ok, 3.1M/4.1G | Ok, 15M/16G |
WRW+WR+poaas+A | Forbid | — | Ok, 0/235M | Ok, 0/2.8G | Ok, 0/4.4G |
3.2W | Allow | — | Ok, 1.0k/661M | Ok, 9.3M/1.7G | Ok, 29M/4.0G |
3.2W+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.6G | Ok, 0/4.1G |
3.SB | Allow | = | Ok, 1.4M/622M | Ok, 91M/1.7G | Ok, 73M/4.0G |
3.SB+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.6G | Ok, 0/4.1G |
3.LB | Allow | = | No, 0/888M | No, 0/3.6G | No, 0/9.2G |
Allow unseen | Allow unseen | Allow unseen | |||
3.LB+poaas | Forbid | — | Ok, 0/230M | Ok, 0/1.9G | Ok, 0/4.1G |
ISA2 | Allow | = | Ok, 3/91M | Ok, 72/26M | Ok, 1.0k/3.8M |
ISA2+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.6G | Ok, 0/4.1G |
W+RWC | Allow | = | Ok, 457k/623M | Ok, 20M/1.7G | Ok, 40M/4.0G |
W+RWC+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.6G | Ok, 0/4.1G |
Z6.0 | Allow | = | Ok, 175k/704M | Ok, 6.3M/1.7G | Ok, 13M/4.0G |
Z6.0+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.6G | Ok, 0/4.1G |
Z6.1 | Allow | — | Ok, 27/758M | Ok, 2.1M/1.7G | Ok, 6.9M/4.0G |
Z6.1+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.6G | Ok, 0/4.1G |
Z6.2 | Allow | = | No, 0/888M | Ok, 43k/1.8G | Ok, 1.2M/4.2G |
Allow unseen | |||||
Z6.2+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.6G | Ok, 0/4.1G |
Z6.3 | Allow | = | Ok, 71k/651M | Ok, 5.0M/1.7G | Ok, 26M/4.0G |
Z6.3+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.6G | Ok, 0/4.1G |
Z6.4 | Allow | = | Ok, 1.1M/622M | Ok, 53M/1.7G | Ok, 66M/4.0G |
Z6.4+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.6G | Ok, 0/4.1G |
Z6.5 | Allow | — | Ok, 383k/622M | Ok, 25M/1.7G | Ok, 41M/4.0G |
Z6.5+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.6G | Ok, 0/4.1G |
IRIW | Allow | = | Ok, 220k/2.6G | Ok, 1.3M/13G | Ok, 16M/83G |
IRIW+poaas+AA | Forbid | — | Ok, 0/230M | Ok, 0/2.2G | Ok, 0/3.4G |
IRRWIW | Allow | = | Ok, 18k/739M | Ok, 22k/1.7G | Ok, 57k/3.3G |
IRRWIW+poaas+AA | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
IRWIW | Allow | — | No, 0/888M | Ok, 1.0k/1.8G | Ok, 3.8k/3.5G |
Allow unseen | |||||
IRWIW+poaas+AA | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RR+WR+WR | Allow | — | Ok, 112k/91M | Ok, 4.7k/790k | Ok, 4.7k/435k |
W+RR+WR+WR+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RR+WR+WW | Allow | — | Ok, 30k/91M | Ok, 2.4k/900k | Ok, 606/435k |
W+RR+WR+WW+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RR+WW+RR | Allow | — | Ok, 75/91M | Ok, 222/1.0M | Ok, 140/1.3M |
W+RR+WW+RR+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RR+WW+RW | Allow | — | Ok, 12k/91M | Ok, 165/965k | Ok, 50/2.0M |
W+RR+WW+RW+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RR+WW+WR | Allow | — | Ok, 47k/91M | Ok, 1.8k/995k | Ok, 1.0k/440k |
W+RR+WW+WR+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RR+WW+WW | Allow | — | Ok, 32/91M | Ok, 103/3.2M | Ok, 42/1.5M |
W+RR+WW+WW+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RW+RR+WR | Allow | — | Ok, 4.0k/91M | Ok, 156/925k | Ok, 184/550k |
W+RW+RR+WR+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RW+RR+WW | Allow | — | Ok, 471/110M | Ok, 9/39M | Ok, 20/38M |
W+RW+RR+WW+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RW+RW+RR | Allow | — | Ok, 3/132M | Ok, 10/36M | Ok, 8/175M |
W+RW+RW+RR+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RW+RW+RW | Allow | — | No, 0/230M | Ok, 5/184M | Ok, 5/496M |
Allow unseen | |||||
W+RW+RW+RW+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RW+RW+WR | Allow | — | Ok, 171/91M | Ok, 121/1.1M | Ok, 54/705k |
W+RW+RW+WR+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RW+RW+WW | Allow | — | No, 0/230M | Ok, 8/37M | Ok, 11/40M |
Allow unseen | |||||
W+RW+RW+WW+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RW+WR+WR | Allow | — | Ok, 6.9k/91M | Ok, 3.5k/790k | Ok, 2.5k/415k |
W+RW+WR+WR+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RW+WR+WW | Allow | — | Ok, 11k/91M | Ok, 1.7k/950k | Ok, 449/585k |
W+RW+WR+WW+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RW+WW+RR | Allow | — | Ok, 4/91M | Ok, 131/3.2M | Ok, 87/3.1M |
W+RW+WW+RR+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RW+WW+RW | Allow | — | No, 0/230M | Ok, 37/28M | Ok, 19/100M |
Allow unseen | |||||
W+RW+WW+RW+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RW+WW+WR | Allow | — | Ok, 6.1k/91M | Ok, 1.2k/985k | Ok, 545/710k |
W+RW+WW+WR+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
W+RW+WW+WW | Allow | — | No, 0/230M | Ok, 25/10M | Ok, 13/14M |
Allow unseen | |||||
W+RW+WW+WW+poaas+A | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
4.2W | Allow | — | Ok, 6/110M | Ok, 28/3.9M | Ok, 55/975k |
4.2W+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
4.SB | Allow | — | Ok, 48k/91M | Ok, 10k/745k | Ok, 12k/425k |
4.SB+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
4.LB | Allow | — | No, 0/230M | No, 0/1.6G | No, 0/3.2G |
Allow unseen | Allow unseen | Allow unseen | |||
4.LB+poaas | Forbid | — | Ok, 0/230M | Ok, 0/1.6G | Ok, 0/3.2G |
WW+RR+WR+WR | Allow | — | Ok, 25k/91M | Ok, 2.8k/830k | Ok, 2.0k/405k |
WW+RR+WR+WR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+RR+WW+RR | Allow | — | Ok, 24/91M | Ok, 85/1.5M | Ok, 76/1.9M |
WW+RR+WW+RR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+RR+WW+RW | Allow | — | Ok, 176/110M | Ok, 131/8.6M | Ok, 20/2.3M |
WW+RR+WW+RW+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+RR+WW+WR | Allow | — | Ok, 82k/91M | Ok, 911/860k | Ok, 404/495k |
WW+RR+WW+WR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+RW+RR+WR | Allow | — | Ok, 2.0k/91M | Ok, 165/1.1M | Ok, 227/740k |
WW+RW+RR+WR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+RW+RW+RR | Allow | — | Ok, 1/91M | Ok, 10/37M | Ok, 11/162M |
WW+RW+RW+RR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+RW+RW+RW | Allow | — | No, 0/230M | Ok, 11/45M | Ok, 12/185M |
Allow unseen | |||||
WW+RW+RW+RW+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+RW+RW+WR | Allow | — | Ok, 3.8k/91M | Ok, 75/1.0M | Ok, 42/1.0M |
WW+RW+RW+WR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+RW+WR+WR | Allow | — | Ok, 18k/91M | Ok, 1.9k/850k | Ok, 874/455k |
WW+RW+WR+WR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+RW+WW+RW | Allow | — | No, 0/230M | Ok, 135/22M | Ok, 9/163M |
Allow unseen | |||||
WW+RW+WW+RW+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+RW+WW+WR | Allow | — | Ok, 4.0k/91M | Ok, 810/1.0M | Ok, 126/575k |
WW+RW+WW+WR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+WR+WR+WR | Allow | — | Ok, 113k/91M | Ok, 4.8k/810k | Ok, 5.4k/415k |
WW+WR+WR+WR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+WR+WW+WR | Allow | — | Ok, 33k/91M | Ok, 3.6k/870k | Ok, 2.1k/480k |
WW+WR+WW+WR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+WW+RR+WR | Allow | — | Ok, 41k/91M | Ok, 1.2k/915k | Ok, 321/485k |
WW+WW+RR+WR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+WW+RW+RR | Allow | — | Ok, 2.7k/91M | Ok, 11/29M | Ok, 21/7.9M |
WW+WW+RW+RR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+WW+RW+RW | Allow | — | No, 0/230M | Ok, 8/27M | Ok, 9/161M |
Allow unseen | |||||
WW+WW+RW+RW+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+WW+RW+WR | Allow | — | Ok, 3.9k/91M | Ok, 816/855k | Ok, 74/570k |
WW+WW+RW+WR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+WW+WR+WR | Allow | — | Ok, 18k/91M | Ok, 2.3k/895k | Ok, 1.4k/470k |
WW+WW+WR+WR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+WW+WW+RR | Allow | — | Ok, 7/91M | Ok, 36/1.4M | Ok, 41/4.6M |
WW+WW+WW+RR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+WW+WW+RW | Allow | — | Ok, 1/110M | Ok, 49/7.5M | Ok, 18/18M |
WW+WW+WW+RW+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |
WW+WW+WW+WR | Allow | — | Ok, 46k/91M | Ok, 745/880k | Ok, 901/520k |
WW+WW+WW+WR+poaas | Forbid | — | Ok, 0/230M | Ok, 0/2.1G | Ok, 0/3.2G |