TY - GEN
T1 - EnforceMOP
T2 - 22nd International Symposium on Software Testing and Analysis, ISSTA 2013
AU - Luo, Qingzhou
AU - Roşu, Grigore
N1 - Copyright:
Copyright 2013 Elsevier B.V., All rights reserved.
PY - 2013
Y1 - 2013
N2 - Multithreaded programs are hard to develop and test. In order for programs to avoid unexpected concurrent behaviors at runtime, for example data-races, synchronization mechanisms are typically used to enforce a safe subset of thread interleavings. Also, to test multithreaded programs, devel- opers 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 specifying 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 applications. First, to enforce general properties in multithreaded programs, as a formal, semantic alternative to the existing rigid and sometimes expensive syntactic synchronization 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.
AB - Multithreaded programs are hard to develop and test. In order for programs to avoid unexpected concurrent behaviors at runtime, for example data-races, synchronization mechanisms are typically used to enforce a safe subset of thread interleavings. Also, to test multithreaded programs, devel- opers 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 specifying 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 applications. First, to enforce general properties in multithreaded programs, as a formal, semantic alternative to the existing rigid and sometimes expensive syntactic synchronization 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.
KW - Concurrency
KW - Enforcement
KW - Testing
UR - http://www.scopus.com/inward/record.url?scp=84883104918&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84883104918&partnerID=8YFLogxK
U2 - 10.1145/2483760.2483766
DO - 10.1145/2483760.2483766
M3 - Conference contribution
AN - SCOPUS:84883104918
SN - 9781450321594
T3 - 2013 International Symposium on Software Testing and Analysis, ISSTA 2013 - Proceedings
SP - 156
EP - 166
BT - 2013 International Symposium on Software Testing and Analysis, ISSTA 2013 - Proceedings
Y2 - 15 July 2013 through 20 July 2013
ER -