https://arxiv.org/api/LemII7nfr7RH/HgIzEDamo+7Z60 2026-09-11T20:10:24Z 10292 30 15 http://arxiv.org/abs/2509.16248v5 2026-09-03T18:38:22Z

This paper presents GraphMend, a compiler technique that automatically fixes FX graph breaks in PyTorch 2 programs. Although PyTorch 2 introduced TorchDynamo and TorchInductor to enable just-in-time graph compilation, certain code patterns still cause graph breaks that force execution to fall back to Python eager mode, introducing costly CPU-GPU synchronization and reducing optimization opportunities. Our investigation of 195 Hugging Face models reveals that 13.8% of models exhibit graph breaks. GraphMend automatically eliminates fixable breaks through source-level program analysis and transformations. It analyzes AST-level program structure to identify graph-break patterns and applies transformations only when their semantic preservation can be statically established. These transformations enable PyTorch to capture larger, uninterrupted FX graphs without manual refactoring by developers. We evaluate GraphMend on all 27 models found to exhibit graph breaks in our investigation. GraphMend eliminates 107 of 147 graph breaks (73%), fully fixing all breaks in 21 models. In our experiments on NVIDIA GPUs, GraphMend achieves up to 26x cold-start speedup, 5x on average, and up to 1.39x steady-state forward pass speedup. These results demonstrate that semantics-aware source-level analysis and transformation are effective complements to PyTorch's dynamic JIT compilation pipeline, substantially improving both usability and performance.

2025-09-17T17:15:35Z Accepted for publication at the International Symposium on Code Generation and Optimization (CGO 2027) Savini Kashmira Jayanaka Dantanarayana Thamirawaran Sathiyalogeswaran Krisztian Flautner Lingjia Tang Jason Mars http://arxiv.org/abs/2609.04372v1 2026-09-03T18:37:50Z

We present Corten, a foundational verification framework for Rust programs in the Rocq theorem prover, built on the Iris separation logic framework. Corten provides the first semantics of surface-level Rust mechanized in a proof assistant with an attached program logic, directly grounded in the Rust Reference: it deeply embeds the Typed High-level Intermediate Representation (THIR) into Rocq and formalises Rust's dynamic semantics as a weakest-precondition predicate transformer calculus. By operating at THIR rather than on internal compiler representations, Corten proof goals display the THIR AST, which pretty-prints to surface Rust, keeping verification close to the source code and facilitating maintainability as code evolves. Atop this semantics, Corten develops a program logic and a syntax-directed proof automation layer; the program logic includes defunctionalized continuation stacks that keep proof goals first-order and compact. Soundness is established incrementally, construct by construct, against an interaction-trees denotation. A synthetic test suite demonstrates a two-to-four times reduction in proof size compared to raw semantic proofs. We further showcase Corten on a buddy allocator case study, verifying memory safety of the allocation and deallocation functions, laying the groundwork for end-to-end verification in a shared Rocq semantic foundation spanning hardware-software boundaries.

2026-09-03T18:37:50Z 41 pages, 13 figures František Farka Carmine Abate Sven Linker Sebastian Ertel http://arxiv.org/abs/2609.03998v1 2026-09-03T15:38:56Z

Slotted e-graphs represent open terms modulo consistent renaming, while algebraic operators benefit from canonical sequence, bag, or set children. We compose the two at a specification level: typed slot-mapped invocations inhabit operator-declared ports whose sibling quotient and recursive flattening licenses are certified separately. A generic finite quotient presentation proves exactness of its least-orbit normal form, while certified records specify effective-support kernel extraction and collision. For abstract obligation traces carrying local endpoint certificates, we prove finite-unfolding equational soundness. An Alloy case study compares seven related pipeline arms on a frozen corpus and a controlled transformation suite. Its measurements characterize bounded capability and structural consolidation; they do not establish refinement of the Java artifact or experimental replay against the formal model.

