Abstract
We present an imperative object calculus where types are annotated with two modifiers for aliasing control. The \({\mathtt{lent}}\) modifier prevents objects to be aliased, whereas the \({\mathtt{capsule}}\) modifier characterizes expressions that will reduce to isolated portions of store. There are two key novelties w.r.t. similar proposals. First, the expressivity of the type system is greatly enhanced by promotion and swapping rules. The former recognizes as \({\mathtt{capsule}}\) an expression which only uses external references as \({\mathtt{lent}}\). The latter allows a \({\mathtt{lent}}\) reference to be freely aliased, if all the other references are regarded as \({\mathtt{lent}}\). Second, execution is modeled in a pure setting, where it is simpler to understand alias control. That is, properties of modifiers can be directly expressed on source terms, rather than as invariants on an auxiliary structure which mimics physical memory. Formally, this is achieved by the block construct, introducing local variable declarations, which play the role of store when evaluated.
This work has been partially supported by MIUR CINA -Compositionality, Interaction, Negotiation, Autonomicity for the future ICT society.
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
Similar content being viewed by others
Notes
- 1.
In the examples, we omit for readability the brackets of the outermost block.
- 2.
More precisely, \({\mathtt{lent}}\) references can be temporarily aliased, e.g., when passed as parameter of a method, but cannot be stored within other objects. That is, aliasing here means static aliasing in the sense of [10].
- 3.
Reduction rules will be given in Sect. 4.
- 4.
As will be formalized by congruence rule (new) in Sect. 4.
- 5.
To avoid access to objects not initialized yet as in the example.
- 6.
See rule (capsule-elim). Note that, correspondingly, the association of a right value to a \({\mathtt{capsule}}\) variable is not kept in the store, formally there is no such case in the production for \(\textit{dv}\).
- 7.
This notion will be formalized in Sect. 4.
- 8.
It is not straightforward to soundly apply \({\mathtt{capsule}}\) and \({\mathtt{lent}}\) on fields. We plan to present such extensions in future work, whereas the current paper is focused on promotion and swapping.
- 9.
This function will be used in Sect. 4.
- 10.
As will be formalized in Sect. 4.
- 11.
Recall that, in the declaration of clone, lent is the modifier of the receiver, that is, the method takes the receiver as lent.
- 12.
See [3] for another alternative to destructive reads, in a work aiming to ensure shallow uniqueness.
- 13.
In an hypothetical extension, we would need to prevent storage also within closures or threads.
References
Almeida, P.S.: Balloon types: controlling sharing of state in data types. In: Akşit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 32–59. Springer, Heidelberg (1997)
Bloch, J.: Effective Java (2Nd Edition) (The Java Series), 2nd edn. Prentice Hall PTR, Upper Saddle River (2008)
Boyland, J.: Alias burying: Unique variables without destructive reads. Softw. Pract. Exper. 31(6), 533–553 (2001)
Boyland, J.: Semantics of fractional permissions with nesting. ACM Trans. Program. Lang. Syst. 32(6), 1–33 (2010)
Capriccioli, A., Servetto, M., Zucca, E.: An imperative pure calculus. In: ICTCS 2015 - Italian Conference on Theoretical Computer Science (2015)
Clarke, D., Wrigstad, T.: External uniqueness is unique enough. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, pp. 176–200. Springer, Heidelberg (2003)
Clarke, D.G., Potter, J., Noble, J.: Ownership types for flexible alias protection. In: ACM Symposium on Object-Oriented Programming: Systems, Languages and Applications 1998, pp. 48–64 (1998)
Dietl, W., Drossopoulou, S., Müller, P.: Generic universe types. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 28–53. Springer, Heidelberg (2007)
Gordon, C.S., Parkinson, M.J., Parsons, J., Bromfield, A., Duffy, J.: Uniqueness and reference immutability for safe parallelism. In: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2012), pp. 21–40. ACM Press (2012)
Hogg, J.: Islands: aliasing protection in object-oriented languages. In: ACM Symposium on Object-Oriented Programming: Systems, Languages and Applications 1991, pp. 271–285. ACM Press (1991)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3), 396–450 (2001)
Li, P., Cameron, N., Noble, J.: Cloning in ownership. In: Proceedings of the ACM International Conference Companion on Object Oriented Programming Systems Languages and Applications Companion, OOPSLA 2011, pp. 63–66. ACM, New York (2011)
Milner, R.: Communicating and Mobile Systems - The Pi-Calculus. Cambridge University Press, Cambridge (1999)
Naden, K., Bocchino, R., Aldrich, J., Bierhoff, K.: A type system for borrowing permissions. In: ACM Symposium on Principles of Programming Languages 2012, pp. 557–570. ACM Press (2012)
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the IEEE Symposium on Logic in Computer Science 2002, pp. 5–74. IEEE Computer Society (2002)
Servetto, M., Groves, L.: True small-step reduction for imperative object-oriented languages. IN: FTfJP 2013- Formal Techniques for Java-like Programs (2013)
Servetto, M., Mackay, J., Potanin, A., Noble, J.: The billion-dollar fix: safe modular circular initialisation with placeholders and placeholder types. In: Castagna, G. (ed.) ECOOP 2013. LNCS, vol. 7920, pp. 205–229. Springer, Heidelberg (2013)
Servetto, M., Pearce, D.J., Groves, L., Potanin, A.: Balloon types for safe parallelisation over arbitrary object graphs. In: WODET 2014 - Workshop on Determinism and Correctness in Parallel Programming (2013)
Tschantz, M.S., Ernst, M.D.: Javari: adding reference immutabilityto Java. In: Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2005), San Diego, CA, USA, October 18–20, pp. 211–230 (2005)
Zibin, Y., Potanin, A., Li, P., Ali, M., Ernst, M.D.: Ownership and immutability in generic Java. In: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2010), pp. 598–617 (2010)
Acknowledgement
We thank the anonymous referees for their helpful comments, and Matthew Parkinson (author of [9]) for his help in the comparison with our work.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Servetto, M., Zucca, E. (2015). Aliasing Control in an Imperative Pure Calculus. In: Feng, X., Park, S. (eds) Programming Languages and Systems. APLAS 2015. Lecture Notes in Computer Science(), vol 9458. Springer, Cham. https://doi.org/10.1007/978-3-319-26529-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-26529-2_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-26528-5
Online ISBN: 978-3-319-26529-2
eBook Packages: Computer ScienceComputer Science (R0)