arXiv subjects

Thomas Koehler

Publications and source records attributed to Thomas Koehler.

13 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↗

arXiv2025

Technical Note: Low-Dose Simulation for Grating-Based X-Ray Dark-Field Radiography Using a Virtually Decreased Irradiation Area

Background: X-ray dark-field radiography uses small-angle scattering to visualize the structural integrity of lung alveoli. To study the influence of dose reduction on clinical dark-field radiographs, one can simulate low-dose images by virtually reducing the irradiated area. However, these simulations can exhibit stripe artifacts. Purpose: Validation of the low-dose simulation algorithm reported by Schick & Bast et al., PLoS ONE, 2024. Furthermore, we want to demonstrate that stripe artifacts observed in simulated images at very low-dose levels are introduced by limitations of the algorithm and would not appear in actual low-dose dark-field images. Methods: Dark-field radiographs of an anthropomorphic chest phantom were acquired at different tube currents equaling different radiation doses. Based on the measurement with a high radiation dose, dark-field radiographs corresponding to lower radiation doses were simulated by virtually reducing the irradiated area. The simulated low-dose radiographs were evaluated by a quantitative comparison of the dark-field signal using different regions of interests. Results: Dark-field radiographs acquired at one quarter of the standard dose were artifact-free. The dark-field signal differed from the simulated radiographs by up to 10%. Algorithm-induced stripe artifacts decrease the image quality of the simulated radiographs. Conclusions: Virtually reducing the irradiation area is a simple approach to generate low-dose radiographs based on images acquired with scanning-based dark-field radiography. However, as the algorithm creates stripe artifacts in the dark-field images, particularly at higher dose reductions, that are not present in measured low-dose images, simulated images have reduced image quality compared to their measured counterparts.

physics.med-ph↗

arXiv2025

Beam Hardening Correction in Clinical X-ray Dark-Field Chest Radiography using Deep Learning-Based Bone Segmentation

Dark-field radiography is a novel X-ray imaging modality that enables complementary diagnostic information by visualizing the microstructural properties of lung tissue. Implemented via a Talbot-Lau interferometer integrated into a conventional X-ray system, it allows simultaneous acquisition of perfectly temporally and spatially registered attenuation-based conventional and dark-field radiographs. Recent clinical studies have demonstrated that dark-field radiography outperforms conventional radiography in diagnosing and staging pulmonary diseases. However, the polychromatic nature of medical X-ray sources leads to beam-hardening, which introduces structured artifacts in the dark-field radiographs, particularly from osseous structures. This so-called beam-hardening-induced dark-field signal is an artificial dark-field signal and causes undesired cross-talk between attenuation and dark-field channels. This work presents a segmentation-based beam-hardening correction method using deep learning to segment ribs and clavicles. Attenuation contribution masks derived from dual-layer detector computed tomography data, decomposed into aluminum and water, were used to refine the material distribution estimation. The method was evaluated both qualitatively and quantitatively on clinical data from healthy subjects and patients with chronic obstructive pulmonary disease and COVID-19. The proposed approach reduces bone-induced artifacts and improves the homogeneity of the lung dark-field signal, supporting more reliable visual and quantitative assessment in clinical dark-field chest radiography.

physics.med-ph↗

arXiv2025

Look-Up Table-Correction for Beam Hardening-Induced Signal of Clinical Dark-Field Chest Radiographs

Background: Material structures at the micrometer scale cause ultra-small-angle X-ray scattering, e.g., seen in lung tissue or plastic foams. In grating-based X-ray imaging, this causes a reduction of the fringe visibility, forming a dark-field signal. Polychromatic beam hardening also changes visibility, adding a false dark-field signal due to attenuation, even in homogeneous, non-scattering materials. Purpose: The objective of this study is to develop a fast, simple, and robust method to correct dark-field signals and bony structures present due to beam hardening on dark-field chest radiographs of study participants. Methods: The method is based on calibration measurements and image processing. Beam hardening by bones and soft tissue is modeled by aluminum and water, respectively, which have no microstructure and thus only generate an artificial dark-field signal. Look-up tables were then created for both. By using a weighted mean of these, forming a single look-up table, and using the attenuation images, the artificial dark-field signal and thus the bone structures present are reduced for study participants. Results: It was found that applying a correction using a weighted look-up table leads to a significant reduction of bone structures in the dark-field image. The weighting of the aluminum component has a substantial impact on the degree to which bone structures remain visible in the dark-field image. Furthermore, a large negative bias in the dark-field image, dependent on the aluminum weighting, was successfully corrected. Conclusions: The beam-hardening-induced signal in the dark-field images was successfully reduced using the method described. The choice of aluminum weighting to suppress rib structures, as well as the selection of bias correction, should be evaluated based on the specific clinical question.

physics.med-ph↗

arXiv2025

Deformable Image Registration of Dark-Field Chest Radiographs for Local Lung Signal Change Assessment

