Jevgenia Smorgun, Jaeheon Yi
11/09/2009 09:00 AM
Computer Science
Type-and-effect systems can guard against race conditions by statically enforcing a locking discipline. A program's synchronization structure enforces a program’s locking discipline. Whether or not a program's locking discipline is enforced by its synchronization structure is a previously studied question.
A yield is a multithreading synchronization mechanism for automatic mutual exclusion (AME), where multithreading is explicitly allowed at selected yield points, and excluded elsewhere. AME's semantics have cooperative multithreading, where the yield command explicitly permits preemptions to occur. We consider yields as a specification in a non-cooperative semantics, such that yields indicate program points where the programmer expects a preemption to possibly occur: a yielding discipline. Given a program, are its synchronization structure and yielding discipline consistent with each other? We propose an effect system for this problem.
