Reasoning similar to this enabled me to write a rather powerful test recently. We had a queue that was behaving strangely and we didn't reallz know how to tack

Reasoning similar to this enabled me to write a rather powerful test recently. We had a queue that was behaving strangely and we didn't reallz know how to tackle this. Thus I just went ahead and realized: If we take enqueue and dequeue as parenthesis open and parenthesis close, then a balanced string of opening and closing parenthesis will leave the queue empty. And furthermore, if the queue is thread safe, I can execute multiple such execution sequences in parallel and the queue will still be empty in the end and no execution sequence will be infinitely blocked. The threads might steal some elements back and forth, but no thread will ever starve, because for every stolen dequeue, and enqueue will be orphaned and thus, stolen in retaliation. From there, I could just write myself an execution sequence generator based on the CFG for balanced parenthesis trees, execute a number of these things in parallel and check if the queue was empty in the end. This test failed and it appears to be highly sensitive and precise.