编程与软件工程randomascii.wordpress.com
浮点数只有四十亿个,那就全部测试一遍
There are only four billion floats, so test them all (2014)
2014 — 2020,它一次次回到首页
黑点是上首页(≥ 50 分)的那次投稿,空心点是没冲上去的投稿,点越大分数越高。
导读
这篇博客讨论一个看似疯狂但可行的测试思路:32 位单精度浮点数总共只有约 40 亿个,因此与其抽样,不如把全部输入跑一遍。作者结合实例说明,对有限输入空间做穷举测试能发现随机测试容易漏掉的问题,并改变我们对“不可能全测”的直觉。
为什么经久不衰:因为它把“输入空间有限”和“算力足够”这两件事连起来,提醒读者重新评估穷举测试的可行性,今天在 GPU/SMT 时代仍很有启发。
HN 评论精选
用穷举搜索人为制造哈希碰撞,为碰撞慢路径建立可重复单元测试,说明有限空间穷举能省下长期调试成本。
很多年前我们做过一个用 URI 的 60 位截断哈希的东西。这个空间小得让人担心碰撞,但对数亿到十亿级规模又足够大,碰撞不太可能发生。因此我们可以为碰撞情况准备一条慢路径,只要慢路径正确就行。做单元测试时,我们至少需要制造一次碰撞,以便在真实用户撞上之前验证设计。我们有超过十亿 URI 的测试集,但据我们所知没有碰撞。于是我写了代码,用一个小整数种子生成无意义 URI(如 https://foo.example/123456789),然后启动一台有 8-12GB 内存的机器遍历每个种子,存下哈希和种子,直到在几 GB 内存后遇到碰撞,再输出两个碰撞种子对应的 URI。这样我们终于有了单元测试数据,证明即使两个不同 URI 哈希相同,系统也能正常工作。大概一天能搭好,之后每月估计能省下数小时调试奇怪碰撞 bug 的时间,因为单元测试会告诉我们碰撞是否漏过去了。
tialaramex查看英文原文
Many years ago now we built something that used a 60-bit truncated hash of URIs. So that's far too small to be comfortable that you won't run into collisions, but it's big enough that for modest sizes (hundreds of millions up to billions) a collision is unlikely. So you can have a slow path for the collision case, so long as that slow path is correct. For unit testing we needed at least one collision so we could see that everything behaves as designed before some real user hits one. We had test data sets with over a billion URIs in them, but none that (as far as we could tell) had a collision. So I just wrote code to mint nonsense URIs for our system based on a small integer seed (like https://foo.example/123456789), then span up a system with a bunch of RAM (maybe 8-12GB) to iterate through each seed, storing the hash and seed it was generated from, until it hit a collision after a few gigabytes of RAM, then it spat out the two URIs from the colliding seeds. Bingo, now we had data for unit testing to show that stuff works even in the unlikely case that two distinct URIs have the same hash. Probably a day's work to build that, and then I'd guess several hours every month saved debugging weird collision bugs because our unit tests would now tell us if we'd screwed up and collisions were slipping past.
GPU 算力已使一个月穷举 2^64 空间变得现实,穷举测试的边界继续外扩。
从那时起事情变得更快了。目标:64 位空间(2^64)。GPU 更灵活也更快。Vega64(几年前的产品)有 4096 个着色器,1.6 GHz,可以在不到一秒内搜完整个 32 位浮点(或整数)空间。1.6 GHz × 4096 shaders == 2^42.5 每秒。愿意穷举搜索的人相对有耐心,愿意等几个月。60 秒 × 60 分钟 × 24 小时 × 30 天 == 2^21.3。1.6 GHz × 4096 shaders × 60 秒 × 60 分钟 × 24 小时 × 30 天 约等于 2^63.8。我们做到了:一个月的 GPU 算力就足以穷举 64 位空间。我们大约三年前进入了一个世界:只要你愿意等一个月,暴力穷举 64 位空间是合理的。不愿等就用 2 块、4 块 GPU 或 DGX A100 集群。
dragontamer查看英文原文
Things have gotten even faster since then. * Target: 64-bit space (2^64). * GPUs are more flexible and faster. A Vega64 (a few years old now) has 4096 shaders ("CudaThreads") at 1.6 GHz. It can search the entire 32-bit floating point (or integer) space in less than a second. 1.6 GHz x 4096 shaders == 2^42.5 bitspace per second. * People exhaustively searching a space are relatively patient: and willing to wait months for the results. 60 seconds x 60 minutes x 24 hours x 30 days == 2^21.3 1.6 GHz x 4096 shaders x 60 seconds x 60 minutes x 24 hours x 30 days is roughly equal to 2^63.8. We've done it: a month of GPU effort is all you need to exhaustively search the 64-bit space ------- We've entered a world (~3 years ago), where it is reasonable to brute force the 64-bit space, so long as you're willing to wait about a month for the results. If you're not willing to wait a month, then use 2 GPUs, or 4 GPUs, or a cluster of GPUs like the DGX A100 (or multiple clusters).
对高维输入无法全测时,可用数学剪枝把穷举搜索压缩到可接受范围。
关于“把它们全测一遍”,我在那篇关于复数乘法误差界和最坏情况的论文里写道:[寻找最坏输入] 采用的方法是穷举搜索,在第二作者笔记本电脑上花几个小时搜索 IEEE 单精度输入,只用定理 1 的几个论证来剪枝。尽管 (2^32)^4 大到无法测试所有单精度输入四元组,但“剪枝”搜索能轻松覆盖和/或排除整个搜索空间。
cperciva查看英文原文
On the topic of "test them all", I wrote this in my paper about error bounds and worst cases for complex multiplication (http://www.daemonology.net/papers/complexmultiply.pdf): [For finding worst-case inputs] the approach taken was to perform an exhaustive search, taking several hours on the second author’s laptop, of IEEE single-precision inputs, using only a few arguments from Theorem 1 to prune the search. Even though (2^32)^4 was far too large for it to be tractable to test all 4-tuples of single-precision inputs, a "pruned" search was able to easily cover and/or exclude the entire search space.
SMT 求解器可符号化剪枝,把穷举思路扩展到 double 和多输入场景。
不幸的是,这不能很好地扩展到单个 32 位浮点数之外。好消息是,如果你的代码使用 double 或多输入,也许仍能用 Z3 这类支持浮点理论的 SMT 求解器做穷举测试。这类求解器在二进制层面符号化建模浮点运算,用高效剪枝搜索解决关于浮点精确行为的问题。我没亲自试过,不知道扩展性如何,但它肯定比遍历所有可能输入的循环更好。
tikhonj查看英文原文
Unfortunately, this doesn't scale well beyond a single 32-bit floating point number. The good news is that if your code works with doubles or multiple inputs, you might still be able to test it exhaustively using an SMT solver like Z3 which supports a "theory of floating point numbers"[1]. A solver like this symbolically models floating point operations at a binary level, letting it use an efficient pruning search to solve problems about the exact behavior of floating point numbers. I haven't tried it myself so I don't know quite how well it scales, but it should definitely work better than a loop across all possible inputs! [1]: https://pdfs.semanticscholar.org/db9f/2cc0bf18c4661f5629b088dfb8c8a2193506.pdf
历次讨论
同类还值得读
开源应用架构
The Architecture of Open Source Applications
《开源软件架构》(AOSA)是一本在线免费书,邀请知名开源项目的作者亲自剖析其内部设计,涵盖 SQLAlchemy、LLVM、Audacity、Apache、Bash 等系统。
编程与软件工程上首页 9 次 · 2011–2024aosabook.org编辑精选编程语言简史:简短、不完整且多半错误
A Brief, Incomplete, and Mostly Wrong History of Programming Languages
一篇以戏谑、故意不准确的方式回顾编程语言史的博客文章,用夸张轶事和讽刺定义串起 Lisp、C、C++、Java、JavaScript、PHP 等语言。
编程与软件工程上首页 8 次 · 2009–2021james-iry.blogspot.comSQLite 是如何测试的
How SQLite is tested
SQLite 官方文档页,系统介绍 SQLite 的测试体系:多种测试方法(TCL 测试、模糊测试、回归测试、静态分析等)和海量测试用例,展示了这个小型开源项目如何靠极致测试获得…
编程与软件工程上首页 8 次 · 2009–2025sqlite.org编辑精选高级编程语言(2009)
Advanced programming languages (2009)
Matt Might 的经典文章,按用途推荐“高级编程语言”:如果追求就业就选主流语言,如果追求表达力、学术研究或创业,则推荐 Haskell、OCaml、Scala 等函数式语…
编程与软件工程上首页 8 次 · 2009–2022matt.might.net我的 Forth 与栈机器经历
Yosefk - My history with Forth & stack machines
作者以亲身经历回顾了使用 Forth 语言和栈式机器的历程:既赞叹其简洁优雅、代码量小、可自举的优点,也坦率指出栈操作在实际编程中的痛苦,以及 Forth 社区文化中的问题。
编程与软件工程上首页 8 次 · 2010–2024yosefk.com编辑精选