coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] CompCertTSO release

From: Jaroslav Sevcik <jarin.sevcik AT gmail.com>
To: coq-club AT inria.fr
Cc: Peter Sewell <Peter.Sewell AT cl.cam.ac.uk>, Francesco Zappa Nardelli <francesco.zappa_nardelli AT inria.fr>, Suresh Jagannathan <suresh AT cs.purdue.edu>, Viktor Vafeiadis <viktor AT mpi-sws.org>
Subject: [Coq-Club] CompCertTSO release
Date: Mon, 4 Apr 2011 11:56:35 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:cc:content-type; b=gPRp3drdrGG26TOL+mExWWbpZ3/VMeqVGVNQC1J5tRWE4NyEHMfW1Sagj/M/bXM+lJ rKwTx1QizEudNo98r494WYKN+82Hz+0LdemHX+0j1ShywFcjI7Mr6lP+bjoG47rQnqb9 0KOt/BdPq6jcj3lQaTF2wZISNCpdscVwFtOY0=

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

[Coq-Club] CompCertTSO release, Jaroslav Sevcik