SACS | Rely-Guarantee Based Reasoning for Message-Passing Programs

Published in Volume XXIV, Issue 2, 2014, pages 217-252, doi: 10.7561/SACS.2014.2.217

Authors: J. Lei, Z. Qiu

Abstract

The difficulties of verifying concurrent programs lie in their inherent non-determinism and interferences. Rely-Guarantee reasoning is one useful approach to solve this problem for its capability in formally specifying inter- thread interferences. However, modern verification requires better locality and modularity. It is still a great challenge to verify a message-passing program in a modular and composable way.

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 behav- iors of agents by their local traces with regard to environmental assumptions — an idea inspired by Rely-Guarantee reasoning. Based on trace semantics, the verification is compositional in both temporal and spatial dimensions. To show validity, we apply our logic to modularly prove several examples.

Full Text (PDF)

References

[1] Mark Bickford and Robert L. Constable. A causal logic of events in formalized computational type theory. Technical report, Cornell University, 2005.

[2] Stephen D. Brookes. A semantics for concurrent separation logic. In Philippa Gardner and Nobuko Yoshida, editors, Proceedings of the 15th International Conference on Concurrency Theory (CONCUR 2004), volume 3170 of Lecture Notes in Computer Science, pages 16–34. Springer, 2004. http://dx.doi.org/10.1007/978-3-540-28644-8_2 .

[3] Bernadette Charron-Bost, Friedemann Mattern, and Gerard Tel. Synchronous, asynchronous, and causally ordered communication. Distributed Computing, 9(4):173–191, 1996. http://dx.doi.org/10.1007/s004460050018 .

[4] Willem-Paul de Roever, Frank de Boer, Ulrich Hanneman, Jozef Hooman, Yassine Lakhnech, Mannes Poel, and Job Zwiers. Concurrency Verifica- tion: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press, January 2012.

[5] Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkin- son, and Viktor Vafeiadis. Concurrent abstract predicates. In Theo D’Hondt, editor, Proceedings of the 24th European Conference on Object- Oriented Programming (ECOOP 2010), volume 6183 of Lecture Notes in Computer Science, pages 504–528. Springer, 2010. http://dx.doi.org/10.1007/978-3-642-14107-2_24 .

[6] Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In Rocco De Nicola, editor, Proceedings of the 16th European Symposium on Programming (ESOP 2007), volume 4421 of Lecture Notes in Computer Science, pages 173–188. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-71316-6_13 .

[7] C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, 1978. http://dx.doi.org/10.1145/359576.359585 .

[8] Cliff B. Jones. Tentative steps toward a development method for interfer- ing programs. ACM Transactions on Programming Languages and System, 5(4):596–619, 1983. http://dx.doi.org/10.1145/69575.69577 .

[9] Gilles Kahn. The semantics of simple language for parallel programming. In IFIP Congress, pages 471–475, 1974.

[10] Leslie Lamport. Time, clocks, and the ordering of events in a distributed sys- tem. Communications of the ACM, 21(7):558–565, 1978. http://dx.doi.org/10.1145/359545.359563 .

[11] Jinjiang Lei and Zongyan Qiu. Modular reasoning for message-passing programs. In Gabriel Ciobanu and Dominique Me´ry, editors, Proceedings of the 11th International Colloquium on Theoretical Aspects of Computing (ICTAC 2014), volume 8687 of Lecture Notes in Computer Science, pages 277–294. Springer, 2014. http://dx.doi.org/10.1007/978-3-319-10882-7_17 .

[12] Jinjiang Lei and Zongyan Qiu. Modular reasoning for message-passing programs. Technical report, School of Mathematical Sciences, Peking Univer- sity, Sep 2014. Available from: hhttps://sites.google.com/site/jinjianglei/publications/rgdsep_journal.

[13] Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. http://dx.doi.org/10.1007/3-540-10235-3 .

[14] RRobin Milner. Communication and Concurrency. PHI Series in computer science. Prentice Hall, 1989.

[15] Robin Milner. The polyadic pi-calculus (abstract). In Rance Cleaveland, editor, Proceedings of the Third International Conference on Concurrency Theory (CONCUR 1992), volume 630 of Lecture Notes in Computer Science, page 1. Springer, 1992. http://dx.doi.org/10.1007/BFb0084778 .

[16] Robin Milner. Communicating and mobile systems – the Pi-calculus. Cam- bridge University Press, 1999.

[17] Matthew J. Parkinson, Richard Bornat, and Cristiano Calcagno. Variables as resource in Hoare logics. In Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), pages 137–146. IEEE Computer Society, 2006. http://dx.doi.org/10.1109/LICS.2006.52 .

[18] Uday S. Reddy and John C. Reynolds. Syntactic control of interference for separation logic. In John Field and Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012), pages 323–336. ACM, 2012. http://dx.doi.org/10.1145/2103656.2103695 .

[19] John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pages 55–74. IEEE Computer Society, 2002. http://dx.doi.org/10.1109/LICS.2002.1029817 .

[20] Viktor Vafeiadis and Matthew J. Parkinson. A marriage of rely/guarantee and separation logic. In Luís Caires and Vasco Thudichum Vasconcelos, editors, Proceedings of the 18th International Conference on Concurrency Theory (CONCUR 2007), volume 4703 of Lecture Notes in Computer Science, pages 256–271. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-74407-8_18 .

[21] Jules Villard, Étienne Lozes, and Cristiano Calcagno. Proving copyless message passing. In Zhenjiang Hu, editor, Proceedings of the 7th Asian Symposium on Programming Languages and Systems (APLAS’09), volume 5904 of Lecture Notes in Computer Science, pages 194–209. Springer, 2009. http://dx.doi.org/10.1007/978-3-642-10672-9_15 .

[22] Ian Wehrman, C. A. R. Hoare, and Peter W. O’Hearn. Graphical models of separation logic. Information Processing Letters, 109(17):1001–1004, 2009. http://dx.doi.org/10.1016/j.ipl.2009.06.003 .

Bibtex

@article{sacscuza:lei2014rbrfmp,
  title={Rely-Guarantee Based Reasoning for Message-Passing Programs},
  author={J. Lei and Z. Qiu},
  journal={Scientific Annals of Computer Science},
  volume={24},
  number={2},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2014},
  pages={217--252},
  doi={10.7561/SACS.2014.2.217},
  publisher={``A.I. Cuza'' University Press}
}