2026-09-03T15:38:56Z 47 pages, including 21 for the main part and 26 for appendix Guanxuan Wu Allison Sullivan http://arxiv.org/abs/2609.03778v1 2026-09-03T12:51:10Z

In this paper, we introduce a notion of abstract quantum data type within the framework of universal algebra. This notion provides an algebraic foundation for describing data abstraction in quantum programming. We formally define a quantisation of classical data types and show that their equational specifications can be soundly lifted to the quantum setting. Two standard quantisation methods for classical functions, namely the bit oracle and the phase oracle, arise as special cases of this general construction. We illustrate the framework with applications to quantum arrays and quantum error-correcting codes, showing how they can be understood through the lens of data-type quantisation. We further establish conditions under which quantisation preserves structural relationships and constructions of classical data types, including embeddings, isomorphisms, and products.

2026-09-03T12:51:10Z 37 pages Mingsheng Ying Zhicheng Zhang Kean Chen http://arxiv.org/abs/2609.03114v1 2026-09-02T19:50:00Z

This paper describes our experience extending the polyhedral compiler Pluto with a lightweight, coordinate-wise hill-climbing tuner that adjusts numeric transformation parameters, such as tile sizes and thread-block dimensions, after Pluto selects the kernel's loop structure. To ensure fast convergence and escape local minima, hill climbing is augmented with two techniques: expanded neighborhood exploration and a shortest-hop refinement phase. On x86 and ARM CPUs, tuned kernels outperform Pluto's default configuration (1.06-1.28x geometric mean speedup across 11 benchmarks) and static optimizers (Clang -O3, Polly, IOOpt), reaching performance competitive with the AutoTVM autotuner at substantially lower search cost. Applying the same technique to GPU thread-block allocation on an NVIDIA A100 yields 5.5-8.5% improvement over default configurations. These results position post-optimization parameter tuning as a practical middle ground between fixed-cost-model polyhedral compilation and full autotuning.

2026-09-02T19:50:00Z 26 pages, 75 references, 15 figures and 3 tables Gaurav Verma Michael Canesche Fernando Magno Quintão Pereira http://arxiv.org/abs/2609.02873v1 2026-09-02T17:54:57Z

We introduce a do-notation metalanguage for causal probabilistic programming. The metalanguage is based on magmads: non-associative monads. We derive causal probabilistic programming constructs from non-associativity and the primitives of probabilistic programming.

2026-09-02T17:54:57Z 11 pages Mario Román http://arxiv.org/abs/2608.00029v3 2026-09-02T07:30:49Z

The performance of deep learning models at scale relies heavily on how effectively high-level mathematical operations are mapped to underlying physical hardware. While high-level tensor frameworks provide flexible abstractions, their execution models inherently lack the whole-graph visibility required to maximize hardware utilization, often forcing a reliance on opaque, hand-written kernel libraries for complex operations like Attention. To bridge this gap, we present the next iteration of Nova, an automated end-to-end JIT compiler that achieves absolute control over hardware mapping by synthesizing fine-grained kernels directly from the computation's structure. In this work, we extend Nova's compilation pipeline to natively support full Transformer architectures. By capturing eager executions and unifying forward and backward passes into a single value-semantic dialect, Nova unlocks aggressive whole-graph optimizations. Rather than relying on rigid, pre-compiled library calls, Nova focuses on extensive cross-operator fusions, collapsing complex causal attention sub-graphs, element-wise operations, and memory-bound normalizations directly into single fused kernels to drastically reduce global memory roundtrips. In our evaluations training a full GPT-2 architecture on Ada 6000 GPUs, Nova demonstrates superior end-to-end throughput, averaging 441K tokens/second compared to 406K for our own eager execution and 405K for torch.compile. By drastically reducing memory-bound overheads through compiler-native fusion, Nova enables efficient full LLM compilation on modern hardware while strictly maintaining numerical parity.

2026-07-15T05:16:28Z Adwaid Suresh Aparna A Harshini V M Jona Delcy C A Killi Uma Maheswara Rao Ram Charan Golla Surendra Vendra http://arxiv.org/abs/2609.02048v1 2026-09-02T03:25:29Z

