Controlling Non-determinism for Semantic Guarantees

Concurrent programs are hard to design, develop, and debug. It is widely accepted that we lack good abstractions to design and reason about concurrent programs, and good tools to debug concurrent programs. Recent technology trends, such as the increasing prevalence of multicore processors, make concurrent programming more important than ever. Non-determinism arises in concurrent programs when the order in which threads can execute is unconstrained. While executions of concurrent programs on multiprocessors inherently exhibit non-determinism, the executions on uniprocessors exhibit non-determinism due to the choices of the thread scheduler in the underlying O/S. Undesired non-determinism is a major cause of errors in concurrent programs. Nevertheless, we believe that non-determinism can be safely, permissively, and automatically controlled to tolerate runtime errors in concurrent programs and to provide various desirable semantic guarantees. In this position paper, we sketch some recent work we have done in this direction and outline our longer term goals along the same direction.