The trend toward system specialization is leading to a proliferation of accelerators, exposing interconnects as serious bottlenecks, both in functionality and performance. As a result, several alternative approaches have been proposed which promise to expand the coherence domain beyond homogeneous sockets to rack scale heterogeneous systems. In parallel, GPU vendors have developed their own high bandwidth interconnects also aiming for heterogeneous coherence beyond the CPU. This expansion of the coherency domain raises many questions that remain unanswered, in particular, how devices other than CPUs will interact with the coherence protocol and whether applications can take advantage of these expanded domains. As protocols such as CXL are still evolving, it is important to explore alternative designs that go beyond what the commercial specifications dictate. For this purpose, we developed CCKit, an open-source, server-class toolkit comprising a complete cache coherency stack on reconfigurable accelerators. CCKit is more flexible than commercial products and its performance is highly competitive with hardware-based implementations, thus enabling important and novel application use-cases for expanded coherence domains. Experimental data from real workloads provide the ability to influence and expand future interconnects, protocols, and applications.

Writing device drivers is notoriously hard, and driver bugs are a major cause of system failures and vulnerabilities. The problem is particularly acute in bus-based protocols like (IC)-C-2, where driver correctness is only half the story: correct functioning of the complete subsystem depends on all components on the bus interoperating correctly. Unfortunately, developers cannot control all aspects of a platform, and must interact with existing devices (peripherals and/or hardware bus controllers) which may misbehave. Failures in a protocol like (IC)-C-2, often used in critical low-level system management, can result in permanent damage to the hardware, whether a server or a satellite. Existing techniques for creating high assurance drivers rarely tackle this interoperability issue. We present Efeu, a framework for implementing verifiably interoperable drivers for (IC)-C-2 devices. Using model checking-based verification, Efeu generates driver implementations in software, reconfigurable logic for FPGAs, and, notably, combinations of both. The split between software and hardware can be varied at implementation time and the hardwarfeu, we design and evaluate a verified (IC)-C-2 driver stack, and demonstrate that Efeu finds optimal hardwae/software interface is generated automatically, enabling efficient exploration of the design space. Using Ere/software tradeoffs to favor either throughput, CPU usage or FPGA footprint. For each objective, Efeu generates drivers with performance comparable with hand-optimized hardware/software drivers.

Modern hardware platforms are increasingly complex and heterogeneous. System software uses a hodgepodge of different mechanisms and representations to express the memory topology of the target platform. Considerable maintenance effort is required to keep them in sync while often sharing is impossible due to hard-coded values. Incorrect platform-specific values in the hardware initialization sequence can lead to security critical and hard-to-find bugs because of misconfigured translation hardware, inaccessible devices, or the use of bad pointers. We present a better way for system software to express and initialize memory hardware. We adopt an existing, powerful hardware description language, and efficiently compile it to generate correct initial page tables and memory maps for OS kernels and firmware from a single system description. We evaluate our system on multiple architectures and platforms, and demonstrate that we can use the generated data structures to successfully initialize translation hardware, devices, memory maps, and allocators enabling easy support of new hardware platforms.

The immense hardware complexity of modern computers, both mobile phones and datacenter servers, is a seemingly endless source of bugs and vulnerabilities in system software. Classical OSes cannot address this, since they only run on a small subset of the machine. The issue is interactions within the entire ensemble of firmware blobs, co-processors, and CPUs that we term the de facto OS. The current "whac-a-mole" approach will not solve this problem, nor will clean-slate redesign: it is simply not possible to replace some firmware components and the engineering effort is too great. Our response, instead, is to build a high-level model of exactly what a given real hardware and software platform consists of, and captures for the first time the necessary and assumed trust relationships between the software contexts executing on different components (CPUs, devices, etc.). This principled but pragmatic approach allows us to make rigorous statements about the hodgepodge of soft- and firmware at the heart of modern computers. We expect these statements to be, at first, depressingly weak, but it may be the only way to identify changes that provably increase the trustworthiness of a real system, and quantify the benefits of these changes.

