From 755eba2174ffc46baeb78ba2f189fd19a30555a0 Mon Sep 17 00:00:00 2001 From: Jan Siwiec <jan.siwiec@vsb.cz> Date: Tue, 17 Mar 2020 12:58:44 +0100 Subject: [PATCH] Update aislinn.md --- docs.it4i/software/debuggers/aislinn.md | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/docs.it4i/software/debuggers/aislinn.md b/docs.it4i/software/debuggers/aislinn.md index 1c9a0b064..127b89a1a 100644 --- a/docs.it4i/software/debuggers/aislinn.md +++ b/docs.it4i/software/debuggers/aislinn.md @@ -1,12 +1,12 @@ # Aislinn -* Aislinn is a dynamic verifier for MPI programs. For a fixed input it covers all possible runs with respect to nondeterminism introduced by MPI. It allows to detect bugs (for sure) that occurs very rare in normal runs. +* Aislinn is a dynamic verifier for MPI programs. For a fixed input, it covers all possible runs with respect to nondeterminism introduced by MPI. It allows to detect bugs that very rarely occur in normal runs. * Aislinn detects problems like invalid memory accesses, deadlocks, misuse of MPI, and resource leaks. -* Aislinn is open-source software; you can use it without any licensing limitations. +* Aislinn is an open-source software, so you can use it without any licensing limitations. * [Web page][a] of the project. !!! note - Aislinn is software developed at IT4Innovations and some parts are still considered experimental. If you have any questions or experienced any problems, contact the author: <mailto:stanislav.bohm@vsb.cz>. + Aislinn is developed at IT4Innovations and some parts are still considered experimental. If you have any questions or experience any problems, contact the author: <mailto:stanislav.bohm@vsb.cz>. ## Usage @@ -59,9 +59,9 @@ Now we compile the program by Aislinn implementation of MPI. There are `mpicc` f $ mpicc -g test.cpp -o test ``` -The `-g` flag is not necessary, but it puts more debugging information into the program, hence Aislinn may provide more detailed report. The command produces executable file `test`. +The `-g` flag is not necessary, but it puts more debugging information into the program, hence Aislinn may a provide more detailed report. The command produces an executable file `test`. -Now we run the Aislinn itself. The argument `-p 3` specifies that we want to verify our program for the case of three MPI processes +Now we run the Aislinn itself. The argument `-p 3` specifies that we want to verify our program for the case of three MPI processes: ```console $ aislinn -p 3 ./test @@ -71,13 +71,13 @@ $ aislinn -p 3 ./test ==AN== INFO: Report written into 'report.html' ``` -Aislinn found an error and produced HTML report. To view it, we can use any browser, e.g.: +Aislinn found an error and produced an HTML report. To view it, we can use any browser, for example: ```console $ firefox report.html ``` -At the beginning of the report there are some basic summaries of the verification. In the second part (depicted in the following picture), the error is described. +At the beginning of the report, there are some basic summaries of the verification. In the second part (depicted in the following picture), the error is described.  @@ -85,20 +85,20 @@ It shows us: * Error occurs in process 0 in test.cpp on line 16. * Stdout and stderr streams are empty. (The program does not write anything). -* The last part shows MPI calls for each process that occurs in the invalid run. The more detailed information about each call can be obtained by mouse cursor. +* The last part shows MPI calls for each process that occurs in the invalid run. More detailed information about each call can be obtained by hovering the mouse cursor over the respective MPI call. ### Limitations -Since the verification is a non-trivial process there are some of limitations. +Since the verification is a non-trivial process, there are some of limitations. * The verified process has to terminate in all runs, i.e. we cannot answer the halting problem. -* The verification is a computationally and memory demanding process. We put an effort to make it efficient and it is an important point for further research. However covering all runs will be always more demanding than techniques that examines only a single run. The good practise is to start with small instances and when it is feasible, make them bigger. The Aislinn is good to find bugs that are hard to find because they occur very rarely (only in a rare scheduling). Such bugs often do not need big instances. +* The verification is a computationally and memory demanding process. We put an effort to make it efficient and it is an important point for further research. However covering all runs will always be more demanding than techniques that examine only a single run. The good practice is to start with small instances and when it is feasible, make them bigger. Aislinn is good for finding bugs that are hard to find because they occur very rarely (only in a rare scheduling). Such bugs often do not need big instances. * Aislinn expects that your program is a "standard MPI" program, i.e. processes communicate only through MPI, the verified program does not interacts with the system in some unusual ways (e.g. opening sockets). There are also some limitations bounded to the current version and they will be removed in the future: -* All files containing MPI calls have to be recompiled by MPI implementation provided by Aislinn. The files that does not contain MPI calls, they do not have to recompiled. Aislinn MPI implementation supports many commonly used calls from MPI-2 and MPI-3 related to point-to-point communication, collective communication, and communicator management. Unfortunately, MPI-IO and one-side communication is not implemented yet. +* All files containing MPI calls have to be recompiled by MPI implementation provided by Aislinn. The files that do not contain MPI calls, do not have to be recompiled. Aislinn MPI implementation supports many commonly used calls from MPI-2 and MPI-3 related to point-to-point communication, collective communication, and communicator management. Unfortunately, MPI-IO and one-side communication is not implemented yet. * Each MPI can use only one thread (if you use OpenMP, set OMP_NUM_THREADS to 1). -* There are some limitations for using files, but if the program just reads inputs and writes results, it is ok. +* There are some limitations for using files, but if the program just reads inputs and writes results, it is OK. [a]: http://verif.cs.vsb.cz/aislinn/ -- GitLab