12 ms·

SMT Solving on an iPhone (2018)

224 points by marcobambini 6y ago

1f60c 6y ago
(2018)
- NietTim 6y ago
  Makes me wonder what the article would look like today, or next month when the new generation iPhone hardware comes out. I guess benchmarks like geekbench can give us a general picture
  - 1f60c 6y ago
    The author's code is open source[0] if anyone wants to take a look. [0]: https://github.com/jamesbornholt/z3-ios https://github.com/jamesbornholt/z3-ios
PaulHoule 6y ago
Smt solvers and other 'old a.i.' workloads depend mainly on memory performance under unpredictably branching workloads, which the iPhone chips seem to be strong in. Compare that to 'new a.i.' workloads that eliminate branch misprediction almost entirely.
- egsmi 6y ago
  New AI workloads also run on dedicated blocks. I.e. https://en.m.wikipedia.org/wiki/Apple_A11#Neural_Engine https://en.m.wikipedia.org/wiki/Apple_A11#Neural_Engine
- hinkley 6y ago
  I have a hard time putting SAT, SMT, and at least some linear algebra algorithms into the AI category. They are all logic, just of a sort that’s far more mind-numbing than our usual data processing workflows. I know the AI people get grumpy about all of the problem spaces that have been harvested or “stolen” and called conventional code, but in this case I’m not so sure that’s accurate. It feels more like a bunch of people who wanted to use advanced math and logic jumped on the AI gravy train while it was going past, and then hopped off again when they had their fill.
  - pirocks 6y ago
    I don't know if you know but 20 odd years ago what was called AI at universities was SMT/prolog etc. People where doing stuff like expressing common sense facts in logic and using programs to derive more common sense.
  - PaulHoule 6y ago
    Academic computer scientists are like that. Research priorities in the U.S. driven by what the Department of Defense will pay for. DoD had some bad experiences with FPGA and now they want to build ASIC supercompilers. One thing I find funny is that the production rules engines that we have today (Drools, Clara) are dramatically better than the ones we had when production rules were popular (e.g. CLIPS, eMYCIN) Today we have improved RETE algorithms, hash indices, etc. Production rules only seem to survive in a few niches, one of which is inside banks, another is complex event processing.
  - kaik 6y ago
    SMT, SAT, etc are absolutely AI. In fact, Machine Learning is just another field inside AI (albeit a famous and successful one). As someone that got his PhD doing his research in "classical" AI, it's surprising that nowadays most people think that AI is just machine learning.
    - zero_k 6y ago
      +1. I am always surprised that they used to do (and of course still must do) proper full-on formal verification of e.g. train track scheduling systems, so train accidents, and consequently 100s of deaths don't just happen because "sorry for the bug, ver 1.2 fixes it" -- but people are happy to sit into a Tesla going at 120km/h and allow a well-tested, but not formally verified deep learning system to make decisions. BTW, I know it's not formally verified, because formally verifying deep learning systems is a currently very much unsolved problem for anything but toy examples.
    - smabie 6y ago
      Is linear regression AI? How about logistic regression? Many people would consider the latter to be ML/AI while the former statistics. Ultimately, I think the distinction is pretty meaningless.
- fooker 6y ago
  > Compare that to 'new a.i.' workloads that eliminate branch misprediction almost entirely. Wait a few more years, and your statement will be wrong. :) So far, ML/DL workloads work with traditional matrices which are hitting a scaling wall. The natural next step is sparse matrices, where branching comes back with a vengeance.
wslh 6y ago
I am always amazed how the user experience of an iPad mini (~USD 400) is much better than a top end 13" Windows based notebook (~USD 2700). I know I am comparing apples with oranges in term of running processes and multitasking but the foreground app experience is much better.
- chefandy 6y ago
  Comparing apples to windows?
  - jagged-chisel 6y ago
    ios to windows; apple to microsoft;
    - chefandy 6y ago
      I understand the relationships— it was merely a play on words.
      - jagged-chisel 6y ago
        Correction was not my intent. Apologies. I didn't really think through communicating my intent when I wrote the comment. I was actually hoping to elicit someone else chiming in with a clever comparison. Alas...
        robertlagrant 6y ago
        Dust to dust?
- epistasis 6y ago
  My uninformed hunch: There's likely a lot to be said for 1) requiring all apps to use a single modern GUI toolkit, and 2) optimizing that toolkit for the use case of touch. Rather than having a single codebase that's supposed to solve all use cases in addition to 30 years of baggage.
mcny 6y ago
> So, in a fit of procrastination, I decided to cross-compile Z3 to iOS, and see just how fast my new phone (or hypothetical future Mac) is. > I bet the new iPad Pro’s A12X is even faster thanks to the larger thermal envelope a tablet affords. iirc Apple intends to complete transition to Apple Silicon within three years (and they often tend to be conservative with their estimates) so I'd imagine the 2023 or 2024 mac pro will be interesting given (I'd assume) it won't have the thermal constraints an iPhone has. Thoughts?
- matt2000 6y ago
  They are planning to complete the transition in 2 years: https://www.apple.com/newsroom/2020/06/apple-announces-mac-transition-to-apple-silicon/ https://www.apple.com/newsroom/2020/06/apple-announces-mac-t... Makes your question even more interesting though, what will a Mac Pro look like running Apple silicon inside 2 years from now?
