-
- IntegerSet prevSet, concurSet;
- ForEach(m, PREV) {
- prevSet->insert(LOCAL(m, x));
- }
- ForEach (m, Subset(CONCURRENT, "STORE")) {
- concurSet->insert(Value(m, STORE, val));
- }
- return prevSet->contains(RET) || concurSet->contains(RET);
-@SideEffect:
- LOCAL.x = RET;
+
+ Subset(Prev, readSet1, LOCAL(x) == RET);
+ if (Size(readSet1) > 0) return true;
+ Subset(Concurrent, readSet2, NAME == "Store" && VALUE(Store, val) == RET);
+ return Size(readSet2) > 0;
+@SideEffect: LOCAL(x) = RET;