In general, the answer typically involves formal specification and formal methods that check the code against these specifications, combined with testing and coding standards that result in analysable code.
You might want to look into coding standards for C and special languages like Ada (like C, but less writeable, more readable with strong types) and Esterel (deterministic multithread scheduling). Seriously, Esterel is probably the coolest thing you'll read about this week.
There's also various specification languages for multithreaded behaviour, which allows you to analyse your programs behaviour using software tools, for example SPIN[0].
In general, the answer typically involves formal specification and formal methods that check the code against these specifications, combined with testing and coding standards that result in analysable code.
More references:
https://www.cs.umd.edu/~mvz/cmsc630/clarke96formal.pdf
http://research.microsoft.com/en-us/um/people/lamport/tla/fo...