Verification of any operating system is inevitably relative to a model of the underlying hardware. Within the context of kernel verification, the underlying hardware model usually comprises of architectural correctness of the executing cores, but pays little attention to devices underneath barring the assumption that they are "trusted". Recent work has pointed out that the de facto operating system of a machine includes not only the kernel and processes running on top, but the multitude of other devices driving the actual hardware: security (co-)processors, DMA engines, network firmware, and more. The concept of the de facto OS shines light on a critical boundary between a kernel and the rest of hardware which is crucial to reasoning about both kernel isolation, and the security properties of the whole operating system. In this paper we report on our experience to date in specifying the de facto OS environment of a production System-on-Chip, and the implications of this effort so far for assured kernel isolation.

Hybrid computing platforms, comprising CPU cores and FPGA logic, are increasingly used for accelerating data-intensive workloads in cloud deployments, and are a growing topic of interest in systems research. However, from a research perspective, existing hardware platforms are limited: they are often optimized for concrete, narrow use-cases and, therefore lack the flexibility needed to explore other applications and configurations. We show that a research group can design and build a more general, open, and affordable hardware platform for hybrid systems research. The platform, Enzian, is capable of duplicating the functionality of existing CPU/FPGA systems with comparable performance but in an open, flexible system. It couples a large FPGA with a server-class CPU in an asymmetric cache-coherent NUMA system. Enzian also enables research not possible with existing hybrid platforms, through explicit access to coherence messages, extensive thermal and power instrumentation, and an open, programmable baseboard management processor. Enzian is already being used in multiple projects, is open source (both hardware and software), and available for remote use. We present the design principles of Enzian, the challenges in building it, and evaluate it with a range of existing research use-cases alongside other, more specialized platforms, as well as demonstrating research not possible on existing platforms.

With the computational systems of even embedded devices becoming ever more powerful, there is a need for more effective and pro-active methods of dynamic power management. The work presented in this paper demonstrates the effectiveness of a reinforcement-learning based dynamic power manager placed in a software framework. This combination of Q-learning for determining policy and the software abstractions provide many of the benefits of co-design, namely, good performance, responsiveness and application guidance, with the flexibility of easily changing policies or platforms. The Q-learning based Quality of Service Manager (2QoSM) is implemented on an autonomous robot built on a complex, powerful embedded single-board computer (SBC) and a high-resolution path-planning algorithm. We find that the 2QoSM reduces power consumption up to 42% compared to the Linux on-demand governor and 10.2% over a state-of-the-art situation aware governor. Moreover, the performance as measured by path error is improved by up to 6.1%, all while saving power.

Modern Systems-on-Chip (SoCs) are networks of heterogeneous cores, intelligent devices, and memory, connected through multiple configurable address translation and protection units like IOMMUs and System MMUs. Modern OS kernels like Linux are based on traditional MMUs and have no clear abstractions to represent this complexity, mostly leaving IOMMU configuration to device drivers. This has led to a recent spate of serious bugs, and increasing concern over "cross-SoC" attacks on memory security. To address this, we propose a new kernel primitive, mmapx, based on a decoding net a rich and detailed representation of the memory addressing semantics of a complex SoC from the recent formal methods literature. mmapx provides a uniform facility for securely configuring all the address translation facilities in a system. mmapx leverages existing Unix facilities wherever possible: the file system for naming, discovery, and coarse-grained access control, and file descriptors for fine-grained authorization. We show how mmapx can eliminate bugs caused by device drivers programming IOMMUs directly, but also the detail captured by the underlying model has further benefits while incurring minimal overhead.

I2C is a pervasive bus protocol used for querying sensors and actuators, but it is plagued with incompatible devices, violating the specification at various levels. Interacting with partially compliant devices poses several challenges. Compatibility of the controller interface, as well as the driver code, must be checked manually and potentially changed. This is a difficult process, as interactions with other bus devices must also be considered. We propose a model checking approach to quickly write high-assurance drivers and layers of the I2C stack. We do not propose a single, true formalization of I2C, but a framework that allows rapid modelling of non-compliant devices and verify the correct interaction with a host driver process. Our contribution is twofold: First, we develop a framework that allows the specification of device and driver behavior together, and verification of their correct interaction. Second, we provide already verified, fine-grained building blocks, representing layers of the I2C stack that can be reused to interact with partially-compliant devices, as well as reducing model checking complexity. Our specifications are stated in a machine-readable, executable, and layered DSL. From the DSL, we generate both Promela and C code. The Promela is used to apply model checking to ensure the layer implementations follow the abstract specifications. The C code is used to build and verify an EEPROM model and driver running on a Raspberry Pi.

