我的新iPhone运行Z3的速度比我的(相当贵的)英特尔台式机快

有趣的实验：我的新iPhone运行Z3的速度比我的(相当昂贵的)英特尔台式机还快！是时候开始在我的手机pic.twitter.com/9Faz9qNvAI上做我所有的正式方法研究了。

-James Bornholt(@sidereated)2018年10月31日。

关于苹果处理器设计团队取得的令人难以置信的进步，以及Mac电脑很快就会使用苹果自己的ARM处理器，我已经看到了一些讨论。这些报告通常会引用一些跨平台基准测试，比如Geekbench，以表明苹果的移动处理器至少和英特尔的笔记本电脑和台式机芯片一样快。但我一直对这些跨平台基准测试(就像其他测试一样)持怀疑态度--它们真的代表了我使用Mac电脑的那种工作负荷吗？

作为一名正式的方法研究人员，我经常运行的唯一真正的计算密集型工作是SMT解决方案，通常是Z3 SMT解决方案。在这一点上，我花了很多时间了解Z3的性能特征，而且它还有一些基准测试套件无法捕捉到的特性(Z3通常是单线程的)。我最近买了一台新的iPhone XS，配备了苹果最新的A12处理器。所以，在一段拖延的时间里，我决定将Z3交叉编译到iOS，看看是如何实现的。

交叉编译Z3被证明是非常简单的，只需要修改几行代码；我开源了代码，以便在您自己的iOS设备上运行Z3。为了进行基准测试，我从我最近关于分析符号求值的工作中引出了一些疑问，在每种情况下都提取了Rosette生成的SMT输出。

作为第一次测试，我将我的iPhone XS与我的一台台式机进行了比较，这台台式机使用的是英特尔酷睿i7-7700K，这是18个月前我们制造这台机器时英特尔卖得最好的消费类台式机芯片。我本以为英特尔芯片会在这里相当轻松地获胜，但事实并非如此：

在这个23秒的基准测试中，iPhone XS大约快了11%！这是我在推特上提到的结果，但Twitter没有留下太多细微差别，所以我在这里补充一些：

该基准测试位于SMT的QF_BV片段中，因此Z3使用位爆破和SAT求解来释放它。

如果基准测试循环运行10次，这个结果相当不错-iPhonecan可以维持这种性能，而且似乎不受热量限制。1也就是说，基准仍然相当短。

有几个人问我这是否归因于非决定论--也许是由于使用了随机数或其他原因，求解器在不同的平台上采用了不同的路径--但我使用Z3的冗长输出相当彻底地检查了一下，似乎不是这样的。

这两个系统都运行Z34.8.1，这是我使用Clang编译的，具有相同的优化设置。我也使用Z3的预构建二进制文件(使用GCC)在i7-7700K上进行了测试，但实际上速度较慢。

这怎么可能呢？i7-7700K是台式CPU；当运行单线程工作负载时，它的功耗约为45瓦，时钟频率为4.5 GHz。相比之下，iPhone没有拔出电源，很可能没有消耗10%的电量，并且运行在(我们认为)2 GHz范围内的某个地方。事实上，在基准测试之后，我查看了iPhone的电池使用报告，报告显示，尽管屏幕显示的时间更短，但Slake的能耗是Z3应用的4倍。

苹果没有公开足够的信息来了解Z3在iPhone上的表现，但幸运的是，英特尔为他们的台式机处理器提供了足够的信息。我花了一些时间使用VTune来查看在台式机上运行Z3时的瓶颈在哪里。正如Mate Soos观察到的那样，大部分SAT求解时间都花在传播上，这对缓存非常敏感。VTune对此表示同意，并表示Z3在迭代观看的文字时会花费大量时间等待内存。因此，这里性能的关键似乎是成为了。并且与7700K相比，在高速缓存未命中之后似乎具有更好的存储器等待时间。

为了测试这个诊断是否正确，我做了一个更广泛的实验，收集了我能拿到的所有苹果设备。我还选择了一个速度慢约10倍(即台式机上4分钟)的基准测试，以缓解人们对移动猝发性能的任何担忧。

以下是我收集的设备的结果，根据它们的发布日期绘制成图表，并相对于Apple A7，这是他们第一个64位定制CPU设计：

首先要注意的是，i7-7700K台式机处理器在这个不同的、更长的基准上击败了iPhone XS。但iPhone的竞争令人难以置信，介于7700K和它的前身i7-6700K之间，直到不到两年前，i7-6700K还是最快的消费类台式机处理器。

为了好玩，我还增加了英特尔酷睿M7-6Y75，这是我2016年MacBook的处理器。iPhone XS在运行Z3时比我的笔记本电脑快50%左右。

这里真正值得注意的是苹果的趋势：Z3基准测试与去年同期相比提高了30%。显然，我们不应该从这个愚蠢的基准测试中得出太多结论，但似乎只需要再重复一到两次这种趋势，苹果CPU就会对我的工作负载产生完全的意义。老实说，我没想到会这么近--现代智能手机架构太不可思议了！

感谢梅根·考恩(Meghan Cowan)、马克斯·威尔西(Max Willsey)和埃迪·严(Eddie Yan)帮助我追踪更多设备并进行实验。

麦克斯指出，苹果手机是防水的，所以我可以通过在冰浴中浸泡来检验这一理论，但我花了很多钱买了我的手机，他不会自愿把他的↩。

我打赌新的iPad Pro的A12X速度会更快，这要归功于平板电脑提供的更大的散热外壳。-↩