| 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, Oghenevwogaga Ebresafe, Yizhou Zhang | |||
| Abstract | to come | |||
| Date | to come | |||
| Report | to come | |||
| CS-2025-04 | ||||
| Title | Zero-Overhead Lexical Effect Handlers (Extended Version) | |||
| Authors | Cong Ma, Zhaoyi Ge, Max Jung, Yizhou Zhang | |||
| Abstract | to come | |||
| Date | to come | |||
| Report | to come | |||