SUMMARYGaze stabilization reflexes reduce motion blur and simplify the processing of visual information by keeping the eyes level. These reflexes typically depend on estimates of the rotational motion of the body, head, and eyes, acquired by visual or mechanosensory systems. During rapid movements, there can be insufficient time for sensory feedback systems to estimate rotational motion, requiring additional mechanisms. Solutions to this common problem are likely to be adapted to an animal’s behavioral repertoire. Here, we examine gaze stabilization in three families of dipteran flies, each with distinctly different flight behaviors. Through frequency response analysis based on tethered-flight experiments, we demonstrate that fast roll oscillations of the body lead to a stable gaze in hoverflies, whereas the reflex breaks down at the same speeds in blowflies and horseflies. Surprisingly, the high-speed gaze stabilization of hoverflies does not require sensory input from the halteres, their low-latency balance organs. Instead, we show how the behavior is explained by a hybrid control system that combines a sensory-driven, active stabilization component mediated by neck muscles, and a passive component which exploits physical properties of the animal’s anatomy—the mass and inertia of its head. This adaptation requires hoverflies to have specializations of the head-neck joint that can be employed during flight. Our comparative study highlights how species-specific control strategies have evolved to support different visually-guided flight behaviors.SIGNIFICANCE STATEMENTAcross the animal kingdom, reflexes are found which stabilize the eyes to reduce the impact of motion blur on vision—analogous to the image stabilization functions found in modern cameras. These reflexes can be complex, often combining predictions about planned movements with information from multiple sensory systems which continually measure self-motion and provide feedback. The processing of this information in the nervous system incurs time delays which impose limits on performance when fast stabilization is required. Hoverflies overcome the limitations of sensory-driven stabilization reflexes by exploiting the passive stability provided by the head during roll perturbations with particularly high rotational kine-matics. Integrating passive and active mechanisms thus extends the useful range of vision and likely facilitates distinctive aspects of hoverfly flight.

Modern computer server systems are increasingly managed at a low level by baseboard management controllers (BMCs). BMCs are processors with access to the most critical parts of the platform, below the level of OS or hypervisor, including control over power delivery to every system component. Buggy or poorly designed BMC software not only poses a security threat to a machine, it can permanently render the hardware inoperative. Despite this, there is little published work on how to rigorously engineer the power management functionality of BMCs so as to prevent this happening. This article takes a first step toward putting BMC software on a sound footing by specifying the hardware environment and the constraints necessary for safe and correct operation. This is best accomplished through automation: correct-by-construction power control sequences can be efficiently generated from a simple, trustworthy model of the platform’s power tree that incorporates the sequencing requirements and safe voltage ranges of all components. We present both a modeling language for complex power-delivery networks and a tool to automatically generate safe, efficient power sequences for complex modern platforms. This not only increases the trustworthiness of a hitherto opaque yet critical element of platform firmware: regulator and chip power models are significantly simpler to produce than hand-written power sequences. This, combined with model reuse for common components, reduces both time and cost associated with platform bring-up for new hardware. We evaluate our tool using a new high-performance 2-socket server platform with >100W per socket TDP, tight voltage limits and 25 distinct power regulators needing configuration, showing both fast (<10s) tool runtime, and correct power sequencing of a live system.

This paper describes the design and performance of Q-learning-based quality-of-service manager (2QoSM) for compute-aware applications (CAAs) as part of platform-agnostic resource management framework. CAAs and hardware are able to share metrics of performance with the 2QoSM and the 2QoSM can attempt to reconfigure CAAs and hardware to meet performance targets. This enables many co-design benefits while allowing for policy and platform portability. The use of Q-Learning allows online generation of the power management policy without requiring details about system state or actions, and can meet different goals including error, power minimization, or a combination of both. 2QoSM, evaluated using an embedded MCSoC controlling a mobile robot, reduces power compared to the Linux on-demand governor by 38.7-42.6% and a situation-aware governor by 4.0-10.2%. An error-minimization policy obtained a reduction in path-following error of 4.6-8.9%.

