Types for Precise Thread Interference
The potential for unexpected interference between threads makes multi-threaded programming notoriously difficult. Programmers use a variety of synchronization idioms such as locks and barriers to restrict where interference may actually occur. Unfortunately, the resulting actual interference points are typically never documented and must be manually reconstructed as the first step in any subsequent programming task (code review, refactoring, etc). This paper proposes explicitly documenting actual interference points in the program source code, and it presents a type and effect system for verifying the correctness of these interference specifications.