ABSTRACT
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.
- C. Allan, P. Avgustinov, A. S. Christensen, L. J. Hendren, S. Kuzins, O. Lhoták, O. de Moor, D. Sereni, G. Sittampalam, and J. Tibble. Adding trace matching with free variables to AspectJ. In OOPSLA, 2005. Google ScholarDigital Library
- Apache Software Foundation. Apache Commons Collections. http://commons.apache.org/ collections/.Google Scholar
- Apache Software Foundation. Apache Commons Pool. http://commons.apache.org/pool/.Google Scholar
- Apache Software Foundation. Apache Hadoop. http://hadoop.apache.org/.Google Scholar
- Apache Software Foundation. Apache Lucene. http:// lucene.apache.org/.Google Scholar
- Apache Software Foundation. Apache MINA. http:// mina.apache.org/.Google Scholar
- Apache Software Foundation. LOG4J-50213. https:// issues.apache.org/bugzilla/show_bug.cgi? id=50213.Google Scholar
- Apache Software Foundation. TOMCAT-25841. https://issues.apache.org/bugzilla/show_bug. cgi?id=25841.Google Scholar
- H. Barringer, B. Finkbeiner, Y. Gurevich, and H. Sipma, editors. RV 05, volume 144 of ENTCS, 2005.Google Scholar
- R. Behrends and R. E. K. Stirewalt. The universe model: an approach for improving the modularity and reliability of concurrent programs. In FSE, 2000. Google ScholarDigital Library
- A. Betin-Can and T. Bultan. Verifiable concurrent programming using concurrency controllers. In ASE, 2004. Google ScholarDigital Library
- E. Bodden and K. Havelund. Racer: Effective race detection using AspectJ. In ISSTA, 2008. Google ScholarDigital Library
- J. Burnim, T. Elmas, G. Necula, and K. Sen. CONCURRIT: Testing concurrent programs with programmable state-space exploration. In HotPar, 2012. Google ScholarDigital Library
- R. H. Campbell and A. N. Habermann. The specification of process synchronization by path expressions. In OS, 1974. Google ScholarDigital Library
- F. Chen and G. Ro¸su. Java-MOP: A monitoring oriented programming environment for Java. In TACAS, 2005. Google ScholarDigital Library
- F. Chen and G. Rosu. Mop: an efficient and generic runtime verification framework. In OOPSLA, 2007. Google ScholarDigital Library
- Codehaus. Sysunit. http://docs.codehaus.org/ display/SYSUNIT/Home.Google Scholar
- K. Coons, S. Burckhardt, and M. Musuvathi. Gambit: Effective unit testing for concurrency libraries. In PPoPP, 2010. Google ScholarDigital Library
- M. d’Amorim and K. Havelund. Event-based runtime verification of Java programs. ACM SIGSOFT SEN, 30:1–7, 2005. Google ScholarDigital Library
- X. Deng, M. B. Dwyer, J. Hatcliff, and M. Mizuno. Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. In ICSE, 2002. Google ScholarDigital Library
- J. Dolby, C. Hammer, D. Marino, F. Tip, M. Vaziri, and J. Vitek. A data-centric approach to synchronization. ACM TOPLAS, 34:4:1–4:48, 2012. Google ScholarDigital Library
- O. Edelstein, E. Farchi, E. Goldin, Y. Nir, G. Ratsaby, and S. Ur. Framework for Testing Multi-Threaded Java Programs. CCPE, 2003.Google ScholarCross Ref
- C. Flanagan and S. N. Freund. FastTrack: efficient and precise dynamic race detection. In PLDI, 2009. Google ScholarDigital Library
- C. Flanagan, S. N. Freund, and J. Yi. Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In PLDI, 2008. Google ScholarDigital Library
- S. Goldsmith, R. O’Callahan, and A. Aiken. Relational queries over program traces. In OOPSLA, 2005. Google ScholarDigital Library
- K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. Journal on STTT, 2:366–381, 2000.Google ScholarCross Ref
- K. Havelund and G. Ro¸su, editors. RV 01, RV 02, RV 04, volume 55, 70, 113 of ENTCS, 2001, 2002, 2004.Google Scholar
- K. Havelund and G. Rosu. An overview of the runtime verification tool Java PathExplorer. FMSD, 2004. Google ScholarDigital Library
- IBM. ECLIPSE-369251. https://bugs.eclipse.org/ bugs/show_bug.cgi?id=369251.Google Scholar
- V. Jagannath, M. Gligoric, D. Jin, Q. Luo, G. Rosu, and D. Marinov. Improved multithreaded unit testing. In FSE, 2011. Google ScholarDigital Library
- Java Community Process. JSR 166: Concurrency utilities. http://g.oswego.edu/dl/ concurrency-interest/.Google Scholar
- JBoss Community. JBoss Cache. http://www.jboss. org/jbosscache.Google Scholar
- G. Kiczales, E. Hilsdale, J. Hugunin, M. Kersten, J. Palm, and W. G. Griswold. An overview of AspectJ. In ECOOP, 2001. Google ScholarDigital Library
- M. Kim, S. Kannan, I. Lee, O. Sokolsky, and M. Viswanathan. Java-MaC: a run-time assurance tool for Java programs. ENTCS, 55:218–235, 2001.Google ScholarCross Ref
- B. Long, D. Hoffman, and P. Strooper. Tool Support for Testing Concurrent Java Components. IEEE TSE, 29:555–566, 2003. Google ScholarDigital Library
- M. C. Martin, V. B. Livshits, and M. S. Lam. Finding application errors and security flaws using PQL: a program query language. In OOPSLA, 2005. Google ScholarDigital Library
- M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI, 2007. Google ScholarDigital Library
- Object Refinery. JFREECHART-1051. http:// sourceforge.net/p/jfreechart/bugs/1051/.Google Scholar
- Object Refinery. JFREECHART-187. http:// sourceforge.net/p/jfreechart/bugs/187/.Google Scholar
- Oracle. JavaDoc ArrayList. http://docs.oracle. com/javase/6/docs/api/java/util/ArrayList.html.Google Scholar
- S. Park, S. Lu, and Y. Zhou. CTrigger: Exposing atomicity violation bugs from their hiding places. In ASPLOS, 2009. Google ScholarDigital Library
- S. Park, R. W. Vuduc, and M. J. Harrold. Falcon: fault localization in concurrent programs. In ICSE, 2010. Google ScholarDigital Library
- W. Pugh and N. Ayewah. Unit testing concurrent software. In ASE, 2007. Google ScholarDigital Library
- O. Sokolsky and M. Viswanathan, editors. RV 03, volume 89 of ENTCS, 2003.Google Scholar
- M. Vaziri, F. Tip, and J. Dolby. Associating synchronization constraints with data in an object-oriented language. In POPL, 2006. Google ScholarDigital Library
Index Terms
- EnforceMOP: a runtime property enforcement system for multithreaded programs
Recommendations
Dynamically checking ownership policies in concurrent c/c++ programs
POPL '10Concurrent programming errors arise when threads share data incorrectly. Programmers often avoid these errors by using synchronization to enforce a simple ownership policy: data is either owned exclusively by a thread that can read or write the data, ...
Testing multithreaded programs via thread speed control
ESEC/FSE 2018: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software EngineeringA multithreaded program's interleaving space is discrete and astronomically large, making effectively sampling thread schedules for manifesting concurrency bugs a challenging task. Observing that concurrency bugs can be manifested by adjusting thread ...
Dynamically checking ownership policies in concurrent c/c++ programs
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesConcurrent programming errors arise when threads share data incorrectly. Programmers often avoid these errors by using synchronization to enforce a simple ownership policy: data is either owned exclusively by a thread that can read or write the data, ...
Comments