nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Process-Local Static Analysis of Synchronous Processes

verfasst von : Jan Midtgaard, Flemming Nielson, Hanne Riis Nielson

Erschienen in: Static Analysis

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Verifying Bounded Subset-Closed Hyperproperties

Nächstes Kapitel The Impact of Program Transformations on Static Program Analysis

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

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_5CrossRef

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

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)

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)

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)

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)

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_65CrossRefMATH

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

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_8CrossRefMATH

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_6CrossRef

11.

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

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/BFb0032742CrossRef

13.

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

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_16CrossRef

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_10CrossRef

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)

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_4CrossRef

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_27CrossRef

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_16CrossRef

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)

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_17CrossRef

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_3CrossRefMATH

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)

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)

25.

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

26.

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

27.

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

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_9CrossRef

29.

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

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_7CrossRef

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_21CrossRefMATH

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_15CrossRef

33.

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

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_9CrossRef

Titel: Process-Local Static Analysis of Synchronous Processes
verfasst von: Jan Midtgaard
Flemming Nielson
Hanne Riis Nielson
Verlag: Springer International Publishing
Buch: Static Analysis
Print ISBN: 978-3-319-99724-7

Electronic ISBN: 978-3-319-99725-4

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-99725-4_18

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"