Abstract
The use of shared mutable state, commonly seen in object-oriented systems, is often problematic due to the potential conflicting interactions between aliases to the same state. We present a substructural type system outfitted with a novel lightweight interference control mechanism, rely-guarantee protocols, that enables controlled aliasing of shared resources. By assigning each alias separate roles, encoded in a novel protocol abstraction in the spirit of rely-guarantee reasoning, our type system ensures that challenging uses of shared state will never interfere in an unsafe fashion. In particular, rely-guarantee protocols ensure that each alias will never observe an unexpected value, or type, when inspecting shared memory regardless of how the changes to that shared state (originating from potentially unknown program contexts) are interleaved at run-time.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ahmed, A., Fluet, M., Morrisett, G.: L3: A linear language with locations. Fundam. Inf. (2007)
Beckman, N.E., Bierhoff, K., Aldrich, J.: Verifying correct usage of atomic blocks and typestate. In: OOPSLA (2008)
Beckman, N.E., Kim, D., Aldrich, J.: An empirical study of object protocols in the wild. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol. 6813, pp. 2–26. Springer, Heidelberg (2011)
Bierhoff, K., Aldrich, J.: Modular typestate checking of aliased objects. In: OOPSLA (2007)
Caires, L., Seco, J.A.C.: The type discipline of behavioral separation. In: POPL (2013)
Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: Proc. Logic in Computer Science (2007)
DeLine, R., Fähndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 465–490. Springer, Heidelberg (2004)
Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL (2013)
Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504–528. Springer, Heidelberg (2010)
Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-guarantee reasoning. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 363–377. Springer, Heidelberg (2009)
Fähndrich, M., DeLine, R.: Adoption and focus: practical linear types for imperative programming. In: PLDI (2002)
Fähndrich, M., Leino, K.R.M.: Heap monotonic typestate. In: IWACO (2003)
Gay, S.J., Vasconcelos, V.T., Ravara, A., Gesbert, N., Caldeira, A.Z.: Modular session types for distributed object-oriented programming. In: POPL (2010)
Girard, J.-Y.: Linear logic. Theor. Comput. Sci. (1987)
Gordon, C.S., Ernst, M.D., Grossman, D.: Rely-guarantee references for refinement types over aliased mutable data. In: PLDI (2013)
Jensen, J.B., Birkedal, L.: Fictional separation logic. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 377–396. Springer, Heidelberg (2012)
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. (1983)
Krishnaswami, N.R., Turon, A., Dreyer, D., Garg, D.: Superficially substructural types. In: ICFP (2012)
Leino, K.R.M., Müller, P.: A basis for verifying multi-threaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 378–393. Springer, Heidelberg (2009)
Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: ICFP (2003)
Militão, F., Aldrich, J., Caires, L.: Rely-guarantee protocols (technical report). CMU-CS-14-107 (2014)
Militão, F., Aldrich, J., Caires, L.: Substructural typestates. In: PLPV (2014)
Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL (2005)
Pilkiewicz, A., Pottier, F.: The essence of monotonic state. In: TLDI (2011)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. Logic in Computer Science (2002)
Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. In: Proc. LISP and Functional Programming (1992)
Smith, F., Walker, D.W., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 366–381. Springer, Heidelberg (2000)
Strom, R.E.: Mechanisms for compile-time enforcement of security. In: POPL (1983)
Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Eng. (1986)
Svendsen, K., Birkedal, L., Parkinson, M.: Modular reasoning about separation of concurrent data structures. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems. LNCS, vol. 7792, pp. 169–188. Springer, Heidelberg (2013)
Tov, J.A., Pucella, R.: Practical affine types. In: POPL (2011)
Vafeiadis, V., Parkinson, M.: 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)
Yorsh, G., Skidanov, A., Reps, T., Sagiv, M.: Automatic assume/guarantee reasoning for heap-manipulating programs. Electron. Notes Theor. Comput. Sci. (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Militão, F., Aldrich, J., Caires, L. (2014). Rely-Guarantee Protocols. In: Jones, R. (eds) ECOOP 2014 – Object-Oriented Programming. ECOOP 2014. Lecture Notes in Computer Science, vol 8586. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44202-9_14
Download citation
DOI: https://doi.org/10.1007/978-3-662-44202-9_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44201-2
Online ISBN: 978-3-662-44202-9
eBook Packages: Computer ScienceComputer Science (R0)