LLOV

LLOV: un controlador de carrera de datos estático rápido para programas OpenMP.

LLOV representa el verificador LLVM OpenMP. Es una herramientas de detección de carrera de datos estáticas en LLVM para programas OpenMP. LLOV puede detectar carreras de datos en los programas OpenMP V4.5 escritos en C/C ++ y Fortran.

LLOV utiliza técnicas de compilación poliédrica para detectar condiciones de carrera en el momento de la compilación.

A diferencia de otra herramienta de detección de carreras, LLOV puede marcar una región de código como la carrera de datos libre.

Cómo ejecutar LLOV

Si OpenMP no está instalado en su sistema o la ruta no se establece correctamente, puede señalar el encabezado incluido y LIB con banderas del compilador adicional. -Iinclude/ -Llib/

Ejecutando el código LLOV en OpenMP C/C ++ desde Clang desde 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

Ejecutando el código LLOV en OpenMP C/C ++ desde OPT 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

Ejecutando LLOV en el código 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

Para obtener más ejemplos de Fortran con condiciones de carrera conocidas, consulte nuestro Microbenchmark DataraceBench Fortran

Autores

UTPAL BORA [email protected].

Créditos

Las siguientes personas contirigieron a LLov de diferentes maneras.
Pankaj Kukreja <[email protected]>
Santanu das <[email protected]>
Sitio web de Saurabh Joshi
Sitio web de Ramakrishna Upadrasta
Sitio web de Sanjay Rajopadhye

Liberar

La fuente de LLOV se lanzará pronto bajo la licencia BSD.

Contenedor de acopolador

Registro de Docker: Hub.docker.com
Repositorio: LLVM
Etiqueta: Llov

Docker Image Contians Llov, junto con las siguientes herramientas de detección de carrera-
TSAN-LLVM, Archer, Sword, Helgrind y Valgrind Drd.

Hay tres puntos de referencia OpenMP para la experimentación.
DataraceBench v1.2,
DataraceBench fortran, y
OMPSCR v2.0.

Cómo citar LLov en una publicación

 @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}
}

Limitaciones actuales

Las siguientes son las limitaciones de la versión actual de LLOV.

• No admite la sincronización explícita en OpenMP. Esto podría dar lugar a casos de FN para programas con dependencias en los SCOP.
• No maneja el flujo de control dinámico.
• No admite construcciones de descarga de objetivos.
• No admite tareas OpenMP.
• No se puede manejar accesos irregulares (a [b [i]]).
• Podría producir FP para el código de mosaico y/o paralelo generado por herramientas automáticas de generación de código como Plutón, Polly y Polyopt.
• Podría producir FP para la construcción de secciones OpenMP.
• Las llamadas de función dentro de las construcciones OpenMP se manejan solo si la función se puede ingresar.
• Para algunos casos, el mapeo de números de línea de origen en Polly no se conserva. Para esos casos, la raza se marca en el número de línea de bucle correspondiente.

Contacto

Si tiene alguna consulta, comuníquese con "Utpal Bora" <[email protected]>.
Por favor, presente un error si encuentra que el comprobante de carreras no funciona según sea necesario.

Saludos,
Utpal