tyingq 6y ago
Interesting. Is it possible that this particular workload takes a big hit due to the Spectre/Meltdown mitigations?
- corty 6y ago
  Yes. Mitigations drastically increase the cost of branch mispredictions, which has always been expensive on x86 and has gotten even worse. See also the sister comment. Cache misses have the same problem.
  - riscy 6y ago
    I highly doubt the author compiled Z3 with those mitigations enabled, because they are opt-in compiler options. Perhaps if the program makes frequent system calls then the kernel’s mitigations would introduce overhead.
    - tyingq 6y ago
      My impression is that the mitigations that would hit hardest are Intel microcode patches that load at boot time, and it may not have been obvious to revert those. Or perhaps not wise to, depending on the production environment.
      - gowld 6y ago
        Why? If performance matters, don't browse Reddit on your lab machine. I don't run antivirus on my microwave oven. There's no need.
        corty 6y ago
        Support for most hardware depends on applying latest patches for HW and SW. Only if you explicitly bought as HPC or Lab environment with the appropriate contract specifying performance you might get around that.
        mschuster91 6y ago
panpanna 6y ago
Note that this sort of software can be extremely sensitive to cache arrangement. Not only actual performance but also small details such as data arrangement, line size, replacement model and coherency model. Source: I worked on performance improvement for a related piece of software.
- sitkack 6y ago
  https://emeryberger.com/research/stabilizer/ https://emeryberger.com/research/stabilizer/
api 6y ago
When Apple releases ARM Macs I think we are all going to be really impressed. Take these phone chips, beef them up a bit with more cores and maybe more cache, clock them a bit higher, and give them better cooling so they can sustain higher speeds. If it goes how I think it will go, X86 is done. People will really start wanting ARM on servers.
- rowanG077 6y ago
  Unfortunately there are no other ARM designs that can compete with X86. And Apple CPUs will only run in Apple Hardware executing Apple Software.
  - otterley 6y ago
    Have you looked at AWS' new Graviton2 instances? They compete handily with x86-64 instance performance, and are cheaper to boot. https://www.anandtech.com/show/15578/cloud-clash-amazon-graviton2-arm-against-intel-and-amd https://www.anandtech.com/show/15578/cloud-clash-amazon-grav...
    - rowanG077 6y ago
      Graviton can't compete with x86. It can only compete on AWS on server workloads. I can't buy a Graviton workstation/server. There are no Graviton laptops.
- corty 6y ago
  People have been wanting ARM servers since the first ones were announced. But there are two big problems. First, there is no unified boot- and device initialisation-standard. So you cannot just put in a bootable USB stick and expect it to work. Second, you can not reliably order any hardware, just very small series just above prototype stages...
  - my123 6y ago
    > First, there is no unified boot- and device initialisation-standard. There is. UEFI + ACPI. > So you cannot just put in a bootable USB stick and expect it to work. That's how it works today for Arm servers. Windows on Arm platforms also use UEFI + ACPI, and ship with the bootloader unlocked.
