[mafribe]

CompCert uses tame optimisations, and compiles to mainstream architectures nothing exotic. Most of all, CompCert does not deal with concurrency as far as I'm aware. Concurrency is where memory models matter.

The problem with memory models is not so much verifying it in a mechanised way, but inventing something suitable at all.

[groar]

  The problem with memory models is not some much verifying it in a mechanised way, but inventing something suitable at all.

Agreed.

I'm aware of some work done a few years ago by people working on weak memory models and extending CompCert with some concurrency primitives: http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/