Feature request: atomic builtins

[danielsn]

CBMC currently has support for the gcc atomic builtins. However, these are added by the C front end, and hence there is no irep to directly target. It would be great to have support for these as first class ireps

[hannes-steffenhagen-diffblue]

@danielsn Could you please elaborate? Which builtins do you want and how exactly would you like to "target" them?

[danielsn]

I'm trying to support intrinsics like https://doc.rust-lang.org/std/intrinsics/fn.atomic_cxchg.html - these vary over both the type, and the memory model. CBMC has facilities that generate builtins that do exactly this, but its done on the C front end, and there is hence no backend model to target. If instead we had a set of Ireps that handled these in the backend, it would make them available to all language front-ends.

[martin-cs]

ansi-c/library/intrin.c contain a number of models of this form. I think having them implemented as library functions using atomic and fence avoids having too many irept's with complex semantics and interactions. You should be able to link against this kind of library even if you are using an alternative front-end. The Ada front-end links against them for example.

[danielsn]

That appears to be for the windows builtin intrinsics, which don't handle the different memory ordering models. I know CBMC supports the gcc intrinsics, which do, but I believe that is done on demand and I can't actually find a c file to link against. Is there one?

[tautschnig]

ansi-c/library/intrin.c contain a number of models of this form. I think having them implemented as library functions using atomic and fence avoids having too many irept's with complex semantics and interactions. You should be able to link against this kind of library even if you are using an alternative front-end. The Ada front-end links against them for example.

@martin-cs Would you mind pointing us towards where in https://github.com/diffblue/gnat2goto this is being done to better understand current best practice?

[hannes-steffenhagen-diffblue]

Linking against the builtin-library happens automatically (see here), you just need to reference the functions in your goto binary. @danielsn I don't really understand your other point, what exactly were you trying to do / why does what @martin-cs suggested not work for you?

FWIW for now concurrency support is broken enough that I don't think you'll be able to write a rust program that won't be rejected, I'm not sure how much energy it's worth spending on getting these completely right until that's fixed.

[danielsn]

The rust builtins differentiate between different memory ordering constraints, as do the gcc builtins https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html My understanding is that the CBMC implementation of these gcc builtins does model the memory ordering, but is not exposed in the backend.

The Windows builtins you linked against don't. So we can get the same basic behaviour (interlocked op), but without memory ordering. But if the concurrency solver is broken anyway, this may all be moot.

[martin-cs]

On Mon, 2021-03-01 at 08:55 -0800, Michael Tautschnig wrote: > `ansi-c/library/intrin.c` contain a number of models of this form. > I think having them implemented as library functions using atomic > and fence avoids having too many irept's with complex semantics and > interactions. You should be able to link against this kind of > library even if you are using an alternative front-end. The Ada > front-end links against them for example. @martin-cs Would you mind pointing us towards where in https://github.com/diffblue/gnat2goto this is being done to better understand current best practice?

We haven't got as far as handling concurrency in gnat2goto yet. I was referring to the use of C library functions. We simply generate a symbol table entry for the function and the body gets patched in when linking libraries.

[feliperodri]

@danielsn is this still an issue?