Fix default configuration for litmus tests #720
Conversation
|
Please add some title to the merge request. Now it is just "717". |
| properties); | ||
| throw new IllegalArgumentException(error); | ||
| logger.warn(warn); | ||
| properties = EnumSet.of(Property.PROGRAM_SPEC); |
There was a problem hiding this comment.
I think it is fine as a quick fix, but in the long term we probably want to have a more consistent solution. For example, does it make sense to verify data races for litmus tests at all? There will be many races for tests like MP.
There was a problem hiding this comment.
Why should litmus tests have many races? Hardware models lack a notion of race. Language models like (R)C11 need to use proper atomics for MP which also ensure that no data races occur.
Is this different for GPUs?
There was a problem hiding this comment.
Language models like (R)C11 need to use proper atomics for MP which also ensure that no data races occur.
This is not true, even for (R)C11. In the usual MP litmus tests (i.e. without having a spinloop), marking the accesses to flag as release-acquire, but keeping the accesses to data as plain, is enough to prevent the reordering related to the exists. However, you will have races in any execution where the acquire-load does not read from the release-store.
We probably want to have a more consistent solution.
Checking races in litmus tests is useful to understand the definition of data race specific to the model. If the user does not want this, they can simply choose a different/single property.
There was a problem hiding this comment.
Language models like (R)C11 need to use proper atomics for MP which also ensure that no data races occur.
This is not true, even for (R)C11. In the usual MP litmus tests (i.e. without having a spinloop), marking the accesses to
flagas release-acquire, but keeping the accesses todataas plain, is enough to prevent the reordering related to theexists. However, you will have races in any execution where the acquire-load does not read from the release-store.
Fair enough. Executions that fail the exists clause may indeed be racy.
Co-authored-by: Hernan Ponce de Leon <[email protected]>
No description provided.