Harrison (Intel Corporation, United States): Formal Verification
of Mathematical Algorithms
Algorithms for computing floating-point approximations to standard mathematical functions (e.g. basic operations like division and transcendentals like "exp" and "sin"), are an important part of most computing environments. The algorithms may be realized in hardware, microcode, software, or some mixture thereof, but are usually considered among the most fundamental components of a computer system. These algorithms, especially those that are aggressively designed to optimize performance, can be quite complicated, relying on various results from pure mathematics and subtly exploiting the special features of floating-point operations. This means that they are relatively difficult to design without error, while the costs to a company like Intel of a failure, especially at the hardware level, can be huge.
Traditional approaches to ensuring correctness of hardware and software usually rely on extensive testing. However, for many functions this is not realistically feasible, even if a reliable source of comparison is available. An alternative is to prove by detailed mathematical analysis that the algorithm obeys a formal specification (e.g. correct rounding or an error bound). Since such proofs can be tedious and error-prone, it seems wise to check them, or even partly generate them, by a reliable mechanical proof-checker. We report on our experience of using the HOL Light theorem prover to formally prove correct some key floating-point algorithms used in the Intel Itanium architecture. We will sketch how some of the formal proofs are conducted, and draw some general conclusions concerning the promise of this approach.
Peter Markstein (Hewlett-Packard, United States): A Fast Quad Precision Elementary Function Library for Itanium
This talk will describe Itanium's floating point architecture and how it has been used to produce a high performance, highly accurate quad precision elementary function library.
Itanium's floating-point features will first be described, from the point of view of a computer architect. Many conflicting requirements vie for consideration during the design of a new computer architecture. These include instruction word size, number of registers, the set of operations, arithmetic precisions supported, and memory access. Some of the trade-offs during the design phase will be discussed.
One of the objectives of the original Itanium design was to accelerate quad precision arithmetic. The talk will describe how the Itanium elementary function library was constructed, with attention to performance and accuracy. Because a pair of double-extended floating point words are used for internal operations involving quad precision numbers, intermediate results, holding 128 bits, provide 15 guard bits during intermediate calculations, resulting in a very low percentage of misrounded results.
Bernard Mourrain (INRIA, France): ROXANE: Reliable Open Software-Components for Algebraic and Numeric Efficiency
Modeling questions in geometry and in many other areas lead to the treatment of algebraic problems, where efficiency and reliability are crucial. In such a context, approximate computation is needed to handle large practical situations but some algorithmic part used in the branching tests have however to be certified, in order for instance, to avoid infinite loops.
The fundamental question which arises here is how to treat efficiently real algebraic numbers. This involves numerical approximations of roots of polynomials, isolation techniques, sign evaluation of polynomials expressions of these numbers, ... In this talk, I will present a few methods and tools for handling such a combination of approximate and certified computation, based on standard or extended arithmetic, filtering techniques and their use in algebraic algorithms. The methods and their performances will be illustrated on problems in domains such as computational geometry on curved objects, which involve intensive operations on numerous but small algebraic objects.
This will also motivate the presentation of a framework called ROXANE, integrating different software components for symbolic and numeric computation. Its design and the way these components can work efficiently together will be discussed, and illustrated by experimentations.