From a language standpoint, OCaml extends the core Caml language with afull-fledged object and class layer, as well as a powerful modulesystem, all joined together by a sound, polymorphic type systemfeaturing type inference. The OCaml system is anindustrial-strength implementation of this language, featuring ahigh-performance native-code compiler for several processor architectures(x86-32 bits, x86-64 bits, PowerPC, ARM, etc.),as well as a bytecode compiler and an interactive loop for quickdevelopment and portability. The OCaml distribution includesa standard library and a number of programming tools:a replay debugger, lexer and parser generators,a documentation generator, etc.
The CompCert verified compiler is a compiler for a large subset ofthe C programming language that generates code for the PowerPCprocessor. The distinguishing feature of CompCert is that it has beenformally verified using the Coq proof assistant: the generatedassembly code is formally guaranteed to behave as prescribed by thesemantics of the source C code. By ruling out the possibility ofcompiler-introduced bugs, verified compilers strengthen the guaranteesthat can be obtained by applying formal methods to critical embeddedprograms.
The diy suite provides a set of tools for testing shared memorymodels: the litmus tool for running tests on hardware, variousgenerators for producing tests from concise specifications, andherd, a memory model simulator. Tests are small programs writtenin the C language, in x86, Power or ARM assembler that can thusbe generated from concise specifications, run on hardware, orsimulated on top of memory models. Memory models are written inthe domain-specific language cat. Test results can be handled andcompared using additional tools.