diff options
Diffstat (limited to 'tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus')
| -rw-r--r-- | tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus index 235195e87d4e6..025b0462ec9bc 100644 --- a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus +++ b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus @@ -1,5 +1,16 @@ C ISA2+pooncerelease+poacquirerelease+poacquireonce +(* + * Result: Never + * + * This litmus test demonstrates that a release-acquire chain suffices + * to order P0()'s initial write against P2()'s final read. The reason + * that the release-acquire chain suffices is because in all but one + * case (P2() to P0()), each process reads from the preceding process's + * write. In memory-model-speak, there is only one non-reads-from + * (AKA non-rf) link, so release-acquire is all that is needed. + *) + {} P0(int *x, int *y) |