Work partially funded by Spanish MEC, projects ARES – CONSOLIDER INGENIO 2010 CSD2007-00004 – and eAEGIS – TSI2007-65406-C03-02

We present Barra, a simulator of Graphics Processing Units (GPU) tuned for general purpose processing (GPGPU). It is based on the UNISIM framework and it simulates the native instruction set of the Tesla architecture at the functional level. The inputs are CUDA executables produced by NVIDIA tools. No alterations are needed to perform simulations. As it uses parallelism, Barra generates detailed statistics on executions in about the time needed by CUDA to operate in emulation mode. We use it to understand and explore the micro-architecture design spaces of GPUs.

Gappa is a tool designed to formally verify the correctness of numerical software and hardware. It uses interval arithmetic and forward error analysis to bound mathematical expressions that involve rounded as well as exact operators. It then generates a theorem and its proof for each verified enclosure. This proof can be automatically checked with a proof assistant, such as Coq or HOL Light. It relies on a large companion library of facts that we have developed. This Coq library provides theorems dealing with addition, multiplication, division, and square root, for both fixed- and floating-point arithmetics. Gappa uses multiple-precision dyadic fractions for the endpoints of intervals and performs forward error analysis on rounded operators when necessary. When asked, Gappa reports the best bounds it is able to reach for a given expression in a given context. This feature can be used to identify where the set of facts and automatic techniques implemented in Gappa becomes insufficient. Gappa handles seamlessly additional properties expressed as interval properties or rewriting rules in order to establish more intricate bounds. Recent work showed that Gappa is suited to discharge proof obligations generated for small pieces of software. They may be produced by third-party tools and the first applications of Gappa use proof obligations written by designers or obtained from traces of execution.

The Cody and Waite argument reduction technique works perfectly for reasonably large arguments, but as the input grows, there are no bits left to approximate the constant with enough accuracy. Under mild assumptions, we show that the result computed with a fused multiply-add provides a fully accurate result for many possible values of the input with a constant almost accurate to the full working precision. We also present an algorithm for a fully accurate second reduction step to reach full double accuracy (all the significand bits of two numbers are accurate) even in the worst cases of argument reduction. Our work recalls the common algorithms and presents proofs of correctness. All the proofs are formally verified using the Coq automatic proof checker.

Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or proof assistant in a convenient and highly automated as well as interactive way. First, we formally establish upper and lower bounds for elementary functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations take place in an algebraic setting. In order to reduce the dependency effect of interval arithmetic, we integrate two techniques: interval splitting and Taylor series expansions. This pragmatic approach has been developed, and formally verified, in a theorem prover. The formal development also includes a set of customizable strategies to automate proofs involving explicit calculations over real numbers. Our ultimate goal is to provide guaranteed proofs of numerical properties with minimal human theorem-prover interaction.

Graphics processing units (GPUs) are now powerful and flexible systems adapted and used for other purposes than graphics calculations (general purpose computation on GPU — GPGPU). We present here a prototype to be integrated into simulation codes that estimate temperature, velocity and pressure to design next generations of solar receptors. Such codes will delegate to our contribution on GPUs the computation of heat transfers due to radiations. We use Monte-Carlo line-by-line ray-tracing through finite volumes. This means data-parallel arithmetic transformations on large data structures. Our prototype is inspired on the source code of GPUBench. Our performances on two recent graphics cards (Nvidia 7800GTX and ATI RX1800XL) show some speed-up higher than 400 compared to CPU implementations leaving most of CPU computing resources available. As there were some questions pending about the accuracy of the operators implemented in GPUs, we start this report with a survey and some contributed tests on the various floating point units available on GPUs.

This paper presents a set of tools for mechanical reasoning of numerical bounds using interval arithmetic. The tools implement two techniques for reducing decorrelation: interval splitting and Taylor's series expansions. Although the tools are designed for the proof assistant system PVS, expertise on PVS is not required. The ultimate goal of the tools is to provide guaranteed proofs of numerical properties with a minimal human-theorem prover interaction.