haunter 6y ago
I really want to see the Apple Silicon under some real world load running a current gen AAA video game in 4K ultra settings while streaming with OBS, playing music, and having Chrome open with 100+ tabs. Because that's what my current PC does for example so I'm really curious about everything (performance, temps etc.) To some extent it's just hard to believe that the iPhone CPU is better in every thing compared to the current gen top of the line Intel and AMD desktop CPUs.
- stinos 6y ago
  Chrome open with 100+ tabs Bit off topic, but I don't use Chrome so I wonder: do you mean 100+ visited i.e. active tabs, or are you counting all of them, or doesn't Chrome have a distinction between those cases like e.g. Firefox does (i.e. when starting the application it doesn't actually load all tabs until you activate them - so once opened perfomance wise it doesn't matter a lot if it's 10+ or 100+ tabs)?
  - snazz 6y ago
    I'm pretty sure that Chrome does have a distinction between loaded and unloaded tabs (suspended tabs, maybe?), but it definitely manages tabs in a different way from Firefox and Safari. Both Chrome and Firefox can trivially handle 100 suspended tabs on any machine; both would struggle with that many active tabs if the machine didn't have enough RAM to fit them all. This metric really only has to do with the amount of memory that a machine has, in my experience.
  - neurostimulant 6y ago
    Chrome will suspend/discard inactive tabs when when the memory pressure is high, and reload it back when you activate the tab again, so you probably can open 1000 tabs and leave it alone without much impact (this feature is exposed as an api and can be triggered by extensions: https://developer.chrome.com/extensions/tabs#method-discard https://developer.chrome.com/extensions/tabs#method-discard ). But when you activate them all I imagine it would consume too much system resource.
- deleted 6y ago
  [deleted]
aminozuur 6y ago
Apple Silicon has been pretty impressive as it outperforms many laptops and desktops in benchmarks. This guy even used the A12 chip from 2018. The A13 is even faster and ships on all iPhone 11's and even the $399 iPhone SE 2nd gen. I am eager to see how Apple Silicon will do in the upcoming MacBooks.
- Mandatum 6y ago
  It's going to be awesome to see chips that actually utilize the board space specifically for the functions the end-device is used for. I get general-purpose boards are the defacto to suit the masses and it's favoured by OEM's because they're easier to ship, but I think we're past the point we need that, adoption is no longer a problem. I signed up for the Apple DTK, hoping they approve more people abroad..
pinewurst 6y ago
>Indeed, after benchmarking I checked the iPhone’s battery usage report, which said Slack had used 4 times more energy >than the Z3 app despite less time on screen.
samfisher83 6y ago
The a12 has about 3-4 times the number of transistors as i7-7700k. I know there are a lot of other on than the SOC core than the cpu for a12, but they still have a pretty large transistor budget. It was made with 7nm transistors vs 14nm that intel was using at the time when 7700k came out. Apple did a good job designing the chips, but TSMC is a huge part of why these chips are so good. For the longest time Intel manufacturing process was way ahead of anyone else which reflected in their performance. If I give you way more transistors I can probably make a better chip. If I give you more cache, decoders, execution units etc. I can make a faster chip. Also if you used all cores for sustained amount of time the intel would win out just because it can handle all that heat.
- nknealk 6y ago
  I think the dimension you’re missing is that the a12 also consumes significantly less power. While we don’t know exact numbers, the author speculates it draws about a tenth of the power as the i7.
  - samfisher83 6y ago
    Because its running at a much higher clock rate and its a much older process. The apple isn't running 4 big cores either.
  - zamadatix 6y ago
    It's the cache that makes this fast, not the higher clock higher voltage cores on an older process. Not that x86 particularly in 2018 is the pinnacle of perf per watt but the power dimension is non linear on some of these variables and this particular benchmark doesn't happen to gain much from it.
m3kw9 6y ago
Could be Apple arm chips have certain instructions that are more optimized
ashleyn 6y ago
Are smartphone architectures really this amazing, or is Intel just dropping the ball so hard that they're getting lapped by mobile hardware?
- danaris 6y ago
  From what I've seen, it's a combination of Intel dropping the ball hard, and Apple aggressively pushing to make better and better chips for the iPhone and iPad—and, now, for their computers. This isn't something that you're going to see in "mobile hardware" more generally, I don't think, at least not unless Intel continues to be unable to find its balls for a few more years.
- bgorman 6y ago
  The smartphone architecture is smart and well executed, but it is nothing revolutionary. The key is definitely that Intel has lost its manufacturing lead, which is letting other chip companies release competitive CPU architectures. Moore's law ending has leveled the playing field for ASICs.
- PaulHoule 6y ago
  Intel has focused most on data center performance, where you are operating at scale and frequently using entirely different algorithms than people usually use on a PC or Phone. For instance https://en.wikipedia.org/wiki/Column-oriented_DBMS https://en.wikipedia.org/wiki/Column-oriented_DBMS dominates the competition for ad-hoc analytics under "enterprise" conditions. There the point is to maximize the use of memory bandwidth and never stall the pipelines, to turn a commercial data processing job into something that looks like HPC to the memory bus. (Actually columnar organization improves performance reliably for small data; video game programmers in the 1980s knew that it was better to put the x coordinates of all the spaceships together, then put the y coordinates together, then put the sprite id's together, ...) Most muggles though go with the row-orientation that comes with structs, classes, record types, and don't care. Pythoners know their language is slow but they know enough to use 'pandas' which is an object-oriented interface to an in-memory column store. Intel has sold it's performance on the basis of what a sophisticated organization could get out of complex programming. For instance, the AVX-512 instructions can nearly double performance for some workloads. If you are a cloud provider that will rack 1000s of identical machines that run the same software, it can be a big win. The average PC user runs software that has to run on a wide range of hardware and may be supported by lower-tier organizations. They will rightly privilege having a trouble-free product and low support costs vs giving every user the highest performance possible.)
zero_k 6y ago
Hah, funny to see my blog referenced. Yeah, cache misses are a huge part of SAT solving (modern solvers have prefetch code specifically for this loop, some seemingly following the code I wrote). And SAT solving is about 95+% of SMT solving. So, yeah, cache is where it's at. I once had an old, but "enthusiast" i7 that had a 3-lane mem setup, and "upgraded" to a consumer dual-lane i7 that was 2-3 gens ahead. It had the same performance(!) for SAT solving. Was pretty eye-opening.
- HALtheWise 6y ago
  At the end of the day, cache miss latency should be bounded by the speed of light and the distance to memory. It's entirely unsurprising to me that by putting main memory on the same board as the CPU, as well as the optimizations that come from allowing a custom communication protocol between them, better performance is possible. I wonder what a desktop machine designed for cache and memory latency would look like.
  - janekm 6y ago
    Not just same board... the RAM is literally stacked right on top of the SoC. It’ll be interesting to see what Apple will do on desktop... maybe some stacked RAM plus more on the board? Having full control over memory / bus architecture (and the OS) creates lots of opportunities for optimization.
  - vvanders 6y ago
    It's SRAM vs DRAM not the speed of light. Go take a look a DRAM CAS values as clock speeds have increased. The ns/fetch has stayed pretty static(~10ns) since DDR first showed up. There's been slight improvements but nothing like the order of magnitudes you seen in other areas. If you want to pay the power and cost of SRAM it can be done but it doesn't usually pencil out beyond what you see in caches today.
- josalhor 6y ago
  Has there been a study of the bottleneck of the performance of modern sat solvers? Some modern x86 CPUs have enormous cache sizes.
amelius 6y ago
Beware: Apple devices are not general purpose computers. Whether you can use them as such may be subject to change.
jcims 6y ago
Not particularly apropos to the thrust of the article, but I want to apply SMT to some tricky infosec use cases. Is there a good place to start for someone without an academic background in math/logic/etc?
- mhh__ 6y ago
  The chapter of Norvig on it may suffice as a self contained introduction. There is a book called SMT by Example (IIRC) which is good.
  - jcims 6y ago
    Will definitely check out Norvig. Not sure if this is what you had in mind but the linked PDF appears to be a treasure trove, thank you!! https://news.ycombinator.com/item?id=19075599 https://news.ycombinator.com/item?id=19075599
    - mhh__ 6y ago
      Yep. Knuth also has a chapter on it.
- panpanna 6y ago
  I suggest you start with this paper: "SMT Solvers in Software Security", Julien Vanegue, Sean Heelan, Rolf Rolles https://www.usenix.org/system/files/conference/woot12/woot12-final26.pdf https://www.usenix.org/system/files/conference/woot12/woot12...
  - jcims 6y ago
    Looks perfect, thank you!!!
derefr 6y ago
> Both systems ran Z3 4.8.1, compiled by me using Clang with the same optimization settings. Hypothesis: LLVM's AArch64 backend has had more work put into it (by Apple, at least) than LLVM's x86_64 backend has, specifically for "finishing one-off tasks quickly" (as opposed to "achieving high throughput on long-running tasks.") To me, this would make sense—until recently, AArch64 devices were mostly always-mobile, and so needed to be optimized for performing compute-intensive workloads on battery, and so have had more thought into the efficiency of their single-threaded burst performance (the whole "race to sleep" thing.) I'd expect, for example, AArch64-optimized code-gen to favor low-code-size serial loops over large-code-size SIMD vector ops, ala GCC -Os, in order to both 1. keep the vector units powered down, and 2. keep cache-line contention lower and thereby keep now-unneeded DMA channels powered down; both keeping the chip further from the TDP ceiling; and thus keeping the rest of the core that is powered on able to burst-clock longer. In such a setup, the simple serial-processing loop may potentially outperform the SIMD ops. (Presuming the loop has a variable number of executions that may be long or short, and is itself run frequently.) x86_64 devices, meanwhile, generally are only expected to perform compute-intensive tasks while connected to power, and so the optimizations contributed to compilers like LLVM that specifically impact x86_64, are likely more from the HPC and OLTP crowds, who favor squeezing out continuous aggregate throughput, at the expense of per-task time-to-completion (i.e. holding onto Turbo Boost-like features at maximum duty cycle, to increase mean throughput, even as the overheat conditions and license-switching overhead lower modal task performance.)
- my123 6y ago
  The LLVM x86_64 backend just gets as much work, and HPC is just one of the reasons. The NVIDIA PGI compilers for example use LLVM as a code generation backend, and that's one commercial option.
- tedunangst 6y ago
  This seems like a trivially testable hypotheses. Compile the code and look at the instructions generated. No need for elaborate speculation.
nickysielicki 6y ago
On the topic of the portability of Z3, does anyone know why this example runs fine on native amd64 but fails to solve when built with emscripten/wasm? https://github.com/sielicki/z3wasm https://github.com/sielicki/z3wasm Do a build by running, “mkdir bld && cd bld && emcmake cmake ../ -GNinja && emmake ninja”
nromiun 6y ago
For anyone trying to reproduce it in an Android phone you don't need to compile anything. Just "apt install z3" in Termux. It will probably be pretty slow but it will work.
- panpanna 6y ago
  Z3 is not available on termux (I am pretty sure it has been before). Back to the issue at hand. It is possible z3 is faster on arm64 due to the aarch64 bitfield instructions, but I find that unlikely.
  - nromiun 6y ago
    It was recently merged but it is available. https://github.com/termux/termux-packages/tree/master/packages/z3 https://github.com/termux/termux-packages/tree/master/packag...
    - panpanna 6y ago
      Sounds it, thanks. Had to update the yermux app first to see it. Yes, z3 performs slightly betteron aarch64. But performance seems to be mostly cache dependent. Also, z3 is threades which would favor Apple with their fewer but faster cores compare to others with more but weaker cores.
      - panpanna 6y ago
        Hmmm... I think my autocorrect had a meltdown. Hopefully people can figure it out anyway.
vbezhenar 6y ago
It's very fun suggestion to put an iPhone in the cold water. Imagine cluster of iPhones working under-water for math problems :)
dang 6y ago
Discussed at the time: https://news.ycombinator.com/item?id=18383851 https://news.ycombinator.com/item?id=18383851

224 points by marcobambini 6y ago

1f60c 6y ago

(2018)

NietTim 6y ago
Makes me wonder what the article would look like today, or next month when the new generation iPhone hardware comes out. I guess benchmarks like geekbench can give us a general picture
- 1f60c 6y ago
  The author's code is open source[0] if anyone wants to take a look. [0]: https://github.com/jamesbornholt/z3-ios https://github.com/jamesbornholt/z3-ios

PaulHoule 6y ago

Smt solvers and other 'old a.i.' workloads depend mainly on memory performance under unpredictably branching workloads, which the iPhone chips seem to be strong in. Compare that to 'new a.i.' workloads that eliminate branch misprediction almost entirely.

egsmi 6y ago
New AI workloads also run on dedicated blocks. I.e. https://en.m.wikipedia.org/wiki/Apple_A11#Neural_Engine https://en.m.wikipedia.org/wiki/Apple_A11#Neural_Engine
hinkley 6y ago
I have a hard time putting SAT, SMT, and at least some linear algebra algorithms into the AI category. They are all logic, just of a sort that’s far more mind-numbing than our usual data processing workflows. I know the AI people get grumpy about all of the problem spaces that have been harvested or “stolen” and called conventional code, but in this case I’m not so sure that’s accurate. It feels more like a bunch of people who wanted to use advanced math and logic jumped on the AI gravy train while it was going past, and then hopped off again when they had their fill.
- pirocks 6y ago
  I don't know if you know but 20 odd years ago what was called AI at universities was SMT/prolog etc. People where doing stuff like expressing common sense facts in logic and using programs to derive more common sense.
- PaulHoule 6y ago
  Academic computer scientists are like that. Research priorities in the U.S. driven by what the Department of Defense will pay for. DoD had some bad experiences with FPGA and now they want to build ASIC supercompilers. One thing I find funny is that the production rules engines that we have today (Drools, Clara) are dramatically better than the ones we had when production rules were popular (e.g. CLIPS, eMYCIN) Today we have improved RETE algorithms, hash indices, etc. Production rules only seem to survive in a few niches, one of which is inside banks, another is complex event processing.
- kaik 6y ago
  SMT, SAT, etc are absolutely AI. In fact, Machine Learning is just another field inside AI (albeit a famous and successful one). As someone that got his PhD doing his research in "classical" AI, it's surprising that nowadays most people think that AI is just machine learning.
  - zero_k 6y ago
    +1. I am always surprised that they used to do (and of course still must do) proper full-on formal verification of e.g. train track scheduling systems, so train accidents, and consequently 100s of deaths don't just happen because "sorry for the bug, ver 1.2 fixes it" -- but people are happy to sit into a Tesla going at 120km/h and allow a well-tested, but not formally verified deep learning system to make decisions. BTW, I know it's not formally verified, because formally verifying deep learning systems is a currently very much unsolved problem for anything but toy examples.
  - smabie 6y ago
    Is linear regression AI? How about logistic regression? Many people would consider the latter to be ML/AI while the former statistics. Ultimately, I think the distinction is pretty meaningless.
fooker 6y ago
> Compare that to 'new a.i.' workloads that eliminate branch misprediction almost entirely. Wait a few more years, and your statement will be wrong. :) So far, ML/DL workloads work with traditional matrices which are hitting a scaling wall. The natural next step is sparse matrices, where branching comes back with a vengeance.

wslh 6y ago

I am always amazed how the user experience of an iPad mini (~USD 400) is much better than a top end 13" Windows based notebook (~USD 2700). I know I am comparing apples with oranges in term of running processes and multitasking but the foreground app experience is much better.

chefandy 6y ago
Comparing apples to windows?
- jagged-chisel 6y ago
  ios to windows; apple to microsoft;
  - chefandy 6y ago
    I understand the relationships— it was merely a play on words.
    - jagged-chisel 6y ago
      Correction was not my intent. Apologies. I didn't really think through communicating my intent when I wrote the comment. I was actually hoping to elicit someone else chiming in with a clever comparison. Alas...
      - robertlagrant 6y ago
        Dust to dust?
epistasis 6y ago
My uninformed hunch: There's likely a lot to be said for 1) requiring all apps to use a single modern GUI toolkit, and 2) optimizing that toolkit for the use case of touch. Rather than having a single codebase that's supposed to solve all use cases in addition to 30 years of baggage.

mcny 6y ago

> So, in a fit of procrastination, I decided to cross-compile Z3 to iOS, and see just how fast my new phone (or hypothetical future Mac) is. > I bet the new iPad Pro’s A12X is even faster thanks to the larger thermal envelope a tablet affords. iirc Apple intends to complete transition to Apple Silicon within three years (and they often tend to be conservative with their estimates) so I'd imagine the 2023 or 2024 mac pro will be interesting given (I'd assume) it won't have the thermal constraints an iPhone has. Thoughts?

