# # A model of the work-stealing queue from Cilk 5, as presented in # # Matteo Frigo, Charles E. Leiserson, and Keith H. Randall. The implementation # of the cilk-5 multithreaded language. SIGPLAN Not., 33(5):212–223, May 1998. # # IS NOT robust. # # There are happens-before cycles involving pop and steal. # # Memory layout: # 0 — H # 1 — T # 2 — L thread release_lock initial q0 transition q0 q1 write 1 2 end thread push1 initial push0 transition push0 push1 read T 1 transition push1 push2 write + T 1 1 end thread pop1 initial pop0 transition pop0 pop1 read T 1 transition pop1 pop2 local T - T 1 transition pop2 pop3 write T 1 transition pop3 pop4 read H 0 transition pop4 success check <= H T transition pop4 pop5 check > H T transition pop5 pop6 read T 1 transition pop6 pop7 write + 1 T 1 transition pop7 pop8 lock transition pop8 pop9 read L 2 transition pop9 pop10 check != L 0 transition pop10 pop11 write - L 1 2 transition pop11 pop12 unlock transition pop11 pop12 read T 1 transition pop12 pop13 write - T 1 1 transition pop13 pop14 read H 0 transition pop14 pop16 check <= H T transition pop14 pop20 check > H T transition pop16 pop17 lock transition pop17 pop18 read L 2 transition pop18 pop19 write + 1 L 2 transition pop19 success unlock transition pop20 pop21 read T 1 transition pop21 pop22 write + T 1 1 transition pop22 pop23 lock transition pop23 pop24 read L 2 transition pop24 pop25 write + 1 L 2 transition pop25 failure unlock end thread pop2 initial pop0 transition pop0 pop1 read T 1 transition pop1 pop2 local T - T 1 transition pop2 pop3 write T 1 transition pop3 pop4 read H 0 transition pop4 success check <= H T transition pop4 pop5 check > H T transition pop5 pop6 read T 1 transition pop6 pop7 write + 1 T 1 transition pop7 pop8 lock transition pop8 pop9 read L 2 transition pop9 pop10 check != L 0 transition pop10 pop11 write - L 1 2 transition pop11 pop12 unlock transition pop11 pop12 read T 1 transition pop12 pop13 write - T 1 1 transition pop13 pop14 read H 0 transition pop14 pop16 check <= H T transition pop14 pop20 check > H T transition pop16 pop17 lock transition pop17 pop18 read L 2 transition pop18 pop19 write + 1 L 2 transition pop19 success unlock transition pop20 pop21 read T 1 transition pop21 pop22 write + T 1 1 transition pop22 pop23 lock transition pop23 pop24 read L 2 transition pop24 pop25 write + 1 L 2 transition pop25 failure unlock end thread steal1 initial steal0 transition steal0 steal1 lock transition steal1 steal2 read L 2 transition steal2 steal3 check != L 0 transition steal3 steal4 write - L 1 2 transition steal4 steal5 unlock transition steal5 steal6 read H 0 transition steal6 steal7 local H + 1 H transition steal7 steal8 write H 0 transition steal8 steal9 read T 1 transition steal9 steal10 check <= H T transition steal9 steal14 check > H T transition steal10 steal11 lock transition steal11 steal12 read L 2 transition steal12 steal13 write + 1 L 2 transition steal13 success unlock transition steal14 steal15 write - H 1 0 transition steal15 steal16 lock transition steal16 steal17 read L 2 transition steal17 steal18 write + 1 L 2 transition steal18 failure unlock end