Stream: general

Topic: Validate atomic fence usages?


Charles Lew (May 04 2019 at 04:38, on Zulip):

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.

Charles Lew (May 04 2019 at 04:39, on Zulip):

@RalfJ

nagisa (May 04 2019 at 10:06, on Zulip):

There is appears to be some research done, mostly around automatic insertion of the memory barriers, but I’m sceptical.

nagisa (May 04 2019 at 10:07, on Zulip):

See e.g. http://www.kroening.com/papers/toplas2017-musketeer.pdf

nagisa (May 04 2019 at 10:09, on Zulip):

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.

Charles Lew (May 04 2019 at 15:24, on Zulip):

@nagisa thank you!

RalfJ (May 05 2019 at 13:16, on Zulip):

uh... there's probably tools but I dont know much about automated stuff like that, sorry^^

Last update: Nov 20 2019 at 11:35UTC