matt2000 6y ago
They are planning to complete the transition in 2 years: https://www.apple.com/newsroom/2020/06/apple-announces-mac-transition-to-apple-silicon/ https://www.apple.com/newsroom/2020/06/apple-announces-mac-t... Makes your question even more interesting though, what will a Mac Pro look like running Apple silicon inside 2 years from now?

tyingq 6y ago

Interesting. Is it possible that this particular workload takes a big hit due to the Spectre/Meltdown mitigations?

corty 6y ago
Yes. Mitigations drastically increase the cost of branch mispredictions, which has always been expensive on x86 and has gotten even worse. See also the sister comment. Cache misses have the same problem.
- riscy 6y ago
  I highly doubt the author compiled Z3 with those mitigations enabled, because they are opt-in compiler options. Perhaps if the program makes frequent system calls then the kernel’s mitigations would introduce overhead.
  - tyingq 6y ago
    My impression is that the mitigations that would hit hardest are Intel microcode patches that load at boot time, and it may not have been obvious to revert those. Or perhaps not wise to, depending on the production environment.
    - gowld 6y ago
      Why? If performance matters, don't browse Reddit on your lab machine. I don't run antivirus on my microwave oven. There's no need.
      - corty 6y ago
        Support for most hardware depends on applying latest patches for HW and SW. Only if you explicitly bought as HPC or Lab environment with the appropriate contract specifying performance you might get around that.
      - mschuster91 6y ago

