SMT Solving on an iPhone

#1

Post by sidereal » Mon, Nov 05, 2018, 4:57 PM UTC

SMT Solving on an iPhone
homes.cs.washington.edu

Re: SMT Solving on an iPhone

#2

Post by aquamo » Mon, Nov 05, 2018, 7:29 PM UTC

Thanks for this - with the release of the A12X Bionic, I've wanted to do something similar - i.e. build some specialized tools to leverage that CPU for atypical / non-mobile use cases.

I wish Apple would get on with it and include Terminal.App and the FreeBSD user land and Xcode for iOS so we can start running a shell and doing interesting things with this new hardware :-)

Re: SMT Solving on an iPhone

#3

Post by yazr » Mon, Nov 05, 2018, 7:38 PM UTC

a. single threaded code

b. extended benchmark duration - no thermal throttling encountered

c. straight forward C compiler - no special code for the GPU unit or whatever

d. main reason is probably memory and cache configuration

I think it is time to consider A(RM) and Intel cores at par. Qualcomm cores maybe X% slower but they will close the gap.

It is now a question of system trade-offs, as designers jangle memory sizes, cache sizes, cores, cooling, vector extensions, etc

This is a really pivotal event.

And dont forget AMD challenging Intel on like-for-like cores.

Its pretty amazing that noone has put together a real ARM alternative for the server side.

Re: SMT Solving on an iPhone

#4

Post by cosmic_ape » Mon, Nov 05, 2018, 8:05 PM UTC

Exciting. And the cache size is likely the main reason. But that can not be concluded from the analysis.

>>VTune agrees, and says that Z3 spends a lot of time waiting on memory while iterating through watched literals.

But how much is "a lot" is not specified. And the propagation also allocates memory sometimes, to keep the learned clauses. Not sure how Z3 manages this, but couldn't it be that the mallocs are just slower on that desktop, so an OS issue?

Re: SMT Solving on an iPhone

#5

Post by slededit » Mon, Nov 05, 2018, 8:19 PM UTC

aquamo wrote: post #2

Thanks for this - with the release of the A12X Bionic, I've wanted to do something similar - i.e. build some specialized tools to leverage that CPU for atypical / non-mobile use cases. I wish Apple would get on with it and include Terminal.App and the FreeBSD user land and Xcode for iOS so we can start running a shell and doing interesting things with this new hardware :-)

The common refrain I hear from hardware guys is that the uncore is the hardest part by far. The bulk of design time is spent connecting multiple cores together. Great single thread perf doesn't imply an easy path to multicore.

Re: SMT Solving on an iPhone

#6

Post by jSully24 » Mon, Nov 05, 2018, 9:01 PM UTC

Could Apple's next "innovation" not be a consumer product but to own the chip world? The iPhone "just" being the beta test for the chips?

Re: SMT Solving on an iPhone

#7

Post by macintux » Mon, Nov 05, 2018, 9:12 PM UTC

slededit wrote: post #5

aquamo wrote: post #2

Thanks for this - with the release of the A12X Bionic, I've wanted to do something similar - i.e. build some specialized tools to leverage that CPU for atypical / non-mobile use cases. I wish Apple would get on with it and include Terminal.App and the FreeBSD user land and Xcode for iOS so we can start running a shell and doing interesting things with this new hardware :-)

The common refrain I hear from hardware guys is that the uncore is the hardest part by far. The bulk of design time is spent connecting multiple cores together. Great single thread perf doesn't imply an easy path to multicore.

Still, the A-series multicore benchmarks have been pretty impressive as well.

Re: SMT Solving on an iPhone

#8

Post by slededit » Mon, Nov 05, 2018, 9:14 PM UTC

macintux wrote: post #7

slededit wrote: post #5

Earlier quoted context omitted.

The common refrain I hear from hardware guys is that the uncore is the hardest part by far. The bulk of design time is spent connecting multiple cores together. Great single thread perf doesn't imply an easy path to multicore.

Still, the A-series multicore benchmarks have been pretty impressive as well.

The problems arise when you start getting into double digit core counts. At 4 you can make pretty reasonable MUXes still. Above that you need to start making serious trade-offs to either Fmax or latency.

Re: SMT Solving on an iPhone

#9

Post by jimbokun » Mon, Nov 05, 2018, 9:18 PM UTC

jSully24 wrote: post #6

Could Apple's next "innovation" not be a consumer product but to own the chip world? The iPhone "just" being the beta test for the chips?

They probably don't want to sell those chips for Android to keep their competitive advantage, and the PC market is probably too small to be worth the investment compared to the iOS market.

Re: SMT Solving on an iPhone

#10

Post by ekr » Mon, Nov 05, 2018, 9:18 PM UTC

yazr wrote: post #3

a. single threaded code b. extended benchmark duration - no thermal throttling encountered c. straight forward C compiler - no special code for the GPU unit or whatever d. main reason is probably memory and cache configuration I think it is time to consider A(RM) and Intel cores at par. Qualcomm cores maybe X% slower but they will close the gap. It is now a question of system trade-offs, as designers jangle memory si…

The consequences of that are big. This will lead to commoditization of IP cores, cpus, and this will lead to a race to the bottom with the likes of Allwinner, Amlogic, Rockchip, NXP offering products competitive with Intel, Amd, Apple, Samsung. As the margins will go to near-0, companies like Intel will suffer the most.

This is assuming that semiconductor process improvements will significantly slow down or completely stop.