herd / herdtools7

The Herd toolsuite to deal with .cat memory models (version 7.xx)
Other
215 stars 54 forks source link

[all]: Add support for SVE fault tolerant instructions #876

Open murzinv opened 2 months ago

murzinv commented 2 months ago

SVE adds instructions which can suppresses memory fault, specifically:

murzinv commented 2 months ago

@maranget , @relokin I've run into inserting case where SVE load instructions can suppress fault. I noticed that non-vector instructions use lift_memop yet it seems it doesn't fit into vector case:

So, I'm seeking your advice on how to progress with that?

Thanks!

relokin commented 1 month ago

Thanks for this @murzinv, perhaps before adding support for these new instructions, or in parallel with this change, we need to add vmsa support for the existing vector instructions. Looking at the pseudocode, it looks like we have one translation/tag check per element memory read/write.

I am looking specifically at store_scatter_predicated_elem_or_merge what is that prevents from wrapping the call to do_write_mem inside a call to lift_memop?

maranget commented 1 month ago

Hi @murzinv and @relokin, I have no precise idea on the next step. I agree with @relokin that combining SVE and VMSA is a prerequisite for this PR. Another, perhaps less interesting but less ambitious direction could be to implement additional arithmetical and logical operations.

murzinv commented 1 month ago

we need to add vmsa support for the existing vector instructions

Cannot disagree with that :smile:

Looking at the pseudocode, it looks like we have one translation/tag check per element memory read/write.

Correct.

I am looking specifically at store_scatter_predicated_elem_or_merge what is that prevents from wrapping the call to do_write_mem inside a call to lift_memop?

I assume that in such case every store of the element would end-up with either B.next1T or B.Exit, I'm not sure if it is effect we want :thinking: I also noticed that load/store pairs do not do lift_memop for each element of the pair (that's why I mentioned #813 ) and I suspect that there is a good reason for that... Anyway, I can explore your suggestion and report back.

relokin commented 1 month ago

I assume that in such case every store of the element would end-up with either B.next1T or B.Exit, I'm not sure if it is effect we want 🤔 I also noticed that load/store pairs do not do lift_memop for each element of the pair (that's why I mentioned #813 ) and I suspect that there is a good reason for that... Anyway, I can explore your suggestion and report back.

I think it's B.Next or B.Fault that we want. The instruction should raise a fault, but, also, I suspect that it's architecturally allowed to see from 0 to all non-faulting, active element write happening before entering the fault handler. That might mean multiple architecturally allowed executions just because one element read/write generates a fault.