Document Open Access Logo

Designing with Static Capabilities and Effects: Use, Mention, and Invariants (Pearl)

Author Colin S. Gordon

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.10.pdf
  • Filesize: 0.55 MB
  • 25 pages

Document Identifiers

Author Details

Colin S. Gordon
  • Department of Computer Science, Drexel University, Philadelphia, PA, USA

Acknowledgements

Many thanks are due to the audience at the OCAP 2018 workshop where these ideas were initially presented, and to the ECOOP 2020 reviewers, for helpful feedback on the ideas, presentation, and paper itself.

Cite AsGet BibTex

Colin S. Gordon. Designing with Static Capabilities and Effects: Use, Mention, and Invariants (Pearl). In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 10:1-10:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ECOOP.2020.10

Abstract

Capabilities (whether object or reference capabilities) are fundamentally tools to restrict effects. Thus static capabilities (object or reference) and effect systems take different technical machinery to the same core problem of statically restricting or reasoning about effects in programs. Any time two approaches can in principle address the same sets of problems, it becomes important to understand the trade-offs between the approaches, how these trade-offs might interact with the problem at hand. Experts who have worked in these areas tend to find the trade-offs somewhat obvious, having considered them in context before. However, this kind of design discussion is often written down only implicitly as comparison between two approaches for a specific program reasoning problem, rather than as a discussion of general trade-offs between general classes of techniques. As a result, it is not uncommon to set out to solve a problem with one technique, only to find the other better-suited. We discuss the trade-offs between static capabilities (specifically reference capabilities) and effect systems, articulating the challenges each approach tends to have in isolation, and how these are sometimes mitigated. We also put our discussion in context, by appealing to examples of how these trade-offs were considered in the course of developing prior systems in the area. Along the way, we highlight how seemingly-minor aspects of type systems - weakening/framing and the mere existence of type contexts - play a subtle role in the efficacy of these systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Software and its engineering → Language features
Keywords
  • Effect systems
  • reference capabilities
  • object capabilities

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Robert L. Bocchino, Jr., Vikram S. Adve, Danny Dig, Sarita V. Adve, Stephen Heumann, Rakesh Komuravelli, Jeffrey Overbey, Patrick Simmons, Hyojin Sung, and Mohsen Vakilian. A Type and Effect System for Deterministic Parallel Java. In OOPSLA, 2009. URL: https://doi.org/10.1145/1640089.1640097.
  2. John Boyland and Aaron Greenhouse. Mayequal: A new alias question. In International Workshop on Aliasing in Object-Oriented Systems (IWAOOS), 1999. Google Scholar
  3. John Boyland, James Noble, and William Retert. Capabilities for sharing. In European Conference on Object-Oriented Programming, pages 2-27. Springer, 2001. Google Scholar
  4. Luca Cardelli and John C Mitchell. Operations on records. Mathematical structures in computer science, 1(01):3-48, 1991. Google Scholar
  5. Elias Castegren and Tobias Wrigstad. Reference capabilities for concurrency control. In 30th European Conference on Object-Oriented Programming, ECOOP 2016, 2016. Google Scholar
  6. Elias Castegren and Tobias Wrigstad. Relaxed linear references for lock-free programming. In 31st European Conference on Object-Oriented Programming, ECOOP 2017, 2017. Google Scholar
  7. Satish Chandra, Colin S. Gordon, Jean-Baptiste Jeannin, Cole Schlesinger, Manu Sridharan, Frank Tip, and Young-Il Choi. Type Inference for Static Compilation of JavaScript. In Proceedings of the 2016 ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016), Amsterdam, The Netherlands, November 2016. URL: https://doi.org/10.1145/2983990.2984017.
  8. Jeffrey S. Chase, Henry M. Levy, Edward D. Lazowska, and Miche Baker-Harvey. Lightweight shared objects in a 64-bit operating system. In Conference Proceedings on Object-oriented Programming Systems, Languages, and Applications, OOPSLA '92, pages 397-413, New York, NY, USA, 1992. ACM. URL: https://doi.org/10.1145/141936.141969.
  9. Philip Wontae Choi, Satish Chandra, George Necula, and Koushik Sen. SJS: a Typed Subset of JavaScript with Fixed Object Layout. Technical Report UCB/EECS-2015-13, UC Berkeley, 2015. Google Scholar
  10. Dave Clarke, Johan Östlund, Ilya Sergey, and Tobias Wrigstad. Ownership types: A survey. In Aliasing in Object-Oriented Programming. Types, Analysis and Verification, pages 15-58. Springer, 2013. Google Scholar
  11. David G Clarke, John M Potter, and James Noble. Ownership types for flexible alias protection. In Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, pages 48-64, 1998. Google Scholar
  12. Sylvan Clebsch, Sophia Drossopoulou, Sebastian Blessing, and Andy McNeil. Deny capabilities for safe, fast actors. In Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control, pages 1-12. ACM, 2015. Google Scholar
  13. Aaron Craig, Alex Potanin, Lindsay Groves, and Jonathan Aldrich. Capabilities: Effects for Free. In International Conference on Formal Engineering Methods (ICFEM), 2018. Google Scholar
  14. Donald Davidson. Quotation. Theory and decision, 11(1):27, 1979. Google Scholar
  15. David L. Detlefs, K. Rustan M. Leino, and Greg Nelson. Wrestling with rep exposure. Technical Report SRC-RR-156, Digital Equipment Corporation, July 1998. URL: https://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-156.html.
  16. Werner Dietl, Sophia Drossopoulou, and Peter Müller. Generic Universe Types. In E. Ernst, editor, ECOOP, volume 4609 of Lecture Notes in Computer Science, pages 28-53, Berlin, Germany, July 2007. Springer-Verlag. Google Scholar
  17. Werner Dietl and Peter Müller. Universes: Lightweight ownership for jml. Journal of Object Technology, 4(8):5-32, 2005. Google Scholar
  18. Sophia Drossopoulou, James Noble, Mark S Miller, and Toby Murray. Permission and authority revisited towards a formalisation. In Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs, pages 1-6, 2016. Google Scholar
  19. Joe Duffy. Blogging about Midori, November 2015. URL: http://joeduffyblog.com/2015/11/03/blogging-about-midori/.
  20. Andrzej Filinski. Monads in action. In POPL, 2010. Google Scholar
  21. Jeffrey S. Foster, Manuel Fähndrich, and Alexander Aiken. A theory of type qualifiers. In Proceedings of the ACM SIGPLAN 1999 Conference on Programming Language Design and Implementation, PLDI '99, pages 192-203. ACM, 1999. URL: https://doi.org/10.1145/301618.301665.
  22. Ronald Garcia, Éric Tanter, Roger Wolff, and Jonathan Aldrich. Foundations of typestate-oriented programming. ACM Trans. Program. Lang. Syst., 36(4):12:1-12:44, October 2014. URL: https://doi.org/10.1145/2629609.
  23. Paola Giannini, Marco Servetto, Elena Zucca, and James Cone. Flexible recovery of uniqueness and immutability. Theoretical Computer Science, 764:145-172, 2019. Google Scholar
  24. David K. Gifford and John M. Lucassen. Integrating Functional and Imperative Programming. In Proceedings of the 1986 ACM Conference on LISP and Functional Programming, LFP '86, 1986. Google Scholar
  25. Colin S. Gordon. Verifying Concurrent Programs by Controlling Alias Interference. PhD thesis, University of Washington, Seattle, WA, USA, August 2014. URL: URL: https://digital.lib.washington.edu/researchworks/handle/1773/26020.
  26. Colin S. Gordon, Werner Dietl, Michael D. Ernst, and Dan Grossman. JavaUI: Effects for Controlling UI Object Access. In ECOOP, 2013. Google Scholar
  27. Colin S. Gordon, Michael D. Ernst, and Dan Grossman. Rely-Guarantee References for Refinement Types Over Aliased Mutable Data. In PLDI, Seattle, WA, USA, June 2013. URL: https://doi.org/10.1145/2491956.2462160.
  28. Colin S. Gordon, Michael D. Ernst, Dan Grossman, and Matthew J. Parkinson. Verifying Invariants of Lock-free Data Structures with Rely-Guarantee and Refinement Types. ACM Transactions on Programming Languages and Systems (TOPLAS), 39(3), May 2017. URL: https://doi.org/10.1145/3064850.
  29. Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. Uniqueness and Reference Immutability for Safe Parallelism. In OOPSLA, Tucson, AZ, USA, October 2012. URL: https://doi.org/10.1145/2384616.2384619.
  30. Aaron Greenhouse and John Boyland. An object-oriented effects system. In European Conference on Object-Oriented Programming, pages 205-229. Springer, 1999. Google Scholar
  31. Philipp Haller and Martin Odersky. Capabilities for Uniqueness and Borrowing. In ECOOP, 2010. Google Scholar
  32. Wei Huang, Werner Dietl, Ana Milanova, and Michael D. Ernst. Inference and checking of object ownership. In European Conference on Object-Oriented Programming (ECOOP 2012), pages 181-206. Springer, 2012. Google Scholar
  33. Wei Huang, Ana Milanova, Werner Dietl, and Michael D. Ernst. Reim & reiminfer: Checking and inference of reference immutability and method purity. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '12, pages 879-896. ACM, 2012. Google Scholar
  34. Butler W Lampson. Protection. ACM SIGOPS Operating Systems Review, 8(1):18-24, 1974. Google Scholar
  35. Henry M Levy. Capability-based computer systems. Digital Press, 1984. URL: https://homes.cs.washington.edu/~levy/capabook/.
  36. Paul Liétar. Formalizing Generics for Pony, 2017. Imperial College London Bachelor’s Thesis. Google Scholar
  37. Sam Lindley and James Cheney. Row-based effect types for database integration. In Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation, pages 91-102. ACM, 2012. Google Scholar
  38. Fengun Liu, Sandro Stucki, Nada Amin, Paolo Giosuè, and Martin Odersky. Stoic: Towards Disciplined Capabilities. Technical report, École Polytechnique Fédérale de Lausanne, 2020. URL: https://infoscience.epfl.ch/record/273642.
  39. Fengyun Liu. A Study of Capability-Based Effect Systems, 2016. Master of Computer Science Thesis, École Polytechnique Fédérale de Lausanne. URL: https://infoscience.epfl.ch/record/219173.
  40. J. M. Lucassen and D. K. Gifford. Polymorphic Effect Systems. In POPL, 1988. Google Scholar
  41. Daniel Marino and Todd Millstein. A Generic Type-and-Effect System. In TLDI, 2009. URL: https://doi.org/10.1145/1481861.1481868.
  42. Darya Melicher, Yangqingwei Shi, Valerie Zhao, Alex Potanin, and Jonathan Aldrich. Using Object Capabilities and Effects to Build and Authority-Safe Module System. In Workshop on Object-Capability Languages, Systems, and Applications (OCAP), 2017. Google Scholar
  43. Filipe Militão, Jonathan Aldrich, and Luís Caires. Rely-Guarantee Protocols. In 28th European Conference on Object-Oriented Programming, ECOOP 2014, 2014. Google Scholar
  44. Filipe Militão, Jonathan Aldrich, and Luís Caires. Composing interfering abstract protocols. In 30th European Conference on Object-Oriented Programming, ECOOP 2016, 2016. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2016.16.
  45. Mark Samuel Miller. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. PhD thesis, Johns Hopkins University, Baltimore, Maryland, USA, May 2006. Google Scholar
  46. Eugenio Moggi. Computational lambda-calculus and monads. In LICS, 1989. Google Scholar
  47. AW Moore. How significant is the use/mention distinction? Analysis, 46(4):173-179, 1986. Google Scholar
  48. Karl Naden, Robert Bocchino, Jonathan Aldrich, and Kevin Bierhoff. A type system for borrowing permissions. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 557-570, 2012. Google Scholar
  49. James Noble, Jan Vitek, and John Potter. Flexible alias protection. In European Conference on Object-Oriented Programming, pages 158-185. Springer, 1998. Google Scholar
  50. Leo Osvald, Grégory Essertel, Xilun Wu, Lilliam I González Alayón, and Tiark Rompf. Gentrification gone too far? affordable 2nd-class values for fun and (co-) effect. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 234-251, 2016. Google Scholar
  51. Alex Potanin, Monique Damitio, and James Noble. Are your incoming aliases really necessary? counting the cost of object ownership. In 2013 35th International Conference on Software Engineering (ICSE), pages 742-751. IEEE, 2013. Google Scholar
  52. François Pottier. Hiding local state in direct style: a higher-order anti-frame rule. In 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pages 331-340. IEEE, 2008. Google Scholar
  53. John C Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pages 55-74. IEEE, 2002. Google Scholar
  54. Lukas Rytz, Nada Amin, and Martin Odersky. A flow-insensitive, modular effect system for purity. In Proceedings of the 15th Workshop on Formal Techniques for Java-like Programs, page 4. ACM, 2013. Google Scholar
  55. Benno Stein, Lazaro Clapp, Manu Sridharan, and Bor-Yuh Evan Chang. Safe stream-based programming with refinement types. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, pages 565-576, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3238147.3238174.
  56. Jean-Pierre Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of functional programming, 2(03):245-271, 1992. URL: https://doi.org/10.1017/S0956796800000393.
  57. Mads Tofte and Jean-Pierre Talpin. Implementation of the Typed Call-by-value λ-calculus Using a Stack of Regions. In POPL, 1994. Google Scholar
  58. Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Information and computation, 132(2):109-176, 1997. Google Scholar
  59. Matthew S. Tschantz and Michael D. Ernst. Javari: Adding Reference Immutability to Java. In OOPSLA, 2005. URL: https://doi.org/10.1145/1094811.1094828.
  60. Tom Van Cutsem and Mark S. Miller. Proxies: Design principles for robust object-oriented intercession apis. In Proceedings of the 6th Symposium on Dynamic Languages, DLS '10, pages 59-72, New York, NY, USA, 2010. ACM. URL: https://doi.org/10.1145/1869631.1869638.
  61. Tom Van Cutsem and Mark S Miller. Trustworthy proxies. In European Conference on Object-Oriented Programming, pages 154-178. Springer, 2013. Google Scholar
  62. David Walker. Substructural type systems. In Advanced topics in types and programming languages, pages 3-44. The MIT Press, 2005. Google Scholar
  63. David Walker, Karl Crary, and Greg Morrisett. Typed memory management via static capabilities. ACM Trans. Program. Lang. Syst., 22(4):701-771, July 2000. URL: https://doi.org/10.1145/363911.363923.
  64. Mitchell Wand. Type inference for record concatenation and multiple inheritance. In Logic in Computer Science, 1989. LICS'89, Proceedings., Fourth Annual Symposium on, pages 92-97. IEEE, 1989. Google Scholar
  65. Yoav Zibin, Alex Potanin, Mahmood Ali, Shay Artzi, Adam Kiezun, and Michael D. Ernst. Object and Reference Immutability Using Java Generics. In ESEC-FSE, 2007. URL: https://doi.org/10.1145/1287624.1287637.
  66. Yoav Zibin, Alex Potanin, Paley Li, Mahmood Ali, and Michael D. Ernst. Ownership and Immutability in Generic Java. In OOPSLA, 2010. URL: https://doi.org/10.1145/1869459.1869509.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact