test f [expect=pass,memmodel=tso] thread init { -- all the threads have not yet started r = (pointer 2) *r = 0 r = (pointer 3) *r = 0 r = (pointer 4) *r = 0 r = (pointer 5) *r = 0 r = (pointer 6) *r = 0 -- count = 5 count = (pointer 1) *count = 5 } thread t0 { -- thread number 0 starts r = (pointer 2) *r = 1 -- atomic counter decrement count = (pointer 1) atomic { x = *count x = (subtract x 1) *count = x } -- wait for zero counter await spinforzero { x = *count b = (notequals x 0) if (b) defer spinforzero } -- assert that threads 1,2,3,4 have started r = (pointer 3) b = *r r = (pointer 4) aux = *r b = (bitand b aux) r = (pointer 5) aux = *r b = (bitand b aux) r = (pointer 6) aux = *r b = (bitand b aux) assert(b) } thread t1 { -- thread number one starts r = (pointer 3) *r = 1 -- atomic counter decrement count = (pointer 1) atomic { x = *count x = (subtract x 1) *count = x } -- wait for zero counter await spinforzero { x = *count b = (notequals x 0) if (b) defer spinforzero } -- assert threads 0,2,3,4 have started r = (pointer 2) b = *r r = (pointer 4) aux = *r b = (bitand b aux) r = (pointer 5) aux = *r b = (bitand b aux) r = (pointer 6) aux = *r b = (bitand b aux) assert(b) } thread t2 { -- threads number two starts r = (pointer 4) *r = 1 -- atomic counter decrement count = (pointer 1) atomic { x = *count x = (subtract x 1) *count = x } -- wait for zero counter await spinforzero { x = *count b = (notequals x 0) if (b) defer spinforzero } -- assert that threads 0,1,3,4 have started r = (pointer 2) b = *r r = (pointer 3) aux = *r b = (bitand b aux) r = (pointer 5) aux = *r b = (bitand b aux) r = (pointer 6) aux = *r b = (bitand b aux) assert(b) } thread t3 { -- threads number three starts r = (pointer 5) *r = 1 -- atomic counter decrement count = (pointer 1) atomic { x = *count x = (subtract x 1) *count = x } -- wait for zero counter await spinforzero { x = *count b = (notequals x 0) if (b) defer spinforzero } -- assert that threads 0,1,2,4 have started r = (pointer 2) b = *r r = (pointer 3) aux = *r b = (bitand b aux) r = (pointer 4) aux = *r b = (bitand b aux) r = (pointer 6) aux = *r b = (bitand b aux) assert(b) } thread t4 { -- threads number four starts r = (pointer 6) *r = 1 -- atomic counter decrement count = (pointer 1) atomic { x = *count x = (subtract x 1) *count = x } -- wait for zero counter await spinforzero { x = *count b = (notequals x 0) if (b) defer spinforzero } -- assert that threads 0,1,2,3 have started r = (pointer 2) b = *r r = (pointer 3) aux = *r b = (bitand b aux) r = (pointer 4) aux = *r b = (bitand b aux) r = (pointer 5) aux = *r b = (bitand b aux) assert(b) } end