Skip to main content
SpringerLink
Log in

Modular Reasoning for Message-Passing Programs

  • Conference paper
Book cover Theoretical Aspects of Computing – ICTAC 2014 (ICTAC 2014)

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

Included in the following conference series:

Abstract

Verification of concurrent systems is difficult because of the inherent nondeterminism. Modern verification requires better locality and modularity. Reasoning of shared memory systems has gained much progress in these aspects. However, modular verification of distributed systems is still in demand. In this paper, we propose a new reasoning system for message-passing programs. It is a novel logic that supports Hoare style triples to specify and verify distributed programs modularly. We concretize the concept of event traces to represent interactions among distributed agents, and specify behaviors of agents by their local traces with regard to environmental assumptions. Based on trace semantics, the verification is compositional in both temporal and spatial dimensions. As an example, we show how to modularly verify an implementation of merging network.

Supported by NNSF of China, Grant No. 61272160, 61100061, and 61202069.

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. Bickford, M., Constable, R.L.: A causal logic of events in formalized computational type theory (2005)

    Google Scholar 

  2. Brookes, S.D.: A semantics for concurrent separation logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 16–34. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Charron-Bost, B., Mattern, F., Tel, G.: Synchronous, asynchronous, and causally ordered communication. Distributed Computing 9(4), 173–191 (1996)

    Article  MathSciNet  Google Scholar 

  4. de Roever, W.-P., de Boer, F., Hanneman, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press (January 2012)

    Google Scholar 

  5. Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  6. Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)

    Article  MATH  Google Scholar 

  7. Kahn, G.: The semantics of simple language for parallel programming. In: IFIP Congress, pp. 471–475 (1974)

    Google Scholar 

  8. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)

    Article  MATH  Google Scholar 

  9. Lei, J., Qiu, Z.: Modular reasoning for message-passing programs. Technical report, School of Mathematical Sciences, Peking University (June 2014), https://sites.google.com/site/jinjianglei/publications/rgdsep.

  10. Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)

    Book  Google Scholar 

  11. Milner, R.: Communication and concurrency. PHI Series in computer science. Prentice Hall (1989)

    Google Scholar 

  12. Milner, R.: The polyadic pi-calculus (abstract). In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, p. 1. Springer, Heidelberg (1992)

    Google Scholar 

  13. Milner, R.: Communicating and mobile systems - the Pi-calculus. Cambridge University Press (1999)

    Google Scholar 

  14. Parkinson, M.J., Bornat, R., Calcagno, C.: Variables as resource in hoare logics. In: LICS, pp. 137–146 (2006)

    Google Scholar 

  15. Reddy, U.S., Reynolds, J.C.: Syntactic control of interference for separation logic. In: POPL, pp. 323–336 (2012)

    Google Scholar 

  16. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)

    Google Scholar 

  17. Vafeiadis, V., Parkinson, M.J.: A marriage of rely/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Villard, J., Lozes, É., Calcagno, C.: Proving copyless message passing. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 194–209. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  19. Wehrman, I., Hoare, C.A.R., O’Hearn, P.W.: Graphical models of separation logic. Inf. Process. Lett. 109(17), 1001–1004 (2009)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LMAM and Department of Informatics, School of Math, Peking University, P.R. China

    Jinjiang Lei & Zongyan Qiu

Authors
  1. Jinjiang Lei
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zongyan Qiu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Computer Science, Romanian Academy, Blvd. King Carol I no.8, 700505, Iaşi, Romania

    Gabriel Ciobanu

  2. LORIA, Université de Lorraine, Campus Scientifique, BP 239, 54506, Vandœvre-lès-Nancy, France

    Dominique Méry

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Lei, J., Qiu, Z. (2014). Modular Reasoning for Message-Passing Programs. In: Ciobanu, G., Méry, D. (eds) Theoretical Aspects of Computing – ICTAC 2014. ICTAC 2014. Lecture Notes in Computer Science, vol 8687. Springer, Cham. https://doi.org/10.1007/978-3-319-10882-7_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10882-7_17

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10881-0

  • Online ISBN: 978-3-319-10882-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation