Publications
- Interactive Source-to-Source Optimizations Validated using Static Resource Analysis
-
SOAP 2024: ACM SIGPLAN International Workshop on the State Of the Art in Program AnalysisPDF
Abstract
Developments in hardware have delivered formidable computing power. Yet, the increased hardware complexity has made it a real challenge to develop software that exploits the hardware to its full potential. Numerous approaches have been explored to help programmers turn naive code into high-performance code, finely tuned for the targeted hardware. However, these approaches have inherent limitations, and it remains common practice for programmers seeking maximal performance to follow the tedious and error-prone route of writing optimized code by hand.
This paper presents OptiTrust, an interactive source-to-source optimization framework that operates on general-purpose C code. The programmer develops a script describing a series of code transformations. The framework provides continuous feedback in the form of human-readable diffs over conventional C code. OptiTrust supports advanced code transformations, including transformations exploited by the state-of-the-art DSL tools Halide and TVM, and transformations beyond the reach of existing tools. OptiTrust also supports user-defined transformations, as well as defining complex transformations by composition of simpler transformations. Crucially, to check the validity of code transformations, OptiTrust leverages a static resource analysis in a simplified form of Separation Logic. Starting from user-provided annotations on functions and loops, our analysis deduces precise resource usage throughout the code.
- Source-to-Source Optimizations Validated using Separation Logic
-
JFLA 2024: Journées Francophones des Langages ApplicatifsPDF
Abstract
We present a demo of OptiTrust, an interactive framework for optimizing general-purpose programs via series of programmer-guided, source-to-source transformations. Optimization steps are described in transformation scripts, expressed as OCaml programs. At every step, the programmer may interactively visualize the effect of the transformation as the difference between two pieces of human-readable code. The framework currently applies to C code. That said, our internal AST is based on the imperative lambda-calculus, thus we expect it to be straightforward to extend OptiTrust for optimizing OCaml code.
A central question is how to verify that nontrivial transformations preserve the semantics of the code. To that end, we require the programmer to provide Separation Logic annotations, and use them to compute resource usage throughout the code. As we show, this information suffices to justify the correctness of numerous essential source-to-source transformations, such as swapping of instructions, swapping of loops, hoisting of instructions out of loops, etc.
- An AST for representing programs with invariants and proofs
-
JFLA 2023: Journées Francophones des Langages ApplicatifsPDF
Abstract
Deductive verification enables one to check that a program satisfies its specification. There are mainly two approaches: either the user provides invariants in the form of annotations and use a tool to extract proof obligations, like in, e.g., Why3; or the user verifies the program through interactive proofs, like in, e.g., CFML, by providing invariants during the proof steps.
We are interested in expressing in Coq the representation of a program, accompanied with not only its invariants but also its proof terms. Concretely, we present an AST for representing source code and specification in a deep embedding style, and embedded lemmas in shallow embedding style. Such lemmas can be established using the full capabilities of the prover.
We develop a way to build these ASTs from source code using CFML-style interactive tactics. We also develop a way to build these ASTs by extracting proof obligations from source code already annotated with its invariants. Besides, we provide a way to validate our ASTs by reifying them as Coq proof terms.
This work is a first step towards a long term project to devise a trustworthy, userguided, source-to-source optimization framework. On the one hand, we may need to exploit invariants to justify the correctness of code transformations. On the other hand, to be able to chain transformations, we also need every transformation to update the program annotations.
- Towards seamless interfacing between dynamic languages and native code
-
VMIL 2019: Proceedings of the 11th ACM SIGPLAN International Workshop on Virtual Machines and Intermediate LanguagesPDF
Abstract
Existing approaches to interfacing high- and low-level code push considerable burdens onto the programmer, such as wrapper maintenance, explicit code generation, interface re-declaration, and/or signalling to garbage collectors. We note that run-time information on data layout and allocations in native code is available, and may be extended with knowledge of object lifetimes to assist in automating garbage collection. We describe work in progress towards an extension of the CPython virtual machine along these lines. We report initial experience building a first working prototype, and some early performance experiments.
- Primitive Floats in Coq
-
ITP 2019: International Conference on Interactive Theorem ProvingPDF
Abstract
Some mathematical proofs involve intensive computations, for instance: the four-color theorem, Hales’ theorem on sphere packing (formerly known as the Kepler conjecture) or interval arithmetic. For numerical computations, floating-point arithmetic enjoys widespread usage thanks to its efficiency, despite the introduction of rounding errors.
Formal guarantees can be obtained on floating-point algorithms based on the IEEE 754 standard, which precisely specifies floating-point arithmetic and its rounding modes, and a proof assistant such as Coq, that enjoys efficient computation capabilities. Coq offers machine integers, however floating-point arithmetic still needed to be emulated using these integers.
A modified version of Coq is presented that enables using the machine floating-point operators. The main obstacles to such an implementation and its soundness are discussed. Benchmarks show potential performance gains of two orders of magnitude