The aspects of shared-memory multithreading that induce the most errors in programs is that shared memory is implicitly shared and that code running in separate threads may implicitly communicate as a result. Maintaining safe and correct sharing and communication requires explicit synchronization by the programmer; this job is made exceedingly difficult by the fact that sharing and communication are implicit, and programmers have no direct feedback mechanism to determine when it occurs or when their synchronization is sufficient. Some behaviors even carry weak or undefined semantics in modern memory consistency models. Previous research has offered debugging tools to report problematic concurrency behaviors, but we believe that the execution model itself should make these behaviors explicit.
More concretely, this project posits that shared-memory multithreaded concurrency errors should be precisely detected and fail-stop at runtime in the way that segmentation faults or division-by-zero errors are today. Making these errors explicit and exceptional allows programmers to make stronger assumptions about the semantics of their programs and rely on the execution model to raise an error at runtime if these assumptions are violated. Embedding such error-checking in the execution model also allows better debugging of deployed applications: explicit concurrency errors avoid mysterious and unpredictable program behavior associated with silent errors.
Our work focuses on a range of concurrency errors, including data races and sequential consistency violations, which are easy to define independent of application semantics, as well as more subtle application-specific invariants, such as which code is allowed to perform inter-thread communication. We aim to generalize some support for concurrency exceptions throughout the system stack. Specifically, we are investigating the semantics and specification of concurrency exceptions at the language level, their implications in the compiler and runtime systems, how they should be delivered, and how they are enabled by efficient architecture support.