Write a Blog >>
Fri 24 Jan 2020 14:00 - 14:21 at Ile de France III (IDF III) - Language Design Chair(s): Amin Timany

Type systems are useful not just for the safety guarantees they provide, but also for helping compilers generate more efficient code by simplifying important program analyses. In Rust, the type system imposes a strict discipline on pointer aliasing, and it is an express goal of the Rust compiler developers to make use of that alias information for the purpose of program optimizations that reorder memory accesses. The problem is that Rust also supports unsafe code, and programmers can write unsafe code that bypasses the usual compiler checks to violate the aliasing discipline. To strike a balance between optimizations and unsafe code, the language needs to provide a set of rules such that unsafe code authors can be sure, if they are following these rules, that the compiler will preserve the semantics of their code despite all the optimizations it is doing.

In this work, we propose Stacked Borrows, an operational semantics for memory accesses in Rust. Stacked Borrows defines an aliasing discipline and declares programs violating it to have undefined behavior, meaning the compiler does not have to consider such programs when performing optimizations. We give formal proofs (mechanized in Coq) showing that this rules out enough programs to enable optimizations that reorder memory accesses around unknown code and function calls, based solely on intraprocedural reasoning. We also implemented this operational model in an interpreter for Rust and ran large parts of the Rust standard library test suite in the interpreter to validate that the model permits enough real-world unsafe Rust code.

Slides (pdf) (talk.pdf)2.4MiB

Fri 24 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

14:00 - 15:05: Research Papers - Language Design at Ile de France III (IDF III)
Chair(s): Amin Timanyimec-Distrinet KU-Leuven
POPL-2020-Research-Papers14:00 - 14:21
Ralf JungMPI-SWS, Hoang-Hai DangMPI-SWS, Jeehoon KangKAIST, Derek DreyerMPI-SWS
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers14:21 - 14:43
Michael GreenbergPomona College, Austin J. BlattPuppet Labs
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers14:43 - 15:05
Sam WestrickCarnegie Mellon University, Rohan YadavCarnegie Mellon University, Matthew FluetRochester Institute of Technology, Umut A. AcarCarnegie Mellon University
Link to publication DOI Media Attached File Attached