From 911fd6cd65c43d3338eb6a6b3928423d69b874ed Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Thu, 28 Jan 2016 17:14:09 -0800 Subject: [PATCH 1/1] edits --- notes/definition.cc | 193 ++++++++++++++++++++++++++------------- notes/nondeterm-spec.txt | 71 ++++++-------- 2 files changed, 161 insertions(+), 103 deletions(-) diff --git a/notes/definition.cc b/notes/definition.cc index 46fdc84..457b609 100644 --- a/notes/definition.cc +++ b/notes/definition.cc @@ -1,10 +1,13 @@ #include #include +#include #include #include #include #include +#include + using namespace std; typedef struct MethodCall { @@ -13,17 +16,21 @@ typedef struct MethodCall { // value and the arguments void *localState; // The pointer that points to the struct that represents // the (local) state - vector *prev; // Method calls that are hb right before me - vector *next; // Method calls that are hb right after me - vector *concurrent; // Method calls that are concurrent with me + set *prev; // Method calls that are hb right before me + set *next; // Method calls that are hb right after me + set *concurrent; // Method calls that are concurrent with me } MethodCall; typedef MethodCall *Method; -typedef vector *MethodSet; +typedef set *MethodSet; + +typedef vector IntVector; +typedef list IntList; +typedef set IntSet; -typedef vector IntList; +/********** More general specification-related types and operations **********/ -#define NewSet new vector +#define NewSet new set #define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */ #define CAT_HELPER(a, b) a ## b @@ -33,59 +40,87 @@ typedef vector IntList; The set here is a vector* type, or the MethodSet type. And the item would become the MethodCall* type, or the Method type */ -#define ForEach(item, set) \ +#define ForEach1(item, set) \ int X(i) = 0; \ for (Method item = (set)->size() > 0 ? (*(set))[0] : NULL; \ X(i) < (set)->size(); X(i)++, item = X(i) < (set)->size() ? (*(set))[X(i)] : NULL) -inline MethodSet Subset(MethodSet set, string name) { - MethodSet _subset = NewSet; - ForEach (_m, set) { - if (_m->interfaceName == name) - _subset->push_back(_m); - } - return _subset; -} +#define ForEach(item, container) \ + auto X(_container) = (container); \ + auto X(iter) = X(_container)->begin(); \ + for (auto item = *X(iter); X(iter) != X(_container)->end(); item = ((++X(iter)) != \ + X(_container)->end()) ? *X(iter) : 0) + +/** + The subset operation is only for the MethodCall set +*/ + +#define _M ME + +#define NAME Name(_M) + +#define LOCAL(field) Local(_M, field) + +#define VALUE(type, field) Value(_M, type, field) -#define Size(set) (set->size()) +#define Subset(s, subset, condition) \ + MethodSet original = s; \ + MethodSet subset = NewSet; \ + ForEach (_M, original) { \ + if ((condition)) \ + subset->insert(_M); \ + } \ -#define Belong(set, method) (std::find(set->begin(), set->end(), method) \ - != set->end()) +/** General for set, list & vector */ +#define Size(container) ((container)->size()) -inline MethodSet Intersect(MethodSet set1, MethodSet set2) { - MethodSet res = NewSet; - ForEach (m, set1) { - if (Belong(set2, m)) - res->push_back(m); +#define _BelongHelper(type) \ + template \ + inline bool Belong(type *container, T item) { \ + return std::find(container->begin(), \ + container->end(), item) != container->end(); \ + } + +_BelongHelper(set) +_BelongHelper(vector) +_BelongHelper(list) + +/** General set operations */ +template +inline set* Intersect(set *set1, set *set2) { + set *res = new set; + ForEach (item, set1) { + if (Belong(set2, item)) + res->insert(item); } return res; } -inline MethodSet Union(MethodSet set1, MethodSet set2) { - MethodSet res = NewSet(*set1); - ForEach (m, set2) { - if (!Belong(set1, m)) - res->push_back(m); - } +template +inline set* Union(set *s1, set *s2) { + set *res = new set(*s1); + ForEach (item, s2) + res->insert(item); return res; } -inline MethodSet Subtract(MethodSet set1, MethodSet set2) { - MethodSet res = NewSet; - ForEach (m, set1) { - if (!Belong(set2, m)) - res->push_back(m); +template +inline set* Subtract(set *set1, set *set2) { + set *res = new set; + ForEach (item, set1) { + if (!Belong(set2, item)) + res->insert(item); } return res; } -inline bool Insert(MethodSet set, Method m) { - if (Belong(set, m)) - return false; - else { - set->push_back(m); - return true; - } +template +inline void Insert(set *s, T item) { s->insert(item); } + +template +inline void Insert(set *s, set *others) { + ForEach (item, others) + s->insert(item); } inline MethodSet MakeSet(int count, ...) { @@ -95,21 +130,20 @@ inline MethodSet MakeSet(int count, ...) { va_start (ap, count); res = NewSet; for (int i = 0; i < count; i++) { - Method m = va_arg (ap, Method); - if (!Belong(res, m)) - res->push_back(m); + Method item = va_arg (ap, Method); + res->insert(item); } va_end (ap); return res; } +/********** Method call related operations **********/ +#define Name(method) method->interfaceName #define Local(method, field) ((StateStruct*) method->localState)->field #define Value(method, type, field) ((type*) method->value)->field -#define Label(method) method->interfaceName - #define Prev(method) method->prev #define PREV ME->prev @@ -122,7 +156,7 @@ inline MethodSet MakeSet(int count, ...) { // This auto-generated struct can have different fields according to the read // state declaration. Here it's just a test example typedef struct StateStruct { - IntList *list; + int x; } StateStruct; // These auto-generated struct can have different fields according to the return @@ -139,19 +173,56 @@ typedef struct Load { } Load; int main() { - Method ME = NULL; - MethodSet set = NewSet; - ForEach (m, Subset(set, "Store")) { - IntList *l = Local(m, list); - int ret = Value(m, Load, RET); - string name = Label(m); - } - ForEach (m, Prev(ME)) { - - } - - int size = Size(PREV); - bool flag = Belong(CONCURRENT, ME); - flag = Belong(MakeSet(3, ME, ME, ME), ME); + set *is1 = new set; + set *is2 = new set; + + list *il1 = new list; + list *il2 = new list; + + il1->push_back(2); + il1->push_back(3); + + is1->insert(1); + is1->insert(3); + + is2->insert(4); + is2->insert(5); + + + MethodSet ms = NewSet; + Method m = new MethodCall; + m->interfaceName = "Store"; + StateStruct *ss = new StateStruct; + ss->x = 1; + m->localState = ss; + Store *st = new Store; + st->val = 2; + m->value = st; + ms->insert(m); + + m = new MethodCall; + m->interfaceName= "Store"; + ss = new StateStruct; + ss->x = 2; + m->localState = ss; + st = new Store; + st->val = 0; + m->value = st; + ms->insert(m); + + m = new MethodCall; + m->interfaceName= "Load"; + ss = new StateStruct; + ss->x = 0; + m->localState = ss; + Load *ld = new Load; + ld->RET = 2; + m->value = ld; + ms->insert(m); + + //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0); + Subset(ms, sub, NAME == "Store" && VALUE(Store, val) >= 0 && LOCAL(x) == 0); + + cout << "Size=" << Size(sub) << endl; return 0; } diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt index f86c661..e6dfb05 100644 --- a/notes/nondeterm-spec.txt +++ b/notes/nondeterm-spec.txt @@ -156,19 +156,14 @@ b. The RA (release/acquire) C/C++ atomics @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) @@ -189,14 +184,7 @@ Our model cannot prevent such a case from happening. However, we can still have 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 @@ -297,7 +285,7 @@ inline MethodSet Subtract(MethodSet set1, MethodSet set2) { // 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) @@ -309,21 +297,26 @@ inline MethodSet Subtract(MethodSet set1, MethodSet set2) { // 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; - - 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; int load(int *loc); d. The C/C++ normal memory accesses @@ -350,9 +343,8 @@ on the admissible executions // 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 @@ -363,25 +355,20 @@ void enq(queue_t *q, int val); // 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; - ForEach (m, Subset(CONCURRENT, "Deq")) { - if (Value(m, Deq, RET) && *Value(m, Deq, 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); -- 2.34.1