/**
@Begin
@Interface: Get
- @Commit_point_set: GetReadValue1 | GetReadEntry | GetReadValue2
+ @Commit_point_set: GetReadValue1 | GetReadValue2 | GetReadNothing
@ID: __RET__
@Action:
int res = getIntegerMap(__map, key);
// lock, we ignore this operation for the SC analysis, and otherwise we
// take it into consideration
- /**** UL ****/
+ /**** UL (main.cc) ****/
Entry *firstPtr = first->load(acquire);
e = firstPtr;
while (e != NULL) {
if (key, e->key) {
- /**** inadmissible ****/
+ /**** inadmissible (testcase1.cc) ****/
res = e->value.load(seq_cst);
/**
@Begin
// Synchronized by locking, no need to be load acquire
Entry *newFirstPtr = first->load(relaxed);
- /**
- @Begin
- @Commit_point_define_check: true
- @Label: GetReadEntry
- @End
- */
if (e != NULL || firstPtr != newFirstPtr) {
e = newFirstPtr;
while (e != NULL) {
}
}
seg->unlock(); // Critical region ends
+ /**
+ @Begin
+ @Commit_point_define_check: true
+ @Label: GetReadNothing
+ @End
+ */
return 0;
}
// with the previous put()), no need to be acquire
oldValue = e->value.load(relaxed);
- /**** inadmissible ****/
+ /**** inadmissible (testcase1.cc) ****/
e->value.store(value, seq_cst);
/**
@Begin
// Add to front of list
Entry *newEntry = new Entry(hash, key, value, firstPtr);
- /**** UL ****/
+ /**** UL (main.cc) ****/
// Publish the newEntry to others
first->store(newEntry, release);
+ /**
+ @Begin
+ @Commit_point_clear: true
+ @Label: PutClear
+ @End
+ */
+
/**
@Begin
@Commit_point_define_check: true