Current compiler analyses and programming idioms really are good enough tho', if it can't actually magically find and set the right CPUID checks at exactly the right places then why bother /s
and it's actually worse because each architecture has its own model for SIMD execution.
Conversation
Fair enough! As I say I don't know the specifics of this situation (I realise things like SIMD can be fraught the more you look into it), and I'm certainly naive here. I'm curious about the issues and if we can do better, but I understand if you are fine with the status quo. 😅
1
2
well like,
x86-64 has 128, 256, or 512 bit registers.
Arm Neon has 128 bit registers.
Arm SVE2 will have 128 * N bit registers.
RISCVV allows vector registers to have almost any length starting at 32 bits.
And users don't care about this and want their program to "just work".
1
1
They don't really wanna write a lemma about program validity for each different architecture, y'see, and each of these arches has subtly different rules about how these instructions are legalized and so on, but they want the maximum perf the hardware affords anyways.
1
2
Yeah, I can see how this stuff is painful… and yeah I'm definitely not advocating for forcing you to write validity lemmas for this stuff – sorry if I sounded like I was! Most of the stuff I'm interested in is a bit more high level and automated (there are limits there though).
2
1
Ah and see this is where we differ:
I am deranged!
I read papers on things like dependently typed assembly.
2
2
Ooooh I want it
1
1
I want a dependently typed assembly language - and some higher level dependently typed IRs that I can use as targets for my imaginary type preserving compiler for my dependently typed programming language. 🙃
1
1
Which papers were you looking at re. dependently typed assembly?
1
1
there's actually quite a few, since the first treatment of a DTAL was in 2001 by Xi and Harper, "A Dependently Typed Assembly Language"
1
2
Cool, think I've heard of that one! I'm interested in is how one might be able to embed a typed assembly language like this in a higher level language for inline-asm - wondering if it might end up looking like something like two-level type theory? But yeah no idea.