From b0d8b3898499e22a6fc094b2824fb451cb4bd4bc Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Fri, 29 Jan 2016 14:59:33 -0800 Subject: [PATCH] edits --- notes/definition.cc | 121 ++++++++++++++++++++++++++++++++++++--- notes/nondeterm-spec.txt | 37 +++++------- 2 files changed, 127 insertions(+), 31 deletions(-) diff --git a/notes/definition.cc b/notes/definition.cc index 457b609..054ff89 100644 --- a/notes/definition.cc +++ b/notes/definition.cc @@ -6,6 +6,8 @@ #include #include +#include + #include using namespace std; @@ -55,6 +57,19 @@ typedef set IntSet; The subset operation is only for the MethodCall set */ +/** + This is a common macro that is used as a constant for the name of specific + variables. We basically have two usage scenario: + 1. In Subset operation, we allow users to specify a condition to extract a + subset. In that condition expression, we provide NAME, RET(type), ARG(type, + field) and LOCAL(field) to access each item's (method call) information. + 2. In general specification (in pre- & post- conditions and side effects), + we would automatically generate an assignment that assign the current + MethodCall* pointer to a variable namedd _M. With this, when we access the + local state of the current method, we use LOCAL(field) (this is a reference + for read/write). +*/ +#define ITEM _M #define _M ME #define NAME Name(_M) @@ -62,7 +77,10 @@ typedef set IntSet; #define LOCAL(field) Local(_M, field) #define VALUE(type, field) Value(_M, type, field) +#define RET(type) VALUE(type, RET) +#define ARG(type, arg) VALUE(type, arg) +/* #define Subset(s, subset, condition) \ MethodSet original = s; \ MethodSet subset = NewSet; \ @@ -70,6 +88,81 @@ typedef set IntSet; if ((condition)) \ subset->insert(_M); \ } \ +*/ + + +/** + This operation is specifically for Method set. For example, when we want to + construct an integer set from the local state field "x" (which is an + integer) of the previous set of method calls (PREV), and the new set goes to + "readSet", we would call "MakeSet(int, PREV, readSet, LOCAL(x));". Then users + can use the "readSet" as an integer set (set) +*/ +#define MakeSet(type, oldset, newset, field) \ + auto newset = new set; \ + ForEach (_M, oldset) \ + newset->insert(field); \ + +/** + We provide a more general subset operation that takes a plain boolean + expression on each item (access by the name "ITEM") of the set, and put it + into a new set if the boolean expression (Guard) on that item holds. This is + used as the second arguments of the Subset operation. An example to extract + a subset of positive elements on an IntSet "s" would be "Subset(s, + GeneralGuard(int, ITEM > 0))" +*/ +#define GeneralGuard(type, expression) std::function ( \ + [](type ITEM) -> bool { return (expression);}) \ + +/** + This is a more specific guard designed for the Method (MethodCall*). It + basically wrap around the GeneralGuard with the type Method. An example to + extract the subset of method calls in the PREV set whose local state "x" is + equal to "val" would be "Subset(PREV, Guard(Local(x) == val))" +*/ +#define Guard(expression) GeneralGuard(Method, expression) + +/** + A general subset operation that takes a condition and returns all the item + for which the boolean guard holds. +*/ +template +inline set* Subset(set *original, std::function condition) { + set *res = new set; + ForEach (_M, original) { + if (condition(_M)) + res->insert(_M); + } + return res; +} + +/** + A general sublist operation that takes a condition and returns all the item + for which the boolean guard holds in the same order as in the old list. +*/ +template +inline list* Sublist(list *original, std::function condition) { + list *res = new list; + ForEach (_M, original) { + if (condition(_M)) + res->push_back(_M); + } + return res; +} + +/** + A general subvector operation that takes a condition and returns all the item + for which the boolean guard holds in the same order as in the old vector. +*/ +template +inline vector* Subvector(vector *original, std::function condition) { + vector *res = new vector; + ForEach (_M, original) { + if (condition(_M)) + res->push_back(_M); + } + return res; +} /** General for set, list & vector */ #define Size(container) ((container)->size()) @@ -123,6 +216,7 @@ inline void Insert(set *s, set *others) { s->insert(item); } +/* inline MethodSet MakeSet(int count, ...) { va_list ap; MethodSet res; @@ -136,6 +230,7 @@ inline MethodSet MakeSet(int count, ...) { va_end (ap); return res; } +*/ /********** Method call related operations **********/ #define Name(method) method->interfaceName @@ -143,15 +238,17 @@ inline MethodSet MakeSet(int count, ...) { #define Local(method, field) ((StateStruct*) method->localState)->field #define Value(method, type, field) ((type*) method->value)->field +#define Ret(method, type) Value(method, type, RET) +#define Arg(method, type, arg) Value(method, type, arg) #define Prev(method) method->prev -#define PREV ME->prev +#define PREV _M->prev #define Next(method) method->next -#define NEXT ME->next +#define NEXT _M->next #define Concurrent(method) method->concurrent -#define CONCURRENT ME->concurrent +#define CONCURRENT _M->concurrent // This auto-generated struct can have different fields according to the read // state declaration. Here it's just a test example @@ -172,6 +269,10 @@ typedef struct Load { int *loc; } Load; +bool f1(Method m) { + return true; +} + int main() { set *is1 = new set; set *is2 = new set; @@ -219,10 +320,16 @@ int main() { 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; + MakeSet(int, ms, newis, LOCAL(x)); + cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl; + ForEach (i, newis) { + cout << "elem: " << i << endl; + } + + + //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0); + //cout << "Size=" << Size(Subset(ms, Guard(NAME == "Store" && ARG(Store, val) + //>= 0 && LOCAL(x) >= 0 ))) << endl; return 0; } diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt index e6dfb05..8dca63c 100644 --- a/notes/nondeterm-spec.txt +++ b/notes/nondeterm-spec.txt @@ -161,8 +161,7 @@ void store(int *loc, int val); @Interface: Load @PreCondition: - Subset(PREV, subset, LOCAL(x) == RET); - return Size(subset) > 0; + Size(Subset(PREV, LOCAL(x) == RET)) > 0; @SideEffect: LOCAL(x) = RET; int load(int *loc); @@ -214,21 +213,8 @@ interface label name. ********************************************* - -TODO:We want subset operation by the equality and inequality of the interface -name, a specific (or combined) state and a specific (or combined) of the value -(RET & arguments) - -// 1.1 Subset(set, name) --> to get a subset of method calls by name -inline vector* Subset(vector *set, string name) { - vector _subset = new vector; - for (int i = 0; i < set->size(); i++) { - MethodCall *_m = (*set)[i]; - if (_m->interfaceName == name) - _subset->push_back(_m); - } - return _subset; -} +// 1.1 Subset(set, guard) --> to get a subset of method calls by a boolean +// expression; This takes advantage of C++11 std::function features and C macros. // 1.2 Size(set) --> to get the size of a method set #define Size(set) set->size() @@ -284,6 +270,11 @@ inline MethodSet Subtract(MethodSet set1, MethodSet set2) { // 3. Value(method, type, field) #define Value(method, type, field) ((type*) method->value)->field +3.1 Return +#define Ret(method, type) Value(method, type, RET) +3.2 Arguments +#define Arg(method, type, arg) Value(method, type, arg) + // 4. Name(mehtod) #defien Lable(method) method->interfaceName @@ -312,10 +303,9 @@ void store(int *loc, int val); // Auto generated code // MethodCall *ME = ((SomeTypeConversion) info)->method; - 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; + int count = Size(Subset(Prev, LOCAL(x) == RET)) + + Size(Subset(CONCURRENT, NAME == "Store" && ARG(Store, val) == RET)) + return count > 0; @SideEffect: LOCAL(x) = RET; int load(int *loc); @@ -359,9 +349,8 @@ void enq(queue_t *q, int val); // Otherwise check there must be other concurrent dequeuers ForEach (item, Local(q)) { // Check there's some concurrent dequeuer for this item - Subset(CONCURRENT, concurSet, NAME == "Deq" && VALUE(Deq, RET) && - *VALUE(Deq, res) == item); - if (Size(concurSet) == 0) return false; + if (Size(Subset(CONCURRENT, NAME == "Deq" && RET(Deq) && + *ARG(Deq, res) == item)) == 0) return false; } return true; } else { // Check the global queue state -- 2.34.1