The use of disaggregated or far memory systems such as CXL memory pools has renewed interest in Near-Data Processing (NDP): situating cores close to memory to reduce bandwidth requirements to and from the CPU. Hardware designs for such accelerators are appearing, but there lack clean, portable OS abstractions for programming them. We propose a programming model for NDP devices based on familiar OS abstractions: virtual processors (processes) and inter-process communication channels (like Unix pipes). While appealing from a user perspective, a naive implementation of such abstractions is inappropriate for NDP accelerators: the paucity of processing power in some hardware designs makes classical processes overly heavyweight, and IPC based on shared buffers makes no sense in a system designed to reduce memory bandwidth. Accordingly, we show how to implement these abstractions in a lightweight and efficient manner by exploiting compilation and interconnect protocols. We demonstrate them with a real hardware platform runing applications with a range of memory access patterns, including bulk memory operations, in-memory databases and graph applications. Crucially, we show not only the benefits over CPU-only implementations, but also the critical importance of efficient, low-latency communication channels between CPU and NDP accelerators, a feature largely neglected in existing proposals.

Systems programmers have to consolidate the ever growing hardware mess present on modern System-on-Chips (SoCs). Correctly programming a multitude of components, providing functionality but also security, is a difficult problem: semantics of individual units are described in English prose, descriptions are often underspecified, and prone to inaccuracies. Rigorous statements about platform security are often impossible. We introduce a domain-specific language to describe hardware semantics, assumptions about software behavior, and desired security properties. We then create machine-readable specifications for a diverse set of eight SoCs from their reference manuals, and formally prove their (in-)security. In addition to security proofs about memory confidentiality and integrity, we discover a handful of documentation errors. Finally, our analysis also revealed a vulnerability on a real-world server chip. Our tooling offers system integrators a way of formally describing security properties for entire SoCs, and means to prove them or find counterexamples to them.

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.

Despite the promise of alleviating the main memory bottleneck, and the existence of commercial hardware implementations, techniques for Near-Data Processing have seen relatively little real-world deployment. The idea has received renewed interest with the appearance of disaggregated or "far" memory, for example in the use of CXL memory pools. However, we argue that the lack of a clear OS-centric abstraction of Near-Data Processing is a major barrier to adoption of the technology. Inspired by the channel controllers which interface the CPU to disk drives in mainframe systems, we propose memory channel controllers as a convenient, portable, and virtualizable abstraction of Near-Data Processing for modern disaggregated memory systems. In addition to providing a clean abstraction that enables OS integration while requiring no changes to CPU architecture, memory channel controllers incorporate another key innovation: they exploit the cache coherence provided by emerging interconnects to provide a much richer programming model, with more fine-grained interaction, than has been possible with existing designs.

The network interface adapter (NIC) is a critical component of a cloud server occupying a unique position. Not only is network performance vital to efficient operation of the machine, but unlike compute accelerators like GPUs, the network subsystem must react to unpredictable events like the arrival of a network packet and communicate with the appropriate application end point with minimal latency. Current approaches to server stacks navigate a trade-off between flexibility, efficiency, and performance: the fastest kernel-bypass approaches dedicate cores to applications, busy-wait on receive queues, etc. while more flexible approaches appropriate to more dynamic workload mixes incur much greater software overhead on the data path. However, we reject this trade-off, which we ascribe to an arbitrary (and sub-optimal) split in system state between the OS and the NIC. Instead, by exploiting the properties of cache-coherent interconnects and integrating the NIC closely with the OS kernel, we can achieve something surprising: performance for RPC workloads better than the fastest kernelbypass approaches without sacrificing the robustness and dynamic adaptation of kernel-based network subsystems.

Low level software is often granted high privilege, yet this need not be the case. Although vendor firmware plays a critical role in the operation and management of the machine, most of its functionality does not require unfettered access to security critical software and data. In this paper we demonstrate that vendor firmware can be safely and efficiently deprivileged, decoupling its functionality from isolation enforcement. We introduce a new class of systems, called virtual firmware monitors, that run unmodified vendor firmware in userspace through software-based virtualization of the highest privilege mode of the application CPU. We describe the implementation of Miralis, a RISC-V virtual firmware monitor, and develop three security policies to protect the OS, enclaves, and confidential VMs from malicious firmware. We verify key components of Miralis, such as instruction emulation and memory protection, through exhaustive symbolic execution. Finally, we demonstrate that Miralis can effectively virtualize unmodified vendor firmware for two hardware platforms with no performance degradation compared to native execution.

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.

A single tracing component embedded into a high-frequency processor may produce up to 1 GB/s of trace data or more. These data are vital in debugging, monitoring, verification, and performance analysis in System-on-chip and heterogeneous system development. Hardware trace decoders and analyzers have emerged to support online processing of trace data for real-time applications. However, the existing hardware trace decoders designed for the Embedded Trace Macrocell version 4 (ETMv4), a standard feature in most modern ARM processors, can only process trace data at a maximum rate of 250 MB/s. This paper proposes an optimized and parallelized trace decoder for the ETMv4 specification implemented on a Xilinx Ultrascale+ processing up to 1 GB/s of trace data from a single ETM.

