Abstract
In the quest for tractable methods for reasoning about concurrent algorithms both rely/guarantee logic and separation logic have made great advances. They both seek to tame, or control, the complexity of concurrent interactions, but neither is the ultimate approach. Rely-guarantee copes naturally with interference, but its specifications are complex because they describe the entire state. Conversely separation logic has difficulty dealing with interference, but its specifications are simpler because they describe only the relevant state that the program accesses.
We propose a combined system which marries the two approaches. We can describe interference naturally (using a relation as in rely/guarantee), and where there is no interference, we can reason locally (as in separation logic). We demonstrate the advantages of the combined approach by verifying a lock-coupling list algorithm, which actually disposes/frees removed nodes.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. Prog. Lang. Syst. 17(3), 507–534 (1995)
Bornat, R., Calcagno, C., Yang, H.: Variables as resource in separation logic. ENTCS 155, 247–276 (2006)
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)
Calcagno, C., Gardner, P., Zarfaty, U.: Context logic as modal logic: completeness and parametric inexpressivity. In: POPL, pp. 123–134. ACM Press, New York (2007)
Calcagno, C., O’Hearn, P., Yang, H.: Local action and abstract separation logic. LICS (to appear, 2007)
Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: SAS. LNCS, Springer, Heidelberg (2007)
Coleman, J.W., Jones, C.B.: A structural proof of the soundness of rely/guarantee rules. Technical Report CS-TR-987, Newcastle University (October 2006)
Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. In: Proceedings of ESOP (2007)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Hoare, C.A.R.: Towards a theory of parallel programming. Operating Systems Techniques (1971)
Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)
Jones, C.B.: Wanted: a compositional approach to concurrency, pp. 5–15. Springer, New York (2003)
Morgan, C.: The specification statement. ACM Trans. Program. Lang. Syst. 10(3), 403–419 (1988)
O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Proceedings of CSL, pp. 1–19 (2001)
O’Hearn, P.W.: Resources, concurrency and local reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 49–67. Springer, Heidelberg (2004)
Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica 6, 319–340 (1976)
Parkinson, M.J., Bornat, R., O’Hearn, P.W.: Modular verification of a non-blocking stack. In: POPL (2007)
Prensa Nieto, L.: The rely-guarantee method in Isabelle/HOL. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 348–362. Springer, Heidelberg (2003)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, Washington, DC, USA, pp. 55–74. IEEE Computer Society Press, Los Alamitos (2002)
Reynolds, J.C.: Toward a grainless semantics for shared-variable concurrency. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 35–48. Springer, Heidelberg (2004)
Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: PPoPP, ACM Press, New York (2006)
Vafeiadis, V., Parkinson, M.: A marriage of rely/guarantee and separation logic. Technical Report UCAM-CL-TR-687, University of Cambridge (June 2007), http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-687.html
Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing 9(2), 149–174 (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vafeiadis, V., Parkinson, M. (2007). A Marriage of Rely/Guarantee and Separation Logic. In: Caires, L., Vasconcelos, V.T. (eds) CONCUR 2007 – Concurrency Theory. CONCUR 2007. Lecture Notes in Computer Science, vol 4703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74407-8_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-74407-8_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74406-1
Online ISBN: 978-3-540-74407-8
eBook Packages: Computer ScienceComputer Science (R0)