| CS-2025-01 | ||||
|---|---|---|---|---|
| Title | Towards a High-Speed Programmable Hardware Architecture for the Network Transport Layer | |||
| Authors | Kimiya Mohammadtaheri, Nachiket Kapre, Mina Tahmasbi Arashloo | |||
| Abstract | As network speeds keep increasing, there is a growing interest in accelerating network functions using programmable Network Interface Cards (NICs). Transport protocols play a critical role in managing traffic flow and resource allocation, yet their high-speed implementation on NICs remains a challenge due to the complexity of stateful operations and the need for low-level hardware expertise. This project introduces a high-level programming platform called MTP that allows users to specify transport protocols without concerning themselves with hardware-specific details. We will then introduce a compiler that can translate this code to a low level hardware design. We will then explain the general structure of such hardware design and the challenges of mapping the components of the high-level platform to hardware and leveraging the capabilities of hardware. | |||
| Date | February 9, 2025 | |||
| Report | CS-2025-01 (395 kB PDF) | |||
| CS-2025-02 | ||||
| Title | Certified Compilers à la Carte (Extended Version) | |||
| Authors | Oghenevwogaga Ebresafe, Ian Zhao, Ende Jin, Arthur Bright, Charles Jian, Yizhou Zhang | |||
| Abstract | Certified compilers are complex software systems. Like other large systems, they demand modular, extensible designs. While there has been progress in extensible metatheory mechanization, scaling extensibility and reuse to meet the demands of full compiler verification remains a major challenge. We respond to this challenge by introducing novel expressive power to a proof language. Our language design equips the Rocq prover with an extensibility mechanism inspired by the object-oriented ideas of late binding, mixin composition, and family polymorphism. We implement our design as a plugin for Rocq, called Rocqet. We identify strategies for using Rocqet’s new expressive power to modularize the monolithic design of large certified developments as complex as the CompCert compiler. The payoff is a high degree of modularity and reuse in the formalization of intermediate languages, ISAs, compiler transformations, and compiler extensions, with the ability to compose these reusable components—certified compilers à la carte. We report significantly improved proof-compilation performance compared to earlier work on extensible metatheory mechanization. We also report good performance of the extracted compiler. |
|||
| Date | July 2, 2025 | |||
| Report | CS-2025-02 (851 kB PDF) | |||
| CS-2025-03 | ||||
| Title | Compiling with Generating Functions (Extended Version) | |||
| Authors | Jianlin Li, Yizhou Zhang | |||
| Abstract | We present a new approach to scaling exact inference for probabilistic programs, using generating functions (GFs) as a compilation target. Existing methods that target representations like binary decision diagrams (BDDs) achieve strong state-of-the-art results. We show that a compiler targeting GFs can be similarly competitive—and, in some cases, more scalable—on a range of inference problems where BDD-based methods perform well. We present a formal model of this compiler, providing the first definition of GF compilation for a functional probabilistic language. We prove that this compiler is correct with respect to a denotational semantics. Our approach is implemented in a probabilistic programming system called Geni and evaluated on a range of inference problems. Our results establish GF compilation as a principled and powerful paradigm for exact inference: it offers strong scalability, good expressiveness, and a solid theoretical foundation. This technical report is an extended version of the following paper: Jianlin Li and Yizhou Zhang. 2025. Compiling with Generating Functions. Proc. ACM Program. Lang. 9, ICFP, Article 265 (August 2025). |
|||
| Date | September 22, 2025 | |||
| Report | CS-2025-03 (482 kb PDF) | |||
| CS-2025-04 | ||||
| Title | Zero-Overhead Lexical Effect Handlers (Extended Version) | |||
| Authors | Cong Ma, Zhaoyi Ge, Max Jung, Yizhou Zhang | |||
| Abstract | Exception handlers—and effect handlers more generally—are language mechanisms for structured nonlocal control flow. A recent trend in language-design research has introduced lexically scoped handlers, which address a modularity problem with dynamic scoping. While dynamically scoped handlers allow zero-overhead implementations when no effects are raised, existing implementations of lexically scoped handlers require programs to pay a cost just for having handlers in the lexical context. In this paper, we present a novel approach to implementing lexically scoped handlers of exceptional effects. It satisfies the zero-overhead principle—a property otherwise met by most modern compilers supporting dynamically scoped exception handlers. The key idea is a type-directed translation that emits information indicating how handlers come into the lexical context. This information guides the runtime in walking the stack to locate the right handler. Crucially, no reified lexical identifiers of handlers are needed, and mainline code is not slowed down by the presence of handlers in the program text. We formalize the essential aspects of this compilation scheme and prove it correct. We integrate our approach into the Lexa language, allowing the compilation strategy to be customized for each declared effect based on its expected invocation rate. Empirical results suggest that the new Lexa compiler reduces run-time overhead in low-effect or no-effect scenarios while preserving competitive performance for effect-heavy workloads. This technical report is an extended version of the following paper: Cong Ma, Zhaoyi Ge, Max Jung, and Yizhou Zhang. 2025. Zero-Overhead Lexical Effect Handlers. Proc. ACM Program. Lang. 9, OOPSLA2, Article 399 (October 2025). |
|||
| Date | September 22, 2025 | |||
| Report | CS-2025-04 (701 kb PDF) | |||