From 05a47c2a14f45d4b4cd766139776872793f029e7 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Wed, 27 Jan 2016 18:31:07 -0800 Subject: [PATCH] more edits --- notes/nondeterm-spec.txt | 205 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 197 insertions(+), 8 deletions(-) diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt index 3608274..7eee23d 100644 --- a/notes/nondeterm-spec.txt +++ b/notes/nondeterm-spec.txt @@ -58,7 +58,11 @@ current method in the execution graph --- most recent method calls that are hb/SC before the current method call --- and returns as a set. For each method in this set, the current method's specification can access their local state. -3. LOCAL: This primitive allows users to access the local state of a method +3. NEXT: This primitive extracts all the methods that execute right after the +current method in the execution graph, and returns as a set. For each method in +this set, the current method's specification cannot access their local state. + +4. LOCAL: This primitive allows users to access the local state of a method call. It is worth noting that in order to calculate the local state of a method call, one can only access the set of method calls that happen before the current method call. @@ -69,13 +73,73 @@ calls that happen before the current method call in the sequential order, and a the user-customized approach supports users to calculate the local state by using the PREV primitive to access the local state of previous method calls. -4. COPY: This is the function that users provide to deep-copy the state. We +5. COPY: This is the function that users provide to deep-copy the state. We require users to provide such a primitive function because each local state should be have its own copy. +6. FINALLY: This is the function that allows users to specify some final check +on the state. Initially, this check will only access the global state. However, +for the concern of expressiveness, we allow users to access the initial state, +meaning that users can basically access the whole graph and the local state of +each method call. This will enable to users to use the graph model (the relaxed +atomics can be specified) although the complxity of using that can get quite +complex. + IV. Examples -1. The register examples. +// Global specification +@DeclareState: // Declare the state structure +@InitState: // How do we initialize the state +@CopyState: // A function on how to copy an existing state +@Commutativity: Method1 <-> Method2 (Guard) // Guard can only access the return + // value and the arguments of the two method calls + +// Interface specification +@Interface: InterfaceName // Required; a label to represent the interface +@LocalState: // Optional; to calculate the accumulative local state before this + // method call in a customized fashion. If not specified here, the + // local state would be default, which is the result of the + // execution on the subset of method calls in the sequential order +@PreCondition: // Optional; checking code +@LocalSideEffect: // Optional; to calculate the side effect this method call + // have on the local state in a customized fashion. If this + // field is not stated, it means we don't care about it. +@SideEffect: // Optional; to calculate the side effect on the global state. When + // the "@LocalSideEffect" specification is ommitted, we also impose the + // same side effect on the set of method calls that happen before this + // method call in the sequential order. +@PostCondition: // Optional; checking code + +// Ordering point specification +@OPDefine: condition // If the specified condition satisfied, the atomic + // operation right before is an ordering point + +@PotentialOP(Label): condition // If the specified condition satisfied, the + // atomic operation right before is a potential + // ordering point, and we label it with a tag + +@OPCheck(Label): condition // If the specified condition satisfied, the + // potential ordering point defined earlier with the + // same tag becomes an ordering point + +@OPClear: condition // If the specified condition satisfied, all the + // ordering points and potential ordering points will be + // cleared + +@OPClearDefine: condition // If the specified condition satisfied, all the + // ordering points and potential ordering points will + // be cleared, and the atomic operation right before + // becomes an ordering point. This is a syntax sugar + // as the combination of an "OPClear" and "OPDefine" + // statement + + +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. + ---------- Interfae ---------- void init(atomic_int &loc, int initial); int load(atomic_int &loc); @@ -134,14 +198,81 @@ any store that either immediately happens before it or concurrently executes. 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 +typedef struct MethodCall { + string interfaceName; // The interface label name + void *value; // The pointer that points to the struct that have the return + // 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 +} MethodCall; + +We will automatically generate two types of struct. One is the state struct, and +we will call it StateStruct. This state is shared by all the global and local +state. The other one is a per interface struct, and it wraps the return value +(RET) and the arguments as its field. We will name those struct with the +interface label name. + +// Some very nice C/C++ macro definition to make specifications a lot easier +// 1. ForEach --> to iterate all +#define ForEach(item, list) \ + for (iterator _mIter = list->begin(), \ + MethodCall *item = *_mIter; _mIter != list->end(); item = (++iter != \ + list->end()) ? *_mIter : NULL) + + +********************************************* + +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; +} + +// 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) +#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 + @Interface: Load @PreCondition: - IntegerSet *prevSet = new IntegerSet; - IntegerSet *concurSet = new IntegerSet; - for (m in PREV) { - prevSet->add(m.LOCAL.x); + // Auto generated code + // MethodCall *ME = ((SomeTypeConversion) info)->method; + // vector PREV = Me->prev; + // vector NEXT = Me->next; + // vector CONCURRENT = Me->concurrent; + + IntegerSet prevSet, concurSet; + ForEach(m, PREV) { + prevSet.add(LOCAL(m, x)); } - for (m in CONCURRENT("STORE")) { + ForEach (m, CONCURRENT("STORE")) { concurSet->add(m.val); } return prevSet->contains(RET) || concurSet->contains(RET); @@ -153,6 +284,64 @@ d. The C/C++ normal memory accesses - Use the admissibility requirement, then the classic linearizability approach on the admissible executions +2. The FIFO queue example. +---------- Specification ---------- +// A FIFO queue should have the following properties held: +// 1. The enq() methods should conflict +// 2. The deq() methods that succeed should conflict +// 3. Corresponding enq() and deq() methods should conflict +// 4. An enqueued item can be dequeued by at most once +// 5. A dequeued item must have a corresponding enqueued item +// 6. When a queue is NOT "empty" (users can tightly or loosely define +// emptiness), and there comes a deq() method, the deq() method should succeed + + +@DeclareVar: vector *q; +@InitVar: q = new voctor; +@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)) + +@Interface: Enq +@SideEffect: + LOCAL.x = val; +void enq(queue_t *q, int val); + +@Interface: Deq +@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 + // dequeue them + if (!RET) { + // Local state is empty + 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]; + // 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; + } + return true; + } else { // Check the global queue state + return q->back() == *res; + } +@SideEffect: + if (RET) + Global.q->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 { -- 2.34.1