The following sections are structured as follows:
loop | |
NE1: | tail := Tail |
NE2: | next := tail -> nxt |
NE3: | if next = NULL then |
NE4: | return tail -> seq |
NE5: | else CAS(Tail, tail, next) |
endif | |
endloop |
EE1: | node -> seq := seen_tail; |
EE2: | n := random(CA.size); // goto if CA is empty |
EE3: | colnode := CA[n]; |
EE4: | if isNULL(colnode) then |
EE5: | if CAS(& CA[n], & colnode, node x colnode.vnr + 1) then |
//Short delay | |
EE6: | colnode.ref := CA[n].ref |
EE7: | if (isDONE(colnode) or |
EE8: | not CAS(CA[n], colnode.ref x colnode.vnr +1, NULL(colnode.vnr +1))) |
then | |
EE9: | CA[n] := NULL(colnode.vnr +1) |
EE10: | goto E6 // successful |
endif | |
endif | |
endif | |
EE11: | goto AE1 // unsuccessful |
// code directly starts at NE1 (NumEnqs) | |
seen_tail := NumEnqs | |
E2: | node := new node(val) |
loop // directly starts at AE1 | |
if AttemptEnq then // successful/unsuccessful attempts jumps to E4/EE1 | |
E4: | return |
else if ElimEnq then // successful/unsuccessful attempt jumps to E6/AE1 | |
E6: | return |
endif | |
endloop |
AE1: | tail := Tail |
AE2: | next := tail->nxt |
AE3: | if tail = Q->CQ.Tail then |
AE4: | if next = NULL then |
AE5: | node->seq := tail->seq + 1 |
AE6: | if CAS(tail->nxt, next, node) then |
AE7: | CAS(Tail, tail, node) |
AE8: | goto E4 // successful |
endif | |
AE9: | else CAS(Tail, tail, next) |
endif | |
endif | |
AE10: | goto EE1 // unsuccessful |
// code directly starts at AD1 | |
loop | |
if AttemptDeq then //successful/unsuccessful attempts jump to D2/ED1 | |
D2: | return pval |
D3: | else if ElimDeq //successful/unsuccessful attempts jump to D4/AD1 |
D4: | return pval |
endif | |
endloop |
ED1: | seen_head := NumDeqs(Q) |
ED2: | n := random(CA.size) |
ED3: | colnode := CA[n] |
ED4: | if not isNULL(colnode) and not isDONE(colnode) then |
ED5: | if colnode.ref -> seq<= seen_head then |
ED6: | pval := colnode.ref -> val |
ED7: | if CAS(CA[n], colnode , DONE(colnode.vnr)) then |
ED8: | goto D4 // success |
endif | |
  endif | |
endif | |
ED9: | goto AD1 // unsuccessful |
AD1 : | head := Head |
AD2 : | tail := Tail |
AD3 : | next := head->nxt |
AD4 : | if head = Head then |
AD5 : | if head = tail then |
AD6 : | if next = NULL |
AD7 : | pval := EMPTY |
AD8 : | goto D2 //successful |
else | |
AD9 : | CAS(Tail, tail, next) |
endif | |
else | |
AD10: | pval := next->val |
AD11: | if CAS(Head, head, next) then |
AD12: | goto D2 //successful |
endif | |
endif | |
endif | |
AD13: | goto ED1 //unsuccessful |
ND1: | head := Q.Head |
ND2: | seen_head = head->seq; goto ED2 |
[TOCL2014] |
A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structure John Derrick, Gerhard Schellhorn and Heike Wehrheim ACM Trans. Comput. Logic, 2014, vol. 15, no. 4. |
[MoirNussbaumShalevShavit2005] |
Using elimination to implement scalable and lock-free FIFO queues
M. Moir and D. Nussbaum and O. Shalev and N. Shavit SPAA 2005, ACM press, p. 253--262 |