sas*_*cha 4 floating-point glibc floating-accuracy double-precision ieee-754
我正在努力将sqrt函数(对于64位双精度数)从fdlibm移植到我目前正在使用的模型检查器工具(cbmc).
作为我的一部分,我阅读了很多关于ieee-754标准的内容,但我认为我不理解基本操作(包括sqrt)的精度保证.
测试我的fdlibm的sqrt端口,我在64位double上使用sqrt进行了以下计算:
sqrt(1977061516825203605555216616167125005658976571589721139027150498657494589171970335387417823661417383745964289845929120708819092392090053015474001800648403714048.0) = 44464159913633855548904943164666890000299422761159637702558734139742800916250624.0
(这个案例在我的测试中打破了关于精度的简单后置条件;我不确定是否可以使用IEEE-754来实现这种后置条件)
为了进行比较,几个多精度工具计算如下:
sqrt(1977061516825203605555216616167125005658976571589721139027150498657494589171970335387417823661417383745964289845929120708819092392090053015474001800648403714048.0) =44464159913633852501611468455197640079591886932526256694498106717014555047373210.truncated
可以看出,左起第17个数字是不同的,意味着如下错误:
3047293474709469249920707535828633381008060627422728245868877413.0
问题1:是否允许这么大的错误？
标准是说每个基本操作(+, - ,*,/,sqrt)应该在0.5 ulps之内,这意味着它应该等于数学上精确的结果四舍五入到最近的fp表示(维基说的是一些库)只保证1 ulp,但目前并不重要).
问题2:这是否意味着,每个基本操作都应该有一个错误<2.220446e-16,64位双精度(机器epsilon)？
我用x86-32 linux系统(glibc/eglibc)计算了相同的结果,并得到了与fdlibm相同的结果,让我想到:
printf将成为候选人,但我不知道是否可能是这个原因)Ste*_*non 14
IEEE-754标准要求所谓的"基本操作"(包括加法,乘法,除法和平方根)被正确舍入.这意味着存在唯一的允许答案,并且它是所谓的"无限精确"操作结果的最接近的可表示浮点数.
在双精度中,数字具有53个精度的二进制数字,因此正确的答案是舍入到53位有效数字的确切答案.正如Rick Regan在答案中所表明的那样,这正是你得到的结果.
您的问题的答案是:
问题1:是否允许这么大的错误？
是的,但将此错误称为"巨大"是非常误导的.事实是,没有可以返回具有较小错误的双精度值.
问题2:这是否意味着,每个基本操作都应该有一个错误<2.220446e-16,64位双精度(机器epsilon)？
不是.这意味着每个基本操作都应根据当前的舍入模式四舍五入到(唯一的)最接近可表示的浮点数.这与说机器epsilon限制相对误差并不完全相同.
问题3:使用x86硬件和gcc + libc获得了哪些结果？
你做了同样的答案,因为sqrt在任何合理的平台上都是正确的.
在二进制中,任意精度答案的前58位是1011111111111111111111110101010101111111111111111011010001 ...
double值的53位有效数字是
10111111111111111111111101010101011111111111111110111
这意味着double值被正确舍入到53个有效位,并且在1/2 ULP内.(错误是"大"只是因为数字本身很大).