Trusted Execution Environments (TEEs) provide hardware-supported isolation through enclaves that protect code and data independently of software abstractions. However, TEEs alone cannot enforce information-flow security. This problem is further aggravated in LLVM-like low-level languages that allow unrestricted pointer manipulation and unstructured control flow. Moreover, using TEEs effectively typically requires manually partitioning applications into enclave and non-enclave components, a process that is labor-intensive, error-prone, and lacks fine-grained control. We address these challenges with a three-step approach. First, we formalize SIR, an enclave-oblivious calculus based on LLVM IR, equipped with a novel permissive type system that enforces security against low-level attackers. To obtain meaningful guarantees, SIR combines information-flow control with security-aware coarse-grained memory safety. Second, we extend SIR to SIREN, an enclave-aware calculus that enforces noninterference against stronger attackers capable of observing arbitrary non-enclave memory. Third, we develop a type-driven, type-preserving compilation from SIR to SIREN that automatically produces secure enclave-aware programs, eliminating manual partitioning while providing fine-grained control over host-enclave boundaries. We implement and evaluate SPLITR on thirteen microbenchmarks and real-world workloads, including applications from SGXGauge, on Intel SGX hardware. SPLITR scales to OpenSSL (425,953 LLVM IR instructions) and supports multiple objectives that expose trade-offs among enclave TCB size, host-enclave transitions, and boundary data movement. For OpenSSL, optimizing for transitions reduces them from 393 to 187. Runtime overhead is dominated by fixed enclave costs for short-running workloads, whereas long-running applications better amortize these costs and approach native performance.

2026-09-02T03:25:29Z Wesley B. Nuzzo Samuel Dodson Benjamin Houle Tarakaram Gollamudi Anitha Gollamudi http://arxiv.org/abs/2609.02005v1 2026-09-02T02:30:20Z

Bidirectional typing mixes type synthesis and type checking into a single process. Existing bidirectional type systems can be classified into two styles based on whether, given a function application, a bidirectional typing algorithm synthesizes the function's type first and typechecks the argument against the synthesized argument type, or it synthesizes the arguments' types first and typechecks the function against the synthesized arguments' types. We call the former _function-first_ and the latter _argument-first_. Not only do the two styles significantly differ in how the type systems and typing algorithms are formalized, but also they lead to incompatible typeabilities, forcing a language designer to select one style and to give up the other's typeabilities. In this paper, we unify the two styles and develop \lang with a new bidirectional type system for higher-rank polymorphism. Key ideas of the unification are twofold. Each function application is annotated with a bit of information to represent whether function- or argument-first typing is used, to allow a language designer (or even a programmer) to switch between the two styles at their discretion. We reformulate the function- and argument-first type systems by using ideas from colored types and boxy types, which can specify which part of a type should be synthesized or used for checking in a flexible manner. We also develop a typing algorithm based on the worklist approach by Zhao et al. The (declarative) type system of $λ^{BH}$ is shown to be sound and to subsume two representative function- and argument-first systems. Our typing algorithm is shown to be sound with respect to the type system of $λ^{BH}$ and complete with respect to representative function- and argument-first systems. We mechanically prove the metatheorems using the Abella theorem prover.

2026-09-02T02:30:20Z Accepted as a short version at APLAS 2026 (Springer LNCS). This extended version includes substantial new material and results Takuma Yoshioka Taro Sekiyama Atsushi Igarashi http://arxiv.org/abs/2609.01771v1 2026-09-01T18:42:13Z

