[bonzini]

Not Linux but the Linux formal memory model. The idea is that the compiler optimizations can be as nasty as the Alpha out of order execution engine and cache. The Linux code has to cater for these optimizations even though it will not result in an actual assembly instruction on anything except the Alpha. Problem is, on Alpha there's indeed an actual price to pay in performance for that nastiness.

[asveikau]

I suspect you misunderstand the question. My question is if anybody is presently using alpha hardware to verify such correctness. I understand memory models and barriers etc. and that alpha is one of the most relaxed on this front, that it historically influenced the kernel code and was previously very important test hardware. But the hardware is now very dated, to the point where it might not be good test hardware.

[bonzini]

The answer to that question is no, but the Alpha is still considered the least common denominator even though the hardware is obsolete. When people write litmus tests for the Linux memory model they are still validated against Alpha semantics, because compiler optimizations have the same reordering effects as the weird caches of Alpha processors.

(The stroke of genius of the C++11 memory model, compared to the older Java memory model, was that reordering could be treated the same way no matter if performed by processors or compilers).