panpanna 6y ago

Note that this sort of software can be extremely sensitive to cache arrangement. Not only actual performance but also small details such as data arrangement, line size, replacement model and coherency model. Source: I worked on performance improvement for a related piece of software.

sitkack 6y ago
https://emeryberger.com/research/stabilizer/ https://emeryberger.com/research/stabilizer/

api 6y ago

When Apple releases ARM Macs I think we are all going to be really impressed. Take these phone chips, beef them up a bit with more cores and maybe more cache, clock them a bit higher, and give them better cooling so they can sustain higher speeds. If it goes how I think it will go, X86 is done. People will really start wanting ARM on servers.

rowanG077 6y ago
Unfortunately there are no other ARM designs that can compete with X86. And Apple CPUs will only run in Apple Hardware executing Apple Software.
- otterley 6y ago
  Have you looked at AWS' new Graviton2 instances? They compete handily with x86-64 instance performance, and are cheaper to boot. https://www.anandtech.com/show/15578/cloud-clash-amazon-graviton2-arm-against-intel-and-amd https://www.anandtech.com/show/15578/cloud-clash-amazon-grav...
  - rowanG077 6y ago
    Graviton can't compete with x86. It can only compete on AWS on server workloads. I can't buy a Graviton workstation/server. There are no Graviton laptops.
