Git Product home page Git Product logo

liangminghuang / llov Goto Github PK

View Code? Open in Web Editor NEW

This project forked from utpalbora/llov

0.0 0.0 0.0 303.17 MB

LLOV: LLVM OpenMP Verifier - : A Fast Static Data-Race Checker for OpenMP Programs

License: Other

Shell 0.01% JavaScript 0.05% C++ 85.50% Python 0.38% Perl 0.23% C 12.25% PHP 0.01% Emacs Lisp 0.04% Assembly 0.56% AppleScript 0.01% CSS 0.02% Pawn 0.01% CMake 0.91% Roff 0.03%

llov's Introduction

LLOV: A Fast Static Data-Race Checker for OpenMP Programs.

LLOV stands for LLVM OpenMP Verifier. It is a static data race detection tools in LLVM for OpenMP Programs. LLOV can detect data races in OpenMP v4.5 programs written in C/C++ and FORTRAN.

LLOV uses polyhedral compilation techniques to detect race conditions at compile time.

Unlike other race detection tool, LLOV can mark a region of code as Data Race Free.

How to Run LLOV

If OpenMP is not installed on your system or the path is not properly set, you can point to the included header & lib with additional compiler flags. -Iinclude/ -Llib/

Running LLOV on OpenMP C/C++ code from 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

Running LLOV on OpenMP C/C++ code from 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

Running LLOV on OpenMP FORTRAN code

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

For more FORTRAN examples with known race conditions, check out our microbenchmark DataRaceBench FORTRAN

Authors

Utpal Bora [email protected].

Credits

The following people contirbuted to LLOV in different ways.
Pankaj Kukreja <[email protected]>
Santanu Das <[email protected]>
Saurabh Joshi website
Ramakrishna Upadrasta website
Sanjay Rajopadhye website

Release

Source of LLOV will be released soon under BSD license.

Docker container

Docker Registry: hub.docker.com
repository: llvm
tag: llov

The docker image contians LLOV, along with the following race detection tools-
TSan-LLVM, Archer, SWORD, Helgrind, and Valgrind DRD.

There are three OpenMP benchmarks for experimentation-
DataRaceBench v1.2,
DataRaceBench FORTRAN, and
OmpSCR v2.0.

How to cite LLOV in a 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}
}

Current Limitations

Following are the limitations of the current version of LLOV.

  • Does not support explicit synchronization in OpenMP. This might result in FN cases for programs with dependences across SCoPs.
  • Does not handle dynamic control flow.
  • Does not support target offloading constructs.
  • Does not support OpenMP tasks.
  • Can not handle irregular accesses (a[b[i]]).
  • Might produce FP for tiled and/or parallel code generated by automatic code generation tools such as Pluto, Polly and PolyOPT.
  • Might produce FP for OpenMP sections construct.
  • Function calls within OpenMP constructs are handled only if the function can be inlined.
  • For some cases, source line number mapping in Polly is not preserved. For those cases, race is flagged at the corresponding loop line number.

Contact

If you have any query, please contact "Utpal Bora" <[email protected]>.
Please file a bug if you find the race checker is not working as required.

Regards,
Utpal

llov's People

Contributors

utpalbora avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.