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.
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);
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<MethodCall*> *prev; // Method calls that are hb right before me
+ vector<MethodCall*> *next; // Method calls that are hb right after me
+ vector<MethodCall*> *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<MethodCall*> _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<MethodCall*>* Subset(vector<MethodCall*> *set, string name) {
+ vector<MethodCall*> _subset = new vector<MethodCall*>;
+ 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<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));
}
- for (m in CONCURRENT("STORE")) {
+ ForEach (m, CONCURRENT("STORE")) {
concurSet->add(m.val);
}
return prevSet->contains(RET) || concurSet->contains(RET);
- 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<int> *q;
+@InitVar: q = new voctor<int>;
+@Copy: New.q = new vector<int>(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 {
projects / cdsspec-compiler.git / blobdiff