arXiv subjects

Arthur Charguéraud

Publications and source records attributed to Arthur Charguéraud.

3 recordsLinked to original sources

arXiv2026

Source-to-Source Transformations for GPU Code Generation

GPUs have become essential in modern high performance computing, but programming them correctly remains a significant challenge. This difficulty arises from subtle concurrency bugs that result from the explicit management of synchronization primitives and data movement across intricate hierarchies of memory and parallel threads. At the same time, the ability to control these aspects explicitly is at the core of the performance gains granted by GPUs. These challenges have motivated interest in safe GPU programming: tools and languages that can prevent or detect such bugs statically. However, existing approaches make tradeoffs in three dimensions: the strength of their guarantees, the degree of low-level control they allow, and the amount of additional effort required to achieve these safety guarantees. This thesis presents OptiGPU, a system for GPU programming with strong safety guarantees-data race freedom, deadlock freedom, and full functional correctness-that minimizes tradeoffs in the other two dimensions compared to previous approaches. OptiGPU applies proof-preserving compilation to GPU programming, allowing verification of low-level, optimized GPU programs through refinement of simple, verified CPU programs. An OptiGPU user thus avoids the substantial proof burden of directly verifying complex optimized GPU programs, instead directing this refinement with source-to-source transformations that automatically preserve proofs. OptiGPU is implemented as a set of extensions to OptiTrust, an existing framework for proof-preserving compilation on CPUs. OptiGPU models essential GPU programming features, including kernel launches, shared memory, and synchronous barriers, and produces both device and host-side code. We evaluate OptiGPU on two case studies, matrix transpose and tree-based parallel reduction, showing it can derive CUDA code matching techniques found in handwritten references.

cs.PL↗

arXiv2017

Parallel Work Inflation, Memory Effects, and their Empirical Analysis

In this paper, we propose an empirical method for evaluating the performance of parallel code. Our method is based on a simple idea that is surprisingly effective in helping to identify causes of poor performance, such as high parallelization overheads, lack of adequate parallelism, and memory effects. Our method relies on only the measurement of the run time of a baseline sequential program, the run time of the parallel program, the single-processor run time of the parallel program, and the total amount of time processors spend idle, waiting for work. In our proposed approach, we establish an equality between the observed parallel speedups and three terms that we call parallel work, idle time, and work-inflation, where all terms except work inflation can be measured empirically, with precision. We then use the equality to calculate the difficult-to-measure work-inflation term, which includes increased communication costs and memory effects due to parallel execution. By isolating the main factors of poor performance, our method enables the programmer to assign blame to certain properties of the code, such as parallel grain size, amount of parallelism, and memory usage. We present a mathematical model, inspired by the work-span model, that enables us to justify the interpretation of our measurements. We also introduce a method to help the programmer to visualize both the relative impact of the various causes of poor performance and the scaling trends in the causes of poor performance. Our method fits in a sweet spot in between state-of-the-art profiling and visualization tools. We illustrate our method by several empirical studies and we describe a few experiments that emphasize the care that is required to accurately interpret speedup plots.

cs.DC↗

arXiv2015

Improving Type Error Messages in OCaml

Cryptic type error messages are a major obstacle to learning OCaml or other ML-based languages. In many cases, error messages cannot be interpreted without a sufficiently-precise model of the type inference algorithm. The problem of improving type error messages in ML has received quite a bit of attention over the past two decades, and many different strategies have been considered. The challenge is not only to produce error messages that are both sufficiently concise and systematically useful to the programmer, but also to handle a full-blown programming language and to cope with large-sized programs efficiently. In this work, we present a modification to the traditional ML type inference algorithm implemented in OCaml that, by significantly reducing the left-to-right bias, allows us to report error messages that are more helpful to the programmer. Our algorithm remains fully predictable and continues to produce fairly concise error messages that always help making some progress towards fixing the code. We implemented our approach as a patch to the OCaml compiler in just a few hundred lines of code. We believe that this patch should benefit not just to beginners, but also to experienced programs developing large-scale OCaml programs.

cs.PL↗