[llvm] r179005 - AArch64: remove barriers from AArch64 atomic operations.

[Jeffrey Yasskin]

On Mon, Apr 8, 2013 at 11:27 AM, Tim Northover <t.p.northover at gmail.com> wrote:
>> AArch64: remove barriers from AArch64 atomic operations.
>
> Bother, I meant to ask for some review from any memory order Guru's
> before committing this but "git svn dcommit" thwarted me. It basically
> removes the use of barriers for AArch64 memory operations, switching
> to exclusively acquire/release instructions in the ldxr/stxr loop.
>
> At first sight it looks a little dodgy; acquiring a lock:
>
> loop:
>     ldxr x1, [x2]
>     [...]
>     stxr w0, x1, [x2]
>     cbnz w0, loop
>     dmb
>
> becomes:
>
> loop:
>    ldaxr x1, [x2]
>    [...]
>    stxr w0, x1, [x2]
>    cbnz w0, loop
>
> where the barrier has moved much earlier in the sequence, and so in
> particular the final store which asserts ownership can be reordered
> with operations making use of that ownership.
>
> However, the important point is that another observer taking the lock
> wouldn't see this because their stxr would fail. Another point in
> favour of validity is that this is what the Linux kernel does.
>
> I've also managed to convince myself that similar reasoning holds for
> other atomic operations, but if I'm honest I'm not even entirely sure
> what a formal proof of that would look like, never mind having it.
>
> So any comments on this would be particularly welcome.

I haven't read the patch, and I'm not familiar with
AArch64's memory model, but using ld-acquire for an acquire rmw sounds
correct, as does using st-release for a release rmw. The sequentially
consistent option is harder to demonstrate, but you should look at
http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/pldi12.pdf or
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2008/n2745.html for
the style of argument you need.