Dark-field radiography of the human chest has been demonstrated to have promising potential for the analysis of the lung microstructure and the diagnosis of respiratory diseases. However, previous studies of dark-field chest radiographs evaluated the lung signal only in the inspiratory breathing state. Our work aims to add a new perspective to these previous assessments by locally comparing dark-field lung information between different respiratory states. To this end, we discuss suitable image registration methods for dark-field chest radiographs to enable consistent spatial alignment of the lung in distinct breathing states. Utilizing full inspiration and expiration scans from a clinical chronic obstructive pulmonary disease study, we assess the performance of the proposed registration framework and outline applicable evaluation approaches. Our regional characterization of lung dark-field signal changes between the breathing states provides a proof-of-principle that dynamic radiography-based lung function assessment approaches may benefit from considering registered dark-field images in addition to standard plain chest radiographs.

eess.IV↗

arXiv2023

Rewriting History: Repurposing Domain-Specific CGRAs

Coarse-grained reconfigurable arrays (CGRAs) are domain-specific devices promising both the flexibility of FPGAs and the performance of ASICs. However, with restricted domains comes a danger: designing chips that cannot accelerate enough current and future software to justify the hardware cost. We introduce FlexC, the first flexible CGRA compiler, which allows CGRAs to be adapted to operations they do not natively support. FlexC uses dataflow rewriting, replacing unsupported regions of code with equivalent operations that are supported by the CGRA. We use equality saturation, a technique enabling efficient exploration of a large space of rewrite rules, to effectively search through the program-space for supported programs. We applied FlexC to over 2,000 loop kernels, compiling to four different research CGRAs and 300 generated CGRAs and demonstrate a 2.2$\times$ increase in the number of loop kernels accelerated leading to 3$\times$ speedup compared to an Arm A5 CPU on kernels that would otherwise be unsupported by the accelerator.

cs.PL↗

arXiv2022

A Domain-Extensible Compiler with Controllable Automation of Optimisations

In high performance domains like image processing, physics simulation or machine learning, program performance is critical. Programmers called performance engineers are responsible for the challenging task of optimising programs. Two major challenges prevent modern compilers targeting heterogeneous architectures from reliably automating optimisation. First, domain-specific compilers such as Halide for image processing and TVM for machine learning are difficult to extend with the new optimisations required by new algorithms and hardware. Second, automatic optimisation is often unable to achieve the required performance, and performance engineers often fall back to painstaking manual optimisation. This thesis shows the potential of the Shine compiler to achieve domain-extensibility, controllable automation, and generate high performance code. Domain-extensibility facilitates adapting compilers to new algorithms and hardware. Controllable automation enables performance engineers to gradually take control of the optimisation process. The first research contribution is to add 3 code generation features to Shine, namely: synchronisation barrier insertion, kernel execution, and storage folding. The second research contribution is to demonstrate how extensibility and controllability are exploited to optimise a standard image processing pipeline for corner detection. The final research contribution is to introduce sketch-guided equality saturation, a semi-automated technique that allows performance engineers to guide program rewriting by specifying rewrite goals as sketches: program patterns that leave details unspecified.

cs.PL↗

arXiv2022

3D helical CT Reconstruction with a Memory Efficient Learned Primal-Dual Architecture

Deep learning based computed tomography (CT) reconstruction has demonstrated outstanding performance on simulated 2D low-dose CT data. This applies in particular to domain adapted neural networks, which incorporate a handcrafted physics model for CT imaging. Empirical evidence shows that employing such architectures reduces the demand for training data and improves upon generalisation. However, their training requires large computational resources that quickly become prohibitive in 3D helical CT, which is the most common acquisition geometry used for medical imaging. Furthermore, clinical data also comes with other challenges not accounted for in simulations, like errors in flux measurement, resolution mismatch and, most importantly, the absence of the real ground truth. The necessity to have a computationally feasible training combined with the need to address these issues has made it difficult to evaluate deep learning based reconstruction on clinical 3D helical CT. This paper modifies a domain adapted neural network architecture, the Learned Primal-Dual (LPD), so that it can be trained and applied to reconstruction in this setting. We achieve this by splitting the helical trajectory into sections and applying the unrolled LPD iterations to those sections sequentially. To the best of our knowledge, this work is the first to apply an unrolled deep learning architecture for reconstruction on full-sized clinical data, like those in the Low dose CT image and projection data set (LDCT). Moreover, training and testing is done on a single GPU card with 24GB of memory.

eess.IV↗

arXiv2022

RISE & Shine: Language-Oriented Compiler Design

