A recent paper by Microsoft research has discovered a concurrency bug in the .Net JIT. They used the F# theorem prover to analyze the JIT il->x86 transformations which were previously thought to comply with the .Net memory model. These bugs show that writing correct concurrent (multi-threaded) code is hard - and in a multi-core world we need to find a way to provably write correct code.

"This discovery means that the current CLR JIT compiler for the x86 platform is not correct; it will be fixed in the future by strictly emitting locked instructions for all volatile stores"

- http://research.microsoft.com/apps/pubs/default.aspx?id=76524

via LtU