corty 6y ago
People have been wanting ARM servers since the first ones were announced. But there are two big problems. First, there is no unified boot- and device initialisation-standard. So you cannot just put in a bootable USB stick and expect it to work. Second, you can not reliably order any hardware, just very small series just above prototype stages...
- my123 6y ago
  > First, there is no unified boot- and device initialisation-standard. There is. UEFI + ACPI. > So you cannot just put in a bootable USB stick and expect it to work. That's how it works today for Arm servers. Windows on Arm platforms also use UEFI + ACPI, and ship with the bootloader unlocked.

haunter 6y ago

I really want to see the Apple Silicon under some real world load running a current gen AAA video game in 4K ultra settings while streaming with OBS, playing music, and having Chrome open with 100+ tabs. Because that's what my current PC does for example so I'm really curious about everything (performance, temps etc.) To some extent it's just hard to believe that the iPhone CPU is better in every thing compared to the current gen top of the line Intel and AMD desktop CPUs.

stinos 6y ago
Chrome open with 100+ tabs Bit off topic, but I don't use Chrome so I wonder: do you mean 100+ visited i.e. active tabs, or are you counting all of them, or doesn't Chrome have a distinction between those cases like e.g. Firefox does (i.e. when starting the application it doesn't actually load all tabs until you activate them - so once opened perfomance wise it doesn't matter a lot if it's 10+ or 100+ tabs)?
- snazz 6y ago
  I'm pretty sure that Chrome does have a distinction between loaded and unloaded tabs (suspended tabs, maybe?), but it definitely manages tabs in a different way from Firefox and Safari. Both Chrome and Firefox can trivially handle 100 suspended tabs on any machine; both would struggle with that many active tabs if the machine didn't have enough RAM to fit them all. This metric really only has to do with the amount of memory that a machine has, in my experience.
- neurostimulant 6y ago
  Chrome will suspend/discard inactive tabs when when the memory pressure is high, and reload it back when you activate the tab again, so you probably can open 1000 tabs and leave it alone without much impact (this feature is exposed as an api and can be triggered by extensions: https://developer.chrome.com/extensions/tabs#method-discard https://developer.chrome.com/extensions/tabs#method-discard ). But when you activate them all I imagine it would consume too much system resource.
deleted 6y ago
[deleted]

aminozuur 6y ago

Apple Silicon has been pretty impressive as it outperforms many laptops and desktops in benchmarks. This guy even used the A12 chip from 2018. The A13 is even faster and ships on all iPhone 11's and even the $399 iPhone SE 2nd gen. I am eager to see how Apple Silicon will do in the upcoming MacBooks.

Mandatum 6y ago
It's going to be awesome to see chips that actually utilize the board space specifically for the functions the end-device is used for. I get general-purpose boards are the defacto to suit the masses and it's favoured by OEM's because they're easier to ship, but I think we're past the point we need that, adoption is no longer a problem. I signed up for the Apple DTK, hoping they approve more people abroad..

pinewurst 6y ago

>Indeed, after benchmarking I checked the iPhone’s battery usage report, which said Slack had used 4 times more energy >than the Z3 app despite less time on screen.

samfisher83 6y ago

The a12 has about 3-4 times the number of transistors as i7-7700k. I know there are a lot of other on than the SOC core than the cpu for a12, but they still have a pretty large transistor budget. It was made with 7nm transistors vs 14nm that intel was using at the time when 7700k came out. Apple did a good job designing the chips, but TSMC is a huge part of why these chips are so good. For the longest time Intel manufacturing process was way ahead of anyone else which reflected in their performance. If I give you way more transistors I can probably make a better chip. If I give you more cache, decoders, execution units etc. I can make a faster chip. Also if you used all cores for sustained amount of time the intel would win out just because it can handle all that heat.

nknealk 6y ago
I think the dimension you’re missing is that the a12 also consumes significantly less power. While we don’t know exact numbers, the author speculates it draws about a tenth of the power as the i7.
- samfisher83 6y ago
  Because its running at a much higher clock rate and its a much older process. The apple isn't running 4 big cores either.
- zamadatix 6y ago
  It's the cache that makes this fast, not the higher clock higher voltage cores on an older process. Not that x86 particularly in 2018 is the pinnacle of perf per watt but the power dimension is non linear on some of these variables and this particular benchmark doesn't happen to gain much from it.

m3kw9 6y ago

Could be Apple arm chips have certain instructions that are more optimized

ashleyn 6y ago

Are smartphone architectures really this amazing, or is Intel just dropping the ball so hard that they're getting lapped by mobile hardware?

danaris 6y ago
From what I've seen, it's a combination of Intel dropping the ball hard, and Apple aggressively pushing to make better and better chips for the iPhone and iPad—and, now, for their computers. This isn't something that you're going to see in "mobile hardware" more generally, I don't think, at least not unless Intel continues to be unable to find its balls for a few more years.
bgorman 6y ago
The smartphone architecture is smart and well executed, but it is nothing revolutionary. The key is definitely that Intel has lost its manufacturing lead, which is letting other chip companies release competitive CPU architectures. Moore's law ending has leveled the playing field for ASICs.
PaulHoule 6y ago
Intel has focused most on data center performance, where you are operating at scale and frequently using entirely different algorithms than people usually use on a PC or Phone. For instance https://en.wikipedia.org/wiki/Column-oriented_DBMS https://en.wikipedia.org/wiki/Column-oriented_DBMS dominates the competition for ad-hoc analytics under "enterprise" conditions. There the point is to maximize the use of memory bandwidth and never stall the pipelines, to turn a commercial data processing job into something that looks like HPC to the memory bus. (Actually columnar organization improves performance reliably for small data; video game programmers in the 1980s knew that it was better to put the x coordinates of all the spaceships together, then put the y coordinates together, then put the sprite id's together, ...) Most muggles though go with the row-orientation that comes with structs, classes, record types, and don't care. Pythoners know their language is slow but they know enough to use 'pandas' which is an object-oriented interface to an in-memory column store. Intel has sold it's performance on the basis of what a sophisticated organization could get out of complex programming. For instance, the AVX-512 instructions can nearly double performance for some workloads. If you are a cloud provider that will rack 1000s of identical machines that run the same software, it can be a big win. The average PC user runs software that has to run on a wide range of hardware and may be supported by lower-tier organizations. They will rightly privilege having a trouble-free product and low support costs vs giving every user the highest performance possible.)

zero_k 6y ago

Hah, funny to see my blog referenced. Yeah, cache misses are a huge part of SAT solving (modern solvers have prefetch code specifically for this loop, some seemingly following the code I wrote). And SAT solving is about 95+% of SMT solving. So, yeah, cache is where it's at. I once had an old, but "enthusiast" i7 that had a 3-lane mem setup, and "upgraded" to a consumer dual-lane i7 that was 2-3 gens ahead. It had the same performance(!) for SAT solving. Was pretty eye-opening.

HALtheWise 6y ago
At the end of the day, cache miss latency should be bounded by the speed of light and the distance to memory. It's entirely unsurprising to me that by putting main memory on the same board as the CPU, as well as the optimizations that come from allowing a custom communication protocol between them, better performance is possible. I wonder what a desktop machine designed for cache and memory latency would look like.
- janekm 6y ago
  Not just same board... the RAM is literally stacked right on top of the SoC. It’ll be interesting to see what Apple will do on desktop... maybe some stacked RAM plus more on the board? Having full control over memory / bus architecture (and the OS) creates lots of opportunities for optimization.
- vvanders 6y ago
  It's SRAM vs DRAM not the speed of light. Go take a look a DRAM CAS values as clock speeds have increased. The ns/fetch has stayed pretty static(~10ns) since DDR first showed up. There's been slight improvements but nothing like the order of magnitudes you seen in other areas. If you want to pay the power and cost of SRAM it can be done but it doesn't usually pencil out beyond what you see in caches today.
josalhor 6y ago
Has there been a study of the bottleneck of the performance of modern sat solvers? Some modern x86 CPUs have enormous cache sizes.

amelius 6y ago

Beware: Apple devices are not general purpose computers. Whether you can use them as such may be subject to change.

jcims 6y ago

Not particularly apropos to the thrust of the article, but I want to apply SMT to some tricky infosec use cases. Is there a good place to start for someone without an academic background in math/logic/etc?

mhh__ 6y ago
The chapter of Norvig on it may suffice as a self contained introduction. There is a book called SMT by Example (IIRC) which is good.
- jcims 6y ago
  Will definitely check out Norvig. Not sure if this is what you had in mind but the linked PDF appears to be a treasure trove, thank you!! https://news.ycombinator.com/item?id=19075599 https://news.ycombinator.com/item?id=19075599
  - mhh__ 6y ago
    Yep. Knuth also has a chapter on it.
panpanna 6y ago
I suggest you start with this paper: "SMT Solvers in Software Security", Julien Vanegue, Sean Heelan, Rolf Rolles https://www.usenix.org/system/files/conference/woot12/woot12-final26.pdf https://www.usenix.org/system/files/conference/woot12/woot12...
- jcims 6y ago
  Looks perfect, thank you!!!

derefr 6y ago

> Both systems ran Z3 4.8.1, compiled by me using Clang with the same optimization settings. Hypothesis: LLVM's AArch64 backend has had more work put into it (by Apple, at least) than LLVM's x86_64 backend has, specifically for "finishing one-off tasks quickly" (as opposed to "achieving high throughput on long-running tasks.") To me, this would make sense—until recently, AArch64 devices were mostly always-mobile, and so needed to be optimized for performing compute-intensive workloads on battery, and so have had more thought into the efficiency of their single-threaded burst performance (the whole "race to sleep" thing.) I'd expect, for example, AArch64-optimized code-gen to favor low-code-size serial loops over large-code-size SIMD vector ops, ala GCC -Os, in order to both 1. keep the vector units powered down, and 2. keep cache-line contention lower and thereby keep now-unneeded DMA channels powered down; both keeping the chip further from the TDP ceiling; and thus keeping the rest of the core that is powered on able to burst-clock longer. In such a setup, the simple serial-processing loop may potentially outperform the SIMD ops. (Presuming the loop has a variable number of executions that may be long or short, and is itself run frequently.) x86_64 devices, meanwhile, generally are only expected to perform compute-intensive tasks while connected to power, and so the optimizations contributed to compilers like LLVM that specifically impact x86_64, are likely more from the HPC and OLTP crowds, who favor squeezing out continuous aggregate throughput, at the expense of per-task time-to-completion (i.e. holding onto Turbo Boost-like features at maximum duty cycle, to increase mean throughput, even as the overheat conditions and license-switching overhead lower modal task performance.)

my123 6y ago
The LLVM x86_64 backend just gets as much work, and HPC is just one of the reasons. The NVIDIA PGI compilers for example use LLVM as a code generation backend, and that's one commercial option.
tedunangst 6y ago
This seems like a trivially testable hypotheses. Compile the code and look at the instructions generated. No need for elaborate speculation.

nickysielicki 6y ago

On the topic of the portability of Z3, does anyone know why this example runs fine on native amd64 but fails to solve when built with emscripten/wasm? https://github.com/sielicki/z3wasm https://github.com/sielicki/z3wasm Do a build by running, “mkdir bld && cd bld && emcmake cmake ../ -GNinja && emmake ninja”

nromiun 6y ago

For anyone trying to reproduce it in an Android phone you don't need to compile anything. Just "apt install z3" in Termux. It will probably be pretty slow but it will work.

panpanna 6y ago
Z3 is not available on termux (I am pretty sure it has been before). Back to the issue at hand. It is possible z3 is faster on arm64 due to the aarch64 bitfield instructions, but I find that unlikely.
- nromiun 6y ago
  It was recently merged but it is available. https://github.com/termux/termux-packages/tree/master/packages/z3 https://github.com/termux/termux-packages/tree/master/packag...
  - panpanna 6y ago
    Sounds it, thanks. Had to update the yermux app first to see it. Yes, z3 performs slightly betteron aarch64. But performance seems to be mostly cache dependent. Also, z3 is threades which would favor Apple with their fewer but faster cores compare to others with more but weaker cores.
    - panpanna 6y ago
      Hmmm... I think my autocorrect had a meltdown. Hopefully people can figure it out anyway.

vbezhenar 6y ago

It's very fun suggestion to put an iPhone in the cold water. Imagine cluster of iPhones working under-water for math problems :)

dang 6y ago

Discussed at the time: https://news.ycombinator.com/item?id=18383851 https://news.ycombinator.com/item?id=18383851