With tomography it is possible to reconstruct the interior of an object without destroying. It is an important technique for many applications in, e.g., science, industry, and medicine. The runtime... Show moreWith tomography it is possible to reconstruct the interior of an object without destroying. It is an important technique for many applications in, e.g., science, industry, and medicine. The runtime of conventional reconstruction algorithms is typically much longer than the time it takes to perform the tomographic experiment, and this prohibits the real-time reconstruction and visualization of the imaged object. The research in this dissertation introduces various techniques such as new parallelization schemes, data partitioning methods, and a quasi-3D reconstruction framework, that significantly reduce the time it takes to run conventional tomographic reconstruction algorithms without affecting image quality. The resulting methods and software implementations put reconstruction times in the same ballpark as the time it takes to do a tomographic scan, so that we can speak of real-time tomographic reconstruction. Show less
This thesis presents the new approaches to improve the performance of a weather forecast model. These approaches require the code complexities, which can be resolved by code generation. In Chapter... Show moreThis thesis presents the new approaches to improve the performance of a weather forecast model. These approaches require the code complexities, which can be resolved by code generation. In Chapter 2 we investigated the extension to the code generation tool CTADEL to generate code for Galerkin finite element methods. Applying to generate code for the Shallow-Water equations, we found that the generated code is 3 and 1.2 times faster than the handwritten code with the gfortran 4.1.2 and pathscale 3.0 compiler, respectively. In Chapter 3, we optimized the parallel implementation of the HIRLAM weather forecast model by overlapping communications with calculations. We found that the performance of this parallel implementation can be significantly improved by overlapping communications with calculations. In Chapter 4 we extended CTADEL to generate parallel programs. By applying this technique we have successfully generated efficient parallel code for the Shallow-Water equations. In Chapter 5 we investigated a method to speed up the HIRLAM weather forecast model. We accelerated the dynamics routine by porting it on GPUs. We found that using GPUs for weather forecasting yields an order of magnitude performance improvement over the use of conventional CPUs. In Chapter 6 we showed our extension to CTADEL to automatically generate high efficient CUDA codes. Then, we applied to generate CUDA stream code for the dynamics routine of the HIRLAM weather forecast model. The results showed that the generated code is more efficient than the optimized handwritten program. Show less
The remainder of this thesis is organized as follows. Chapters 2 and 3 introduce the specification formalisms that are used in this thesis. In Chapter 2 we present the computation language. We show... Show moreThe remainder of this thesis is organized as follows. Chapters 2 and 3 introduce the specification formalisms that are used in this thesis. In Chapter 2 we present the computation language. We show that it facilitates the description of specifications that are not partial to a particular mode of execution. Furthermore, we present a semantics and a logic for reasoning about correctness of programs. In Chapter 3 we present the coordination language. We define its semantics and show how it connects to the computation language. In Chapters 4 and 5 we develop a theory of refinement. This theory provides a number of proof techniques that enable us to incrementally refine the behavioural aspects of a program. These chapters form the most theoretical part of this thesis. It should be possible to get an understanding of the methods derived in these chapters without going through all these proofs. In Chapter 7 we illustrate the method of design by considering some case studies. Comparisons with related work and conclusions are described in Chapters 8 and 9. Show less