On the Challenge of Sound Code for Operating Systems

Workshop on Programming Languages and Operating Systems (PLOS), pp. 83–90

Abstract

The memory-safe systems programming language Rust is gaining more and more attention in the operating system development communities, as it provides memory safety without sacrificing performance or control. However, these safety guarantees only apply to the safe subset of Rust, while bare-metal programming requires some parts of the program to be written in unsafe Rust. Writing abstractions for these parts of the software that are sound, meaning that they guarantee the absence of undefined behavior and thus uphold the invariants of safe Rust, can be challenging. Producing sound code, however, is essential to avoid breakage when the code is used in new ways or the compiler behavior changes.

Authors 3

1. Jonathan Klimt Aachen Institute for Automation of Complex Power Systems

   RWTH Aachen University

   Affiliation as printed

   Institute for Automation of Complex Power Systems, Aachen, Germany

2. Stefan Lankes Aachen Institute for Automation of Complex Power Systems

   RWTH Aachen University

   Affiliation as printed

   Institute for Automation of Complex Power Systems, Aachen, Germany

3. Antonello Monti

   Fraunhofer Institute for Applied Information Technology

   Affiliation as printed

   Institute for Automation of Complex Power Systems, Aachen, Germany, Fraunhofer Institute for Applied Information Technology, Sankt Augustin, Germany