Simulating quantum many-body systems has been one of the most important applications of quantum computation. For simulation, the Hamiltonian of a physical system is compiled into quantum programs with native instructions for quantum hardware. In previous works, the Hamiltonian is represented as Pauli strings, then compiled and optimized based on the quantum circuit model. Such representation paradigm neglects the spatial topology of original physical models, which is vital information to reducing the overhead of compiling many-body systems Hamiltonians. To address such neglect, we introduce a spatial-topology preserving compiler for quantum many-body simulation. Using Pauli gadgets as the representations of the Hamiltonian, we introduce our intermediate representation -- GadIR, to preserve the spatial-topology information of original physical models. Our compiler frontend performs the group reduction algorithm based on Pauli gadget model, which is a hardware-independent optimization. Our compiler backend performs trotterization and scheduling on Pauli gadgets, then synthesizes the Pauli gadgets into hardware-native quantum programs. We evaluate our compiler on all the canonical quantum many-body system models, while achieving a significant reduction on compilation overhead regarding four major quantum architectures. Overall, our spatial-topology preserving IR exploits the compilation optimization space for quantum many-body systems Hamiltonian.

2026-09-01T18:42:13Z 59th IEEE/ACM International Symposium on Microarchitecture (MICRO 2026) Xiangyu Ren Yuexun Huang Zhaohui Yang Yuchen Zhu Tsung-Wei Huang Tsung-Yi Ho Zhiding Liang Antonio Barbalace http://arxiv.org/abs/2609.01762v1 2026-09-01T18:29:11Z

Today's quantum devices are noisy, so reducing circuit size is critical for reliable execution. Existing rule-based optimizers often rely on large rule sets that are difficult to manage and still miss long-distance transformations. We present QSymb, a framework for synthesizing compact and expressive quantum-circuit rewrite rules with formal guarantees. We formalize symbolic rewrite rules in which a symbolic gate represents infinitely many subcircuits. We then define canonical symbolic rules of the form $L;S = S;R$ and prove that they constitute a compact generative core from which general symbolic rules can be derived. On top of this formal foundation, given a gate set, QSymb synthesizes (1) a small, non-derivable concrete rule set that is complete up to chosen size and qubit bounds, and (2) a small but expressive canonical symbolic rule set that captures transformations beyond finite or monomial-only patterns. We further present rule anchoring to derive optimization-effective rules from canonical symbolic rules. Together, these results provide both expressiveness and guarantees: soundness of synthesized rules via validation, non-derivability, and bounded completeness. On the IBM-Eagle gate set, QSymb strictly outperforms state-of-the-art rewrite-based optimizers (Qiskit, Guoq, Quartz, TKET, and Queso) in two-qubit-gate reduction on 90%, 67%, 82%, 85%, and 83% of standard quantum algorithm benchmarks, respectively; on Nam gate set, the corresponding rates are 88%, 74%, 81%, 86%, and 82.9%. It achieves final average two-qubit-gate reductions of 27.44% and 29.95%, respectively.

2026-09-01T18:29:11Z To appear in Proc. ACM Program. Lang. 10, OOPSLA2 (2026) Wei Qiang Ronghui Gu 10.1145/3839450 http://arxiv.org/abs/2609.01525v1 2026-09-01T16:55:11Z

A durable assumption holds that graph analytics requires a purpose-built graph engine, and that relational systems are ill-suited to connected data. We argue the opposite for the workloads enterprises actually run. A columnar relational engine fronted by a graph query language matches or exceeds native graph engines on analytical graph queries, and - decisively - scales past the point where in-memory graph engines fail. We further argue that the node/edge property graph is not a more faithful model of connected data but a re-encoding of relationships that already exist explicitly in relational tables; reconstructing them at query time is pure overhead. We present ClickGraph and its Databricks-dialect sibling DeltaGraph, systems that translate Cypher directly onto the native relational schema - the tables, columns, and foreign keys as they already exist - and execute in place on ClickHouse, Databricks, or in-process on lakehouse files, with no import and no separate cluster. Because the output is ordinary SQL, an underperforming query is an open optimization surface: it can be rewritten, and the engine itself extended. We support the argument with a peer system's own published benchmark, in which a columnar engine outruns Neo4j by two-to-four orders of magnitude, and with reproducible measurements across the LDBC Social Network Benchmark suite.

