Cmmtest
			       *******

The Cmmtest tool performs differential testing to hunt concurrency
compiler bugs in C and C++ compilers against the C11/C++11 memory
model.

Install
*******

0) Prerequisites

The Cmmtest tool only runs on 64bits Linux x86 machines.  The
installation procedure depends on the following preinstalled software:

- standard developer tools

- the ocaml compiler, available from http://caml.inria.fr

- the timeout utility

- creduce depends on several packages; on Ubuntu, prerequisites other
  than LLVM can be installed like this:

  sudo apt-get install indent astyle delta libbenchmark-timer-perl  \
    libexporter-lite-perl libfile-which-perl libgetopt-tabular-perl \
    libregexp-common-perl libsys-cpu-perl flex build-essential

  For instructions to install the creduce prerequisites please check

    https://github.com/csmith-project/creduce/blob/master/INSTALL


1) Instructions

- download the cmmtest-<version>.tgz archive from the project web-page;
- untar -xzvf cmmtest-<version>.tgz
- cd cmmtest-<version>
- ./install.sh <prefix>

The install.sh script will download and install the following third
party software in the <prefix>/cmmtest_distribution/ directory:

- clang\llvm 3.3                   (http://clang.llvm.org)
- the pin tool                     (http://software.intel.com/en-us/articles/
                                      pin-a-dynamic-binary-instrumentation-tool)
- frama-c                          (http://frama-c.com)
- the latest gcc version (via svn) (http://gcc.gnu.org)

Check the relative web-pages for details about licences.

The install_cmmtest script will also install the following software:

- pin_interceptor            
- csmith_with_locks
- csmith_with_atomics
- creduce-cmmtest
- cmmtest

These tools are free software (BSD-licence).  Csmith_with_locks
and Csmith_with_atomics are derived from the Csmith tool
(http://embed.cs.utah.edu/csmith/), Creduce-cmmtest is adapted from the
Creduce tool (http://embed.cs.utah.edu/creduce/).

The install.sh script, when succesful, prints how the environment
variables must be modified to use the Cmmtest distribution.

If one of the components fails to build, a detailed log is left in
<prefix>/cmmtest_distribution/install.log.  You can manually fix the
build process of one component, the install.sh script ought to be
robust enough and avoids re-installing already installed software.

A sample config file is automatically generated in <prefix>/scripts.
You might want to update it to suit your needs.


Usage
*****

To generate and test one program a sample command line is:

$ cmmtest -generate c -compiler gcc -opt -O2 -trace x86 -analyse -dump_traces

The output will include:

- the reference and optimised traces, annotated with eliminable events;
- the a summary of the events in the two traces;
- the result (true/false) of the matching.

The typical invocation of Cmmtest keeps generating new programs until
a bug is found and then performs test-case reduction:

$ cmmtest -generate c -compiler clang -opt -O3 -trace x86 -analyse         \
     -clean -delta c_reduce -real_quiet -repeat

In the real_quiet ouupt:

  '+' stands for a succesfull test
  '-' stands for a miscompilation detected
  '.' stands for timeout of the analysis
  '_' stands for timeout of the tracing (looping program)

Reduced tests will be called <int>_min.c and are left in the current
directory for manual inspection.

The Cmmtest can also be invoked on a user-supplied .c or .c++ file, e.g.:

$ cmmtest -compiler clang -opt -O2 -trace x86 -analyse -dump_traces foo.c

User-supplied files must obey the following syntactic conventions:

- names of global variables must begin with 'g_'
- names of atomic variables must begin with 'a_'
- names of functions must begin with 'func_'
- names of local variables must not begin with 'g_' or 'a_' or 'c'

For a list of options:

$ cmmtest -help

The ARM tracing infrastructure is not currently distributed.


Authors & Licence
*****************

The Cmmtest tool is developed by Pankaj Pawan and Francesco Zappa
Nardelli, with contributions by Robin Morisset, Anirudh Kumar, Pankaj
More and Pankaj Prateek.

The Cmmtest tool is copyright 2012, 2013 Institut National de
Recherche en Informatique et en Automatique (INRIA).

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions 
are met: 
1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
3. The names of the authors may not be used to endorse or promote
products derived from this software without specific prior written
permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS 
OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE 
ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY 
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL 
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE 
GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS 
INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER
IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR 
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.