Document Open Access Logo

Safe Transferable Regions

Authors Gowtham Kaki, G. Ramalingam

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2018.11.pdf
  • Filesize: 0.7 MB
  • 31 pages

Document Identifiers

Author Details

Gowtham Kaki
  • Purdue University, USA
G. Ramalingam
  • Microsoft Research, India

Cite As Get BibTex

Gowtham Kaki and G. Ramalingam. Safe Transferable Regions. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 11:1-11:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.ECOOP.2018.11

Abstract

There is an increasing interest in alternative memory management schemes that seek to combine the convenience of garbage collection and the performance of manual memory management in a single language framework. Unfortunately, ensuring safety in presence of manual memory management remains as great a challenge as ever. In this paper, we present a C#-like object-oriented language called Broom that uses a combination of region type system and lightweight runtime checks to enforce safety in presence of user-managed memory regions called transferable regions. Unsafe transferable regions have been previously used to contain the latency due to unbounded GC pauses. Our approach shows that it is possible to restore safety without compromising on the benefits of transferable regions. We prove the type safety of Broom in a formal framework that includes its C#-inspired features, such as higher-order functions and generics. We complement our type system with a type inference algorithm, which eliminates the need for programmers to write region annotations on types. The inference algorithm has been proven sound and relatively complete. We describe a prototype implementation of the inference algorithm, and our experience of using it to enforce memory safety in dataflow programs.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Allocation / deallocation strategies
  • Software and its engineering → Object oriented languages
  • Software and its engineering → Data flow languages
  • Software and its engineering → Software verification and validation