2026-09-01T16:55:11Z Gene Zhang http://arxiv.org/abs/2609.01502v1 2026-09-01T16:32:46Z

Ruby is a dynamically typed and object-oriented programming language. Its primary implementation, CRuby, contains a bytecode virtual machine and a mature lazy basic block versioning (LBBV) just-in-time (JIT) compiler called YJIT. In order to both implement more advanced optimizations than YJIT supports and also encourage more outside contributions, we present a new method-based JIT called ZJIT. Like YJIT, ZJIT compiles from bytecode to machine code. Unlike YJIT, ZJIT has multiple global and local optimization passes. ZJIT's high-level intermediate representation is in static single assignment (SSA) form. In order to optimize Ruby's local variables, ZJIT lifts local variables into SSA values. This is a departure from how other Ruby compilers handle locals: other JIT compilers either leave local variables as memory loads and stores or do advanced partial evaluation to recover SSA values from memory. While implementing locals, we (re-)discovered what features make local variables in Ruby especially challenging to compile correctly and efficiently. We demonstrate these features and illustrate how we solved these problems in ZJIT.

2026-09-01T16:32:46Z Maxwell Bernstein Takashi Kokubun Aaron Patterson Si Xing "Alan" Wu Kevin Menard 10.1145/3840562.3844969 http://arxiv.org/abs/2609.01292v1 2026-09-01T14:27:06Z

Relational Deep Learning (RDL) has become a powerful paradigm for learning from multi-tabular data. However, manually defining RDL prediction tasks is a laborious process that frequently results in data leakage. To address this issue, we introduce Relational Task Generation Language (RTGL) - an open-source declarative language that streamlines RDL task formulation by abstracting away low-level SQL details. We showcase RTGL by reconstructing existing RDL benchmark tasks and uncovering their inconsistencies stemming from manually crafted SQL definitions of RDL prediction targets, thereby underscoring the value of a dedicated declarative language. In addition, we demonstrate the practical utility of RTGL by designing various new tasks with diverse forms and target types. Our experiments confirm the robustness and usability of RTGL, as well as its seamless integration with the existing RDL frameworks, making it widely accessible to the community.

2026-09-01T14:27:06Z Accepted to MLG 2026 Oleksii Kolesnichenko Jakub Peleška Gustav Šír http://arxiv.org/abs/2609.01110v1 2026-09-01T11:50:45Z

CHERIoT is a novel hardware-software co-design that leverages hardware capabilities to define a notion of compartment, in a minimalistic capability-based OS, CHERIoT RTOS. By default, compartments are isolated to limit damage in case of bugs or malicious behaviour. To allow cross-compartment communication, the OS provides a privileged component, called the switcher. The switcher provides an interface for cross-compartment calls, while enforcing isolation between compartments and guaranteeing stack safety. Together with hardware capabilities, the switcher is critical to enforce the security guarantees of the CHERIoT compartment model. The design of CHERIoT raises two questions: First, how can one formalise the informal notion of compartmentalisation that CHERIoT compartments are designed to provide? And second, given that the safety properties of CHERIoT hinge on the complementary roles of the capability machine and of the switcher, does the design of CHERIoT enforce the desired security properties? In this paper, we introduce Griotte and Griotte OS, idealised but faithful versions of the CHERIoT machine and the CHERIoT RTOS, which we use to answer these two questions: First, we formally capture the aforementioned security guarantees in the form of a continuation-based logical relation which captures the combined behaviour of the switcher and of the capability machine. And second, we define a specification for the Griotte switcher that enforces those guarantees, and prove that the implementation meets the specification. We demonstrate Griotte on a range of key scenarios illustrating different aspects of CHERIoT, including integrity of the local state in the presence of memory sharing with unknown code. Our approach is modular: we verify compartments individually, and then compose their specifications. Together, our contributions give a solid formal foundation to the design of CHERIoT.

2026-09-01T11:50:45Z June Rousseau Aïna Linn Georges Jean Pichon-Pharabod Lars Birkedal