ICOOOLPS '24: "Miri: Practical Undefined ..."
Miri: Practical Undefined Behavior Detection for Rust (Keynote)
Ralf Jung
(ETH Zurich, Switzerland)
Rust is most well-known for it strong type system, guaranteeing memory safety and thread safety despite a low-level programming paradigm that does not require a garbage collector. However, not all code can be written in the confines of a safe type system: sometimes, the programmer has to be more clever than the compiler permits. This is where unsafe Rust comes in, a set of additional operations that come with great power and great responsibility. They give programmers the power to program directly against the underlying machine model, side-stepping all the limitations of the type system. However, it is the programmer’s responsibility to ensure that the preconditions of these unsafe operations are maintained, or else runtime behavior is entirely unconstrained – the infamous Undefined Behavior. Miri is a tool that helps programmers deal with this responsibility. Specifically, Miri can execute Rust code in a way that detects (almost) all Undefined Behavior. It is trivial to deploy, requiring no annotations and being distributed with the Rust nightly toolchain. Miri has found numerous bugs in real-world code and has become a standard tool for unsafe Rust programmers. That makes it the first practical tool for reliably detecting Undefined Behavior – in any language. In this talk, I will give an overview of what kinds of bugs Miri is able to find, how Miri works, and how it helps in the ongoing effort of formally specifying the Rust language.
@InProceedings{ICOOOLPS24p1,
author = {Ralf Jung},
title = {Miri: Practical Undefined Behavior Detection for Rust (Keynote)},
booktitle = {Proc.\ ICOOOLPS},
publisher = {ACM},
pages = {1--1},
doi = {10.1145/3679005.3695733},
year = {2024},
}
Publisher's Version
ICOOOLPS '24: "Stack-Copying Delimited Continuations ..."
Stack-Copying Delimited Continuations for Scala Native
Cao Nguyen Pham and Martin Odersky
(EPFL, Switzerland)
Scala, an industrial-strength functional and object-oriented programming language, is in need for an ergonomic approach to asynchronous programming. Project Loom provides direct-style concurrency to Scala on the JVM, which leaves its low-footprint high-performance backend Scala Native looking for an equivalent mechanism. We present a design and implementation of delimited continuations, a powerful control flow mechanism that provides the fundamental building block for direct-style concurrent and effectful programming, in Scala Native. Our implementation aims to preserve the unique advantages of the Native target: zero-cost C interoperability, runtime modularity and debugger compatibility. Through a detailed discussion of the implementation, we show that despite the limitations with stack address stability, it meets all the requirements of Scala Native while exhibiting comparable performance to our JVM counterpart.
@InProceedings{ICOOOLPS24p2,
author = {Cao Nguyen Pham and Martin Odersky},
title = {Stack-Copying Delimited Continuations for Scala Native},
booktitle = {Proc.\ ICOOOLPS},
publisher = {ACM},
pages = {2--13},
doi = {10.1145/3679005.3685979},
year = {2024},
}
Publisher's Version
ICOOOLPS '24: "Stack-Copying Delimited Continuations ..."
Stack-Copying Delimited Continuations for Scala Native
Cao Nguyen Pham and Martin Odersky
(EPFL, Switzerland)
Scala, an industrial-strength functional and object-oriented programming language, is in need for an ergonomic approach to asynchronous programming. Project Loom provides direct-style concurrency to Scala on the JVM, which leaves its low-footprint high-performance backend Scala Native looking for an equivalent mechanism. We present a design and implementation of delimited continuations, a powerful control flow mechanism that provides the fundamental building block for direct-style concurrent and effectful programming, in Scala Native. Our implementation aims to preserve the unique advantages of the Native target: zero-cost C interoperability, runtime modularity and debugger compatibility. Through a detailed discussion of the implementation, we show that despite the limitations with stack address stability, it meets all the requirements of Scala Native while exhibiting comparable performance to our JVM counterpart.
@InProceedings{ICOOOLPS24p2,
author = {Cao Nguyen Pham and Martin Odersky},
title = {Stack-Copying Delimited Continuations for Scala Native},
booktitle = {Proc.\ ICOOOLPS},
publisher = {ACM},
pages = {2--13},
doi = {10.1145/3679005.3685979},
year = {2024},
}
Publisher's Version