I’ve just been reading a very interesting MSR paper on Verifying Compiler Transforms For Concurrent Programs. The various memory models at both the hardware level on x86, and at the compiler level for C# seem very underspecified. This paper documents work on formalising the memory models, and using the formalisms to check that programs show the same effects after compiler transforms have been applied.
The work is great in two ways. First they have found bugs in the .NET x86 JIT which is obviously practically useful. The work also gives a great formal definition of the effects of the memory model in terms of how it modifies the traces of concurrent threads when they are merged to produce an effective trace. This makes it easier to understand the effects than the various wordy descriptions one finds in various books and blog articles. Of course, the real problem is that hardware level memory model is not formally specified by Intel – hence the authors have had to infer the formal model and then check that it exhibits various effects of the memory model that are specified in Intel design documents.
Of course, most C# programmers don’t care too much about the memory model. They will be writing code that is generally single threaded in its access of data (using lock statements). Joe Duffy’s blog has a great write-up of how he thinks things are going in the future. He points out that weaker memory models than the x86, such as those for the ARM chip, are going to become even more important in the future, and the average programmer is going to using other techniques to get thread safety in their code.
Nevertheless, I would like to understand memory models better, and this paper is a great help in that process.