Local rely-guarantee reasoning

ABSTRACT

Rely-Guarantee reasoning is a well-known method for verification of shared-variable concurrent programs. However, it is difficult for users to define rely/guarantee conditions, which specify threads' behaviors over the whole program state. Recent efforts to combine Separation Logic with Rely-Guarantee reasoning have made it possible to hide thread-local resources, but the shared resources still need to be globally known and specified. This greatly limits the reuse of verified program modules.

In this paper, we propose LRG, a new Rely-Guarantee-based logic that brings local reasoning and information hiding to concurrency verification. Our logic, for the first time, supports a frame rule over rely/guarantee conditions so that specifications of program modules only need to talk about the resources used locally, and the verified modules can be reused in different threads without redoing the proof. Moreover, we introduce a new hiding rule to hide the resources shared by a subset of threads from the rest in the system. The support of information hiding not only improves the modularity of Rely-Guarantee reasoning, but also enables the sharing of dynamically allocated resources, which requires adjustment of rely/guarantee conditions.

REFERENCES

• 1: Nick Benton. Abstracting allocation : The new new thing. In Proc. Computer Science Logic (CSL'06), volume 4207 of phLecture Notes in Computer Science, pages 182--196. Springer, September 2006.
• 2: Richard Bornat , Cristiano Calcagno , Peter O'Hearn , Matthew Parkinson, Permission accounting in separation logic, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.259-270, January 12-14, 2005, Long Beach, California, USA
• 3: Stephen Brookes, A semantics for concurrent separation logic, Theoretical Computer Science, v.375 n.1-3, p.227-270, April, 2007 [doi>10.1016/j.tcs.2006.12.034]
• 4: Cristiano Calcagno , Peter W. O'Hearn , Hongseok Yang, Local Action and Abstract Separation Logic, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, p.366-378, July 10-14, 2007 [doi>10.1109/LICS.2007.30]
• 5: Cristiano Calcagno, Matthew J. Parkinson, and Viktor Vafeiadis. Modular safety checking for fine-grained concurrency. In Proc. 14th Int'l Symposium on Static Analysis (SAS'07), volume 4634 of phLecture Notes in Computer Science, pages 233--248. Springer, August 2007.
• 6: Concurrency verification: introduction to compositional and noncompositional methods, Cambridge University Press, New York, NY, 2001
• 7: Xinyu Feng. Local rely-guarantee reasoning (extended version). Technical Report TTIC-TR-2008-1, Toyota Technological Institute at Chicago, Chicago, IL, U.S.A., October 2008. http://www.tti-c.org/technical_reports/ttic-tr-2008-1.pdf.
• 8: Xinyu Feng , Zhong Shao, Modular verification of concurrent assembly code with dynamic thread creation and termination, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 9: Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In Proc. 16th European Symp. on Prog. (ESOP'07), volume 4421 of phLecture Notes in Computer Science, pages 173--188. Springer, March 2007.
• 10: Cormac Flanagan , Stephen N. Freund , Shaz Qadeer , Sanjit A. Seshia, Modular verification of multithreaded programs, Theoretical Computer Science, v.338 n.1-3, p.153-183, 10 June 2005 [doi>10.1016/j.tcs.2004.12.006]
• 11: Alexey Gotsman , Byron Cook , Matthew Parkinson , Viktor Vafeiadis, Proving that non-blocking algorithms don't block, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
• 12: Maurice Herlihy and Nir Shavit. The Art of Multiprocessor Programming. Morgan Kaufmann Publishers, March 2008.
• 13: Samin S. Ishtiaq , Peter W. O'Hearn, BI as an assertion language for mutable data structures, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-26, January 2001, London, United Kingdom
• 14: C. B. Jones, Tentative steps toward a development method for interfering programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.4, p.596-619, Oct. 1983 [doi>10.1145/69575.69577]
• 15: C. B. Jones, Wanted: a compositional approach to concurrency, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
• 16: Ioannis T. Kassios. Dynamic frames: Support for framing, dependencies and sharing without restrictions. In Proc. 14th International Symposium on Formal Methods (FM'06), volume 4085 of phLecture Notes in Computer Science, pages 268--283. Springer, August 2006.
• 17: Maged M. Michael, Hazard Pointers: Safe Memory Reclamation for Lock-Free Objects, IEEE Transactions on Parallel and Distributed Systems, v.15 n.6, p.491-504, June 2004 [doi>10.1109/TPDS.2004.8]
• 18: Peter W. OHearn, Resources, concurrency, and local reasoning, Theoretical Computer Science, v.375 n.1-3, p.271-307, April, 2007 [doi>10.1016/j.tcs.2006.12.035]
• 19: Peter W. O'Hearn , Hongseok Yang , John C. Reynolds, Separation and information hiding, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 14-16, 2004, Venice, Italy
• 20: Matthew Parkinson , Richard Bornat , Cristiano Calcagno, Variables as Resource in Hoare Logics, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.137-146, August 12-15, 2006 [doi>10.1109/LICS.2006.52]
• 21: Matthew Parkinson , Richard Bornat , Peter O'Hearn, Modular verification of a non-blocking stack, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 22: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 23: Viktor Vafeiadis. Modular Fine-Grained Concurrency Verification. PhD thesis, University of Cambridge, July 2007.
• 24: Viktor Vafeiadis and Matthew J. Parkinson. A marriage of rely/guarantee and separation logic. In Proc. 18th Int'l Conf. on Concurrency Theory (CONCUR'07), volume 4703 of phLecture Notes in Computer Science, pages 256--271, September 2007.
• 25: Hongseok Yang, Relational separation logic, Theoretical Computer Science, v.375 n.1-3, p.308-334, April, 2007 [doi>10.1016/j.tcs.2006.12.036]
• 26: Hongseok Yang , Peter W. O'Hearn, A Semantic Basis for Local Reasoning, Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, p.402-416, April 08-12, 2002
• 27: Dachuan Yu , Zhong Shao, Verification of safety properties for concurrent assembly code, Proceedings of the ninth ACM SIGPLAN international conference on Functional programming, September 19-21, 2004, Snow Bird, UT, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Theory, Verification

Keywords:
concurrency, information hiding, local reasoning, rely-guarantee reasoning, separation logic