The trend towards specialization of software and hardware - fuelled by the end of Moore's law and the still accelerating interest in domain-specific computing, such as machine learning - forces us to radically rethink our compiler designs. The era of a universal compiler framework built around a single one-size-fits-all intermediate representation (IR) is over. This realization has sparked the creation of the MLIR compiler framework that empowers compiler engineers to design and integrate IRs capturing specific abstractions. MLIR provides a generic framework for SSA-based IRs, but it doesn't help us to decide how we should design IRs that are easy to develop, to work with and to combine into working compilers. To address the challenge of IR design, we advocate for a language-oriented compiler design that understands IRs as formal programming languages and enforces their correct use via an accompanying type system. We argue that programming language techniques directly guide extensible IR designs and provide a formal framework to reason about transforming between multiple IRs. In this paper, we discuss the design of the Shine compiler that compiles the high-level functional pattern-based data-parallel language RISE via a hybrid functional-imperative intermediate language to C, OpenCL, and OpenMP. We compare our work directly with the closely related pattern-based Lift IR and compiler. We demonstrate that our language-oriented compiler design results in a more robust and predictable compiler that is extensible at various abstraction levels. Our experimental evaluation shows that this compiler design is able to generate high-performance GPU code.

cs.PL↗

arXiv2021

Sketch-Guided Equality Saturation: Scaling Equality Saturation to Complex Optimizations of Functional Programs

Generating high-performance code for diverse hardware and application domains is challenging. Functional array programming languages with patterns like map and reduce have been successfully combined with term rewriting to define and explore optimization spaces. However, deciding what sequence of rewrites to apply is hard and has a huge impact on the performance of the rewritten program. Equality saturation avoids the issue by exploring many possible ways to apply rewrites, efficiently representing many equivalent programs in an e-graph data structure. Equality saturation has some limitations when rewriting functional language terms, as currently naive encodings of the lambda calculus are used. We present new techniques for encoding polymorphically typed lambda calculi, and show that the efficient encoding reduces the runtime and memory consumption of equality saturation by orders of magnitude. Moreover, equality saturation does not yet scale to complex compiler optimizations. These emerge from long rewrite sequences of thousands of rewrite steps, and may use pathological combinations of rewrite rules that cause the e-graph to quickly grow too large. This paper introduces \emph{sketch-guided equality saturation}, a semi-automatic technique that allows programmers to provide program sketches to guide rewriting. Sketch-guided equality saturation is evaluated for seven complex matrix multiplication optimizations, including loop blocking, vectorization, and multi-threading. Even with efficient lambda calculus encoding, unguided equality saturation can locate only the two simplest of these optimizations, the remaining five are undiscovered even with an hour of compilation time and 60GB of RAM. By specifying three or fewer sketch guides all seven optimizations are found in seconds of compilation time, using under 1GB of RAM, and generating high performance code.

cs.PL↗

arXiv2021

Deep learning based dictionary learning and tomographic image reconstruction

This work presents an approach for image reconstruction in clinical low-dose tomography that combines principles from sparse signal processing with ideas from deep learning. First, we describe sparse signal representation in terms of dictionaries from a statistical perspective and interpret dictionary learning as a process of aligning distribution that arises from a generative model with empirical distribution of true signals. As a result we can see that sparse coding with learned dictionaries resembles a specific variational autoencoder, where the decoder is a linear function and the encoder is a sparse coding algorithm. Next, we show that dictionary learning can also benefit from computational advancements introduced in the context of deep learning, such as parallelism and as stochastic optimization. Finally, we show that regularization by dictionaries achieves competitive performance in computed tomography (CT) reconstruction comparing to state-of-the-art model based and data driven approaches.

stat.ML↗

arXiv2020

X-ray dark-field signal reduction due to hardening of the visibility spectrum

X-ray dark-field imaging enables a spatially-resolved visualization of ultra-small-angle X-ray scattering. Using phantom measurements, we demonstrate that a material's effective dark-field signal may be reduced by modification of the visibility spectrum by other dark-field-active objects in the beam. This is the dark-field equivalent of conventional beam-hardening, and is distinct from related, known effects, where the dark-field signal is modified by attenuation or phase shifts. We present a theoretical model for this group of effects and verify it by comparison to the measurements. These findings have significant implications for the interpretation of dark-field signal strength in polychromatic measurements.

physics.med-ph↗

arXiv2020

A Language for Describing Optimization Strategies

Optimizing programs to run efficiently on modern parallel hardware is hard but crucial for many applications. The predominantly used imperative languages - like C or OpenCL - force the programmer to intertwine the code describing functionality and optimizations. This results in a nightmare for portability which is particularly problematic given the accelerating trend towards specialized hardware devices to further increase efficiency. Many emerging DSLs used in performance demanding domains such as deep learning, automatic differentiation, or image processing attempt to simplify or even fully automate the optimization process. Using a high-level - often functional - language, programmers focus on describing functionality in a declarative way. In some systems such as Halide or TVM, a separate schedule specifies how the program should be optimized. Unfortunately, these schedules are not written in well-defined programming languages. Instead, they are implemented as a set of ad-hoc predefined APIs that the compiler writers have exposed. In this paper, we present Elevate: a functional language for describing optimization strategies. Elevate follows a tradition of prior systems used in different contexts that express optimization strategies as composition of rewrites. In contrast to systems with scheduling APIs, in Elevate programmers are not restricted to a set of built-in optimizations but define their own optimization strategies freely in a composable way. We show how user-defined optimization strategies in Elevate enable the effective optimization of programs expressed in a functional data-parallel language demonstrating competitive performance with Halide and TVM.

cs.PL↗