Document Open Access Logo

ConDRust: Scalable Deterministic Concurrency from Verifiable Rust Programs

Authors Felix Suchert , Lisza Zeidler, Jeronimo Castrillon , Sebastian Ertel

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.33.pdf
  • Filesize: 1.46 MB
  • 39 pages

Document Identifiers

Author Details

Felix Suchert
  • TU Dresden, Germany
Lisza Zeidler
  • Barkhausen Institut, Dresden, Germany
Jeronimo Castrillon
  • TU Dresden, Germany
Sebastian Ertel
  • Barkhausen Institut, Dresden, Germany

Funding

  • Suchert, Felix: was funded by the EU Horizon 2020 Programme under grant agreement No 957269 (EVEREST).
  • Zeidler, Lisza: was funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - 469256231.

Acknowledgements

The authors would like to thank the anonymous reviewers for their invaluable feedback in the submission process.

Cite AsGet BibTex

Felix Suchert, Lisza Zeidler, Jeronimo Castrillon, and Sebastian Ertel. ConDRust: Scalable Deterministic Concurrency from Verifiable Rust Programs. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 33:1-33:39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.33

Abstract

SAT/SMT-solvers and model checkers automate formal verification of sequential programs. Formal reasoning about scalable concurrent programs is still manual and requires expert knowledge. But scalability is a fundamental requirement of current and future programs. Sequential imperative programs compose statements, function/method calls and control flow constructs. Concurrent programming models provide constructs for concurrent composition. Concurrency abstractions such as threads and synchronization primitives such as locks compose the individual parts of a concurrent program that are meant to execute in parallel. We propose to rather compose the individual parts again using sequential composition and compile this sequential composition into a concurrent one. The developer can use existing tools to formally verify the sequential program while the translated concurrent program provides the dearly requested scalability. Following this insight, we present ConDRust, a new programming model and compiler for Rust programs. The ConDRust compiler translates sequential composition into a concurrent composition based on threads and message-passing channels. During compilation, the compiler preserves the semantics of the sequential program along with much desired properties such as determinism. Our evaluation shows that our ConDRust compiler generates concurrent deterministic code that can outperform even non-deterministic programs by up to a factor of three for irregular algorithms that are particularly hard to parallelize.

Subject Classification

ACM Subject Classification
  • Theory of computation → Parallel computing models
  • Software and its engineering → Parallel programming languages
Keywords
  • concurrent programming
  • verification
  • scalability

Metrics

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

Supplementary Materials