Studying floating point arithmetic, authors have shown that the implemented operations (addition, subtraction, multiplication, division and square root) can compute a result and an exact correcting term using the same format as the inputs. Following a path initiated in 1965, many authors supposed that neither underflow nor overflow occurred in the process. Overflow is not critical as this kind of exception creates persisting nonnumeric quantities. Underflow may be fatal to the process as it returns wrong numeric values with little warning. Our new conditions guarantee that the correcting term is exact when the result is a number. We have validated our proofs against Coq automatic proof checker. Our development has raised many questions, some of them were expected while other ones were surprising.

A commonly used argument reduction technique in elementary function computations begins with two positive floating point numbers /spl alpha/ and /spl gamma/ that approximate (usually irrational but not necessarily) numbers 1/C and C, e.g., C = 2/spl pi/ for trigonometric functions and ln 2 for e/sup x/. Given an argument to the function of interest it extracts z as defined by x/spl alpha/ = z + /spl sigmav/ with z = k2/sup -N/ and |sigmav;| /spl les/ 2/sup -N-1/, where k, N are integers and N /spl ges/ 0 is preselected, and then computes u = x - z/spl gamma/. Usually z/spl gamma/ takes more bits than the working precision provides for storing its significant and thus exact x - z/spl gamma/ may not be represented exactly by a floating point number of the same precision. This will cause performance penalty when the working precision is the highest available on the underlying hardware and thus considerable extra work is needed to get all the bits of x - z/spl gamma/ right. We present theorems that show under mild conditions that can be easily met on today's computer hardware and still allow /spl alpha/ /spl ap/ 1/C and /spl gamma/ /spl ap/ C to almost the full working precision, x - z/spl gamma/ is a floating point number of the same precision. An algorithmic procedure based on the theorems is obtained. The results will enhance performance, in particular on machines that has hardware support for fused multiply-add (fma) instruction(s).

Past recorders have added critical path delay for the more frequent case where both inputs are non redundant. Our proposed circuit does not lengthen the time of one multiplication compared to the state-of-the-art encoding, if both inputs are non redundant. We have slightly modified an existing cell to accept a redundant binary number in place of the non redundant number by changing some connections. The recoding operators associated with a high level quantity (the fraction range) all defined in this paper are used to rule out some possibilities as inputs of this newly created cell. We check that the modified cell yields the correct output for the remaining possible inputs.

In modern computers, the floating point unit is the part of the processor delivering the highest computing power and getting most attention from the design team. Performance of any multiple precision application will be dramatically enhanced by adequate use of floating point expansions. We present three multiplication algorithms, faster and more integrated than the stepwise algorithm proposed earlier. We have tested these novel algorithms on an application that computes the determinant of a matrix. In the absence of overflow or underflow, the process is error free and possibly more efficient than its integer based counterpart.

The dot product operation is very prevalent in scientific computation and has therefore been incorporated as a primitive operation in some languages. The implementation of the dot product operation by a sequence of IEEE standard multiplications and additions does not prevent a substantial accumulation of the round-off errors or warn the user about a catastrophic cancellation. We present the design of a double precision dot product operation employing sticky accumulation, where the final rounded result is validated by raising a new exception flag if the result incurred catastrophic cancellation. Sticky accumulation can be implemented in a pipeline or parallel environment to sustain double precision with an extended control of the error. Our design allows that, in the absence of catastrophic cancellation, one ulp accuracy is guaranteed.

A double precision dot product operation is designed in which the final rounded result is validated by raising exception flags if either the result incurs catastrophic cancellation or the result is not accurate to one unit in the last place (ulp). The design guarantees one ulp accuracy in the absence of catastrophic cancellation. The user can thus obtain validated results at marginal extra cost with the ability to trap to alternative routines in those cases where the results are suspicious.>