PARCOACH automatically checks parallel applications to verify the correct use of collectives. This tool uses an inter-procedural control- and data-flow analysis to detect potential errors at compile-time.
We maintain the parcoach package in the guix-hpc channel; see here for information about how to add a channel to Guix.
Once the channel is added, you can use parcoach as any other Guix package, for instance if you want a shell with parcoach, OpenMPI, and clang 15 you would run:
guix shell openmpi parcoach clang@15Check the "Usage" section for more information about how to run the tool on codes!
You can use the docker image from our "demo" repository, which include a ready to use parcoach, OpenMPI, and Clang:
docker run -it registry.gitlab.inria.fr/parcoach/parcoach-demo:2.4.1 bashIt will give you a shell, you may want to mount a local folder to start playing with your codes by passing -v /local/path/to/folder:/path/in/docker to the docker run invocation.
We maintain a spack repository with the parcoach package right here, you just need to clone this repository, add the spack folder as a repository, then install parcoach. The detailed commands are below:
git clone https://gitlab.inria.fr/parcoach/parcoach.git
spack repo add parcoach/spack
spack install parcoach
spack load parcoachIt should load both PARCOACH as well as the Clang/LLVM it's depending on. Check the "Usage" section for more information about how to run the tool on codes!
All PARCOACH releases can be found here.
If you don't want to worry about installing too much dependencies we recommend taking the static-Linux release, it comes with everything bundled.
Then you just need to install OpenMPI and Clang 15 on your system to start running the tool on codes.
We recommend using Guix or spack: they are popular options for managing packages on clusters. If you don't use them on your personal computer then we recommend using the aforementioned docker image!
These instructions will get you a copy of the project up and running on your local machine.
The most straightforward way to setup a working build environment for PARCOACH is to use the docker images used by our Continuous Integration.
As a simple user, the easiest is to use the docker compose shipped with this
project; you can use the following command from the root of this project to start
a shell in a docker container, with your local PARCOACH folder mounted at /home/parcoach/sources:
docker compose run --rm shellIt will build a docker image with the environment to build PARCOACH, without having to install everything on your machine, but while still being able to use your editor out of the docker container (because the source tree will be shared between the host and the docker container).
If you want to take a look at how the docker images are built and how the CI works, please take a look at the dedicated README.
At the time of writing these lines, the two main dependencies are CMake >= 3.16 and LLVM 15.
If you're using Guix, just use our manifest with guix shell -m manifest.scm ;)
With this you don't even have to use pipenv in the next section as the python dependencies are in the manifest.
Assuming you have cloned PARCOACH and have followed the previous section, building PARCOACH and running the tests should be as easy as using the following commands:
cd sources
# This installs necessary python dependencies for tests
pipenv install
pipenv shell
mkdir build && cd build
cmake .. -G Ninja
ninja run-testsIf you are using an installation of LLVM which is not in default paths, you can instruct CMake to use a specific version of LLVM by using the following command:
cmake .. -G Ninja -DLLVM_DIR=/path/to/llvmPARCOACH has a Guix package through the guix-hpc channel. You can also setup a development environment for the current main branch by using the manifest at the root of this repository:
guix shell --pure -m manifest.scm -- bash
# This fixes MPI usage through Guix.
export OMPI_MCA_plm_rsh_agent=`which false`
mkdir build-guix && cd build-guix
cmake .. -G Ninja
ninja run-testsCodes with errors can be found in the Parcoach Microbenchmark Suite and in our tests folders.
PARCOACH is a set of LLVM analysis and transformation passes which can be ran
either using the standalone parcoach executable.
It's also possible to use the opt
wrapper parcoachp, or to directly call opt while loading PARCOACH as a pass
plugin; both these alternative are not recommended, but should work.
The parcoach interface mimics opt's one: it takes LLVM IR as input, either
as bytecode (the .bc files) or as humanly readable IR (the .ll files).
Unless using the instrumentation part, you don't need any output IR and using
-disable-output is recommended.
This can be executed right away on one of our tests files.
The first step is to generated the LLVM IR for the file, for a C file it would
be done with clang for instance.
The command below is meant as an illustrative example, it actually requires MPI
to be installed on your system.
If you don't/can't have it, skip this step as we have LLVM IR examples ready to
use in our codebase.
clang -g -S -emit-llvm tests/MPI/basic/src/MPIexample.c -o MPIexample.llThe next step is to actually run PARCOACH over the IR; for the sake of this example we'll use one of our IR tests files:
parcoach -check-mpi -disable-output tests/MPI/lit/MPIexample.llIt should give you an output with a warning looking like this:
PARCOACH: ../tests/MPI/basic/src/MPIexample.c: warning: MPI_Reduce line 10 possibly not called by all processes because of conditional(s) line(s) 24 (../tests/MPI/basic/src/MPIexample.c) (full-inter)
clang -g -c -emit-llvm file1.c -o file1.bc
clang -g -c -emit-llvm file2.c -o file2.bc
clang -g -c -emit-llvm file3.c -o file3.bcDo not forget to supply the -g option, so PARCOACH can provide more precise debugging information.
llvm-link file1.bc file2.bc file3.bc -o merge.bc3) Finally, run the PARCOACH pass on the generated LLVM bytecode. To detect collective errors in MPI:
./parcoach -check-mpi merge.bcThe executable parcoachcc is shipped with PARCOACH and can be used as a wrapper
to have a single step to compile your code while running the analyses over it.
A call to the wrapper looks like this:
$ parcoachcc clang example.c -c -o example.o
remark: Parcoach: running '/usr/bin/clang example.c -c -o example.o'
remark: Parcoach: running '/usr/bin/clang example.c -g -S -emit-llvm -o parcoach-ir-782df9.ll'
remark: Parcoach: running '/usr/local/bin/parcoach parcoach-ir-782df9.ll'
...As you can see, under the hood parcoachcc will perform three steps:
- it will execute the original command line.
- it will generate a temporary LLVM IR file.
- it will run PARCOACH over that temporary IR.
This wrapper lets you easily integrate PARCOACH in popular build systems; you can check our wiki articles about autotools integration or CMake integration.
Coming soon
PARCOACH has adopted pretty much the same coding style as LLVM. Two tools are used for this:
clang-tidy, which checks wether the naming conventions are respected, or if there are parts of the code which are not easily readable, and many other criteria. It's not mandatory for the output ofclang-tidyto be empty, but it's generally a good idea to look at it. You can enable it by passingPARCOACH_ENABLE_TIDY=ONto CMake.clang-format, which deals with pure formatting checks. It's mandatory for any code landing on the main branch to be correctly formatted. You can automatically format the code by runningninja run-clang-format.
Van Man Nguyen, Emmanuelle Saillard, Julien Jaeger, Denis Barthou and Patrick Carribault, PARCOACH Extension for Static MPI Nonblocking and Persistent Communication Validation Fourth International Workshop on Software Correctness for HPC Applications, 2020.
Pierre Huchant, Emmanuelle Saillard, Denis Barthou and Patrick Carribault, Multi-Valued Expression Analysis for Collective Checking Euro-Par 2019: Parallel Processing, pages 29-43, 2019
Pierre Huchant, Emmanuelle Saillard, Denis Barthou, Hugo Brunie and Patrick Carribault, PARCOACH Extension for a Full-Interprocedural Collectives Verification, 2nd International Workshop on Software Correctness for HPC Applications (Correctness), pages 69-76, 2018
Emmanuelle Saillard, Hugo Brunie, Patrick Carribault, and Denis Barthou, PARCOACH extension for Hybrid Applications with Interprocedural Analysis, In Tools for High Performance Computing 2015: Proceedings of the 9th International Workshop on Parallel Tools for High Performance Computing, pages 135-146, 2016
Emmanuelle Saillard, Patrick Carribault, and Denis Barthou, MPI Thread-Level Checking for MPI+OpenMP Applications, European Conference on Parallel Processing (EuroPar), pages 31-42, 2015
Julien Jaeger, Emmanuelle Saillard, Patrick Carribault, Denis Barthou, Correctness Analysis of MPI-3 Non-Blocking Communications in PARCOACH, European MPI Users’Group Meeting, Sep 2015, Bordeaux, France. EuroMPI’15
Emmanuelle Saillard, Patrick Carribault, and Denis Barthou, PARCOACH: Combining static and dynamic validation of MPI collective communications, Intl. Journal on High Performance Computing Applications (IJHPCA), 28(4):425-434, 2014
Emmanuelle Saillard, Patrick Carribault, and Denis Barthou, Static Validation of Barriers and Worksharing Constructs in OpenMP Applications, Proc. IntL. Workshop on OpenMP (IWOMP), volume 8766 of Lect. Notes in Computer Science, pages 73-86, 2014
Emmanuelle Saillard, Patrick Carribault, and Denis Barthou, Combining Static and Dynamic Validation of MPI Collective Communications, Proceedings of the European MPI User’s Group Meeting (EuroMPI), pages 117-122, 2013
The project is licensed under the LGPL 2.1 license.