References

  1. Jatin Arora, Sam Westrick, and Umut A. Acar. Provably space-efficient parallel functional programming. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434299.
  2. Arvind, Kim P. Gostelow, and Wil Plouffe. Indeterminacy, monitors, and dataflow. In Proceedings of the Sixth ACM Symposium on Operating Systems Principles, SOSP '77, pages 159-169, New York, NY, USA, 1977. Association for Computing Machinery. URL: https://doi.org/10.1145/800214.806559.
  3. Vytautas Astrauskas, Peter Müller, Federico Poli, and Alexander J. Summers. Leveraging rust types for modular specification and verification. Proc. ACM Program. Lang., 3(OOPSLA), October 2019. URL: https://doi.org/10.1145/3360573.
  4. Luiz Barroso, Mike Marty, David Patterson, and Parthasarathy Ranganathan. Attack of the killer microseconds. Commun. ACM, 60(4):48-54, March 2017. URL: https://doi.org/10.1145/3015146.
  5. Micah Beck, Richard Johnson, and Keshav Pingali. From control flow to dataflow. Journal of Parallel and Distributed Computing, 12(2):118-129, 1991. Google Scholar
  6. Mohamed-Walid Benabderrahmane, Louis-Noël Pouchet, Albert Cohen, and Cédric Bastoul. The polyhedral model is more widely applicable than you think. In Compiler Construction: 19th International Conference, CC 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings 19, pages 283-303. Springer, 2010. Google Scholar
  7. Tom Bergan, Owen Anderson, Joseph Devietti, Luis Ceze, and Dan Grossman. Coredet: A compiler and runtime system for deterministic multithreaded execution. In Proceedings of the fifteenth International Conference on Architectural support for programming languages and operating systems, pages 53-64, 2010. Google Scholar
  8. Christian Bienia and Kai Li. Parsec 2.0: A new benchmark suite for chip-multiprocessors. In Proceedings of the 5th Annual Workshop on Modeling, Benchmarking and Simulation, volume 2011, page 37, 2009. Google Scholar
  9. Guy E. Blelloch. NESL: a nested data parallel language. Carnegie Mellon Univ., 1992. Google Scholar
  10. Guy E. Blelloch, Jeremy T. Fineman, Phillip B. Gibbons, and Julian Shun. Internally deterministic parallel algorithms can be fast. In Proceedings of the 17th ACM SIGPLAN symposium on Principles and Practice of Parallel Programming, pages 181-192, 2012. Google Scholar
  11. Robert D. Blumofe, Christopher F. Joerg, Bradley C. Kuszmaul, Charles E. Leiserson, Keith H. Randall, and Yuli Zhou. Cilk: An efficient multithreaded runtime system. In Proceedings of the Fifth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP '95, pages 207-216, New York, NY, USA, 1995. Association for Computing Machinery. URL: https://doi.org/10.1145/209936.209958.
  12. Robert L. Bocchino, Vikram S. Adve, Sarita V. Adve, and Marc Snir. Parallel programming must be deterministic by default. In Proceedings of the First USENIX Conference on Hot Topics in Parallelism, HotPar'09, page 4, USA, 2009. USENIX Association. Google Scholar
  13. 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, pages 97-116, 2009. Google Scholar
  14. Cristiano Calcagno, Philippa Gardner, and Matthew Hague. From separation logic to first-order logic. In Foundations of Software Science and Computational Structures: 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings 8, pages 395-409. Springer, 2005. Google Scholar
  15. Cristiano Calcagno, Hongseok Yang, and Peter W. O’hearn. Computability and complexity results for a spatial assertion language for data structures. In FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science: 21st Conference Bangalore, India, December 13-15, 2001 Proceedings 21, pages 108-119. Springer, 2001. Google Scholar
  16. Dimitrios Chasapis, Marc Casas, Miquel Moretó, Raul Vidal, Eduard Ayguadé, Jesús Labarta, and Mateo Valero. Parsecss: Evaluating the impact of task parallelism in the parsec benchmark suite. ACM Trans. Archit. Code Optim., 12(4), December 2015. URL: https://doi.org/10.1145/2829952.
  17. Peng-Sheng Chen, Ming-Yu Hung, Yuan-Shin Hwang, Roy Dz-Ching Ju, and Jenq Kuen Lee. Compiler support for speculative multithreading architecture with probabilistic points-to analysis. In Proceedings of the ninth ACM SIGPLAN symposium on Principles and practice of parallel programming, pages 25-36, 2003. Google Scholar
  18. Dave Christie, Jae-Woong Chung, Stephan Diestelhorst, Michael Hohmuth, Martin Pohlack, Christof Fetzer, Martin Nowack, Torvald Riegel, Pascal Felber, Patrick Marlier, et al. Evaluation of amd’s advanced synchronization facility within a complete transactional memory stack. In Proceedings of the 5th European conference on Computer systems, pages 27-40, 2010. Google Scholar
  19. Brian F. Cooper, Adam Silberstein, Erwin Tam, Raghu Ramakrishnan, and Russell Sears. Benchmarking cloud serving systems with ycsb. In Proceedings of the 1st ACM symposium on Cloud computing, pages 143-154, 2010. Google Scholar
  20. Giuseppe DeCandia, Deniz Hastorun, Madan Jampani, Gunavardhan Kakulapati, Avinash Lakshman, Alex Pilchin, Swaminathan Sivasubramanian, Peter Vosshall, and Werner Vogels. Dynamo: Amazon’s highly available key-value store. ACM SIGOPS operating systems review, 41(6):205-220, 2007. Google Scholar
  21. Enrico Armenio Deiana, Brian Suchy, Michael Wilkins, Brian Homerding, Tommy McMichen, Katarzyna Dunajewski, Peter Dinda, Nikos Hardavellas, and Simone Campanoni. Program state element characterization. In Proceedings of the 21st ACM/IEEE International Symposium on Code Generation and Optimization, CGO 2023, pages 199-211, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3579990.3580011.
  22. Joseph Devietti, Brandon Lucia, Luis Ceze, and Mark Oskin. Dmp: Deterministic shared memory multiprocessing. In Proceedings of the 14th international conference on Architectural support for programming languages and operating systems, pages 85-96, 2009. Google Scholar
  23. David J. DeWitt, Robert Gerber, Goetz Graefe, Michael Heytens, Krishna Kumar, and Murali Muralikrishna. Gamma-a high performance dataflow database machine. Technical report, University of Wisconsin-Madison Department of Computer Sciences, 1986. Google Scholar
  24. Nuno Diegues, Paolo Romano, and Luís Rodrigues. Virtues and limitations of commodity hardware transactional memory. In Proceedings of the 23rd international conference on Parallel architectures and compilation, pages 3-14, 2014. Google Scholar
  25. Sebastian Ertel, Justus Adam, Norman A Rink, Andrés Goens, and Jeronimo Castrillon. Stclang: State thread composition as a foundation for monadic dataflow parallelism. In Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, pages 146-161, 2019. Google Scholar
  26. Kim P. Gostelow and Wil Plouffe. Indeterminacy, monitors, and dataflow. In Proceedings of the sixth ACM symposium on Operating systems principles, pages 159-169, 1977. Google Scholar
  27. Goetz Graefe. Encapsulation of parallelism in the volcano query processing system. ACM SIGMOD Record, 19(2):102-111, 1990. Google Scholar
  28. Tim Harris, Simon Marlow, Simon Peyton-Jones, and Maurice Herlihy. Composable memory transactions. In Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, pages 48-60, 2005. Google Scholar
  29. Wesley M. Johnston, JR. Paul Hanna, and Richard J. Millar. Advances in dataflow programming languages. ACM computing surveys (CSUR), 36(1):1-34, 2004. Google Scholar
  30. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28:e20, 2018. Google Scholar
  31. Gilles Kahn. The semantics of a simple language for parallel programming. Information processing, 74:471-475, 1974. Google Scholar
  32. Milind Kulkarni, Martin Burtscher, Calin Casçaval, and Keshav Pingali. Lonestar: A suite of parallel irregular programs. In 2009 IEEE International Symposium on Performance Analysis of Systems and Software, pages 65-76. IEEE, 2009. Google Scholar
  33. Lindsey Kuper and Ryan R. Newton. Lvars: lattice-based data structures for deterministic parallelism. In Proceedings of the 2nd ACM SIGPLAN workshop on Functional high-performance computing, pages 71-84, 2013. Google Scholar
  34. Michael Larabel. Intel to disable tsx by default on more cpus with new microcode. https://www.phoronix.com/scan.php?page=news_item&px=Intel-TSX-Off-New-Microcode, 2021. [Online; accessed 02-March-2022].
  35. John Launchbury and Simon L. Peyton Jones. Lazy functional state threads. In Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation, PLDI '94, pages 24-35, New York, NY, USA, 1994. ACM. URL: https://doi.org/10.1145/178243.178246.
  36. Chin Yang Lee. An algorithm for path connections and its applications. IRE transactions on electronic computers, pages 346-365, 1961. Google Scholar
  37. E.A. Lee. The problem with threads. Computer, 39(5):33-42, 2006. URL: https://doi.org/10.1109/MC.2006.180.
  38. Edward A. Lee and David G. Messerschmitt. Synchronous data flow. Proceedings of the IEEE, 75(9):1235-1245, 1987. Google Scholar
  39. Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107-115, July 2009. URL: https://doi.org/10.1145/1538788.1538814.
  40. Yi Lu, Xiangyao Yu, Lei Cao, and Samuel Madden. Aria: A fast and practical deterministic oltp database. Proc. VLDB Endow., 13(12):2047-2060, September 2020. URL: https://doi.org/10.14778/3407790.3407808.
  41. Chi Cao Minh, JaeWoong Chung, Christos Kozyrakis, and Kunle Olukotun. Stamp: Stanford transactional applications for multi-processing. In 2008 IEEE International Symposium on Workload Characterization, pages 35-46. IEEE, 2008. Google Scholar
  42. Donald Nguyen, Andrew Lenharth, and Keshav Pingali. Deterministic galois: On-demand, portable and parameterless. ACM SIGPLAN Notices, 49(4):499-512, 2014. Google Scholar
  43. Peter O'Hearn. Separation logic. Communications of the ACM, 62(2):86-95, 2019. Google Scholar
  44. Matthew J. Parkinson and Alexander J. Summers. The relationship between separation logic and implicit dynamic frames. In ESOP, volume 6602, pages 439-458. Springer, 2011. Google Scholar
  45. Christian Pilato, Stanislav Bohm, Fabien Brocheton, Jeronimo Castrillon, Riccardo Cevasco, Vojtech Cima, Radim Cmar, Dionysios Diamantopoulos, Fabrizio Ferrandi, Jan Martinovic, et al. Everest: A design environment for extreme-scale big data analytics on heterogeneous platforms. In 2021 Design, Automation & Test in Europe Conference & Exhibition (DATE), pages 1320-1325. IEEE, 2021. Google Scholar
  46. Cosmin Radoi, Stephen J. Fink, Rodric Rabbah, and Manu Sridharan. Translating imperative code to mapreduce. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '14, pages 909-927, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2660193.2660228.
  47. Mike Rainey, Ryan R. Newton, Kyle Hale, Nikos Hardavellas, Simone Campanoni, Peter Dinda, and Umut A. Acar. Task parallel assembly language for uncompromising parallelism. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pages 1064-1079, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3453483.3460969.
  48. Ganesan Ramalingam. The undecidability of aliasing. ACM Transactions on Programming Languages and Systems (TOPLAS), 16(5):1467-1471, 1994. Google Scholar
  49. Kaushik Ravichandran, Ada Gavrilovska, and Santosh Pande. Destm: Harnessing determinism in stms for application development. In Proceedings of the 23rd International Conference on Parallel Architectures and Compilation, PACT '14, pages 213-224, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2628071.2628094.
  50. Federico Reghenzani, Giuseppe Massari, and William Fornaciari. Timing predictability in high-performance computing with probabilistic real-time. IEEE Access, 8:208566-208582, 2020. Google Scholar
  51. 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
  52. Fred B. Schneider. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys (CSUR), 22(4):299-319, 1990. Google Scholar
  53. Aaron Turon. Understanding and expressing scalable concurrency. PhD thesis, Northeastern University, 2013. Google Scholar
  54. Alexa VanHattum, Daniel Schwartz-Narbonne, Nathan Chong, and Adrian Sampson. Verifying dynamic trait objects in rust. In Proceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice, ICSE-SEIP '22, pages 321-330, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3510457.3513031.
  55. Philip Wadler. Linear types can change the world! In Programming concepts and methods, volume 3, page 5. Citeseer, 1990. Google Scholar
  56. Philip Wadler. The essence of functional programming. In Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 1-14, 1992. Google Scholar
  57. Yu Xia, Xiangyao Yu, William Moses, Julian Shun, and Srinivas Devadas. Litm: A lightweight deterministic software transactional memory system. In Proceedings of the 10th International Workshop on Programming Models and Applications for Multicores and Manycores, pages 1-10, 2019. Google Scholar
  58. Yuan Yu, Martín Abadi, Paul Barham, Eugene Brevdo, Mike Burrows, Andy Davis, Jeff Dean, Sanjay Ghemawat, Tim Harley, Peter Hawkins, et al. Dynamic control flow in large-scale machine learning. In Proceedings of the Thirteenth EuroSys Conference, pages 1-15, 2018. Google Scholar
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