Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Process-Local Static Analysis of Synchronous Processes

  • Conference paper
  • First Online:
Static Analysis (SAS 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11002))

Included in the following conference series:

Abstract

We develop a modular approach to statically analyse imperative processes communicating by synchronous message passing. The approach is modular in that it only needs to analyze one process at a time, but will in general have to do so repeatedly. The approach combines lattice-valued regular expressions to capture network communication with a dedicated shuffle operator for composing individual process analysis results. We present both a soundness proof and a prototype implementation of the approach for a synchronous subset of the Go programming language. Overall our approach tackles the combinatorial explosion of concurrent programs by suitable static analysis approximations, thereby lifting traditional sequential analysis techniques to a concurrent setting.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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 EPUB and 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

Similar content being viewed by others

Notes

  1. 1.

    The product with singleton sets \(\{ \mathtt {!} \}\) and \(\{ \mathtt {?} \}\) is just presentational: one component denotes writes and another component denotes reads.

References

  1. Botbol, V., Chailloux, E., Le Gall, T.: Static analysis of communicating processes using symbolic transducers. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 73–90. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52234-0_5

    Chapter  Google Scholar 

  2. Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964)

    Article  MathSciNet  Google Scholar 

  3. Colby, C.: Analyzing the communication topology of concurrent programs. In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 202–213 (1995)

    Google Scholar 

  4. Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming, pp. 106–130. Dunod, France (1976)

    Google Scholar 

  5. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, pp. 238–252 (1977)

    Google Scholar 

  6. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages, pp. 269–282 (1979)

    Google Scholar 

  7. Cousot, P., Cousot, R.: Semantic analysis of communicating sequential processes. In: de Bakker, J., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 119–133. Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10003-2_65

    Chapter  MATH  Google Scholar 

  8. Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002)

    Book  Google Scholar 

  9. Feret, J.: Confidentiality analysis of mobile systems. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 135–154. Springer, Heidelberg (2000). https://doi.org/10.1007/978-3-540-45099-3_8

    Chapter  MATH  Google Scholar 

  10. Giachino, E., Kobayashi, N., Laneve, C.: Deadlock analysis of unbounded process networks. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 63–77. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44584-6_6

    Chapter  Google Scholar 

  11. Grätzer, G.: General Lattice Theory. Pure and Applied Mathematics. Academic Press, New York (1978)

    Book  Google Scholar 

  12. Igarashi, A., Kobayashi, N.: Type-based analysis of communication for concurrent programming languages. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol. 1302, pp. 187–201. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0032742

    Chapter  Google Scholar 

  13. Kobayashi, N.: Type-based information flow analysis for the pi-calculus. Acta Informatica 42(4–5), 291–347 (2005)

    Article  MathSciNet  Google Scholar 

  14. Kobayashi, N.: A new type system for deadlock-free processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 233–247. Springer, Heidelberg (2006). https://doi.org/10.1007/11817949_16

    Chapter  Google Scholar 

  15. Kobayashi, N., Sangiorgi, D.: A hybrid type system for lock-freedom of mobile processes. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 80–93. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_10

    Chapter  Google Scholar 

  16. Lange, J., Ng, N., Toninho, B., Yoshida, N.: Fencing off go: liveness and safety for channel-based programming. In: Proceedings of the 44th Annual ACM Symposium on Principles of Programming Languages, pp. 748–761 (2017)

    Google Scholar 

  17. Le Gall, T., Jeannet, B.: Lattice automata: a representation for languages on infinite alphabets, and some applications to verification. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 52–68. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74061-2_4

    Chapter  Google Scholar 

  18. Logozzo, F.: Separate compositional analysis of class-based object-oriented languages. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 334–348. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27815-3_27

    Chapter  Google Scholar 

  19. Mercouroff, N.: An algorithm for analyzing communicating processes. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1991. LNCS, vol. 598, pp. 312–325. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55511-0_16

    Chapter  Google Scholar 

  20. Midtgaard, J., Nielson, F., Nielson, H.R.: Iterated process analysis over lattice-valued regular expressions. In: PPDP 2016: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, pp. 132–145 (2016)

    Google Scholar 

  21. Midtgaard, J., Nielson, F., Nielson, H.R.: A parametric abstract domain for lattice-valued regular expressions. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 338–360. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53413-7_17

    Chapter  Google Scholar 

  22. Miné, A.: Relational thread-modular static value analysis by abstract interpretation. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 39–58. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54013-4_3

    Chapter  MATH  Google Scholar 

  23. Ng, N., Yoshida, N.: Static deadlock detection for concurrent go by global session graph synthesis. In: Proceedings of the 25th International Conference on Compiler Construction, CC 2016, pp. 174–184. ACM (2016)

    Google Scholar 

  24. Nielson, F., Nielson, H.R.: Higher-order concurrent programs with finite communication topology. In: Proceedings of the 21st Annual ACM Symposium on Principles of Programming Languages, pp. 84–97 (1994)

    Google Scholar 

  25. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999). https://doi.org/10.1007/978-3-662-03811-6

    Book  MATH  Google Scholar 

  26. Owens, S., Reppy, J., Turon, A.: Regular-expression derivatives re-examined. J. Funct. Program. 19(2), 173–190 (2009)

    Article  MathSciNet  Google Scholar 

  27. Reppy, J.: Concurrent Programming in ML. Cambridge University Press, Cambridge (1999)

    Book  Google Scholar 

  28. Rydhof Hansen, R., Jensen, J.G., Nielson, F., Nielson, H.R.: Abstract interpretation of mobile ambients. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 134–148. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48294-6_9

    Chapter  Google Scholar 

  29. Skalka, C., Smith, S., Van Horn, D.: Types and trace effects of higher order programs. J. Funct. Program. 18(2), 179–249 (2008)

    Article  MathSciNet  Google Scholar 

  30. Stadtmüller, K., Sulzmann, M., Thiemann, P.: Static trace-based deadlock analysis for synchronous mini-go. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 116–136. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47958-3_7

    Chapter  Google Scholar 

  31. Sulzmann, M., Thiemann, P.: Derivatives for regular shuffle expressions. In: Dediu, A.-H., Formenti, E., Martín-Vide, C., Truthe, B. (eds.) LATA 2015. LNCS, vol. 8977, pp. 275–286. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-15579-1_21

    Chapter  MATH  Google Scholar 

  32. Sulzmann, M., Thiemann, P.: Forkable regular expressions. In: Dediu, A.-H., Janoušek, J., Martín-Vide, C., Truthe, B. (eds.) LATA 2016. LNCS, vol. 9618, pp. 194–206. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-30000-9_15

    Chapter  Google Scholar 

  33. Tarjan, R.E.: Fast algorithms for solving path problems. J. ACM 28(3), 594–614 (1981)

    Article  MathSciNet  Google Scholar 

  34. Venet, A.: Automatic determination of communication topologies in mobile systems. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 152–167. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-49727-7_9

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The Maersk Mc-Kinney Moller Institute, University of Southern Denmark, Odense, Denmark

    Jan Midtgaard

  2. DTU Compute, Technical University of Denmark, Kongens Lyngby, Denmark

    Flemming Nielson & Hanne Riis Nielson

Authors
  1. Jan Midtgaard
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Flemming Nielson
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Hanne Riis Nielson
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jan Midtgaard .

Editor information

Editors and Affiliations

  1. Universität Freiburg, Freiburg, Germany

    Andreas Podelski

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Midtgaard, J., Nielson, F., Nielson, H.R. (2018). Process-Local Static Analysis of Synchronous Processes. In: Podelski, A. (eds) Static Analysis. SAS 2018. Lecture Notes in Computer Science(), vol 11002. Springer, Cham. https://doi.org/10.1007/978-3-319-99725-4_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-99725-4_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-99724-7

  • Online ISBN: 978-3-319-99725-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation