Koushik Sen
Gul Agha
ABSTRACT
Foundational and scalable techniques for runtime safety analysis of multithreaded programs are explored in this paper. A technique based on vector clocks to extract the causal dependency order on state updates from a running multithreaded program is presented, together with algorithms to analyze a multithreaded computation against safety properties expressed using temporal logics. A prototype tool implementing our techniques, is also presented, together with examples where it can predict safety errors in multithreaded programs from successful executions of those programs. This tool is called Java MultiPathExplorer (JMPaX), and available for download on the web. To the best of our knowledge, JMPaX is the first tool of its kind.
- Java Multi PathEXplorer, March 2003. http://fsl.cs.uiuc.edu/jmpax/.Google Scholar
- H. W. Cain and M. H. Lipasti. Verifying sequential consistency using vector clocks. In Proceedings of the 14th annual ACM symposium on Parallel algorithms and Architectures, pages 153--154. ACM, 2002. Google ScholarDigital Library
- C. M. Chase and V. K. Garg. Detection of global predicates: Techniques and their limitations. Distributed Computing, 11(4):191--201, 1998. Google ScholarDigital Library
- R. Cooper and K. Marzullo. Consistent detection of global predicates. ACM SIGPLAN Notices, 26(12):167--174, 1991. Proceedings of the ACM/ONR Workshop on Parallel and Distributed Debugging. Google ScholarDigital Library
- M. Dahm. Byte code engineering with the bcel api. Technical Report B-17-98, Freie Universit at Berlin, Institut für Informatik, April 2001.Google Scholar
- J. E. M. Clarke, O. Grumberg, and D. A. Peled. Model checking. MIT Press, 1999. Google ScholarDigital Library
- C. J. Fidge. Partial orders for parallel debugging. In Proceedings of the 1988 ACM SIGPLAN and SIGOPS workshop on Parallel and Distributed debugging, pages 183--194. ACM, 1988. Google ScholarDigital Library
- K. Havelund and T. Pressburger. Model Checking Java Programs using Java PathFinder. International Journal on Software Tools for Technology Transfer, 2(4):366--381, Apr. 2000.Google ScholarCross Ref
- K. Havelund and G. Rosu. Monitoring Java Programs with Java PathExplorer. In Proceedings of Runtime Verification (RV'01), volume 55 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2001.Google Scholar
- K. Havelund and G. Rosu. Monitoring Programs using Rewriting. In Proceedings, International Conference on Automated Software Engineering (ASE'01), pages 135--143. IEEE, 2001. Google ScholarDigital Library
- K. Havelund and G. Rosu. Runtime Verification 2001, volume 55 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2001. Proceedings of a Computer Aided Verification (CAV'01) satellite workshop.Google Scholar
- K. Havelund and G. Rosu. Synthesizing monitors for safety properties. In Proceedings Tools and Algorithms for Construction and Analysis of Systems (TACAS'02), pages 342--356, 2002. Google ScholarDigital Library
- JTrek Compaq Corp. www.digital.com/java/download/jtrek/.Google Scholar
- M. Kim, S. Kannan, I. Lee, and O. Sokolsky. Java-MaC: a Run-time Assurance Tool for Java. In Proceedings of Runtime Verification (RV'01), volume 55 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2001.Google Scholar
- I. Lee, S. Kannan, M. Kim, O. Sokolsky, and M. Viswanathan. Runtime assurance based on formal specifications. In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 1999.Google Scholar
- Z. Manna and A. Pnueli. Temporal verification of reactive systems: Safety. Springer-Verlag N.Y., Inc., 1995. Google ScholarDigital Library
- F. Mattern. Virtual time and global states of distributed systems. In M. C. et. al., editor, Parallel and Distributed Algorithms: proceedings of the International Workshop on Parallel and Distributed Algorithms, pages 215--226. Elsevier science, 1989.Google Scholar
- K. Sen, G. Rosu, and G. Agha. Runtime safety analysis of multithreaded programs. Technical Report UIUCDCS-R-2003-2334, University of Illinois at Urnaba Champaign, April 2003. Google ScholarDigital Library
- S. D. Stoller. Detecting global predicates in distributed systems with clocks. In Proceedings of the 11th International Workshop on Distributed Algorithms (WDAG'97), pages 185--199, 1997. Google ScholarDigital Library
Index Terms
- Runtime safety analysis of multithreaded programs
Recommendations
Runtime safety analysis of multithreaded programs
Foundational and scalable techniques for runtime safety analysis of multithreaded programs are explored in this paper. A technique based on vector clocks to extract the causal dependency order on state updates from a running multithreaded program is ...
Online efficient predictive safety analysis of multithreaded programs
We present an automated and configurable technique for runtime safety analysis of multithreaded programs that is able to predict safety violations from successful executions. Based on a formal specification of safety properties provided by a user, our ...
Runtime Analysis of Atomicity for Multithreaded Programs
Atomicity is a correctness condition for concurrent systems. Informally, atomicity is the property that every concurrent execution of a set of transactions is equivalent to some serial execution of the same transactions. In multithreaded programs, ...
Comments