Re: [isabelle] I need a fixed mutable array

On 14-06-18 14:26, Ramana Kumar wrote:
I recommend looking at the other (non-x86) processor models in HOL4 too. Not all are complex and huge (though I guess that depends on your perspective).


Thanks for the suggestion. There's always more to say than anyone wants to read.

I'll say the same thing here that I'll say to Peter Lammich about the info he gave me. It's probably better that I didn't get this information from you before now. In particular, my finding this link from your tip:

That would be about ARMv7. The ARM Cortex-A15 was the CPU I thought I was going to go with. Please see [1] and [2] below.

There's like three main factors in looking at CPUs: they need to be sold on a board that's affordable, they need to have a large following, and they need to have some lasting power.

The Sony Playstation 3 CPU looks great, and it's fairly cheap, but then the Sony PS4 is changing to an AMD CPU. That's a bad sign.

Basically, there's GPUs, ARM, and Intel i7. Part of my pursuit began with looking for processors that have 256-bit data registers, because I used to work in graphics image generators, which had 256-bit wide data busses.

It was there all the time with the i7, and even before for 128-bit, with SSE, SSE2, SSS3, SS3, SS4, and now it's there for 256-bit, with AVX extensions.

RISC and ARM sounds like it should be fast, but then I looked at [3], and it's not like they blow everyone away.

I think an i7 is hard to beat, with 4 cores and 8 threads, with a clock at 3 to 4 GHz.. Lots of people have them, and people don't have to do anything special to run them, unlike embedded processors, or external, single board Linux computers.

All these practical considerations have a big part in influencing what route I think I should go. ARM is good, but then there's all sorts of special things I have to do for, among other things, develop tools.


[1] Samsung Exynos 5 Octa:

[2] ODROID-X3: ARM Cortex-A15 / Cortex A7 / Samsung Exynos 5 Octa based computer for $169.

[3] CoreMark integers tests: (sort by CoreMark/MHz)

[4] Brix with i7-4770R:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.