John
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. |