A Compute Express Link (CXL) pod is a group of hosts that share CXL-attached memory. A memory allocator for a CXL pod faces novel challenges: (1) CXL devices may not fully support inter-host hardware cache coherence (HWcc), (2) the allocator may be concurrently accessed from different processes, and (3) with more hosts, failures become more likely.

Current stream processing systems provide exactly-once semantics using checkpointing or a combination of logging and checkpointing. These approaches can introduce high overhead, significantly increasing the latency for normal stream processing because maintaining exactly-once semantics requires coordination across distributed nodes and streams to capture a globally consistent state. We observe that modern distributed shared logs offer a promising solution for maintaining exactly-once semantics with a small overhead. We propose Impeller, a stream processing system that uses a distributed shared log for data storage and exactly-once processing. To maintain exactly-once semantics, Impeller includes a novel and efficient progress marking protocol based on string tags and selective reads in a shared log. The key idea is to leverage the log's record-tagging feature to atomically mark progress across all streams. The experiments over the NEXMark benchmark show that Impeller achieves 1.3× to 5.4× lower p50 latency, or 1.3× to 5.0× higher saturation throughput than Kafka Streams.

P4 is a domain-specific language for programming and specifying packet-processing systems. It is based on an elegant design with high-level abstractions like parsers and match-action pipelines that can be compiled to efficient implementations in software or hardware. Unfortunately, like many industrial languages, P4 has developed without a formal foundation. The P4 Language Specification is a 160-page document with a mixture of informal prose, graphical diagrams, and pseudocode, leaving many aspects of the language semantics up to individual compilation targets. The P4 reference implementation is a complex system, running to over 40KLoC of C++ code, with support for only a few targets. Clearly neither of these artifacts is suitable for formal reasoning about P4 in general. This paper presents a new framework, called Petr4, that puts P4 on a solid foundation. Petr4 consists of a clean-slate definitional interpreter and a core calculus that models a fragment of P4. Petr4 is not tied to any particular target: the interpreter is parameterized over an interface that collects features delegated to targets in one place, while the core calculus overapproximates target-specific behaviors using non-determinism. We have validated the interpreter against a suite of over 750 tests from the P4 reference implementation, exercising our target interface with tests for different targets. We validated the core calculus with a proof of type-preserving termination. While developing Petr4, we reported dozens of bugs in the language specification and the reference implementation, many of which have been fixed.