TSO extension

[hernanponcedeleon]

This paper extends TSO with support for non-temporal stores and different kind of memory types (e.g. uncatchable). It would be interesting to add support for this to dartagnan.

[ThomasHaas]

While I also think that this is interesting in theory, in practice it is probably quite underwhelming as it is going to only work on assembly code (litmus tests). Problematic is the fact that we need to annotate memory locations rather than memory accesses (how would one do this in C?). Annotations of memory locations are also very problematic with any form of access indirection (pointers) where the alias analysis cannot infer the location to be accessed. If the alias analysis is precise (which it surely is for simple litmus tests), one can probably move the memory annotation down to the memory accesses in the form of tags. Otherwise, a full dynamic handling of memory accesses is required. But I guess this could also be an argument for using Refinement here.

[hernanponcedeleon]

Yes, this won't fit for verification of C programs unless such instructions end up in some compilation scheme. I think some (not sure if all) of those instructions are related to NVM. I know Azalea has been working on some C library to support persistency memory so eventually they might become part of compilations schemes.

I don't think you can annotate memory on C, but memory annotations have their use (e.g. arm's MTE is used for security in the Linux kernel by KASAN).

Even if this ends up just working for litmus, it might be a nice thesis work for some student and this is why I want to keep track of such features in the tracker.

[hernanponcedeleon]

Probably not too useful. Closing (the resource will remain available under "closed issues" if we ever want to revisit the idea).