Document Open Access Logo

Linear Promises: Towards Safer Concurrent Programming

Authors Ohad Rau, Caleb Voss, Vivek Sarkar

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2021.13.pdf
  • Filesize: 0.95 MB
  • 27 pages

Document Identifiers

Author Details

Ohad Rau
  • Georgia Institute of Technology, Atlanta, GA, USA
Caleb Voss
  • Georgia Institute of Technology, Atlanta, GA, USA
Vivek Sarkar
  • Georgia Institute of Technology, Atlanta, GA, USA

Cite AsGet BibTex

Ohad Rau, Caleb Voss, and Vivek Sarkar. Linear Promises: Towards Safer Concurrent Programming. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 13:1-13:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ECOOP.2021.13

Abstract

In this paper, we introduce a new type system based on linear typing, and show how it can be incorporated in a concurrent programming language to track ownership of promises. By tracking write operations on each promise, the language is able to guarantee exactly one write operation is ever performed on any given promise. This language thus precludes a number of common bugs found in promise-based programs, such as failing to write to a promise and writing to the same promise multiple times. We also present an implementation of the language, complete with an efficient type checking algorithm and high-level programming constructs. This language serves as a safer platform for writing high-level concurrent code.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Concurrent programming languages
  • Theory of computation → Operational semantics
  • Theory of computation → Type theory
Keywords
  • promises
  • type systems
  • linear typing
  • operational semantics
  • concurrency

Metrics

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

Supplementary Materials

