systems software developers

Abstract: Legacy C codebases remain central to system software and performance-critical infrastructure, but their weak memory safety imposes security and maintenance risks. Recent C-to-Rust translation systems, including LLM-based translators, make automated migration increasingly feasible, yet they still struggle to recover repository-level intent, avoid raw pointers and unsafe constructs, maintain cross-file interfaces, and repair compilation and validation failures efficiently. We propose SpeC2Rust, a specification-driven pipeline for repository-level C-to-Rust translation. It has three stages: (1) Project-Intent Structuring, which decomposes a C repository into semantically coherent modules and generates persistent repository- and module-level specifications; (2) Spec-Guided Generation, which translates each Rust module against these specifications with a live symbol registry to preserve cross-file consistency; and (3) Layered-Feedback Repair, which batches repairs and injects only failure-relevant diagnostics, specification context, and source evidence for efficient compilation and test-driven correction. We evaluate SpeC2Rust on eight repository-level C projects. It generates Rust projects that compile and pass the original end-to-end tests, with no raw-pointer declarations, raw-pointer dereferences, or unsafe lines. On projects shared with an LLM-based baseline, SpeC2Rust reduces cost by 66.1% and input-token usage by 84.7%.

Abstract: Memory tiering has been used to expand memory capacity, particularly in datacenters, by combining fast DRAM with slower tiers, including CXL-attached memory. Its effectiveness depends on keeping useful pages in the fast tier, but existing heuristic policies can lag behind changing hot sets in phased or bursty workloads. To explore these limitations, we introduce ChOMP, a scalable offline optimizer that minimizes placement and bandwidth-sensitive migration costs. We then develop a trace-driven simulator that uses this reference to identify performance opportunities for online policies. Motivated by these results, MANTA predicts future page usefulness from runtime access features and integrates a lightweight learned model into ARMS. Across eight workloads on emulated CXL, MANTA achieves geometric-mean speedups over ARMS of 1.12$\times$ and 1.08$\times$ at 4~GB of fast memory on Linux 6.2 and 6.18, respectively; across six Optane workloads, it achieves 1.69$\times$. On individual workloads, MANTA is up to 1.25$\times$ faster than ARMS with emulated CXL on Linux 6.2, 1.21$\times$ on Linux 6.18, and 5.6$\times$ with Optane.

Abstract: Real-world programs are rarely written in a single language: For example, C programs call assembly routines, and high-level languages like OCaml link with low-level C libraries. Yet program logics---one of the most successful techniques for modular program verification---almost exclusively target single-language programs. We present Hotpot, the first framework for building multi-language program logics. Hotpot enables compilation-independent, cross-language reasoning about languages with heterogeneous views of shared state. Hotpot rests on four key ideas: abstract calls to specify calls to unknown functions, lanes and the switching modality to move between languages inside the program logic, uniform integration of refinement reasoning via lanes, and exchanges to translate between separation logic assertions of different languages. We demonstrate that Hotpot allows reusing specifications across implementations in different languages, supports reasoning about higher-order cross-language function calls, and integrates with verified compilation. Hotpot is built on top of Iris and DimSum and mechanized in the Rocq Prover.