DATm: Diderot's Automated Testing Model

摘要

Diderot is a parallel domain-specific language forthe analysis and visualization of multidimensional scientific images, such as those produced by CT and MRI scanners. Diderot is designed to support algorithms that are based on differential tensor calculus and produces a higher-order mathematical model which allows direct manipulation of tensor fields. One of the main challenges of the Diderot implementation is bridging this semantic gap by effectively translating high-level mathematical notation of tensor calculus into efficient low-level code in the target language. A key question for a high-level language, such as Diderot, is how do we know that the implementation is correct. We have previously presented and defended a core set of rewriting rules, but the full translation from source to executable requires much more work. In this paper, we present DATm, Diderot's automated testing model to check the correctness of the core operations in the programming language. DATm can automatically create test programs, and predict what the outcome should be. We measure the accuracy of the computations written in the Diderot language, based on how accurately the output of the program represents the mathematical equivalent of the computations. This paper describes a model for testing a high-level language based on correctness. It introduces the pipeline for DATm, a tool that can automatically create and test tens of thousands of Diderot test programs and that has found numerous bugs. We make a case for the necessity of extensive testing by describing bugs that are deep in the compiler, and only could be found with a unique application of operations. Lastly, we demonstrate that the model can be used to create other types of tests by visual verification.