Implement new C++26 atomic operations

[mmalcomson]

With C++26 there have been the introduction of a few new atomic operations added.

One example is the atomic reductions: https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3111r0.html .
Another example are the atomic min/max operations.
Both can be seen in the current C++ draft: https://eel.is/c++draft/atomics

It would be nice if some corresponding intrinsics could be handled in C mode.

clang already has __atomic_fetch_min and __atomic_fetch_max, though doesn't seem to have anything defined for reductions.
Would be a blocker for implementing the reductions?

I'm quite interested in having something representing the atomic reductions implemented.

[hernanponcedeleon]

IIRC atomic reductions give different sync offering that normal RMW.

I had a prototype (only for litmus tests and nothing about the memory model) in the atomic-modify-write branch. Feel free to continue working on this direction. I know @gonzalobg and @graymalkin will probably be interested in having this implemented

[ThomasHaas]

That's a very interesting proposal. We can work around the lack of Clang support by providing custom headers I think.
I think the main issue is dealing with the "no-read" semantics for the memory model as it is not formalized in the CAT models yet.
That being said, from my understanding, these operations act like a rmw-pair, a load + store, where the load acts like a regular load from the global point-of-view but is not considered a load by the executing thread for the purpose of determining local orderings. This might not be too hard to implement, possibly by just redefining let R = R \ Red where Red are events coming from atomic reductions.

[hernanponcedeleon]

Feel free to continue working on this direction.

@mmalcomson I confused you with one for the students working on the tool 😅 and thus the suggestion; sorry about that.

If you have a real use case for this we can definitely get it implemented. The hardest part is probably having a .cat model that matches the spec. This is the newest model I am aware of, so we can try to incorporate it there.

[mmalcomson]

Heh -- no problem.
Just to confirm we do indeed have a real use-case -- and TBH I have virtually no idea how to read that model file you linked ;-)

I'm part of a team that work on GCC, we are in the process of implementing intrinsics to enable optimal implementation of the new C++ fetch_min/fetch_max operations, and are starting to look at implementing intrinsics for the atomic reductions.

It would be nice to have the extra validation that our translations between source-level code and assembly are correct, so we are thinking of using Dartagnon to check what behaviours are allowed at each level.

N.b. we're also asking if @lukeg101 can adjust his telechat tool to work with Dartagnon to improve our coverage -- though I have no idea whether he'll end up having the time to make that adjustment.

[graymalkin]

If it is fast/easy to add a Red set to dat3m and expose that to the CAT files, I can experiment extending the c++2w.cat to cover the P3111 change. I think @ThomasHaas's suggestion about R = R \ Red may well do the trick alone.

[lukeg101]

Yeah I was chatting with Matthew about this yesterday, Hernan this was the issue I was talking about :) Assuming Dartagnan accepts the herd-style litmus test format (for C and asm tests of the arch under test). Telechat should 'just work', ie in the make file we can swap out herd for dartagnan with the appropriate flags and compare outcomes.

RE the semantics of reductions, what Simon said, you'll need to add reduction reads to some special read set that is subtracted from release acquire calculations. The AArch64 model has something like this for SWP and friends.

[lukeg101]

and yes - Telechat use cases always welcome!

[lukeg101]

I expect you can reuse the tricky MP-with-red example from this paper to test (renaming C intrinsics, of course).
https://lukegeeson.com/publications/2024-03-05-CGO/

[ThomasHaas]

I implemented some support, see #985

[ThomasHaas]

Yeah I was chatting with Matthew about this yesterday, Hernan this was the issue I was talking about :) Assuming Dartagnan accepts the herd-style litmus test format (for C and asm tests of the arch under test). Telechat should 'just work', ie in the make file we can swap out herd for dartagnan with the appropriate flags and compare outcomes.

We can take herd-style litmus tests as input, though we might have less support for it than herd7 does (depends on how exotic your tests get?). But any issues should be fixable. We just need some concrete tests to work with.

RE the semantics of reductions, what Simon said, you'll need to add reduction reads to some special read set that is subtracted from release acquire calculations. The AArch64 model has something like this for SWP and friends.

I'm not sure how we deal with certain edge-cases like loading into the XZR zero register and how it affects memory semantics. Also, our curent aarch64.cat needs some updating: it does not reason about Noreturn right now. If Noret loads are just those that go into the XZR register, then it should be a very easy to fix though.

