Hi, a friend of mine recently found out in his Rust project that an extremely hard to reoccur deadlock issue is actually caused by incorrect atomic fence usage. I wonder if there're any formal method verification design or tools that can integrate with the language somehow to "reason about" these usages and validate at compile-time that they're correctly used.
There is appears to be some research done, mostly around automatic insertion of the memory barriers, but I’m sceptical.
I’m not aware of any static analysis tools which would look at your fences and say "hey this one is wrong", but automatic insertion in more general and such an analysis tool could be implemented in terms of such an analysis tool.
@nagisa thank you!
uh... there's probably tools but I dont know much about automated stuff like that, sorry^^