User Evaluation of Correctness Conditions: A Case Study of Cooperability

In order to find and fix concurrency bugs, programmers must reason about different possible thread inter-leavings - context switches may occur at any program point, all with the potential for thread interference. To reduce the number of thread interference points to consider, the correctness criterion of co-operability ensures that code executes as if context switches may happen only at specific yield annotations. This paper provides empirical evidence that co-operability makes it easier to find concurrency bugs.