Keywords
  • Memory Safety
  • Formal Methods
  • Type System
  • Type Inference
  • Regions
  • Featherweight Java

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 Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '09, pages 97-116, New York, NY, USA, 2009. ACM. URL: http://dx.doi.org/10.1145/1640089.1640097.
  2. Chandrasekhar Boyapati, Alexandru Salcianu, William Beebee, Jr., and Martin Rinard. Ownership types for safe region-based memory management in real-time java. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, PLDI '03, pages 324-337, New York, NY, USA, 2003. ACM. URL: http://dx.doi.org/10.1145/781131.781168.
  3. Badrish Chandramouli, Jonathan Goldstein, Mike Barnett, Robert DeLine, John C. Platt, James F. Terwilliger, and John Wernsing. Trill: A high-performance incremental query processor for diverse analytics. PVLDB, 8(4):401-412, 2014. URL: http://www.vldb.org/pvldb/vol8/p401-chandramouli.pdf.
  4. Sigmund Cherem and Radu Rugina. Region analysis and transformation for java programs. In Proceedings of the 4th International Symposium on Memory Management, ISMM '04, pages 85-96, New York, NY, USA, 2004. ACM. URL: http://dx.doi.org/10.1145/1029873.1029884.
  5. Dave Clarke, Johan Östlund, Ilya Sergey, and Tobias Wrigstad. Ownership Types: A Survey, pages 15-58. Springer Berlin Heidelberg, Berlin, Heidelberg, 2013. URL: http://dx.doi.org/10.1007/978-3-642-36946-9_3.
  6. Werner Dietl, Michael D. Ernst, and Peter Müller. Tunable static inference for generic universe types. In ECOOP 2011 - Object-Oriented Programming - 25th European Conference, Lancaster, UK, July 25-29, 2011 Proceedings, pages 333-357, 2011. URL: http://dx.doi.org/10.1007/978-3-642-22655-7_16.
  7. Ionel Gog, Jana Giceva, Malte Schwarzkopf, Kapil Vaswani, Dimitrios Vytiniotis, Ganesan Ramalingam, Manuel Costa, Derek Gordon Murray, Steven Hand, and Michael Isard. Broom: Sweeping out garbage collection from big data systems. In 15th Workshop on Hot Topics in Operating Systems, HotOS XV, Kartause Ittingen, Switzerland, May 18-20, 2015, 2015. URL: https://www.usenix.org/conference/hotos15/workshop-program/presentation/gog.
  8. Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. Region-based memory management in cyclone. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, PLDI '02, pages 282-293, New York, NY, USA, 2002. ACM. URL: http://dx.doi.org/10.1145/512529.512563.
  9. Fritz Henglein, Henning Makholm, and Henning Niss. A direct approach to control-flow sensitive region-based memory management. In Proceedings of the 3rd ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP '01, pages 175-186, New York, NY, USA, 2001. ACM. URL: http://dx.doi.org/10.1145/773184.773203.
  10. Michael Hicks, Greg Morrisett, Dan Grossman, and Trevor Jim. Experience with safe manual memory-management in cyclone. In Proceedings of the 4th International Symposium on Memory Management, ISMM '04, pages 73-84, New York, NY, USA, 2004. ACM. URL: http://dx.doi.org/10.1145/1029873.1029883.
  11. Eric Holk, Ryan Newton, Jeremy Siek, and Andrew Lumsdaine. Region-based memory management for gpu programming languages: Enabling rich data structures on a spartan host. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA '14, pages 141-155, New York, NY, USA, 2014. ACM. URL: http://dx.doi.org/10.1145/2660193.2660244.
  12. Wei Huang, Werner Dietl, Ana Milanova, and Michael D. Ernst. Inference and checking of object ownership. In ECOOP 2012 - Object-Oriented Programming - 26th European Conference, Beijing, China, June 11-16, 2012. Proceedings, pages 181-206, 2012. URL: http://dx.doi.org/10.1007/978-3-642-31057-7_9.
  13. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight java: A minimal core calculus for java and gj. ACM Trans. Program. Lang. Syst., 23(3):396-450, 2001. URL: http://dx.doi.org/10.1145/503502.503505.
  14. Martin Maas, Tim Harris, Krste Asanovic, and John Kubiatowicz. Trash day: Coordinating garbage collection in distributed systems. In Proceedings of the 15th USENIX Conference on Hot Topics in Operating Systems, HOTOS'15, pages 1-1, Berkeley, CA, USA, 2015. USENIX Association. URL: http://dl.acm.org/citation.cfm?id=2831090.2831091.
  15. Mads Tofte and Jean-Pierre Talpin. A Theory of Stack Allocation in Polymorphically Typed Languages. Technical Report DIKU-report 93/15, University of Copenhagen, 1993. URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.51.6564.
  16. Thomas W. Reps. Program analysis via graph reachability. Information & Software Technology, 40(11-12):701-726, 1998. URL: http://dx.doi.org/10.1016/S0950-5849(98)00093-7.
  17. The Rust Programming Language, 2015. Accessed: 2015-11-7 13:21:00. URL: https://doc.rust-lang.org/book.
  18. Type-safe off-heap memory, 2016. Accessed: 2016-06-6 13:21:00. URL: https://github.com/densh/scala-offheap.
  19. Nikhil Swamy, Michael Hicks, Greg Morrisett, Dan Grossman, and Trevor Jim. Safe manual memory management in cyclone. Science of Computer Programming, 62(2):122-144, 2006. Special Issue: Five perspectives on modern memory management - Systems, hardware and theory. URL: http://dx.doi.org/10.1016/j.scico.2006.02.003.
  20. Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value λ-calculus using a stack of regions. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '94, pages 188-201, New York, NY, USA, 1994. ACM. URL: http://dx.doi.org/10.1145/174675.177855.
  21. Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Inf. Comput., 132(2):109-176, 1997. URL: http://dx.doi.org/10.1006/inco.1996.2613.
  22. Philip Wadler. Linear Types Can Change the World! In M. Broy and C. B. Jones, editors, IFIP TC 2 Working Conference on Programming Concepts and Methods, pages 561-581, Sea of Gallilee, Israel, 1990. North-Holland. Google Scholar
  23. David Walker and Kevin Watkins. On regions and linear types (extended abstract). In Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming, ICFP '01, pages 181-192, New York, NY, USA, 2001. ACM. URL: http://dx.doi.org/10.1145/507635.507658.
  24. Bennett Norton Yates. A type-and-effect system for encapsulating memory in java. Master’s thesis, Department of Computer Science and Information Science, University of Oregon, 1999. Google Scholar
  25. Matei Zaharia. New developments in spark, 2015. URL: http://www.slideshare.net/databricks/new-developments-in-spark.
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 About DROPS Imprint Privacy Contact