LLOV

LLOV: un vérificateur de race de données statique rapide pour les programmes OpenMP.

Llov signifie LLVM OpenMP Verifier. Il s'agit d'un outil de détection de race de données statique dans LLVM pour les programmes OpenMP. LLOV peut détecter les courses de données dans les programmes OpenMP V4.5 écrits en C / C ++ et FORTRAN.

Llov utilise des techniques de compilation polyédrique pour détecter les conditions de course au moment de la compilation.

Contrairement à d'autres outils de détection de course, LLOV peut marquer une région de code comme des données sans course.

Comment exécuter llov

Si OpenMP n'est pas installé sur votre système ou si le chemin n'est pas correctement défini, vous pouvez pointer vers l'en-tête et la lib inclus avec des indicateurs de compilateur supplémentaires. -Iinclude/ -Llib/

Exécution de Llov sur le code OpenMP C / C ++ de Clang

 ./bin/clang -Xclang -disable-O0-optnone -Xclang -load -Xclang ./lib/OpenMPVerify.so  
  -fopenmp -g test/1.race1.c
./bin/clang++ -Xclang -disable-O0-optnone -Xclang -load -Xclang ./lib/OpenMPVerify.so  
  -fopenmp -g test.cpp

Exécuter LLOV sur le code OpenMP C / C ++ de Opt

 ./bin/clang -fopenmp -S -emit-llvm -g test/1.race1.c -o test.ll
./bin/opt -mem2reg test.ll -S -o test.ssa.ll
./bin/opt -load ./lib/OpenMPVerify.so -openmp-forceinline 
  -inline -openmp-resetbounds test.ssa.ll -S -o test.resetbounds.ll
./bin/opt -load ./lib/OpenMPVerify.so 
  -disable-output 
  -openmp-verify 
  test.resetbounds.ll

Exécution Llov sur le code OpenMP FORTRAN

 flang -fopenmp -S -emit-llvm -g test.f95 -o test.ll
./bin/opt -O1 test.ll -S -o test.ssa.ll
./bin/opt -load ./lib/OpenMPVerify.so -openmp-forceinline 
  -inline -openmp-resetbounds test.ssa.ll -S -o test.resetbounds.ll
./bin/opt -load ./lib/OpenMPVerify.so 
  -disable-output 
  -openmp-verify 
  test.resetbounds.ll

Pour plus d'exemples de FORTRAN avec des conditions de course connues, consultez notre dataracebench de DataraceBench Fortran

Auteurs

Utpal Bora [email protected].

Crédits

Les personnes suivantes ont continué à Llov de différentes manières.
Pankaj Kukreja <[email protected]>
Santanu das <[email protected]>
Site Web de Saurabh Joshi
Site Web de Ramakrishna Upadrasta
Site Web de Sanjay Rajopadhye

Libérer

La source de LLOV sera bientôt publiée sous la licence BSD.

Récipient Docker

Docker Registry: hub.docker.com
Référentiel: LLVM
Tag: llov

L'image Docker Contians llov, ainsi que les outils de détection de course suivants-
Tsan-llvm, Archer, Sword, Helgrind et Valgrind DRD.

Il y a trois repères OpenMP pour l'expérimentation-
Dataracebench v1.2,
Dataracebench FORTRAN, et
Ompscr v2.0.

Comment citer Llov dans une publication

 @article{Bora/taco/2020,
  author = {Bora, Utpal and Das, Santanu and Kukreja, Pankaj and Joshi, Saurabh and Upadrasta, Ramakrishna and Rajopadhye, Sanjay},
  title = {{LLOV: A Fast Static Data-Race Checker for OpenMP Programs}},
  year = {2020},
  issue_date = {November 2020},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {17},
  number = {4},
  issn = {1544-3566},
  url = {https://doi.org/10.1145/3418597},
  doi = {10.1145/3418597},
  abstract = {In the era of Exascale computing, writing efficient parallel programs is indispensable, and, at the same time, writing sound parallel programs is very difficult. Specifying parallelism with frameworks such as OpenMP is relatively easy, but data races in these programs are an important source of bugs. In this article, we propose LLOV, a fast, lightweight, language agnostic, and static data race checker for OpenMP programs based on the LLVM compiler framework. We compare LLOV with other state-of-the-art data race checkers on a variety of well-established benchmarks. We show that the precision, accuracy, and the F1 score of LLOV is comparable to other checkers while being orders of magnitude faster. To the best of our knowledge, LLOV is the only tool among the state-of-the-art data race checkers that can verify a C/C++ or FORTRAN program to be data race free.},
  journal = {ACM Trans. Archit. Code Optim.},
  month = dec,
  articleno = {35},
  numpages = {26},
  keywords = {OpenMP, program verification, polyhedral compilation, static analysis, data race detection, shared memory programming}
}

Limitations actuelles

Voici les limites de la version actuelle de LLOV.

• Ne prend pas en charge la synchronisation explicite dans OpenMP. Cela peut entraîner des cas de FN pour les programmes avec des dépendances à travers les SCOPS.
• Ne gère pas le flux de contrôle dynamique.
• Ne prend pas en charge les constructions de déchargement cible.
• Ne prend pas en charge les tâches OpenMP.
• Ne peut pas gérer les accès irréguliers (a [b [i]]).
• Peut produire FP pour le code carrelé et / ou parallèle généré par des outils de génération de code automatiques tels que Pluton, Polly et Polyopt.
• Pourrait produire FP pour la construction de sections OpenMP.
• Les appels de fonction dans les constructions OpenMP ne sont gérés que si la fonction peut être inclinée.
• Pour certains cas, le mappage du numéro de ligne source dans Polly n'est pas conservé. Pour ces cas, la race est signalée au numéro de ligne de boucle correspondante.

Contact

Si vous avez une requête, veuillez contacter "utpal bora" <[email protected]>.
Veuillez déposer un bogue si vous trouvez que le vérificateur de course ne fonctionne pas selon les besoins.

Salutations,
Utpal