PLOS '17: Proceedings of the 9th Workshop on Programming Languages and Operating Systems

Property-based testing can play an important role in reducing the cost of formal verification: It has been demonstrated to be effective at detecting bugs and finding inconsistencies in specifications, and thus can eliminate effort wasted on fruitless proof attempts. We argue that in addition, property-based testing enables an incremental approach to a fully verified system, by allowing replacement of automatically generated tests of properties stated in the specification by formal proofs. We demonstrate this approach on the verification of systems code, discuss the implications on systems design, and outline the integration of property-based testing into the Cogent framework.

In this paper we address the problem of correctly configuring interrupts. The interrupt subsystem of a computer is increasingly complex: a zoo of different controllers with varying constraints and capabilities form a network with limited connectivity. An OS which aspires to provable correctness must manage a limited set of interrupt vectors, delegate interrupts to device drivers and configure the controllers correctly. No well-specified approach exists.

As a foundation for applying language-level techniques like program sketching and synthesis to this problem, we present a formal model for interrupt routing which can capture all the system topologies and interrupt controllers we have encountered in the wild, show applications of such a model not possible with informal, ad-hoc approaches like DeviceTrees, and finally discuss an implementation based on the model which forms the new interrupt subsystem of the Barrelfish OS.

The actor model is a popular paradigm for programming scalable cloud applications. Building elastic and scalable cloud applications requires application developers to carefully adjust the application scale (the required resources) and the placement of actors at the runtime. Unfortunately, there is no efficient solution which could manage application elasticity automatically during runtime without disrupting ongoing requests. This paper proposes the idea of programmable elasticity approach, which allows application developers to define a set of elasticity rules for different actors. The runtime service endeavors to apply the elasticity rules while relieving the application programmer from dealing with the management of distributed state and efficient utilization of cloud resources.

The combination of improved battery technology and more power-efficient computing hardware has led to the proliferation of heterogeneous distributed systems. This internet of things consists of embedded, wearable, hobbyist, parallel, and commodity devices. Given the different resource and power constraints of such systems, applications must be able to reconfigure or adapt their runtime execution environment in order to make best use of the resources available. In order for the underlying operating system/runtime to support runtime adaptation, an application must be suitably designed. The actor model of computation presents a natural fit for programming such adaptive systems with shared-nothing semantics and use of message passing. This paper addresses the limitations of current actor approaches and argues that an actor is the appropriate unit of adaptation. This is justified through experimentation across heterogeneous platforms.

In prior work, we have shown that the underdiagnosed problem of state spill remains a barrier to realizing complex systems that are easy to maintain, evolve, and run reliably. This paper shares our early experience building Theseus from scratch, an OS with the guiding principle of eliminating state spill. Theseus takes inspiration from distributed systems to rethink state management, and leverages Rust language features for maximum safety, code reuse, and efficient isolation. We intend to demonstrate Theseus as a runtime composable OS, in which entities are easily interchangeable and can evolve independently without reconfiguring or rebooting.

Aspect Oriented Programming (AOP) supports the modular implementation of crosscutting concerns, which are woven into program parts designated by pointcuts, e.g. calls to specific functions. The release of AspectC++ 2.2 introduces the ability to express pointcuts based on C++11-style attributes as well as the definition of custom attributes for annotation purposes. In this paper, we propose the use of such attributes for operating system development. We cover three examples: Replacing non-portable compiler attributes and extending portable ones with domain-specific knowledge, providing implementation-independent joinpoint APIs to core operating system functions, and compile-time support for co-development of source code and corresponding models. We discuss the implementation effort and code size overhead of our ideas on the operating systems CocoOS and RIOT and show that annotations with custom attributes are a helpful addition for system development.

The rise of language-specific, third-party packages simplifies application development. However, relying on untrusted code poses a threat to security and reliability.

In this work, we propose exploiting module boundaries --and the general trend towards more and smaller modules --to achieve fine-grained compartmentalization. Automated transformations can hide compartment boundaries and minimize developer effort. Optional policy expressions can decouple security assumptions at development time from requirements during composition and runtime. Using JavaScript's flourishing ecosystem, we discuss a wide range of risks and sketch how the use of language-level solutions coupled systemic mechanisms can protect against them.

System-level development has been dominated by traditional programming languages such as C and C++ for decades. These languages are inherently unsafe regarding memory management. Even experienced developers make mistakes that open up security holes or compromise the safety properties of software. The Rust programming language is targeted at the systems domain and aims to eliminate memory-related programming errors by enforcing a strict memory model at the language and compiler level. Unfortunately, these compile-time guarantees no longer hold when a Rust program is linked against a library written in unsafe C, which is commonly required for functionality where an implementation in Rust is not yet available.

In this paper, we present Sandcrust, an easy-to-use sand-boxing solution for isolating code and data of a C library in a separate process. This isolation protects the Rust-based main program from any memory corruption caused by bugs in the unsafe library, which would otherwise invalidate the memory safety guarantees of Rust. Sandcrust is based on the Rust macro system and requires no modification to the compiler or runtime, but only straightforward annotation of functions that call the library's API.