Project 25: IEEE floating-point arithmetic standard The group has been actively involved both with the original standard and its revision in 2008. ----------------------------------------------------------------------- Oxford 2016: ============ ADDENDUM The IEEE Standard for Floating-Point Arithmetic has a new revised standard "754-2008 - IEEE Standard for Floating-Point Arithmetic" and is at http://standards.ieee.org/findstds/standard/754-2008.html A minor revision of that standard is in progress and is expected for 2017. ----------------------------------------------------------------------- ----------------------------------------------------------------------- Information from meetings before 2016 (in chronological order): ----------------------------------------------------------------------- Baden 1978: =========== Discussion turned to the proposals for machine arithmetic. It was agreed that if +0 and -0 both exist then they should be equal under comparison. Professor Hull wanted to be clear that a statement A .LT. B could not cause overflow and asked whether it was possible to draw a horizontal line through the ordered list of preferences, above which the preferences were clearly important. After some discussion on the latter question it was generally agreed that the document should consist of paragraphs rather than be in the form of a list. Professor Gear was, entrusted to prepare a document in WG 2.5's name and to send this to the Chairman of the sub-committee of I.E.E.E. together with a covering letter. Personal copies would be sent to Professor Kahan and Dr. M. Payne. Novosibirsk 1979: ================= IEEE Floating point standard. Brown summarized the present situation. The technical arguments are unchanged since the Baden meeting and there is a large measure of agreement. However there remain differences over details; on DEC's part they are largely based on considerations of economy. Reinsch reported that since Gear (IFIP/WG 2.5 (Baden-6) 506) had referred to his paper (IFIP/WG 2.5 (Baden-4) 504), both sides had written to him for approval and he had replied with detailed comments. Reinsch also explained that Robert Reid had proposed to IEEE that more bits be moved into the exponent for both very large and very small numbers. He (and Kahan) is opposed to the proposal. At the end of the computation there is no way of knowing whether precision has been lost in intermediate steps. Rice moved that individuals continue to comment (particularly Reinsch, Cody, Brown) but that the group does nothing official - passed 13 in favour, 1 abstention. Ford expressed thanks to Gear for his work. Rice proposed that he should collaborate with Reinsch and Hull to produce a summary of the Reinsch paper for publication in IEEE Computer. Harwell 1980: ============= C.H. Reinsch: Are we prepared for the proposed IEEE floating-point processor? Consequences and new possibilities for numerical algorithms were discussed; in particular (1) the benefits of a uniquely defined rounding strategy which lets one much better analyze and attack the effects of rounding errors. (2) the comprehensive support it gives for Kahan's "more complete" interval arithmetic, which therefore might considerably gain practical importance. (3) the many options it provides for handling arithmetic exceptions, especially introducing "heaps" with the help of the newly added "trapping NaN's". Discussion: Reid: Surely the storage management problem with heaps (garbage collection) could be treated by holding a pointer back to the NaN from each pair of words holding a complete result. Then, when space runs out, all pairs that are no longer active can be recognized at once. Reinsch: Yes but this gives an overhead which could be costly because large numbers of these trapping NaN's may be created in matrix operations. Hull: What are implications of these facilities for languages? Reinsch: A good list was compiled by Stuart I. Feldman (SIGNUM Newsletter October 1979, p.31). Also, a paper by Ron Hunsinger at the ELECTRO80 in Boston describes interfacing the proposed IEEE floating-point processor to ADA: only difficulty is that arithmetic exception flags are (forbidden) side effects in arithmetic operations. Wichmann: There will be problems within ADA, for example using extended precisions. I suspect that any implementation will set the option "toggles" to standard values. Reinsch: The proponents hope that extended precision is a good instance of the correctness of their viewpoint: let's get the hardware agreed first, then think about the language needed. Gear: Intel have a version of FORTRAN that stores extended intermediate results into main memory. Hull: We need a language facility that expresses the exact precision available in the hardware. --- IEEE floating-point standardization ----------------------------------- Einarsson reviewed the position and drew attention to the document IFIP/WG 2.5 (Harwell-15)715 on the VAX arithmetic. Reinsch summarized the current objections against the KCS proposal (see IFIP/WG 2.5 (Harwell-33)733). Gear reported that the necessary 2/3 majority for the KCS proposal was near [actually it has been obtained, but changes of mind are permitted until mid-June - JKR]. It was agreed nem-con that a sub-committee consisting of Hull (Chairman) and Smith should prepare a statement of support for the KCS proposal and send it to the IEEE Microprocessor Standards Subcommittee (to which the floating-point working group reports). Reinsch drew attention to the paper by Feldman in the special issue of SIGNUM (Oct 79). IFIP 80 ------- Gear reported that he was very worried about the proposed panel discussion on "Standardization of floating-point arithmetic: benefits and implications" (see IFIP/WG 2.5 (Harwell-32)732) at IFIP 80. Reinsch had been unable to obtain funding and funds for Gear and Cody had yet to be confirmed. Feldman is still trying and Freyley/Walther do not know whether either can come. Lawson remarked that it was important to go through with the panel if all possible. He thought Gear / Cody / Brent sufficient though course wider spread would be preferable. Boulder 1981: ============= Brent reported on the IFIP 1980 Congress. The panel discussion on "Standardization of floating-point arithmetic: benefits and implications" by Gear (Chairman), Cody, Brent, and Fraley was attended by about 40 participants and took more the form of a tutorial session than that of a real discussion. Stetter remarked that we only got the panel discussion by making a stand. The group agreed the statement IFIP/WG 2.5 (Boulder-36) 836 of support for the IEEE floating-point standard. It asked Reid to take it to the TC2 meeting at Dijon for onward submission for full IFIP approval. --- Cody explained that IEEE committee P854 is charged with preparing a radix and wordlength independent floating-point standard that is 'upward compatible' with the draft binary standard. The intent is to extend the functionality of the binary standard in response to informal requests from manufacturers committed to other than 32 bit binary arithmetic. The committee has met publicly only twice with the third meeting scheduled for October at the SIAM meeting in Cincinnati. A sub-committee has redrafted important sections of the binary standard, including the crucial section on formats, for discussion at the next meeting. It is too early to forecast the reaction of major manufacturers. Personnel from Cray, IBM, Univac and others have been added to the mailing list at their request. Some have expressed a willingness to actively participate in drafting a standard. Madison 1982: ============= It was noted that a supportive statement (WG2.5 wording from Boulder) was about to be sent from IFIP to IEEE. It was agreed to reopen the project with Cody and Brown as principals. Cody reported on developments within the IEEE committee for floating-point standardization on micros. NaN's are now said to be "signalling" or "quiet". The warning mode has been deleted. This saves some hardware and a lot of documentation. It was never intended as a permanent feature. Work continues on tidying up the document (grammar, spelling, etc.). He told working group members to let him know if they want to join the mailing list. The generalized standard (854) must contain the binary standard (754) as a subset and preserve its properties. The aim is to avoid explicit mention of the radix or wordlength. Battiste asked about progress on standards for functions and was told that there was nothing specific yet. A position paper considers what is reasonable. Kulisch remarked that with his arithmetic there was little to say since all functions can be done within the accuracy of a final roundoff. Dekker said he had been corresponding with Reinsch and was willing to provide details to anyone interested. Einarsson told the group that its motion of support had passed through TC2 to the IFIP council and an official letter was on its way to the IEEE Computer Society president. Soederkoeping 1983: =================== See documents IFIP/WG 2.5 (Soederkoeping-09, 17, 18) 1009, 1017, 1018. The group support of IEEE floating point standard has been endorsed by IFIP. Stetter felt that the influence on computer manufacturers has been quite striking. The group expressed its delight and thanked Cody for working in this area. Pasadena 1984: ============== Status of IEEE Floating-Point Standards (Cody) ---------------------------------------------- There has been no movement within IEEE on the P754 Draft Standard. New management of the standards activities has promised action, and members of the Microprocessor Standards Committee were polled this past spring for willingness to serve on the TC Review Committee for P754, but there has been no movement. P854 was refused permission to publish the draft standard per se, but was urged to produce an expository paper describing the draft. The paper could contain the entire draft standard, provided it was sufficiently broken up that it could not possibly be confused with an official standard. Such a paper has been prepared (see document IFIP/WG 2.5 (Pasadena-08)1108), and will appear in the August issue of IEEE Micro, baning unforeseen circumstances. The P854 committee believes this paper to be a major publication exceeding in importance the mere publication of the draft standard. It explains how certain decision were receded, amplifies the finer points of the standard, and hints at how implementation might be done. We believe that the paper sets a higher-quality precedent for such papers should they now become the recognized vehicle for publishing draft standards for public review. The 854 draft has been fully implemented in the HP 71 B computer. To date, this is the only fully supported implementation of either P754 or P854 (with the possible exception of Intel Fortran support for the 28087). Work continuous on suggestions for proper language support of the draft standards. Them is nothing to report in this regard, except that Apple has documented their approach to language support (the SANE system). Gentleman feels that the problem of support is beyond the language. Cody confirms that there are serious problems of exception handlings on MIMD machines. The group feels this is a very good paper. Validation of floating-point systems ------------------------------------- Wichmann has given Rice a document entitled "A proposal for a validation package for floating point systems" (see document IFIP/WG 2.5 (Pasadena-07) 1107), along with a request that it be brought to WG 2.5's attention. It is discussed at some length and a summary of these discussions is to be sent to Wichmann by Rice. Sophia-Antipolis 1985: ===================== IEEE Standardization (Cody) --------------------------- The binary floating-point standard (P754 Draft 10.1) was accepted by the IEEE in March 1985, and is now an official standard. Copies will be available shortly from IEEE. The generalized draft standard (P854, Draft 1.0) was published in the August issue of IEEE Micro. A preprint appeared in the minutes of our Pasadena meeting, and reprints are available from the authors. Draft 2.0, a slight revision of Draft 1.0, is now under ballot with passage not certain. If the ballot does pass, the draft will be given to the Microprocessor Standards Committee (MSC) on July 8, 1985. The procedure is for MSC to pass the draft along quickly to the sponsoring TO for technical review (typically a three or four month process), and for the TC to pass it along to the IEEE Standards Committee for final procedural review. With luck, P854 could be an accepted standard by Spring, 1986. Reid thanked Cody for all his work on the standard. Argonne 1986: ============= Document: IFIP/WG 2.5 (Argonne-24) 1324, 1 page. B Cody summarized the the status of the P854 document (draft 3.0). The document is being processed by the technical committee, and is also being reviewed outside the committee. Currently no formal support/action by Working Group 2.5 is needed to advance the standardization process. Como 1987: ========== Document: IFIP/WG 2.5 (Como-14) 1414, 2 pages. The final report on IEEE arithmetic standard was accepted by the group. J. Reid will write to J. Cody to express the appreciation and the pleasure the group feels for this important success in standardizing arithmetic. Toronto 1992: ============= Language Independent Arithmetic ------------------------------- Document: IFIP/WG 2.5 (Toronto-9) 1909, 24 pages. C Shaffert presented the Language Independent Arithmetic (LIA). It is meant to be a software standard that is independent of architecture and should be viewed as a set of inquiry functions about the environment as seen by a compiler. Discussion followed. The general feeling was that the standard is premature and not sufficiently well defined. Individual WG 2.5 members undertook to discuss the pros and cons of this issue further and work towards either correction or elimination of this proposal. The WG 2.5 thanked John Reid and Jim Cody for their active involvement in the LIA issues, and C. Shaffert for the presentation. Copenhagen 1993: ================ Language Independent Arithmetic ------------------------------- Reid informed the group that LIA is about to become draft ISO standard. A discussion followed. Reid further informed the groups that he did take action in UK, but UK's vote was still a YES. Ford informed the group that NAG did participate in the Albuquerque meeting, and that US vote was NO. The LIA document is now considerably improved, but still leaves a lot to be desired. For example, although it is not technically unachievable, it is incomplete (Rice) and operations are very complicated (Kulisch). There are still concerns. WG 2.5 will send a written comment to ISO, and will publish it in forums such as SIGNUM. Technical discussion led to the decision that the group remains actively involved in the issues related to the proposed ISO Language Independent Arithmetic (LIA) Standard. Kyoto 1995: =========== Document: Kyoto-2214, "GAMM-IMACS Proposal for Accurate Floating-Point Vector Arithmetic", Mathematics and Computers in Simulation, Vol. 35, No. 4, pp. 375-382, 1993. The Kulisch GAMM-IMACS work and proposal was discussed. IFIP WG 2.5 endorses the effort. Strobl 2003: ============ Design of an Arithmetic Unit ---------------------------- A brief overview of how to effectively implement (in hardware) IEEE floating point arithmetic was presented by Kulisch. This is the subject of a new book aimed at engineers: Kulisch, Ulrich W.; Advanced Arithmetic for the Digital Computer, Design of Arithmetic Units. Springer-Verlag, 2002, XII, 141 p., Softcover ISBN: 3-211-83870-8. Hong Kong 2005: =============== Ron Boisvert reported that revision of IEEE 754 is in progress, with a deadline of December 2006. Areas of consideration are 1. Decimal formats and arithmetic 2. Quad precision (128 bits) 3. Recognize the multiply/addition combination Further information on the web page http://en.wikipedia.org/wiki/IEEE_754r The drafts are available at http://754r.ucbtest.org/drafts/archive/ Prescott 2006: ============== Bo Einarsson was assigned the task to write a message to the IEEE 754 Revision Committee: To the IEEE 754 Revision Committee The IFIP Working Group WG 2.5 at its meeting July 15, 2006, in Prescott, Arizona, discussed certain features of the proposed revision of IEEE 754. We appreciate what the present standard has achieved in assisting the possibilities in writing truly portable numerical software and making it easy to transfer binary data between computers from different manufacturers. We have two suggestions to further improve the standard. The presentation below is based on Draft P754 1.1.4 of August 12, 2006. 1. NaNs (8.2.1 Binary encodings of NaN) We have noted the problem at the transfer of binary data including NaNs between computers from different manufacturers, since the meaning of a specific NaN is not standardized. We therefore suggest that the binary encoding of the NaNs should be as follows in the trailing significand: First bit: 1 for quiet NaN, 0 for signaling NaN Following five bits: Contains coding of the main NaNs, compare the list in 9.2 Invalid operation. Interpreting the bits in decimal form, 0 Disallowed (to surely distinguish a NaN from infinity) 1-30 Thirty different alternatives for NaN 31 Undefined NaN 2. Rounding alternatives (6. Modes and rounding) Of interest to the numerical community is the use of interval arithmetic. In order to obtain as narrow intervals as possible, it is necessary to have directed rounding in hardware. The standard permits switching of rounding mode at the systems level, either in constant-mode or in dynamic mode. Doing interval arithmetic will then require switching the rounding mode almost after every arithmetic operation, which will take a lot of time. For further information see the letters from Ulrich Kulish of May and August, 2005, and June 2006. We would therefore prefer to have operations like AddBinaryRoundingDirectionTowardPositive(a,b) and AddBinaryRoundingDirectionTowardNegative(a,b), as well as similar for the other elementary operations, also available. --------------------------------------------------------------- Subject: [Stds-754] IEEE 754 Revision, comments from IFIP WG 2.5 From: Bob Alverson Date: Tue, 22 Aug 2006 17:35:41 -0700 To: Jeff Kidder CC: Bo Einarsson , scanon@berkeley.edu, stds-754@IEEE.ORG, stds-754@ucbtest.org, wg25@nsc.liu.se, bob@cray.com If you used the ideas in the following paper: http://www.brics.dk/~barnie/RealLib/intervals.pdf you could use round toward positive for all operations. As a side effect, it maps more efficiently to SSE registers which can do 2 64 bit adds in parallel, but they (currently) have to have the same rounding direction. No problem for some people! Bob ---------------------------------------------------------------- Uppsala 2007: ============= The proposed revision of IEEE 754 was discussed in Uppsala and it was decided to send a letter expressing the views of the working group to the IEEE Microprocessor Standards Committee. The final letter is available on the internal pages as http://wg25.taa.univie.ac.at/ifip/intern/IFIPWG-IEEE754R.pdf ADDENDUM ======== From: Marc Daumas Date: Mon, 3 Sep 2007 04:38:23 -0400 Subject: Formal Proofs on Floating Point library Dear NA-Net'ers, The "Formal Proofs on Floating Point" library (FP2) is a set of formal definitions and theorems (including proofs) to reason about floating point numbers. It is now stored in the "FP" section of NetLib for public use. It enables users to formally define types and operations of floating arithmetic and to deduce properties using a mechanized proof checker. http://www.netlib.org/fp/fp2.tgz This library was first designed by Marc Daumas, Laurent Thery* and Laurence Rideau*. Contributors now include Sylvie Boldo*, Jean-Michel Muller, Laurent Fousse*, Ren-Cang Li and Guillaume Melquiond*. Contributors that were directly interacting with Coq are outlined by a star. Latest developments include: - Proved algorithms for argument reduction - Software emulation of the FMA using rounding to odd - A few properties from Prof. W. Kahan - Results on the ulp of the inverse of a floating-point number from Dr. P. Markstein - A link to the IEEE-754 standard - Radix-independent algorithm to compute the exact error of a multiplication - Error of a floating-point division or square root - Conditions for a*x+y to be faithfully computed Sources are in the "source" directory and are to be compiled with version 8.1 of Coq. http://coq.inria.fr/ Detailed documentations are in the "doc" directory and start with the "index.html" file. Documents: ========== 1. IEEE 754-1985 Binary Floating-Point Arithmetic (ANSI/IEEE Standard), IEEE Computer Society Press, Catalog No. SH10116, 1985. 2. IEEE 854-1987 Radix and Format Independent Floating-Point Arithmetic (ANSI/IEEE Standard), IEEE Computer Society Press, Catalog No. SH11460, 1987. 3. ISO/IEC 10967-1:1994, Information technology -- Language independent arithmetic -- "Part 1: Integer and floating point arithmetic". 4. ISO/IEC 10967-2:2001,Information technology -- Language independent arithmetic -- Part 2: Elementary numerical functions 5. ISO/IEC 11404:1996, Information technology -- Programming languages, their environments and system software interfaces -- Language-independent datatypes 6. ISO/IEC 13886:1996, Information technology -- Language-Independent Procedure Calling (LIPC) 7. ISO/IEC TR 14369:1999, Information technology -- Programming languages, their environments and system software interfaces -- Guidelines for the preparation of Language-Independent Service Specifications (LISS) 8. IEEE 754-2008 Standard for Floating-Point Arithmetic, Approved Publication of IEEE, Published Date: Aug 29, 2008 **Revision of IEEE Std 754-1985