References

  1. Saba Alimadadi, Di Zhong, Magnus Madsen, and Frank Tip. Finding broken promises in asynchronous javascript programs. Proc. ACM Program. Lang., 2(OOPSLA), October 2018. URL: https://doi.org/10.1145/3276532.
  2. Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. Linear Haskell: Practical linearity in a higher-order polymorphic language. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158093.
  3. Chandrasekhar Boyapati, Robert Lee, and Martin Rinard. Ownership types for safe programming: Preventing data races and deadlocks. In Proceedings of the 17th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA ’02, page 211–230, New York, NY, USA, 2002. Association for Computing Machinery. URL: https://doi.org/10.1145/582419.582440.
  4. Marco Carbone and Fabrizio Montesi. Deadlock-freedom-by-design: Multiparty asynchronous global programming. SIGPLAN Not., 48(1):263–274, January 2013. URL: https://doi.org/10.1145/2480359.2429101.
  5. Avik Chaudhuri, Panagiotis Vekris, Sam Goldman, Marshall Roch, and Gabriel Levi. Fast and precise type checking for JavaScript. Proc. ACM Program. Lang., 1(OOPSLA), October 2017. URL: https://doi.org/10.1145/3133872.
  6. Maria Christakis and Christian Bird. What developers want and need from program analysis: An empirical study. In Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, page 332–343, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2970276.2970347.
  7. Michael D Ernst. Static and dynamic analysis: Synergy and duality. In WODA 2003: ICSE Workshop on Dynamic Analysis, pages 24-27, 2003. Google Scholar
  8. R. E. Fairley. Tutorial: Static analysis and dynamic testing of computer software. Computer, 11(4):14-23, 1978. URL: https://doi.org/10.1109/C-M.1978.218132.
  9. Kiko Fernandez-Reyes, Dave Clarke, Elias Castegren, and Huu-Phuc Vo. Forward to a promising future. In Giovanna Di Marzo Serugendo and Michele Loreti, editors, Coordination Models and Languages, pages 162-180, Cham, 2018. Springer International Publishing. Google Scholar
  10. Kiko Fernandez-Reyes, Dave Clarke, Ludovic Henrio, Einar Broch Johnsen, and Tobias Wrigstad. Godot: All the Benefits of Implicit and Explicit Futures. In Alastair F. Donaldson, editor, 33rd European Conference on Object-Oriented Programming (ECOOP 2019), volume 134 of Leibniz International Proceedings in Informatics (LIPIcs), pages 2:1-2:28, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2019.2.
  11. Richard C. Holt. Some deadlock properties of computer systems. ACM Comput. Surv., 4(3):179–196, 1972. URL: https://doi.org/10.1145/356603.356607.
  12. ISO. ISO/IEC 14882:2017 Information technology - Programming languages - C++, pages 1391-1407. International Organization for Standardization, Geneva, Switzerland, fifth edition, 2017. URL: https://www.iso.org/standard/68564.html.
  13. Jonathan K. Lee and Jens Palsberg. Featherweight X10: A core calculus for async-finish parallelism. SIGPLAN Not., 45(5):25–36, 2010. URL: https://doi.org/10.1145/1837853.1693459.
  14. B. Liskov and L. Shrira. Promises: Linguistic support for efficient asynchronous procedure calls in distributed systems. SIGPLAN Not., 23(7):260–267, 1988. URL: https://doi.org/10.1145/960116.54016.
  15. Magnus Madsen, Ondřej Lhoták, and Frank Tip. A model for reasoning about JavaScript promises. Proc. ACM Program. Lang., 1(OOPSLA), 2017. URL: https://doi.org/10.1145/3133910.
  16. J. Niehren, J. Schwinghammer, and G. Smolka. A concurrent lambda calculus with futures. Theor. Comput. Sci., 364(3):338–356, 2006. URL: https://doi.org/10.1016/j.tcs.2006.08.016.
  17. Jihyun Park, Byoungju Choi, and Seungyeun Jang. Dynamic analysis method for concurrency bugs in multi-process/multi-thread environments. International Journal of Parallel Programming, 48, December 2020. URL: https://doi.org/10.1007/s10766-020-00661-3.
  18. Raghavan Raman, Jisheng Zhao, Vivek Sarkar, Martin Vechev, and Eran Yahav. Scalable and precise dynamic datarace detection for structured parallelism. In Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, page 531–542, New York, NY, USA, 2012. Association for Computing Machinery. URL: https://doi.org/10.1145/2254064.2254127.
  19. Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin Bierman, and Panagiotis Vekris. Safe & efficient gradual typing for TypeScript. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, page 167–180, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2676726.2676971.
  20. Justin Slepak. Notes on substructural types. URL: http://www.ccs.neu.edu/~jrslepak/substruct-notes.pdf.
  21. Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, and Jean Yang. Secure distributed programming with value-dependent types. Technical Report MSR-TR-2011-37, Microsoft Research, March 2011. This is an extended version of the conference paper (ICFP '11) with the same title. A final version of this full technical report is forthcoming. URL: https://www.microsoft.com/en-us/research/publication/secure-distributed-programming-with-value-dependent-types/.
  22. Caleb Voss and Vivek Sarkar. An ownership policy and deadlock detector for promises, 2021. URL: http://arxiv.org/abs/2101.01312.
  23. P. Wadler. Linear types can change the world! In Programming Concepts and Methods, 1990. Google Scholar
  24. Aaron Weiss, Olek Gierczak, Daniel Patterson, Nicholas D. Matsakis, and Amal Ahmed. Oxide: The essence of Rust, 2020. URL: http://arxiv.org/abs/1903.00982v3.
  25. Edwin Westbrook, Jisheng Zhao, Zoran Budimlić, and Vivek Sarkar. Practical permissions for race-free parallelism. In James Noble, editor, ECOOP 2012 - Object-Oriented Programming, pages 614-639, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  26. Dengping Zhu. To Memory Safety through Proofs. PhD thesis, Boston University, USA, 2006. Google Scholar
  27. Erika Ábrahám, Immo Grabe, Andreas Grüner, and Martin Steffen. Behavioral interface description of an object-oriented language with futures and promises. The Journal of Logic and Algebraic Programming, 78(7):491-518, 2009. The 19th Nordic Workshop on Programming Theory (NWPT 2007). URL: https://doi.org/10.1016/j.jlap.2009.01.001.
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