Michael-Scott queues
Simplified pseudo code
Non-blocking queue
Enqueue() create new node Forever: // Repeat until Append happens tail = Q->tail Check tail == Q->tail // Q is Not changed if tail is the last // next == NULL Append and break else get new Q->tail // Then do it over again get new Q->tail
Dequeue() Forever: // Repeat until Dequeue happens head = Q->head Check head == Q->head // Q is Not changed if potential invalid: // Q->head == Q->tail if empty: return false (break) get new Q->tail // Then do it over again else: read value in head Dequeue and break free head
The two loops can only exit when the break keyword is encountered. And what makes it special is that “Do and break” is implemented by a compare-and-swap (CAS) instruction which checks whether the value that is going to be swapped has been changed by other processes. If the Do instruction is not fulfilled, the whole loop would be repeated again.
Queue with two locks
Enqueue(): create new node lock(Tail) link new node unlock(Tail)
Dequeue(): lock(Head) head = Q->head // Also next = head->next if list is empty: // next = NULL unlock(Head) and return false read and advance // pvalue and Q->head = next unlock(Head) free(head) return True
Nothing special
Â
Lecture Notes
Keywords
+ Wk1 + L1 + Properties + Limits and Boundaries + L2 + LTL + Critical section + Wk2 + Transition Diagram + Floyd Verification + Owicki-Gries Method + Assertion Network + One Big Invariant + Wk3 + L1 + Liveness desiderata + Safety properties + Szymanski's Algorithm + L2 + lock/mutex + test and test and set + Wk4 + L1 + Semaphore + L2 + Monitor + Disadvantage of Semaphore + Persistent data structure + Wk5 + Message Passing + Synchronous transition diagram + Adding Shared auxiliary variables (+Invariant) + Levin & Gries-style proof + AFR style proof + Wk7 + L1 + Termination + Well Founded order + Floyd’s Wellfoundedness Method + Owicki/Gries Deadlock-Freedom Condition + L2 + Compositionality + Partial Correctness + Parallel composition rule + Wk8 + L1 + Calculus of Communicating Systems + Process algebra + labelled transition system + L2 + Neilsen-Mizuno Algorithm + Wk9 + L1 + Commitment and Consensus + Dijkstra-Scholten algorithm + L2 + Distributed System with an Environment Node + Credit-recovery algorithms + Chandy-Lamport
Â
