/* ------------------------------------------ void proc(Object SharedObj, int g) a1 loop a2 local m = LL(SharedObj) in a3 local i = 1 in a4 loop a5 if (i>W) break; a6 local newVersion[i] = m.version[i] in a7 if (newVersion[i] != prvObj.version[i]) a8 copy(prvObj.data[i],m.data[i]); a9 if (!VL(SharedObj)) a10 continue a2; a11 prvObj.version[i] = newVersion[i]; a12 i++; a13 if (!valid(prvObj)) continue a2; a14 compute(prvObj,g); a15 prvObj.version[g]++; a16 if (SC(SharedObj,prvObj)) a17 prvObj = m; a18 return; a19 else a20 prvObj.version[g] = 0; ------------------------------------------ */ #define W 2 /* number of groups of fields, i.e., # of data item in an object, */ /*if changing the value, also need to change the code that chooses g */ #define numThread 3 /* number of thread, if changing the value, also change the code */ /* that chooses dataval */ #define numSharedObject 1 /* number of shared objects */ #define numObject 4 /* total number of objects = numThread + numSharedObjects */ typedef Object{ short data[W]; short version[W]; } /* Index is a structure used only for shared objects, it can be considered as a */ /* pointer to a shared object (actually it is a subscript). The field "val" is */ /* the index of the current shared object in the whole object array. The field */ /* "flag[thr]" is an array to denote whether this object has been written after */ /* thread thr's most recent LL. */ typedef Index{ byte val; bool flag[numThread]; } Object object[numObject]; /* Initially, the first "numThread"(such as 3) objects are */ /* private, the rest are shared. Object[sharedObjectIndex[i]] */ /* is the shared copy of the ith shared object. */ Index sharedObjectIndex[numSharedObject]; /* This worker performs two operations on the specified shared object and then exits. */ /* Performing one operation per thread seems insufficiently thorough. */ proctype Worker(byte shared; byte tID){ byte opNum = 0; /* each thread's private object index is initially set to the thread ID, \ie, 0, 1, ..., numThread */ byte privateObjectIndex = tID; do :: (opNum < 1) -> /* nonderterministically choose a group, assumming W = 2 */ byte g = 0; if :: g = 0; :: g = 1; fi; byte dataval; if :: dataval = 0; :: dataval = 1; /* :: dataval = 2; */ fi; short newVersion[W]; byte m; atomic{ do :: /* this atomic statement corresponds to m = LL(sharedObjectIndex[shared]); */ atomic { m = sharedObjectIndex[shared].val; sharedObjectIndex[shared].flag[tID] = false; } /* i iterates 0..W-1 in this code, instead of 1..W as in the pseudo-code. */ byte i = 0; do :: (i newVersion[i] = object[m].version[i]; if :: (newVersion[i] != object[privateObjectIndex].version[i]) -> object[privateObjectIndex].data[i] = object[m].data[i]; /* the next statement corresponds to the VL operation */ if :: (sharedObjectIndex[shared].flag[tID] == true) -> goto loopend; :: else -> skip; fi; object[privateObjectIndex].version[i] = newVersion[i]; :: else -> skip; fi; i++; :: (i>=W) -> break; od; /* the next statement corresponds to compute(prvObj,g). The use of tID*/ /* nondeterminism means that different threads may perform different operations. */ object[privateObjectIndex].data[g] = (object[privateObjectIndex].data[g] + dataval)%numThread+1; object[privateObjectIndex].version[g]++; if :: /* this atomic statement corresponds to SC operation. "sharedObjectIndex[shared].flag" */ /* is an array whose each element corresponds to a thread; when a thread write value, */ /* the whole array is set to true. In Gao's paper, he used a set instead of array */ atomic { (!sharedObjectIndex[shared].flag[tID]) -> sharedObjectIndex[shared].val = privateObjectIndex; byte j = 0; do :: (j < numThread) -> sharedObjectIndex[shared].flag[j] = true; j++; :: (j >= numThread) -> break; od; } privateObjectIndex = m; break; :: else -> /* the SC fails */ object[privateObjectIndex].version[g] = 0; fi; loopend: skip; od; } /* end of atomic */ /* finish one operation of worker, prepare for the next operation */ opNum++; /* Because the value of g is nonderterministic, we use the value of g to nondeterminitically */ /* choose the next shared object */ shared = (shared+g)%numSharedObject; :: (opNum >= 1) -> break; od; } init { /* initialize sharedObjectIndex */ byte i = 0; do :: (i /* In the "object[]" array, initially, all elements after "numThread" are shared */ sharedObjectIndex[i].val = numThread+i; int k; do :: (k < numThread) -> sharedObjectIndex[i].flag[k] = false; k++; :: (k >= numThread) -> break; od; i++; :: (i>=numSharedObject) -> break; od; /* start threads */ byte j = 0; do :: (j < numThread) -> /* the first paramenter is the chosen shared object index, the second parameter is the tID */ run Worker(j%numSharedObject, j); j++; :: (j >= numThread) -> break; od; }