|Abstract:||Multithreaded programs are hard to develop and test. In order for programs to avoid unexpected concurrent behaviours at runtime, for example data-races, synchronization mechanisms are typically used to enforce a safe subset of thread interleavings. Also, to test multithreaded programs, developers need to enforce the precise thread schedules that they
want to test. These tasks are nontrivial and error prone.
This paper presents EnforceMOP, a framework for spec-
ifying and enforcing complex properties in multithreaded
Java programs. A property is enforced at runtime by blocking the threads whose next actions would violate it. This way the remaining threads, whose execution is safe, can make global progress until the system eventually reaches a global state in which the blocked threads can be safely unblocked and allowed to execute. Users of EnforceMOP can specify the properties to be enforced using the expressive MOP multi-formalism notation, and can provide code to be executed at deadlock (when no thread is safe to continue).
EnforceMOP was used in two different kinds of applica-
tions. First, to enforce general properties in ultithreaded
programs, as a formal, semantic alternative to the exist-
ing rigid and sometimes expensive syntactic snchronization
mechanisms. Second, to enforce testing desirable schedules in unit testing of multithreaded programs, as an alternative to the existing limited and often adhoc techniques. Results show that EnforceMOP is able to effectively express and enforce complex properties and schedules in both scenarios.