More Like this

1. Verified tensor-program optimization via high-level scheduling rewrites

   https://doi.org/10.1145/3498717  

   Liu, Amanda; Bernstein, Gilbert_Louis; Chlipala, Adam; Ragan-Kelley, Jonathan (January 2022, Proceedings of the ACM on Programming Languages)

   We present a lightweight Coq framework for optimizing tensor kernels written in a pure, functional array language. Optimizations rely on user scheduling using series of verified, semantics-preserving rewrites. Unusually for compilation targeting imperative code with arrays and nested loops, all rewrites are source-to-source within a purely functional language. Our language comprises a set of core constructs for expressing high-level computation detail and a set of what we call reshape operators, which can be derived from core constructs but trigger low-level decisions about storage patterns and ordering. We demonstrate that not only is this system capable of deriving the optimizations of existing state-of-the-art languages like Halide and generating comparably performant code, it is also able to schedule a family of useful program transformations beyond what is reachable in Halide. 

   more » « less
2. Optimized Quantum Program Execution Ordering to Mitigate Errors in Simulations of Quantum Systems

   https://doi.org/10.1109/ICRC53822.2021.00013  

   Tomesh, Teague; Gui, Kaiwen; Gokhale, Pranav; Shi, Yunong; Chong, Frederic T.; Martonosi, Margaret; Suchara, Martin (November 2021, 2021 International Conference on Rebooting Computing (ICRC))

   Simulating the time evolution of a physical system at quantum mechanical levels of detail - known as Hamiltonian Simulation (HS) - is an important and interesting problem across physics and chemistry. For this task, algorithms that run on quantum computers are known to be exponentially faster than classical algorithms; in fact, this application motivated Feynman to propose the construction of quantum computers. Nonetheless, there are challenges in reaching this performance potential. Prior work has focused on compiling circuits (quantum programs) for HS with the goal of maximizing either accuracy or gate cancellation. Our work proposes a compilation strategy that simultaneously advances both goals. At a high level, we use classical optimizations such as graph coloring and travelling salesperson to order the execution of quantum programs. Specifically, we group together mutually commuting terms in the Hamiltonian (a matrix characterizing the quantum mechanical system) to improve the accuracy of the simulation. We then rearrange the terms within each group to maximize gate cancellation in the final quantum circuit. These optimizations work together to improve HS performance and result in an average 40% reduction in circuit depth. This work advances the frontier of HS which in turn can advance physical and chemical modeling in both basic and applied sciences. 

   more » « less
3. Reasoning about the garden of forking paths

   https://doi.org/10.1145/3473585  

   Li, Yao; Xia, Li-yao; Weirich, Stephanie (August 2021, Proceedings of the ACM on Programming Languages)

   Lazy evaluation is a powerful tool for functional programmers. It enables the concise expression of on-demand computation and a form of compositionality not available under other evaluation strategies. However, the stateful nature of lazy evaluation makes it hard to analyze a program's computational cost, either informally or formally. In this work, we present a novel and simple framework for formally reasoning about lazy computation costs based on a recent model of lazy evaluation: clairvoyant call-by-value. The key feature of our framework is its simplicity, as expressed by our definition of the clairvoyance monad. This monad is both simple to define (around 20 lines of Coq) and simple to reason about. We show that this monad can be effectively used to mechanically reason about the computational cost of lazy functional programs written in Coq. 

   more » « less
4. Towards Certified Meta-Programming with Typed Template-Coq

   Abhishek Anand, Simon Boulier (July 2018, ITP 2018 - 9th Conference on Interactive Theorem Proving)

   Template-Coq 5 is a plugin for Coq, originally implemented by Malecha, which provides a reifier for Coq terms and global declara- tions, as represented in the Coq kernel, as well as a denotation command. Initially, it was developed for the purpose of writing functions on Coq’s AST in Gallina. Recently, it was used in the CertiCoq certified compiler project, as its front-end language, to derive parametricity properties, and to extract Coq terms to a CBV λ-calculus. However, the syntax lacked semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications in Coq, the semantics of Coq’s type theory itself. The tool was also rather bare bones, providing only rudimentary quoting and unquoting commands. We generalize it to han- dle the entire Calculus of Inductive Constructions (CIC), as implemented by Coq, including the kernel’s declaration structures for definitions and inductives, and implement a monad for general manipulation of Coq’s logical environment. We demonstrate how this setup allows Coq users to define many kinds of general purpose plugins, whose correctness can be readily proved in the system itself, and that can be run efficiently after extraction. We give a few examples of implemented plugins, including a parametricity translation. We also advocate the use of Template-Coq as a foundation for higher-level tools. 

   more » « less
5. Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model

   https://doi.org/10.4230/LIPICS.ITP.2024.36  

   Tolmach, Andrew; Chhak, Chris; Anderson, Sean (September 2024, Schloss Dagstuhl – Leibniz-Zentrum für Informatik)

   Bertot, Yves; Kutsia, Temur; Norrish, Michael (Ed.)

   We propose a concrete ("pointer as integer") memory semantics for C that supports verified compilation to a target environment having simple "public vs. private" data protection based on tagging or sandboxing (such as the WebAssembly virtual machine). Our semantics gives definition to a range of legacy programming idioms that cause undefined behavior in standard C, and are not covered by existing verified compilers, but that often work in practice. Compiler correctness in this context implies that target programs are secure against all control-flow attacks (although not against data-only attacks). To avoid tying our semantics too closely to particular compiler implementation choices, it is parameterized by a novel form of oracle that non-deterministically chooses the addresses of stack and heap allocations. As a proof-of-concept, we formalize a small RTL-like language and verify two-way refinement for a compiler from this language to a low-level machine and runtime system with hardware tagging. Our Coq formalization and proofs are provided as supplementary material. 

   more » « less