Analyzing Multithreaded Code Mathematically

Multithreaded code is hard to debug. Therefore, it helps a lot if one can analyze it mathematically to see whether the code is sound or not.
There are at least 3 approaches to do that:

1. With Petri-Net (http://en.wikipedia.org/wiki/Petri_net)
2. With CSP (http://en.wikipedia.org/wiki/Communicating_sequential_processes)
3. With Pi-Calculus (http://en.wikipedia.org/wiki/%CE%A0-calculus).

I have just started to learn all of them, so I cannot explain the pros and cons of each one of them just yet.