From 007d42509b6f84500bd65ffe710773117cb3d77f Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Fri, 29 Jan 2016 23:28:34 -0800 Subject: [PATCH] edits --- notes/definition.cc | 20 +++- notes/nondeterm-spec.txt | 247 ++++++++++----------------------------- 2 files changed, 77 insertions(+), 190 deletions(-) diff --git a/notes/definition.cc b/notes/definition.cc index 0c5b796..fda4eba 100644 --- a/notes/definition.cc +++ b/notes/definition.cc @@ -127,6 +127,21 @@ inline set* Subset(set *original, std::function condition) { return res; } +/** + A general set operation that takes a condition and returns if there exists + any item for which the boolean guard holds. +*/ +template +inline bool HasItem(set *original, std::function condition) { + ForEach (_M, original) { + if (condition(_M)) + return true; + } + return false; +} + + + /** 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. @@ -313,9 +328,10 @@ int main() { ms->insert(m); MakeSet(int, ms, newis, STATE(x)); - cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl; + //cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl; + cout << "HasItem=" << HasItem(ms, Guard(STATE(x) == 2)) << endl; ForEach (i, newis) { - cout << "elem: " << i << endl; + //cout << "elem: " << i << endl; } diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt index d1011dc..70383b3 100644 --- a/notes/nondeterm-spec.txt +++ b/notes/nondeterm-spec.txt @@ -64,7 +64,7 @@ the initial state. The other way is to define "@EvaluateState" after before it. Usually users calculate the state by using the PREV primitive to access the state of previous method calls. -IV. Examples +IV. Specification Details /// Global specification @State: // Declare the state structure @@ -144,13 +144,39 @@ ForEach(item, container) { ... } // Useful iteration primitive NewMethodSet // Create a new method set (set*) -MakeSet(NewSetType, oldset, newset, field); // +MakeSet(type, oldset, newset, field); // Construct a new set from an + // old set. We extract a specific field of that set item + // and form a new set. Specifically we expect users to + // use this on MethodSet. For example, if we want to + // construct an integer set from the state "x" of + // the previous methods, we use "MakeSet(int, PREV, + // newset, STATE(x))", and the newset contains the new + // set Subset(set, condition) // A generic subset operation that takes a condition and // returns all the item for which the boolean guard // holds. The condition can be specified with GUARD or // GeneralGuard shown as follow. +HasItem(set, condition) // A generic set operation that takes a condition and + // returns if there exists any item in "set" for which + // the condition holds. Its syntax is similar to that of + // Subset() operation + +Size(container) // Return the size of a container type + +Belong(container, item) // Return if item is in the container + +Union(set1, set2) // Union of two sets + +Intesection(set1, set2) // Intersection of two sets + +Subtract(set1, set2) // Returns the new set that represents the result of + // set1-set2 +Insert(set, item) // Insert item to set + +Insert(set, others) // Insert the whole set "others" to "set" + ITEM // Used to refer to the set item in the GeneralGuard shown below GeneralGuard(type, expression) // Used as a condition for any set type. We @@ -177,11 +203,11 @@ To make things easier, we have the following helper macros. 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. + field) and STATE(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 + state of the current method, we use STATE(field) (this is a reference for read/write). */ #define ITEM _M @@ -264,121 +290,6 @@ using our specification checker. ***************************************************************************** -// Some nice C/C++ macro definition to make specifications easier to write - ------------------------------------------------------------------------------ -#define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */ -#define CAT_HELPER(a, b) a ## b -#define X(name) CAT(__##name, __LINE__) /* unique variable */ - - - ------------------------------------------------------------------------------ -1. ForEach --> to iterate a set, list or vector (containers that support using -iterator to iterate) - -#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) - ------------------------------------------------------------------------------ - -/** - 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 - - ------------------------------------------------------------------------------ - -// 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() - -// 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 -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 - -// 5. Prev(method) -#define Prev(method) mehtod->prev - -// 6. Next(method) -#define Next(method) mehtod->next - -// 7. Concurrent(method) -#define Concurrent(method) mehtod->concurrent - - /// Ordering point specification @OPDefine: condition // If the specified condition satisfied, the atomic // operation right before is an ordering point @@ -403,11 +314,12 @@ inline MethodSet Subtract(MethodSet set1, MethodSet set2) { // statement +V. Examples 1. The register examples: Basically, we can think of registers as the cache on a memory system. The effect of a load or store basically tells us what the current value in the cache line is, and a load can read from values that can be potentially in the cache --- either one of the concurrent store update the cache -or it inherites one of the the previous local state in the execution graph. +or it inherites one of the the previous state in the execution graph. ---------- Interfae ---------- void init(atomic_int &loc, int initial); @@ -421,17 +333,21 @@ b. The RA (release/acquire) C/C++ atomics // For RA atomics, a load must read its value from a store that happens before // it. ---------- Specification ---------- -@DeclareVar: int x; -@InitVar: x = 0; +@State: int x; +@Initial: x = 0; +@Commutativity: Store <-> Store(true) +@Commutativity: Load <-> Load(true) +@Commutativity: Store <-> Load(true) +/** No @Transition */ @Interface: Store -@SideEffect: LOCAL(x) = val; +@SideEffect: STATE(x) = val; void store(int *loc, int val); @Interface: Load @PreCondition: - Size(Subset(PREV, LOCAL(x) == RET)) > 0; -@SideEffect: LOCAL(x) = RET; + return HasItem(PREV, STATE(x) == RET); +@SideEffect: STATE(x) = RET; int load(int *loc); c. The C/C++ atomics (a slightly loose specification) @@ -454,11 +370,11 @@ any store that either immediately happens before it or concurrently executes. ---------- Specification ---------- -@DeclareVar: int x; -@InitVar: x = 0; +@State: int x; +@Initial: x = 0; @Interface: Store -@SideEffect: LOCAL(x) = val; +@SideEffect: STATE(x) = val; void store(int *loc, int val); @@ -466,11 +382,10 @@ void store(int *loc, int val); @PreCondition: // Auto generated code // MethodCall *ME = ((SomeTypeConversion) info)->method; - - int count = Size(Subset(Prev, LOCAL(x) == RET)) - + Size(Subset(CONCURRENT, NAME == "Store" && ARG(Store, val) == RET)) - return count > 0; -@SideEffect: LOCAL(x) = RET; + + return HasItem(Prev, STATE(x) == RET) || + + HasItem(CONCURRENT, NAME == "Store" && ARG(Store, val) == RET) +@SideEffect: STATE(x) = RET; int load(int *loc); d. The C/C++ normal memory accesses @@ -494,38 +409,36 @@ on the admissible executions @Copy: New.q = new vector(Old.q); // Fails to dequeue @Commutativity: Deq <-> Deq (!_M1.RET || !_M2.RET) -// The dequeuer doesn't dequeue from that enqueuer -@Commutativity: Enq <-> Deq (!_M2.RET || (_M2.RET && Enq.val != *Deq.res)) +@Commutativity: Enq <-> Deq (true) @Interface: Enq -@SideEffect: q->push_back(val); +@Transition: q->push_back(val); void enq(queue_t *q, int val); @Interface: Deq +@Transition: if (RET) q->pop_back(); @PreCondition: // Check whether the queue is really empty - // Either the local state is an empty queue, or for all those remaining - // elements in the local queue, there should be some concurrent dequeuers to + // Either the state is an empty queue, or for all those remaining + // elements in the queue, there should be some concurrent dequeuers to // dequeue them if (!RET) { - // Local state is empty - if (Local(q)->size() == 0) return true; + // State is empty + if (STATE(q)->size() == 0) return true; // Otherwise check there must be other concurrent dequeuers - ForEach (item, Local(q)) { + ForEach (item, State(q)) { // Check there's some concurrent dequeuer for this item - if (Size(Subset(CONCURRENT, NAME == "Deq" && RET(Deq) && - *ARG(Deq, res) == item)) == 0) return false; + if (!HasItem(CONCURRENT, NAME == "Deq" && RET(Deq) && + *ARG(Deq, res) == item)) return false; } return true; } else { // Check the global queue state return q->back() == *res; } -@SideEffect: - if (RET) q->pop_back(); bool deq(queue_t *q, int *res); - +******************************************************************************* A good example to simulate a queue data structure is as follows. Suppose we have a special structure typedef struct Q { @@ -536,45 +449,3 @@ typedef struct Q { , and we have two interface on Q, read() and write(), where the write and read method calls are synchronized by themselves, and they have to read and write the x and y fields in turn. - - - - - - - - - - - - - - - - - - - ----------------------------------------------------------------------------------------- -We also need to think about the non-ordered queue. - -#### -Combiming Data Structures --- -For example, a queue, a -hb->c, b -hb-> e. - -// T1 -enq(1) -> {1} - {$} // a -enq(2) -> {1, 2} - {$} // b - -// T2 -deq(1) -> {$} - {1} // c -deq($) -> {$} - {1} // d - -// State before this method -JOIN ({1, 2} - {$}, {$} - {1}) = {2} - {1} -deq(2) -> {$} - {1, 2} - - - - - -- 2.34.1