Skip to main content
SpringerLink
Log in

One Stack to Run Them All

Reducing Concurrent Analysis to Sequential Analysis under Priority Scheduling

  • Conference paper
Book cover Model Checking Software (SPIN 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6349))

Included in the following conference series:

Abstract

We present a reduction from a concurrent real-time program with priority preemptive scheduling to a sequential program that has the same set of behaviors. Whereas many static analyses of concurrent programs are undecidable, our reduction enables the application of any sequential program analysis to be applied to a concurrent real-time program with priority preemptive scheduling.

Supported by NSF under grants CCF-0811631 and CCF-0701832.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Godefroid, P., Klarlund, N., Sen, K.: Dart: Directed automated random testing. In: PLDI 2005: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 213–223. ACM, New York (2005)

    Chapter  Google Scholar 

  2. Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: Exe: Automatically generating inputs of death. ACM Trans. Inf. Syst. Secur. 12(2), 1–38 (2008)

    Article  Google Scholar 

  3. Cadar, C., Dunbar, D., Engler, D.R.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Symposium on Operating Systems Design and Implementation, pp. 209–224. USENIX Association (2008)

    Google Scholar 

  4. Sha, L., Rajkumar, R., Lehoczky, J.P.: Priority inheritance protocols: An approach to real-time synchronization. IEEE Trans. Comput. 39(9), 1175–1185 (1990)

    Article  MathSciNet  Google Scholar 

  5. Ball, T., Rajamani, S.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  6. Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Symposium on Principles of Programming Languages, pp. 58–70. ACM, New York (2002)

    Google Scholar 

  7. Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  8. Kahlon, V., Ivancic, F., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 505–518. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. Kahlon, V., Gupta, A.: On the analysis of interacting pushdown systems. In: Symposium on Principles of Programming Languages, pp. 303–314. ACM, New York (2007)

    Google Scholar 

  10. Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technische Universität München (2002)

    Google Scholar 

  11. Kidd, N., Lal, A., Reps, T.: Language strength reduction. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 283–298. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  13. Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Elec. Notes in Theor. Comp. Sci. 9 (1997)

    Google Scholar 

  14. Lal, A., Reps, T.: Reducing concurrent analysis under a context bound to sequential analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 37–51. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  15. Walukiewicz, I.: Model checking CTL properties of pushdown systems. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 127–138. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  16. Ball, T., Rajamani, S.K.: Bebop: a path-sensitive interprocedural dataflow engine. In: PASTE 2001: Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, pp. 97–103. ACM, New York (2001)

    Chapter  Google Scholar 

  17. Kidd, N., Jagannathan, S., Vitek, J.: One stack to run them all. Technical Report 10-005, Purdue University (May 2010)

    Google Scholar 

  18. Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: POPL 2007: Proceedings of the 34th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 339–350. ACM, New York (2007)

    Google Scholar 

  19. Atig, M.F., Bouajjani, A., Touili, T.: Analyzing asynchronous programs with preemption. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum Fuer Informatik, pp. 37–48 (2008)

    Google Scholar 

  20. Qadeer, S., Wu, D.: Kiss: Keep it simple and sequential. In: PLDI 2004: Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, pp. 14–24. ACM, New York (2004)

    Chapter  Google Scholar 

  21. Lindstrom, G., Mehlitz, P.C., Visser, W.: Model checking real-time java using java pathfinder. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 444–456. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  22. The Java PathFinder Team: Java PathFinder (2010), http://babelfish.arc.nasa.gov/trac/jpf/

  23. Bollella, G., Gosling, J., Brosgol, B., Dibble, P., Furr, S., Turnbull, M.: The Real-Time Specification for Java. Addison-Wesley, Reading (2000)

    Google Scholar 

  24. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Purdue University, USA

    Nicholas Kidd, Suresh Jagannathan & Jan Vitek

Authors
  1. Nicholas Kidd
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Suresh Jagannathan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jan Vitek
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Formal Methods and Tools, Department of Computer Science, University of Twente, P.O. Box 217, 7500AE, Enschede, The Netherlands

    Jaco van de Pol  & Michael Weber  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kidd, N., Jagannathan, S., Vitek, J. (2010). One Stack to Run Them All. In: van de Pol, J., Weber, M. (eds) Model Checking Software. SPIN 2010. Lecture Notes in Computer Science, vol 6349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16164-3_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16164-3_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16163-6

  • Online ISBN: 978-3-642-16164-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation