SMT Solving on an iPhone (2018)
cs.utexas.edu
cs.utexas.edu
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.
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.
Note that (1) and (2) are much more important than (3). In particular, you can even arrange the data elements for (1) in an order that you _expect_ them to be dereferenced, and even if your "hit" ratio is only slightly better than zero, you can get a performance improvement. For this latter one, check out https://www.msoos.org/2016/03/memory-layout-of-clauses-in-mi...
Although I'm quite new to the SAT field I have to say I am quite impressed with the performance of cutting edge sat solvers. Looking at the source of some of them (like Glucose) I don’t see that much low-level trickery. I wonder how much down the stack one could go to try to get more out of their processors.
This is theory-dependent, I would say. It is certainly true for bit-vector solvers that bit-blast for example. For other theories, however, this is not necessarily the case. Consider a simplex-based linear integer arithmetic solver for example. If there is a problem that is simple at the Boolean level, you may end up spending more time in the simplex solver.
I work on the STP SMT solver along with a team of very dedicated people (https://github.com/stp/stp/), it's QF_BV (Quantifier Free BV) solver and it tends to do well in the competitions: https://smt-comp.github.io/2020/results.html So I'm probably a bit biased towards BV. For counting (e.g. https://github.com/meelgroup/approxmc) and sampling (e.g. https://github.com/meelgroup/unigen) it's also 99% SAT solver runtime.
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.
I signed up for the Apple DTK, hoping they approve more people abroad..
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.
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.
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.
Ultimately, I think the distinction is pretty meaningless.
Hot take: If SMT, SAT are too simple to be given the coveted badge of AI, then Machine learning should be called as glorified curve-fitting?
I feel that everyone is amazed by the results provided by the good examples of Machine Learning, as only those get popular. The spectacular failures and completely absurd results which reveal that ML is not having any semantic understanding of the problem are completely glossed over.
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.
And we spend a lot of time on the internet complaining about that (nobody likes rejection).
iPadOS seems to be good enough with mouse pointer and keyboard input too now.
I don't know what too end laptops you were looking at but I suspect there are more options there than the one you chose.
iOS 13 supports local USB hard drives and network shares well enough.
You open procreate and have to share/import/export with Google each time. The automatic backup thing I use drive for doesn't seem to work. The files aren't really backed up until they're reshared with Google drive, circumventing the whole point of automatic backups as I'm working.
The file browser is a workaround that lets you drag files but the basic functionality is ruined.
When you open a file within Procreate, it should give you an option within the app to choose Google Drive or whatever other storage provider you have install and load and save files to Google Drive from within the app.
It works for Office.
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.
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)?
This metric really only has to do with the amount of memory that a machine has, in my experience.
I'm sorry? What?!
The vast majority of Apple's customers are Apple fans, people who merely wish to think different, nothing more, nothing less.
Edit: Don't downvote just to disagree. Comment and state your reasoning on why you think I'm wrong. If you work for a company that only issues Apple devices, please speak up with your experience on how this went, and, if possible, why the company didn't go with Windows or Linux computers instead.
For the comments that try to bring up software development roles: most software developers I know either use Windows or use Linux on the desktop, and loath OSX worse than I do. Very few prefer OSX.
The few people I know that prefer OSX (and will die on that hill) are frontend developers.
I wouldn't go so far as to say that this is proof that "Apple's main clientele is business", but it certainly wouldn't surprise me. And it's not true that offices don't allocate Apples to workers.
It even happened at Microsoft until the Surface program was finally given a proper go ahead by Nadella. A lot of former MBP users seem to love the Surfacebook, so they succeeded in making a functional yet veblen good in the same vein that a MBP is.
https://www.macrumors.com/2020/06/29/apple-rosetta-2-a12z-be...
Apparently, a Surface with a Ryzen 4800U exists and is coming out really soon.
The comparison isn't realistic because Apple's acquisition of PA Semi was a brilliant move, and no one makes an ARM that is anywhere near that level of performance, not even Qualcomm. I agree with Apple's decision to put their ARM on the desktop as their answer to the Intel dilemma.
In this case, an ARM vs ARM comparison is not an apples to apples comparison, Apple does not license their design to anyone else, ergo, the only way to make a fair comparison is to use the best commonly available part, which currently, is Zen 2 parts.
I expect a Zen 2 to crush a 2 year old Apple ARM, but I also expect a future Apple desktop and laptop design to keep up with Zen 3. I actually hope Apple can win the fight, but I also wish Apple would license their CPU to other manufacturers to promote the general adoption of more architectures in this space.
As far as Surface sells.
https://appleinsider.com/articles/19/10/24/editorial-why-mic...
That is one of the most absurd takes I have ever seen by an Apple hater. Even haters usually acknowledge that Macs are used extensively in software development, scientific research, film editing, design work, and education. And Apple is the fourth largest PC maker in the world, so they’re also used just about everywhere else at least a little bit.
What are you doing on this website because you clearly don't work in software.
> Please don't comment about the voting on comments. It never does any good, and it makes boring reading.
But anyway, you're talking about a very specific use case that only partially generalises.
I'm typing this on an 2014 11" MacBook Air 6,1 i5-4260U CPU @ 1.40GHz, 2001 Mhz, 2C / 4T with 4GB RAM running Windows 10 with two Chromium Edge and Firefox, 2D CAD and vector graphics programs running.
And there's nothing bizare in OP's real world scenario. Mine is even worse.
I also have multiple Linux OS running on Docker, Windows on a virtual machine with 4 CPU threads dedicated to it and native Windows running Ubuntu over WSL2 performing some tasks. I don't turn any of that off while I'm playing game and streaming.
for the downvoters: https://www.youtube.com/watch?v=PcYA-H3qpTI
2. We haven't seen any real product yet, only the dev kit. The new Macs will be much more powerful than any existing Apple Arm products. We'll see.
1. Like so,
2. for example.
1. Like so,
2. for example.
AFAIK apple CPUs are on-par with high performance desktop class x86 CPUs, but only in integer performance. AAA gaming would probably perform badly since it has plenty of floating point operations.
edit: *in single thread performance
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.
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.)
The difficulties of doing columnar style queries for document and graph databases led at least one person I know to tell a certain three letter agency that they couldn't have the panopticon machine they wanted.
For online transaction processing rows are good, but for OLAP it is not even competitive.
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.)
> 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?
Makes your question even more interesting though, what will a Mac Pro look like running Apple silicon inside 2 years from now?
Cache misses have the same problem.
I don't run antivirus on my microwave oven. There's no need.
Only as long as you have not connected it to any network - "smart" appliances have often enough been used for botnets now.
Oh brother, I got some bad news for you. It's called the Mirai botnet.
>than the Z3 app despite less time on screen.
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.
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.
https://github.com/sielicki/z3wasm
Do a build by running, “mkdir bld && cd bld && emcmake cmake ../ -GNinja && emmake ninja”
"SMT Solvers in Software Security", Julien Vanegue, Sean Heelan, Rolf Rolles
https://www.usenix.org/system/files/conference/woot12/woot12...
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.
https://github.com/termux/termux-packages/tree/master/packag...
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.
Hopefully people can figure it out anyway.
If it goes how I think it will go, X86 is done. People will really start wanting ARM on servers.
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.
https://www.anandtech.com/show/15578/cloud-clash-amazon-grav...