memory-model/Documentation/litmus-tests.txt

202 indicates that the bad result flagged by the "exists" clause never
207 "exists" clause indicates a bad result.  To see this, invert the "exists"
208 clause's condition and run the test.)  The numbers ("0 3") at the end
210 clause (0) and the number not not satisfying that clause (3).
222 "Never" on line 10, the state flagged by the "exists" clause is not
232 "No" says that the "exists" clause was not satisfied by any execution,
235 of end states satisfying and not satisfying the "exists" clause, just
237 clause so that you don't have to look it up in the litmus-test file.
280 means that the "exists" clause on line 23 must change "1:r1=0" to
346 hope that the "exists" clause cannot be satisfied.  LKMM agrees:
380 in the "exists" clause.  But sometimes debugging efforts are greatly
434 "exists" clause.  Someone modifying this test might wish to know the
485 variable, then add that local variable to the "locations" clause.
506 lock using a herd7 "filter" clause.  Note that for exclusive locking, you
560 the "filter" clause on line 28, which tells herd7 to keep only those
565 ignored.  Note well that the "filter" clause keeps those executions
567 evaluates to true.  In other words, the "filter" clause says what to
589 possible "exists"-clause outcomes of program execution in the absence
597 Why not just add the "filter" clause to the "exists" clause, thus
598 avoiding the "filter" clause entirely?  This does work, but is slower.
599 The reason that the "filter" clause is faster is that (in the common case)
601 fails to be satisfied.  In contrast, the "exists" clause is evaluated
612 due to an early mismatch of the "filter" clause?
617 the "filter" clause.  Line 24 does a known-true "if" condition to avoid
618 and static analysis that herd7 might do.  Finally the "exists" clause
655 If the "filter" clause were to check each variable at each point in the
672 so the "filter" clause is evaluated only on the last assignment to
673 the variables that it checks.  In this case, the "filter" clause is a
720 The "exists" clause works the same way, with the "1:r0=x" comparing P1()'s
722 "exists" clause therefore tests whether line 20's load from "y" saw the
755 scenario is flagged by the "exists" clause, and would occur if P1()
875 The "filter" clause on line 35 handles this possibility, rejecting
901 clause can be satisfied.  With this option, herd7 evaluates the above
923 by adding a "filter" clause with exactly the same expression as your
924 "exists" clause.