SMT Solver on iPhone

Why buy an expensive PC if your iPhone solves SMT faster? 3r3204.  
3r3204.  
The problem of the satisfiability of formulas in theories (satisfiability modulo theories, SMT) is the problem of solvability for logical formulas taking into account the theories underlying them. - 3r3179. Wikipedia 3r3186.
3r3204.  
3r3204.  
A few days ago, I'm tweeted : “A curious experiment: on the new iPhone, the Z3 prover runs faster than on my (fairly expensive) Intel desktop. It's time to transfer all the formal research methods to the phone. ” 3r3204.  
3r3204.  
fun experiment: my new iPhone runs Z3 faster than my (rather expensive) Intel desktop! 3r3204. 3r3204. pic.twitter.com/9Faz9qNvAI 3r3331. - James Bornholt (@siderealed) October 3? 201 3r3334.
3r3204.  
I read about the incredible progress that 3r3342 made. Apple
processor developers. , and that poppies will soon be transferred to Apple's own ARM processors . These reports usually refer to some cross-platform tests, such as 3r3346. Geekbench
to demonstrate that Apple’s mobile processors are not inferior to Intel’s mobile and desktop processors. But I was always a bit skeptical of these cross-platform tests (as well as 3-3348. Other 3-333215.) - do they really reflect the speed of the actual tasks for which I use my Mac? 3r3204.  
processor. A12 3r31515. from Apple. And somehow, having nothing to do, I decided to compile Z3 in iOS and see how fast the new phone works (or a hypothetical future Mac). 3r3204.  
3r3204.  
3r3142. The first test 3r3143. 3r3204.  
The cross-compilation of Z3 was surprisingly simple, you only need to change a few lines of code. I posted the source for 3r370. running Z3 on your own iOS device
. For the test, I took a few queries from my recent work on 3r372. profiling symbolic calculations
: for each case, the SMT output generated is extracted. Rosette . 3r3204.  
3r3204.  
In the first test, I compared the iPhone XS with one of the desktops running on the Intel Core i7-7700K - the best Intel chip for the consumer market at the time when I collected the car 18 months ago. Intel was supposed to win without any problems, but it turned out differently: 3r3204.  
3r3204.  
3r3154. SMT Solver on iPhone 3r3204.  
3r3204.  
In this 23-second test, the iPhone XS was about 11% faster! I tweeted this, but twitter does not leave much room for details, so I’ll put it here: 3r3204.  
3r3204.  
3r395.  
3r3114. This benchmark is a fragment of QF_BV 3r3–399. from SMT, so Z3 solves this part with the help of a broadcast (bit-blasting) and SAT-solver. 3r3115.  
3r3114. The result is quite stable, even if you run the cycle ten times: the iPhone supports this performance and does not seem to start to slow down due to overheating. 3r3208. 1 [/sup] VTune , to find performance bottlenecks when running Z3 on the desktop. As noted 3-333130. Mait Soos
, main time SAT solver spends on distribution which is 3r3133. very sensitive to the
cache. . VTune agrees and says that Z3 spends a lot of time waiting in memory when iterating through the observed literals. Thus, the key to performance seems to be cache size and memory latency. This effect may explain why the iPhone is so strong in this test: on the A12 3r3136 chip. Giant L2 cache with low latency
, and also seems to have better memory latency after a cache miss compared to 7700K. 3r3204.  
3r3204.  
3r3142. The rapid progress of Apple processors
3r3204.  
To confirm the results, I conducted a more extensive experiment, collecting all the Apple devices I could get. I also chose about 10 times longer benchmark (i.e. 4 minutes on the desktop) to remove concerns about the spikes in mobile CPU performance. 3r3204.  
3r3204.  
Here are the results for these devices (with their release dates) regarding the A? Apple's first 64-bit user processor: 3r3204.  
3r3204.  
3r3154. 3r3204.  
3r3204.  
Immediately it should be noted that the i7-7700K desktop processor is superior to the iPhone XS in this longer test. But the iPhone is incredibly competitive, showing results between the i7-7700K and its predecessor, the i7-6700K, which was the fastest consumer desktop processor a little less than two years ago. 3r3204.  
3r3204.  
For fun, I added another processor Core m7-6Y75 from my MacBook 2016. In the Z3 test, my phone is about 50% faster than a laptop. 3r3204.  
3r3204.  
The really remarkable thing here is the trend: a fairly consistent improvement of 30% per year for this benchmark Z3. Obviously, one should not draw far-reaching conclusions from one stupid test, but it seems that after a couple of iterations, Apple processors will be quite suitable for workloads. 3r3208. 2 [/sup] 3r3173.
. I honestly did not expect that we are already so close: the modern architecture of smartphones are incredible! 3r3204.  
3r3204.  
3r3179. Thanks Megan Cowan , 3r3198. Max Willsie
and 3r3184. Eddie Ian
for assistance in conducting tests on other devices. 3r3186. 3r3204.  
3r3204.  
3r3191. 3r3204.  
3r3194.
3r3208. 1 [/sup] . 3r3198. Max
I noticed that the iPhone is waterproof, so the theory can be tested by immersing it in an ice bath. But I paid a lot of money for the phone and do not want to voluntarily conduct such an experience. 3r3204.  
3r3204.  
+ 0 -

Add comment