Look at this Relacy Race Detector:
It is designed to detect race conditions, but you have to understand me
Sir and Madam, you have to model your problem with this tool,
and this modeling is prone to error, so that's not good for
safe-critical systems, other that look at this:
If every thread has to increment "a" one time, this form of logic
is nasty, because if we do the follwing in Relacy Race Detector:
How can Relacy Race Detector detect that the logic that every thread has
to increment "a" one time is good ? Relacy Race Detector can
not do it, and this form of logic can become more nasty, so
this is why parallel programming for safe-critical systems
is still too risky.
Amine Moulay Ramdane.