EDIT: Indeed, NoRet in aarch64.cat refers to those load operations that load into XZR/WZR. #986 should add support for this. We are missing litmus tests though.

[hernanponcedeleon]

Assuming Dartagnan accepts the herd-style litmus test format (for C and asm tests of the arch under test). Telechat should 'just work'

IIRC, Telechat compares the number of states under both models. This will not work with dartagnan (at least not without some further work) because we do not explore each execution / state explicitly.

[ThomasHaas]

Assuming Dartagnan accepts the herd-style litmus test format (for C and asm tests of the arch under test). Telechat should 'just work'

IIRC, Telechat compares the number of states under both models. This will not work with dartagnan (at least not without some further work) because we do not explore each execution / state explicitly.

We could add a state-exploration mode though.

[ThomasHaas]

@lukeg101 Maybe you could open a discussion (it would be our first one :)) about Telechat and how it would like to use Dartagnan, i.e., what features you need. From what I got from your paper, it seems you let herd7 dump all reachable states and then compare them using mcompare7 and some state mappings you have computed.
But to me it is not clear (i) the states of which registers/memory locations you are interested in (all of them? those that appear in the exist/forall clause?), (ii) what format mcompare7 uses to compare the outputs and (iii), what exactly mcompare7 even does? :)

@mmalcomson I think it would be helpful if you could describe more closely how you intend to use Dartagnan. For example, if we extend Dartagnan with the new C++26 atomics, how would you use this? I understand that you can write a C test + assertions to understand what is allowed on the C level, but then how do you compare this against the target architecture?
Do you plan to write litmus-style assembly by hand to match your intended compiler output (we cannot take the compiled binary as input unfortunately)?
Do you want us to add the intended compiler mappings to Dartagnan so you can avoid the manual translation step?
And if you end up using Telechat, the support for atomics on real C code is not necessary I think (Telechat takes C litmus as input, right?)

[mmalcomson]

@ThomasHaas I have a base hope and a stretch hope.

The base hope is that we can write C tests & assertions in Dartagnon, then compare them to manual litmus-style assembly and ensure the behaviours are the same.

The stretch hope was why I was looking at Telechat -- I hope to use it by having Telechat generating C tests for us, compiling them with the compiler that we will have developed, then check that the resulting assembly has the same set of allowed behaviours as the C testcase. In order to model the allowed behaviours of the C code and the assembly I believe Telechat would use Dartagnon.
I believe that Telechat constructs litmus tests from the ELF file that our compiler would emit -- so those litmus tests should be able to get passed into Dartagnon. Is that correct @lukeg101 ?

[ThomasHaas]

@ThomasHaas I have a base hope and a stretch hope.

The base hope is that we can write C tests & assertions in Dartagnon, then compare them to manual litmus-style assembly and ensure the behaviours are the same.

Ok, that is certainly possible and reasonably easy for us to provide. The somewhat ugly part about this is that litmus-style assembly has assertions over final values whereas for regular C code we only support inline assertions. Those can also be used to reason about final values, but that requires some more instrumentation.
Going this route, it might actually be easier to write the C test also in litmus-style to have closer correspondence and avoid the need for boilerplate code like a main function that spawns the threads of interest, joins on them, and then collects their results to assert something about the combined observations of the threads.

We will also need to update our support for litmus-style assembly if you want to test the assembly using Dartagnan. Our support for litmus assembly is certainly not as large as that of herd7 for now. I think adding all the different assembly instructions for all hardware targets of interest, which I assume would be at least ARMv8, RISCV, PPC, and X86, is probably the most time consuming part on our side. Restricting this to one target like ARMv8 for now would be feasible though I think.

The stretch hope was why I was looking at Telechat -- I hope to use it by having Telechat generating C tests for us, compiling them with the compiler that we will have developed, then check that the resulting assembly has the same set of allowed behaviours as the C testcase. In order to model the allowed behaviours of the C code and the assembly I believe Telechat would use Dartagnon. I believe that Telechat constructs litmus tests from the ELF file that our compiler would emit -- so those litmus tests should be able to get passed into Dartagnon. Is that correct @lukeg101 ?

That sounds like the best way. Unfortunately, in this case we would still need to add extensive support for more assembly instructions :(.

All of this begs one question though, why do you and @lukeg101 want to use Dartagnan over herd7 in the first place? Is it the support for real C code, or the scalability of the verification that is of interest? I'm not complaining though, I'm happy if people have practical applications for Dartagnan :D.