A standard for computation consumers
It is easy to forget but numerical computation is one of the basic building
blocks of computing. The precision of the operators and programs, their
reliability and their speed are at the heart of a large number of more
or less critical industrial applications.
It is enough to remember a few of the most famous computer errors of the
past years, such as the Pentium bug in 1994, or the explosion of the first
Ariane 5 rocket in 1996, to realize how reliability and precision are
crucial in machine computations. The primary culprits of these infamous
failures are microprocessors and the so-called numerical algorithms that
use floating point arithmetic. Floating point arithmetic is the format
implemented in computers to approximately represent real numbers (see
box).
At the end of the 1970s, engineers and researchers were able to impose
a uniform standardized solution, in spite of divergent commercial interests.
At that time, each manufacturer (Digital, Cray, Hewlett Packard,...) had
their own floating point number representation, but certain choices were
only meant to speed up computations, maybe with less transistors, even
if that meant producing notoriously false results or go contrary to programming
usages. Even the simplest arithmetic operations led to variable results
from one machine to the next. When personal computers appeared, the idea
of standardizing floating point arithmetic had gained ground. A newcomer
in the field, Intel, wanted to carve out a place on a market in which
it had no legitimacy and chose to rely on the work of an influential scientist,
William Kahan, Professor at the University of California at Berkeley.
The rest is history. Kahan's ideas strongly influenced the topic and he
then was awarded the Turing Award for his contributions. Almost all of
his recommendations have been accepted by the IEEE
(Institute of Electrical and Electronic Engineers), the learned society
that is an authority in the fields of computer engineering. The IEEE 754
standard was thus adopted in 1985 by the ANSI (American National Standards
Institute). The standard precisely defines the correct round-off for the
four arithmetical operations (addition, subtraction, multiplication and
division), and for the square root. Practically all current computers
obey this standard, even if certain functionalities are only implemented
via libraries during execution or compilation.
The best way to be at the heart of a topic
Project
ARENAIRE
of INRIA Rhône Alpes has been working in this field since its inception
in 1999, and completely integrates the standardization approach. Its researchers
are naturally involved in the ongoing discussions concerning the revision
of the IEEE 754 standard. “Our technical ideas and our research
work may thus be taken into account in the future standard,” explains
Marc Daumas, a CNRS researchers working in project ARENAIRE. “However,
for us, to participate is first of all a way of exchanging ideas with
the best specialists worldwide, to establish links that will then have
scientific consequences, to see where the wind blows, which all are plusses
to advisedly develop our ideas.” As a matter of fact, the functioning
of this
IEEE technical committee is
especially pragmatic. The standard revision committee of about twenty
persons meets every month in California, and for more efficiency, a subcommittee
works weekly to prepare the proposals to be discussed. ARENAIRE members
visit two or three times a year and then pursue discussions remotely.
In addition to INRIA, only a few British and Israeli scientists participate
in a limited fashion in these meetings, which are open and free of access.
“In this field as in many others, there is no point in developing
cool techniques in your own little corner,” says Marc Daumas. “You
have to take into account the experience of scientists, but also the point
of view of industry, and interferences with the work carried out by other
standardization committees.” Hence the interest of being at the
heart of these expert exchanges, which are at the same time a source of
inspiration for research, and a guarantee of quality for the work. It
is however difficult to isolate direct scientific consequences. One thing
is certain, project ARENAIRE is reputed in its field. ARENAIRE researchers
worked for example with Aerospatiale on the choice of floating point use
for the Airbus A380. Other researchers from the project developed complex
algorithms to reduce division computing times for STMicroelectronics.
Since 2002, they have been developing a floating point library for another
ST processor.
Multiple positive consequences
The consequences are sometimes surprising. Thus, following a consensus
reached between several members of the technical committee in 2004, it
was decided to start working on integrating arbitrary precision floating
point arithmetic into the future standard. This is a field in which another
INRIA team, SPACES of Nancy, has unique know-how. This multiprecision
mode of computation is more precise than floating point computation, but
also slower. The SPACES team developed software called
MPFR
(MultiPrecision Floating-point arithmetic with exact Rounding) that could be compatible
with the IEEE standard when it is completed, for a very reasonable overhead
in terms of computing time. The experience acquired by SPACES clearly
sets it ahead of the competition, including the experts of the standard
revision committee.
Another key area to improve computation precision is the certification
of programs and algorithms with automatic tools based on formal proofs.
Such techniques are beginning to impose themselves in cases where human
lives might be threatened by malfunctioning. They also are increasingly
interesting for industry because of their growing power and automation.
Due to ARENAIRE developments, such techniques can now be applied to programs
that resort to numerical computations. The objective of this approach
is to validate the programs and make sure that their implementation is
correct. In 2000, INRIA launched a cooperative research initiative on
the subject called AOC (Certified Computer Arithmetic) involving several
projects (LEMME, ARENAIRE and SPACES). INRIA has long been developing
a proof assistant software called Coq in the context of formal methods,
that checks the detail of proofs. Since 2002, ARENAIRE researchers have
been working on these topics in collaboration with Nasa researchers of
the Langley Research Center and of the National Institute of Aerospace
(Virginia). Historically, Nasa is strongly supportive of another formal
proof assistant called PVS, which is widely used in the United States
and in industry. Floating point arithmetic is used in a project to automate
small airport air control. Due to a collaboration funded by CNRS and
Nasa,
there will soon be a joint
Coq and PVS specification, which will ipso
facto become a primary world standard. Even if this specification has
little chance of being accepted by the IEEE, because it is expressed in
a formalism that most standard revision committee experts do not master,
its noted contributions once more make the Institute work better known.
Processing very large and very small numbers at the same time, using floating
point arithmetic
To represent real numbers, which are not integers, most computer systems use
a so-called floating point format. This format has been used for decades in
scientific computing. It consists in defining a real number with a triple: its
sign, mantissa and exponent. Changing the latter causes the decimal point to
“float”. This representation is different from the fixed point representation
in which the exponent is fixed.
Thus, in base 10, the electron mass is 9.109381 x 10-31 kg, that is to say a
plus sign, a mantissa of 9.109381 and an exponent of -31.
