@InitVar: x = 0;
@Interface: Store
-@SideEffect:
- LOCAL.x = val;
+@SideEffect: LOCAL(x) = val;
void store(int *loc, int val);
@Interface: Load
@PreCondition:
- IntegerSet *prevSet = new IntegerSet;
- for (m in PREV) {
- prevSet->add(m.LOCAL.x);
- }
- return prevSet->contains(RET);
-@SideEffect:
- LOCAL.x = RET;
+ Subset(PREV, subset, LOCAL(x) == RET);
+ return Size(subset) > 0;
+@SideEffect: LOCAL(x) = RET;
int load(int *loc);
c. The C/C++ atomics (a slightly loose specification)
a slightly loose specification which basically states that a load can read from
any store that either immediately happens before it or concurrently executes.
----------- Specification ----------
-@DeclareVar: int x;
-@InitVar: x = 0;
-@Interface: Store
-@SideEffect:
- LOCAL.x = val;
-void store(int *loc, int val);
// We define a struct called MethodCall to represent the data we would collect
// and communicate between the real execution and the checking process
}
return _subset;
}
+
+// 1.2 Size(set) --> to get the size of a method set
+#define Size(set) set->size()
+
+// 1.3 Belong(set, method) --> whether method belongs to set
+#define Belong(set, method) std::find(set->begin(), set->end(), method) != set->end()
+
+// 1.4 Intersect(set1, set2) --> the intersection of two method sets
+inline MethodSet Intersect(MethodSet set1, MethodSet set2) {
+ MethodSet res = NewSet;
+ ForEach (m, set1) {
+ if (Belong(set2, m))
+ res->push_back(m);
+ }
+ return res;
+}
+
+// 1.5 Union(set1, set2) --> the union of two method sets
+inline MethodSet Union(MethodSet set1, MethodSet set2) {
+ MethodSet res = NewSet(set1);
+ ForEach (m, set2) {
+ if (!Belong(set1, m))
+ res->push_back(m);
+ }
+ return res;
+}
+
+// 1.6 Insert(set, method) --> add a method to the set
+inline bool Insert(MethodSet set, Method m) {
+ if (Belong(set, m))
+ return false;
+ else {
+ set->push_back(m);
+ return true;
+ }
+}
+
+// 1.7 Subtract(set1, set2) --> subtract set2 from set1
+inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
+ MethodSet res = NewSet;
+ ForEach (m, set1) {
+ if (!Belong(set2, m))
+ res->push_back(m);
+ }
+ return res;
+}
+
+// 1.8 MakeSet(count, ...) --> Make a set from the arguments
+
// 2. Local(method, field)
#define Local(method, field) ((StateStruct*) method->localState)->field
// 3. Value(method, type, field)
#define Value(method, type, field) ((type*) method->value)->field
-// 4. Lable(mehtod)
+// 4. Name(mehtod)
#defien Lable(method) method->interfaceName
// 5. Prev(method)
// 7. Concurrent(method)
#define Concurrent(method) mehtod->concurrent
+
+---------- Specification ----------
+@DeclareVar: int x;
+@InitVar: x = 0;
+
+@Interface: Store
+@SideEffect: LOCAL(x) = val;
+void store(int *loc, int val);
+
+
@Interface: Load
@PreCondition:
// Auto generated code
// MethodCall *ME = ((SomeTypeConversion) info)->method;
- // vector<MethodCall*> PREV = Me->prev;
- // vector<MethodCall*> NEXT = Me->next;
- // vector<MethodCall*> CONCURRENT = Me->concurrent;
-
- IntegerSet prevSet, concurSet;
- ForEach(m, PREV) {
- prevSet.add(LOCAL(m, x));
- }
- ForEach (m, CONCURRENT("STORE")) {
- concurSet->add(m.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;
int load(int *loc);
d. The C/C++ normal memory accesses
// The dequeuer doesn't dequeue from that enqueuer
@Commutativity: Enq <-> Deq (!_M2.RET || (_M2.RET && Enq.val != *Deq.res))
-@Interface: Enq
-@SideEffect:
- LOCAL.x = val;
+@Interface: Enq
+@SideEffect: q->push_back(val);
void enq(queue_t *q, int val);
@Interface: Deq
// dequeue them
if (!RET) {
// Local state is empty
- if (Local.q->size() == 0)
- return true;
+ if (Local(q)->size() == 0) return true;
// Otherwise check there must be other concurrent dequeuers
- for (int i = 0; i < Local.q->size(); i++) {
- int item = (*Local.q)[i];
+ ForEach (item, Local(q)) {
// Check there's some concurrent dequeuer for this item
- bool flag = false;
- for (m in CONCURRENT("Deq")) {
- if (m.RET) {
- if (*m.res == item) flag = true;
- }
- }
- if (!flag) return false;
+ Subset(CONCURRENT, concurSet, NAME == "Deq" && VALUE(Deq, RET) &&
+ *VALUE(Deq, res) == item);
+ if (Size(concurSet) == 0) return false;
}
return true;
} else { // Check the global queue state
return q->back() == *res;
}
@SideEffect:
- if (RET)
- Global.q->back()
+ if (RET) q->pop_back();
bool deq(queue_t *q, int *res);