[TYPES/announce] CompCertTSO release
Jaroslav Sevcik
jarin.sevcik at gmail.com
Mon Apr 4 06:51:22 EDT 2011
Dear all,
we are pleased to announce a release of CompCertTSO, a certified
compiler from a multithreaded C-like language with a TSO relaxed
memory model to x86 assembly language with a realistic x86-TSO memory
model; the development builds on CompCert. The code, documentation,
and papers are available here:
http://www.cl.cam.ac.uk/~pes20/CompCertTSO/
They build with Coq 8.3pl1 and OCaml 3.12.0. Any comments would be
very welcome.
Jaroslav, Viktor, Francesco, Suresh, and Peter
More information about the Types-announce
mailing list