Almost all modern hardware, from phone SoCs to high-end servers with accelerators, contain memory translation and protection hardware like IOMMUs, firewalls, and lookup tables which make it impossible to reason about, and enforce protection and isolation based solely on the processor's MMUs. This has led to numerous bugs and security vulnerabilities in today's system software. In this paper we regain the ability to reason about and enforce access control using the proven concept of a reference monitor mediating accesses to memory resources. We present a fine-grained, realistic memory protection model that makes this traditional concept applicable today, and bring system software in line with the complexity of modern, heterogeneous hardware. Our design is applicable to any operating system, regardless of architecture. We show that it not only enforces the integrity properties of a system, but does so with no inherent performance overhead and it is even amenable to automation through code generation from trusted hardware specifications.

Digital voice assistants (e.g., Alexa, and Siri) have increased users’ acceptance and expectations in getting immediate help from smart agents available in smartphones and IoT devices. However, such assistants are capable of performing simple tasks that can be accomplished with specific commands, and minimum user interaction, e.g., “play some music”. A Digital Companion goes beyond assisting to complete a task upon request, a Digital Companion knows its users, the environment they interact with, and their relationship with other users, it learns with time, gathers information from heterogenous sources, analyzes it, and provides relevant and suitable information and recommendations about available services. Thus, a Digital Companion frees users from redundant, boring tasks; allowing them to focus on the meaningful parts of their activities. In this paper, an instance of a Digital Companion is presented, which combines semantic technologies and speech recognition to provide air travelers with a tool that enhances their experience at airports.

We present CleanQ, a high-performance operating-system interface for descriptor-based data transfer with rigorous formal semantics, based on a simple, formally-verified notion of ownership transfer, with a fast reference implementation. CleanQ aims to replace the current proliferation of similar, but subtly diverse, and loosely specified, descriptor-based interfaces in OS kernels and device drivers. CleanQ has strict semantics that not only clarify both the implementation of the interface for different hardware devices and software usecases, but also enable composition of modules as in more heavyweight frameworks like Unix streams. We motivate CleanQ by showing that loose specifications derived from implementation lead to security and correctness bugs in production systems that a clean, formal, and easilyunderstandable abstraction helps eliminate. We further demonstrate by experiment that there is negligible performance cost for a clean design: we show overheads in the tens of cycles for operations, and comparable end-to-end performance to the highly-tuned Virtio and DPDK implementations on Linux.

We present a new least-privilege-based model of addressing on which to base memory management functionality in an OS for modern computers like phones or server-based accelerators. Existing software assumptions do not account for heterogeneous cores with different views of the address space, leading to the related problems of numerous security bugs in memory management code (for example programming IOMMUs), and an inability of mainstream OSes to securely manage the complete set of hardware resources on, say, a phone System-on-Chip. Our new work is based on a recent formal model of address translation hardware which views the machine as a configurable network of address spaces. We refine this to capture existing address translation hardware from modern SoCs and accelerators at a sufficiently fine granularity to model minimal rights both to access memory and configure translation hardware. We then build an executable specification in Haskell, which expresses the model and metadata structures in terms of partitioned capabilities. Finally, we show a fully functional implementation of the model in C created by extending the capability system of the Barrelfish research OS. Our evaluation shows that our unoptimized implementation has comparable (and in some cases) better performance than the Linux virtual memory system, despite both capturing all the functionality of modern hardware addressing and enabling least-privilege, decentralized authority to access physical memory and devices.

Visualizing fast micrometer scale internal movements of small animals is a key challenge for functional anatomy, physiology and biomechanics. We combine phase contrast tomographic microscopy (down to 3.3 μm voxel size) with retrospective, projection-based gating (in the order of hundreds of microseconds) to improve the spatiotemporal resolution by an order of magnitude over previous studies. We demonstrate our method by visualizing 20 three-dimensional snapshots through the 150 Hz oscillations of the blowfly flight motor.

Mobile phones can use their cameras and flashlight Light Emitting Diodes (LEDs) to exchange messages with low-complex Visible Light Communication (VLC) networks, but these interfaces impose serious restrictions when used in a VLC network. In this paper we discuss how to extend mobile phones or tablets with a small peripheral device that is battery-free, uses only passive components, and offers VLC capabilities at the required data rate (kilobit per second). This device plugs into the audio jack; on-board audio signal processing generates the outgoing light signals as well as decodes the incoming light signals. The device is powered from the phone's audio jack output signal, no additional battery is required. The audio signals directly modulate light emissions of an LED. Incoming light is detected by a photodiode and the generated electrical signals are fed into the microphone input. This simple device enables use of existing communication protocols and therefore makes it possible to integrate mobile phones or tablets into existing VLC LED-to-LED networks.