Abstract
An automated and configurable technique for runtime safety analysis of multithreaded programs is presented, which is able to predict safety violations from successful executions. Based on a user provided safety formal specification, the program is automatically instrumented to emit relevant state update events to an observer, which further checks them against the safety specification. The events are stamped with dynamic vector clocks, enabling the observer to infer a causal partial order on the state updates. All event traces that are consistent with this partial order, including the actual execution trace, are analyzed on-line and in parallel, and a warning is issued whenever there is a trace violating the specification. This technique can be therefore seen as a bridge between testing and model checking. To further increase scalability, a window in the state space can be specified, allowing the observer to infer the most probable runs. If the size of the window is 1 then only the received execution trace is analyzed, like in testing; if the size of the window is ∞ then all the execution traces are analyzed, such as in model checking.
Chapter PDF
Similar content being viewed by others
References
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-Based Runtime Verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004) (to appear), http://www.cs.man.ac.uk/cspreprints/PrePrints/cspp24.pdf
Cain, H.W., Lipasti, M.H.: Verifying sequential consistency using vector clocks. In: Proceedings of the 14th annual ACM Symposium on Parallel Algorithms and Architectures, pp. 153–154. ACM, New York (2002)
Dahm, M.: Byte code engineering with the bcel api. Technical Report B-17-98, Freie Universit at Berlin, Institut für Informatik (April 2001)
Fidge, C.J.: Partial orders for parallel debugging. In: Proceedings of the 1988 ACM SIGPLAN and SIGOPS workshop on Parallel and Distributed debugging, pp. 183–194. ACM, New York (1988)
Havelund, K., Roşu, G.: Monitoring Java Programs with Java PathExplorer. In: Proceedings of the 1st Workshop on Runtime Verification (RV 2001). Electronic Notes in Theoretical Computer Science, vol. 55, Elsevier Science, Amsterdam (2001)
Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002)
Kim, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a Run-time Assurance Tool for Java. In: Proceedings of the 1st Workshop on Runtime Verification (RV 2001). Electronic Notes in Theoretical Computer Science, vol. 55, Elsevier Science, Amsterdam (2001)
Marzullo, K., Neiger, G.: Detection of global state predicates. In: Proceedings of the 5th International Workshop on Distributed Algorithms (WADG 1991). LNCS, vol. 579, pp. 254–272. Springer, Heidelberg (1991)
Mattern, F.: Virtual time and global states of distributed systems. In: Parallel and Distributed Algorithms: proceedings of the International Workshop on Parallel and Distributed Algorithms, pp. 215–226. Elsevier, Amsterdam (1989)
Sen, A., Garg, V.K.: Partial order trace analyzer (pota) for distrubted programs. In: Proceedings of the 3rd Workshop on Runtime Verification (RV 2003). Electronic Notes in Theoretical Computer Science (2003)
Sen, K., Roşu, G.: Generating optimal monitors for extended regular expressions. In: Proceedings of the 3rd Workshop on Runtime Verification (RV 2003). ENTCS, vol. 89, pp. 162–181. Elsevier Science, Amsterdam (2003)
Sen, K., Roşu, G., Agha, G.: Java MultiPathExplorer (JMPaX 2.0), Download: http://fsl.cs.uiuc.edu/jmpax
Sen, K., Roşu, G., Agha, G.: Generating Optimal Linear Temporal Logic Monitors by Coinduction. In: Saraswat, V.A. (ed.) ASIAN 2003. LNCS, vol. 2896, pp. 260–275. Springer, Heidelberg (2003)
Sen, K., Roşu, G., Agha, G.: Runtime safety analysis of multithreaded programs. In: Proceedings of 4th joint European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003), ACM, New York (2003)
Sen, K., Roşu, G., Agha, G.: Runtime safety analysis of multithreaded programs. Technical Report UIUCDCS-R-2003-2334, University of Illinois at Urnaba Champaign (April 2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sen, K., Roşu, G., Agha, G. (2004). Online Efficient Predictive Safety Analysis of Multithreaded Programs. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive