Hello, TLA+ newbie here. I'm interested in verifying some lockless concurrency algorithms that rely on explicit memory barriers. Specifically I'm targeting x86_64, which has a fairly strong memory model, but there is also the compiler to consider, which may reorder LOADs and STOREs, so I am providing explicit constraints to the compiler to limit the reordering it's allowed to do. But of course it can still reorder quite a bit within those constraints. It seems possible to model this in TLA+, but an awful lot of work, and being a newbie I'm pretty likely to get it wrong. Is there anything already available that would give me a starting point in modeling this?
Thanks so much,
Randall