In this paper, we extend open-state conformance testing from Mealy FSM specifications to implementations where only a subset of states are observable. We show that the classical transition tour can be used to completely test such implementations for conformance, including unobservable states, under the assumption that in the specification, any trace from an unobservable state eventually reaches an observable state - i.e. that the observable states form a feedback vertex set. Complete transition tour testing can efficiently test for many conformance relations when they are appropriately formulated. Generalized-quasi-reduction (GQR) is useful for protocol testing because it allows for partial, non-deterministic specifications, but establishing GQR in the general setting is complex and expensive. We show a relation that implies GQR and is practical for transition tour testing. Our setting of partial state observability applies to an important class of protocol implementations in modern hardware: cache coherence. These protocols are nearly universal in multi-processor systems, and are notoriously difficult to verify both at the specification and implementation level. We show that their structure lends them naturally to complete open-state testing under this extended definition. During design, coherence protocols are elaborated from an FSM of stable states with atomic, observable transitions by the addition of a large number of unobservable transient states to handle concurrency, including out-of-order and interleaved message delivery. We demonstrate that a real in-silicon implementation on the Cavium ThunderX-1 CN88XX CPU has exactly the required characteristics and we establish the GQR conformance relation against a specification of its inter-socket coherence protocol.

Conventional wisdom holds that an efficient interface between an OS running on a CPU and a high-bandwidth I/O device should be based on Direct Memory Access (DMA), descriptor rings, and interrupts: DMA offloads transfers from the CPU, descriptor rings provide buffering and queuing, and interrupts facilitate asynchronous interaction between cores and device with a lightweight notification mechanism. In this paper we question this wisdom in the light of modern hardware and workloads, particularly in cloud servers. We argue that the assumptions that led to this model are obsolete, and in many use-cases use of programmed I/O, where the CPU explicitly transfers data and control information to and from a device via loads and stores, actually results in a more efficient system. We quantitatively demonstrate these advantages using three use-cases: fine-grained RPC-style invocation of functions on an accelerator, offloading of operators in a streaming dataflow engine, and a network interface targeting for serverless functions. Moreover, we show that while these advantages are significant over a modern PCIe peripheral bus, a truly cache-coherent interconnect offers significant additional efficiency gains.

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.

Function as a Service (FaaS) and the associated serverless computing paradigm alleviates users from resource management and allows cloud platforms to optimize system infrastructure under the hood. Despite significant advances, FaaS infrastructure still leaves much room to improve performance and resource efficiency. We argue that both higher performance and resource efficiency are possible --- while maintaining secure isolation --- if we are willing to revisit the FaaS programming model and system software design. We propose Dandelion, a clean-slate FaaS system that rethinks the programming model by treating serverless functions as pure functions, thereby explicitly separating computation and I/O. This new programming model enables a lightweight yet secure function execution system. It also makes functions more amenable to hardware acceleration and enables dataflow-aware function orchestration. Our initial prototype of Dandelion achieves 45× lower tail latency for cold starts compared to Firecracker. For 95% hot function invocations, Dandelion achieves 5× higher peak throughput.

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.

Function as a Service (FaaS) and the associated serverless computing paradigm alleviates users from resource management and allows cloud platforms to optimize system infrastructure under the hood. Despite significant advances, FaaS infrastructure still leaves much room to improve performance and resource efficiency. We argue that both higher performance and resource efficiency are possible - while maintaining secure isolation - if we are willing to revisit the FaaS programming model and system software design. We propose Dandelion, a clean-slate FaaS system that rethinks the programming model by treating serverless functions as pure functions, thereby explicitly separating computation and I/O. This new programming model enables a lightweight yet secure function execution system. It also makes functions more amenable to hardware acceleration and enables dataflow-aware function orchestration. Our initial prototype of Dandelion achieves 45x lower tail latency for cold starts compared to Firecracker. For 95% hot function invocations, Dandelion achieves 5x higher peak throughput.

Function as a Service (FaaS) and the associated serverless computing paradigm alleviates users from resource management and allows cloud platforms to optimize system infrastructure under the hood. Despite significant advances, FaaS infrastructure still leaves much room to improve performance and resource efficiency. We argue that both higher performance and resource efficiency are possible --- while maintaining secure isolation --- if we are willing to revisit the FaaS programming model and system software design. We propose Dandelion, a clean-slate FaaS system that rethinks the programming model by treating serverless functions as pure functions, thereby explicitly separating computation and I/O. This new programming model enables a lightweight yet secure function execution system. It also makes functions more amenable to hardware acceleration and enables dataflow-aware function orchestration. Our initial prototype of Dandelion achieves 45× lower tail latency for cold starts compared to Firecracker. For 95% hot function invocations, Dandelion achieves 5× higher peak throughput.

Unlike other accelerators, FPGAs are capable of supporting cache coherency, thereby turning them into a more powerful architectural option than just a peripheral accelerator. However, most existing deployments of FPGAs are either non-cache coherent or support only an asymmetric design where cache coherency is controlled from the CPU. Taking advantage of a recently released two socket CPU-FPGA architecture, in this paper we describe ECI, a flexible implementation of cache coherency on the FPGA capable of supporting both symmetric and asymmetric protocols. ECI is open and customizable, given applications the opportunity to fully interact with the cache coherency protocol, thereby opening up many interesting system design and research opportunities not available in existing designs. Through extensive microbenchmarks we show that ECI exhibits highly competitive performance and discuss in detail one use-case illustrating the benefits of having an open cache coherency stack on the FPGA.

Low-latency network stacks have brought down network latencies within end-hosts to the microsecond-regime. However, end-host profilers have such high overheads that they are useful only to confirm a hypothesis, not to diagnose a problem in the first place. Indeed, every one of twenty low-latency network projects we surveyed rolled their own analysis tools instead of using an existing profiler. This paper shows how to build a latency diagnosis tool with full-stack coverage and low overhead that can identify, not just confirm, sources of latency in end hosts. The unique measurement methodology reconstructs network-message lifetimes within end hosts with nanosecond precision, by reconciling CPU and NIC hardware profiling traces across multiple time domains (network and CPU). It uncovers unexpected latency sources in both kernel and user-space stacks. We demonstrate these capabilities by using our implementation, NSight, to systematically identify and remove performance overheads in memcached, reducing 99.9th percentile latency by a factor of 40 from 2.2 ms to 41 mu s.

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.