From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.0 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 67725BC0B for ; Sun, 26 Nov 2006 02:52:01 +0100 (CET) Received: from nef2.ens.fr (nef2.ens.fr [129.199.96.40]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id kAQ1pxLt032574 for ; Sun, 26 Nov 2006 02:52:01 +0100 Received: from di.ens.fr (di.ens.fr [129.199.99.1]) by nef2.ens.fr (8.13.6/1.01.28121999) with ESMTP id kAQ1pwJu035073 ; Sun, 26 Nov 2006 02:51:58 +0100 (CET) X-Envelope-To: caml-list@inria.fr Received: from [192.168.138.142] (mna75-4-82-225-77-14.fbx.proxad.net [82.225.77.14]) (authenticated bits=0) by di.ens.fr (8.13.6/jb-1.1) id kAQ1pvTK029810 ; Sun, 26 Nov 2006 02:51:58 +0100 Message-ID: <4568F338.2060307@ens.fr> Date: Sun, 26 Nov 2006 02:51:52 +0100 From: David Monniaux User-Agent: Thunderbird 1.5.0.8 (X11/20061107) MIME-Version: 1.0 To: Olivier Andrieu Cc: Christophe Raffalli , caml-list@inria.fr Subject: Re: [Caml-list] float rounding References: <89957A27-4B6A-4FCF-A425-1468ECFA8B62@cmu.edu> <4522C131.9010400@univ-savoie.fr> <17698.53404.408141.945571@karryall.dnsalias.org> In-Reply-To: <17698.53404.408141.945571@karryall.dnsalias.org> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-Virus-Scanned: by amavisd-milter (http://amavis.org/) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-2.1.9 (nef2.ens.fr [129.199.96.32]); Sun, 26 Nov 2006 02:51:58 +0100 (CET) X-Miltered: at discorde with ID 4568F33F.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; monniaux:01 monniaux:01 rounding:01 ocaml:01 wrappers:01 rounding:01 libc:01 libc:01 printf:01 fenv:01 gcc:01 biblio:01 pitfalls:01 compilers:01 caml-list:01 In the Astrée project, we use some small C functions and OCaml wrappers to change rounding modes. It's not easy (some systems have fpgetround/fpsetround, others fegetround/fesetround, some have none and you have to use assembly, and old versions of GNU libc on IA32 have fegetround/fesetround that change rounding for the 387 FPU but not for SSE, which may break some external C libraries). [ Hey, we should publish our libraries. ] In addition, some C libraries don't work properly when rounding is not "round to nearest". I filed bugs against FreeBSD libc (printf doesn't work properly with some arguments) and GNU libc (pow() does not work properly). Rounding modes other than the default "round to nearest" tend to be largely untested on many systems and libraries, because few people use them. #pragma FENV_ACCESS is not even implemented on gcc; -frounding-math is supposed to signal rounding modes other than round to nearest, but the documentation states that it's not even sure it works... Not that I want to advertise myself too much, but I think you should read http://www.di.ens.fr/~monniaux/biblio/pitfalls_of_floating_point.pdf if you are concerned about interactions between compilers and floating-point.