// Coarse-grained list with fine-grained lock-free contains // // This is a simple implementation of a set as sorted list with two sentinel // nodes. The add and remove methods are protected by a CCR and are therefore // trivially linearizable. // // The contains method, however, does not use a global CCR; instead it // just protects individual accesses by atomic blocks, and does not use // any form of blocking synchronization with other threads. As a result, // there are executions where its linearization point lies inside code // of other threads. // class Node { int val; Node tl; } Node head, tail; resource r() { constructor { tail = new(); tail->val = 12345; head = new(); head->val = -12345; head->tl = tail; } } // --------------------------------------------------------- // Insert an element into the set // --------------------------------------------------------- bool add(int key) requires -12345 < key && key < 12345 { Node prev, curr, temp2; int temp; prev = head; atomic { curr = prev->tl; temp = curr->val; while(temptl; temp = curr->val; } if (temp>key) { temp2 = new(); temp2->val = key; temp2->tl = curr; prev->tl = temp2; return true; } else { return false; } } } // --------------------------------------------------------- // Remove an element from the set // --------------------------------------------------------- bool remove(int key) requires -12345 < key && key < 12345 { Node prev, curr, temp2; int temp; prev = head; atomic { curr = prev->tl; temp = curr->val; while(temptl; temp = curr->val; } if (temp==key) { temp2 = curr->tl; prev->tl = temp2; return true; } else { return false; } } } // --------------------------------------------------------- // Is the element in the set? // --------------------------------------------------------- bool contains(int key) requires -12345 < key && key < 12345 { Node curr; int temp; atomic { curr = head->tl; } atomic { temp = curr->val; } while(temptl; } atomic { temp = curr->val; } } if (temp==key) { return true; } else { return false; } }