Pith. sign in

REVIEW 4 major objections 4 minor 69 references

LLOR: Automated Repair of OpenMP Programs

T0 review · 4 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read LLOR automatically repairs OpenMP data races by converting each race the verifier finds into a constraint on where to place a barrier or ordered region.

desk verdict A genuinely first OpenMP repair tool with an honest evaluation, but the headline repair numbers are weaker than the '80%' claim because the only race oracle, LLOV, is itself unsound on some Fortran programs. read the letter →

arxiv 2411.14590 v2 pith:NG5I4GMV submitted 2024-11-21 cs.DC cs.SE

Utpal Bora , Saurabh Joshi , Gautam Muduganti , Ramakrishna Upadrasta This is my paper · ORCID
classification cs.DCcs.SE
keywords OpenMPdataraceautomatedprogramrepairbarrierplacementorderedregionLLVMIRC++Fortran
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

LLOR is presented as a tool that automatically repairs data race errors in OpenMP programs written in C, C++, or Fortran. The repair loop marks every read or write of a shared variable inside a parallel region (or a parallel for loop) with a Boolean 'barrier variable', then repeatedly verifies candidate programs; each data race the verifier reports becomes a constraint saying that at least one candidate barrier placement between the two conflicting accesses must be enabled. When the verifier finally reports the candidate safe, that candidate is the repaired program, and the same method can also remove barriers and ordered regions that turn out to be unnecessary. On a suite of 415 programs, the tool repaired 107 of the 147 programs in which the verifier found races, and it correctly flagged 8 programs where the programmer's synchronization could be dropped. The reason to care is that data races are hard to debug by hand and are typically fixed by trial-and-error placement of barriers, which this loop automates.

What carries the argument

The central object is the barrier variable, a Boolean attached at the LLVM IR level to every instruction that reads or writes a shared variable inside a parallel region or a parallel for loop. Setting the variable to true means the repair inserts a barrier before that instruction (in a parallel region) or wraps the statement in an ordered region (in a parallel for loop); false means no synchronization is added. Each data race trace is converted into a positive monotone clause, a disjunction of barrier variables with no negations, requiring that at least one candidate synchronization sits between the conflicting accesses. The repair loop alternates between solving the accumulated clauses, using either a polynomial minimal-hitting-set heuristic or a partial MaxSAT solver, and verifying the resulting candidate, so the machinery carries the whole argument: races become clauses, clauses become placements, and verification decides when to stop.

What would settle it

Run LLOR on a Fortran program of the form in Listing 1.8, where Flang's LLVM IR computes the write address through an offset and LLOV fails to see the race. If LLOV misses the race, LLOR will declare the original program safe and, where a barrier exists, may recommend removing it, which is an observable wrong repair. More generally, the central claim is falsified by any program for which a sound race checker reports a data race that LLOV does not report, since LLOR would then return a repaired program that still races.

Watch

Extended reading notes

Core claim

The paper's central claim is that repairing an OpenMP data race can be reduced to a constraint-solving problem over a set of barrier variables. In a parallel region, each statement that reads or writes a shared variable is given a Boolean that says whether a barrier should be inserted before it; in a parallel for loop, the same Boolean says whether the statement should be moved inside an ordered region. Every race the verifier reports generates a positive monotone clause over the barrier variables lying between the two conflicting accesses, and the solver must pick a minimal set of variables to enable. The tool iterates: solve the clauses, build a repair candidate with the chosen barriers or ordered region enabled, and ask the verifier whether the candidate is safe. If it is, the candidate is returned as the repaired program; if not, the new error trace is added as another clause and the loop continues. The paper further claims that this loop can also delete existing barriers and ordered regions when the verifier reports that they are not needed, and that the repair technique is independent of the specific verifier, so any OpenMP verifier could substitute for LLOV.

Load-bearing premise

The whole repair loop is only as trustworthy as the verifier it uses: if LLOV misses a data race, LLOR can fail to repair it or even recommend removing a synchronization that is actually needed, so the tool's guarantees collapse unless every race that matters is detected.

Editorial extensions

If this is right

  • OpenMP developers can hand a racy program to LLOR and receive a concrete suggested fix, namely where to put a barrier or which statements to enclose in an ordered region, instead of locating and testing placements by hand.
  • Because the instrumentation works on LLVM IR and the loop is verifier-agnostic, the same repair machinery should work for any OpenMP verifier and for any source language that compiles to LLVM IR, not only C, C++, and Fortran.
  • The barrier-removal mode gives programmers a way to clean up over-synchronized code: barriers and ordered regions that the verifier deems unnecessary can be dropped without losing the race-free property.
  • Programs whose races come from write-write conflicts on the same line, or from constructs like sections, simd, teams, and target, cannot be repaired by this technique; the paper classifies those as unsupported rather than claiming to fix them.
  • The solver choice matters in practice: the minimal-hitting-set strategy is faster but occasionally picks a different enabled barrier than MaxSAT would, and MaxSAT guarantees the fewest synchronization constructs when used at the end.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A direct extension would be to feed the same error-trace-to-clause loop with a different verifier, such as a dynamic race detector, to catch the Fortran cases LLOV misses; the paper's own experiments identify those misses as the reason for the three wrong barrier removals.
  • The static-pointer alias failure, where code updates through a pointer copied into a local variable, suggests a concrete improvement: instrument the LLVM IR copy instructions so that barrier variables propagate through address copies, which would likely repair several of the 16 programs LLOR could not fix.
  • The same counterexample-driven loop could be retargeted to other concurrency bugs a verifier can witness as traces, such as atomicity violations or deadlock, by changing what clause the error trace generates; the paper only claims data races, but the architecture does not rely on race-specific features beyond clause generation.
  • A user of LLOR in its current form should still run an independent race checker on the repaired program, because when the verifier misses a race the tool can silently return a program that still races or remove a needed barrier; the paper states this limitation explicitly for Fortran.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper presents LLOR, a tool that automatically repairs data race errors in OpenMP programs written in C/C++ and Fortran. The repair loop instruments LLVM IR to mark candidate barrier locations in parallel regions and candidate ordered-region statements in parallel for loops, then iteratively invokes the LLOV data race checker, generates positive monotone clauses from reported race traces, and solves the clause set with either an mhs or a MaxSAT strategy. The tool also removes existing barriers and ordered regions when they are deemed unnecessary. The evaluation covers 415 programs from DataRaceBench, Exascale, Rodinia, PRK, and a small self-built suite. The paper claims that LLOR is the only tool that can repair OpenMP data races and that it repaired more than 80% of the programs that had a valid data race error.

Significance. If the central claim holds, LLOR is a useful contribution: it is, to my knowledge, the first tool specialized to automatic repair of OpenMP data race errors, it is language-independent across C/C++ and Fortran, and it is evaluated on a large benchmark set with an available artifact. The paper is transparent about the dependence of its guarantees on LLOV and about concrete failure cases. The strength of the empirical claim, however, is weakened by the fact that the same unsound verifier is used both as the repair oracle and as the final validator, so the 107 counted successes are not independently confirmed race-free. The paper would be significantly strengthened by cross-checking repaired candidates with a different race detector or by explicitly reframing the results as repairs certified only with respect to LLOV.

major comments (4)
  1. [§5 and Table 2] The conclusion that LLOR repaired "more than 80% of the programs that had a valid data race error" is not supported by Table 2 as presented. Table 2 reports 147 programs in which LLOV identified data races, and 107 repaired programs, which is 72.8%. If the intended denominator excludes the 9 timeouts and/or the 15 programs unsupported by LLOR, that exclusion must be stated explicitly and justified, since those programs do have data races according to LLOV. As written, the claimed percentage is not derivable from the reported numbers.
  2. [§2.4 and §4.2] The soundness of every repaired program is certified only by LLOV, which the paper itself describes as neither sound nor complete. Because the same verifier is used inside the repair loop and as the final validator, a false negative by LLOV can cause LLOR to count a program as repaired when it still contains a race, or to remove a necessary barrier or ordered region. This failure mode is not hypothetical: Section 4.2 reports that LLOV misses data races in Fortran programs and that LLOR consequently recommends removing necessary synchronization in B05_incorrect_barrier.f95, B07_racefree.f95, and DRB110-ordered-orig-no.f95. The empirical claim that LLOR "fixes" data races therefore needs independent validation of at least a sample of the 107 repaired programs with another static or dynamic race detector, or the claims should be restricted to "repaired with respect to LLOV."
  3. [§2.4] The completeness argument is conditional on an unproven assumption that every data race that is fixable by synchronization can be fixed by one of the four construct changes considered: adding a barrier, creating an ordered region, or removing an existing barrier or ordered region. The proof states this only as a property of the input program P. This assumption is load-bearing for the completeness claim and should be stated explicitly as a limitation of the tool, especially because programs whose races can only be fixed by critical sections, atomics, or lock acquisition are outside the repair space.
  4. [§2.4] The termination proof claims that every newly generated clause c satisfies φ ̸=> c because "Verify will never result in an error trace that has already been encountered before." This is not self-evident: the same race between the same two source lines could reappear in a later repair candidate if the previously enabled synchronization does not actually affect that race. The proof needs a more careful argument for why an already implied clause cannot be generated again, or the termination argument should be weakened accordingly.
minor comments (4)
  1. [§2.4] The sentence "The technique behind LLOV is sound but not complete. However, LLOV is not sound because of programs like Listing 1.8" is contradictory; the first clause should probably read "is not sound but complete" or be rephrased to match the subsequent concession that LLOV is neither sound nor complete.
  2. [§4.2] The paper states that on manual inspection "LLOV was not detecting a data race, even if one existed." The manual inspection method is not described; specifying the ground truth used (e.g., which tool or reasoning established that a race exists) would improve reproducibility of this important observation.
  3. [§A.2, Listing 1.7] The discussion of Listing 1.7 notes that a same-line read-write race is split into two LLVM instructions but that the user must manually split the source line to insert the barrier. This manual step should be explicitly documented as a usability limitation of the output mechanism.
  4. [§4.1 and Table 1] The benchmark set includes 24 programs from the LLOR test suite, which is self-built. The paper reports this, but the aggregate success percentages would be more informative if they were also broken down by benchmark source, so readers can see the impact of the self-built suite on the headline numbers.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: LLOR's repair loop is a verifier-guided counterexample loop with explicitly conditional soundness; reliance on the authors' LLOV is an acknowledged dependency, not a definitional equivalence.

full rationale

LLOR's claimed derivation chain is: instrument candidate barrier/ordered-region placements, call LLOV on each candidate, turn each reported race trace into a positive monotone clause, solve the accumulated clauses, generate the next candidate, and stop when the verifier returns SAFE (Alg. 1, Sec. 2.3). The paper's soundness and completeness arguments (Sec. 2.4) are explicitly conditional: "Assuming that the verifier used in Verify is sound and the solver used in Solve is sound and complete, if Alg. 1 returns a repaired program Psol, Psol would not have any data races." That is a standard conditional theorem, not a circular one; the conclusion is not assumed as an input. The one genuinely load-bearing self-citation is LLOV [12], used both inside the loop and as final validator. This is a dependency and a limitation, and the paper is explicit about it: "Since LLOV is neither sound nor complete, LLOR cannot guarantee soundness or completeness." Section 4.2 documents concrete Fortran false negatives (e.g., Listing 1.8) where LLOR recommends removing necessary barriers in three benchmarks. Because a repaired count of 107 is simply the number of runs on which LLOV returned SAFE, the empirical claim of repairing "data race errors" is only as strong as LLOV's verdicts; but that is an evaluation weakness, not a circular reduction of the kind where a fitted parameter is renamed a prediction or a uniqueness theorem is imported from the authors. No equation or definition in the paper equates the output with the input, and the algorithm is not benchmarked only on self-built tests: 391 of 415 programs come from DataRaceBench, Exascale, Rodinia, and PRK. Therefore no significant circularity is present.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

No free parameters are fitted. The central claim depends on the three assumptions above; two of them are explicitly acknowledged in the paper as not always satisfied.

assumptions (3)
  • domain assumption The verifier (LLOV) detects all data races that matter for the repair and confirms when a repaired program is race-free.
    Invoked in Algorithm 1 and the soundness proof in Section 2.4. The paper admits LLOV is neither sound nor complete and gives a Fortran counterexample (Listings 1.8 and 1.9) where LLOV misses a race.
  • ad hoc to paper Every data race that is fixable by synchronization can be fixed by one of the four construct changes LLOR considers: adding a barrier in a parallel region, creating an ordered region in a parallel for loop, or removing an existing barrier or ordered region.
    This scoping is stated in Sections 1 and 2.2 and excludes sections, simd, tasks, and other OpenMP constructs; the completeness argument of Algorithm 1 depends on it.
  • ad hoc to paper The instrumentation phase identifies every instruction that accesses a shared variable, including through pointer aliases.
    Section 4.2 and Appendix A.2 (Listings 1.5 and 1.6) show a pointer-increment case where this fails, so the assumption is violated in practice for some programs.

how reviews work

0 comments
Cite this review

Pith. "Pith review of LLOR: Automated Repair of OpenMP Programs." pith.science (2026). https://pith.science/paper/NG5I4GMV

@misc{pith2026241114590,
  author       = {Pith},
  title        = {Pith review of: LLOR: Automated Repair of OpenMP Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/NG5I4GMV}},
  note         = {Machine review of arXiv:2411.14590}
}
read the original abstract

In this paper, we present a technique for repairing data race errors in parallel programs written in C/C++ and Fortran using the OpenMP API. Our technique can also remove barriers that are deemed unnecessary for correctness. We implement these ideas in our tool called LLOR, which takes a language-independent approach to provide appropriate placements of synchronization constructs to avoid data races. To the best of our knowledge, LLOR is the only tool that can repair parallel programs that use the OpenMP API. We showcase the capabilities of LLOR by performing extensive experiments on 415 parallel programs.

Figures

Figures reproduced from arXiv: 2411.14590 by the authors.

Figure 1
Figure 1. Architecture of LLOR showcasing the various components involved in the repair process. The solid lines represent the source code, and the dashed lines represent the information flow between the components. If these instructions are in a parallel region, LLOR generates possible repair candidates by inserting barriers in front of these instructions. If these instruc￾tions are in a parallel for loop, LLOR generates pos… view at source ↗
Figure 2
Figure 2. mhs vs. MaxSAT Runtime in milliseconds The behavior of the solver also impacts which strategy performs better. Consider the clause a ∨ b. The mhs solver could choose a to be the solution, and the MaxSAT solver could choose b to be the solution. Both of the solutions are valid for the clause, but choosing b could fix the program, and choosing a may not, thus forcing more iterations. Because of these reasons, we notic… view at source ↗
Figure 3
Figure 3. shows the size of the programs in terms of lines of code. The average number of lines of code for the test suite is 694.92, and the median is 44. 58 programs have more than 100 lines of code, and 184 programs have more than 50 lines of code. 0 50 100 150 200 250 > 100 81 − 100 61 − 80 41 − 60 21 − 40 <= 20 58 5 67 87 177 21 Kernel Count Lines of Code [PITH_FULL_IMAGE:figures/full_fig_p017_3.png] view at source ↗
Figures from the paper (5 more)
Figure 5
Figure 5. Figure 5: Barrier Variables The instrumentation component of LLOR works with LLVM IR and not on the source code. A line of source code could result in zero (e.g., code comments) [PITH_FULL_IMAGE:figures/full_fig_p017_5.png]
Figure 6
Figure 6. Figure 6: LLOR Commands [PITH_FULL_IMAGE:figures/full_fig_p021_6.png]
Figure 7
Figure 7. Figure 7: Sample Makefile LLOR also has the ability to repair programs that have multiple source files. The prerequisite for these programs is that there should be a makefile in the root folder with a target named llov. This target should generate the LLVM IR for the various sou…
Figure 8
Figure 8. Figure 8: Multifile Repair [PITH_FULL_IMAGE:figures/full_fig_p022_8.png]
Figure 9
Figure 9. Figure 9: LLOR Options A.4 OpenMP Verifiers As mentioned in Section 3.1, several static and dynamic tools have been proposed for identifying data races in OpenMP programs. Even though our tool uses LLOV as the verifier, in principle, the technique behind LLOR works for any verif…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

69 extracted references · 68 canonical work pages

  1. [1]

    In: SEFM 2015

    Amighi, A., Darabi, S., Blom, S., Huisman, M.: Specification and Verification of Atomic Operations in GPGPU Programs. In: SEFM 2015. pp. 69–83. Springer (2015) 3.1

    work page 2015

  2. [2]

    In: IPDPS 2016

    Atzeni, S., Gopalakrishnan, G., Rakamaric, Z., Ahn, D.H., Laguna, I., Schulz, M., Lee, G.L., Protze, J., M¨ uller, M.S.: ARCHER: Effectively Spotting Data Races in Large OpenMP Applications. In: IPDPS 2016. pp. 53–62. IEEE Computer Society (2016) A.4

    work page 2016

  3. [3]

    In: IPDPS 2018

    Atzeni, S., Gopalakrishnan, G., Rakamaric, Z., Laguna, I., Lee, G.L., Ahn, D.H.: SWORD: A Bounded Memory-Overhead Detector of OpenMP Data Races in Pro- duction Runs. In: IPDPS 2018. pp. 845–854. IEEE Computer Society (2018) 2.1, 3.1, A.4

    work page 2018

  4. [4]

    In: FMCO 2005

    Barnett, M., Chang, B.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modu- lar Reusable Verifier for Object-Oriented Programs. In: FMCO 2005. pp. 364–387. Springer (2005) 3.3

    work page 2005

  5. [5]

    In: IWOMP 2011

    Basupalli, V., Yuki, T., Rajopadhye, S.V., Morvan, A., Derrien, S., Quinton, P., Wonnacott, D.: ompVerify: Polyhedral Analysis for the OpenMP Programmer. In: IWOMP 2011. pp. 37–53. Springer (2011) 2.1, 3.1, A.4

    work page 2011

  6. [6]

    TOPLAS 37(3), 10:1–10:49 (2015) 3.1

    Betts, A., Chong, N., Donaldson, A.F., Ketema, J., Qadeer, S., Thomson, P., Wick- erson, J.: The Design and Implementation of a Verification Technique for GPU Kernels. TOPLAS 37(3), 10:1–10:49 (2015) 3.1

    work page 2015

  7. [7]

    In: OOPSLA 2012

    Betts, A., Chong, N., Donaldson, A.F., Qadeer, S., Thomson, P.: GPUVerify: a verifier for GPU kernels. In: OOPSLA 2012. pp. 113–132. ACM (2012) 3.1

    work page 2012

  8. [8]

    In: TACAS 2015

    Bjørner, N., Phan, A., Fleckenstein, L.: νZ - An Optimizing SMT Solver. In: TACAS 2015. pp. 194–199. Springer (2015) 4.1

    work page 2015

Show all 69 references
  1. [9]

    Blackshear, S., Gorogiannis, N., O’Hearn, P.W., Sergey, I.: RacerD: Compositional Static Race Detection. Proc. ACM Program. Lang. 2(OOPSLA), 144:1–144:28 (2018) 3.1

    2018

  2. [10]

    Science of Computer Programming 95, 376–388 (2014) 3.1

    Blom, S., Huisman, M., Mihelcic, M.: Specification and verification of GPGPU programs. Science of Computer Programming 95, 376–388 (2014) 3.1

    2014

  3. [11]

    IEEE Trans

    Boehm, B.W., Papaccio, P.N.: Understanding and Controlling Software Costs. IEEE Trans. Software Eng. 14(10), 1462–1477 (1988) 1

    1988

  4. [12]

    ACM Trans

    Bora, U., Das, S., Kukreja, P., Joshi, S., Upadrasta, R., Rajopadhye, S.V.: LLOV: A Fast Static Data-Race Checker for OpenMP Programs. ACM Trans. Archit. Code Optim. 17(4), 35:1–35:26 (2020) 2.1, 2.1, 3.1

    2020

  5. [13]

    In: CA V 2011

    Cern´ y, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quan- titative Synthesis for Concurrent Programs. In: CA V 2011. pp. 243–259. Springer (2011) 3.2

    2011

  6. [14]

    In: ICSE 2011

    Chandra, S., Torlak, E., Barman, S., Bod ´ ık, R.: Angelic debugging. In: ICSE 2011. pp. 121–130. ACM (2011) 3.2

    2011

  7. [15]

    In: LCPC 2016

    Chatarasi, P., Shirako, J., Kong, M., Sarkar, V.: An Extended Polyhedral Model for SPMD Programs and Its Use in Static Data Race Detection. In: LCPC 2016. pp. 106–120. Springer (2016) 3.1, A.4

    2016

  8. [16]

    In: IMPACT 2016

    Chatarasi, P., Shirako, J., Sarkar, V.: Static Data Race Detection for SPMD Pro- grams via an Extended Polyhedral Representation. In: IMPACT 2016. vol. 16 (2016) 2.1, 3.1, A.4

    2016

  9. [17]

    In: IISWC 2009

    Che, S., Boyer, M., Meng, J., Tarjan, D., Sheaffer, J.W., Lee, S., Skadron, K.: Rodinia: A Benchmark Suite for Heterogeneous Computing. In: IISWC 2009. pp. 44–54. IEEE Computer Society (2009) 4.1 LLOR: Automated Repair of OpenMP Programs 15

    2009

  10. [18]

    IEEE Computational Science and Engineering 5(1), 46–55 (1998) 1

    Dagum, L., Menon, R.: OpenMP: An Industry-Standard API for Shared-Memory Programming. IEEE Computational Science and Engineering 5(1), 46–55 (1998) 1

    1998

  11. [19]

    In: ESOP 2010

    Deshmukh, J.V., Ramalingam, G., Ranganath, V.P., Vaswani, K.: Logical Con- currency Control from Sequential Proofs. In: ESOP 2010. pp. 226–245. Springer (2010) 3.2

    2010

  12. [20]

    In: PADD 1991

    Dinning, A., Schonberg, E.: Detecting Access Anomalies in Programs with Critical Sections. In: PADD 1991. pp. 85–96. ACM (1991) 3.1

    1991

  13. [21]

    In: IWOMP 2013

    Eichenberger, A.E., Mellor-Crummey, J.M., Schulz, M., Wong, M., Copty, N., Di- etrich, R., Liu, X., Loh, E., Lorenz, D.: OMPT: An OpenMP Tools Application Programming Interface for Performance Analysis. In: IWOMP 2013. pp. 171–185. Springer (2013) 2.1, 3.1, A.4

    2013

  14. [22]

    In: SOSP 2003

    Engler, D.R., Ashcraft, K.: RacerX: Effective, Static Detection of Race Conditions and Deadlocks. In: SOSP 2003. pp. 237–252. ACM (2003) 3.1

    2003

  15. [23]

    In: SAT 2006

    Fu, Z., Malik, S.: On Solving the Partial MAX-SAT Problem. In: SAT 2006. pp. 252–265. Springer (2006) 2.3, 2.4

    2006

  16. [24]

    In: CA V 2006

    Griesmayer, A., Bloem, R., Cook, B.: Repair of Boolean Programs with an Appli- cation to C. In: CA V 2006. pp. 358–371. Springer (2006) 3.2

    2006

  17. [25]

    In: PLDI 2011

    Jin, G., Song, L., Zhang, W., Lu, S., Liblit, B.: Automated atomicity-violation fixing. In: PLDI 2011. pp. 389–400. ACM (2011) 3.2

    2011

  18. [26]

    In: CA V

    Jobstmann, B., Griesmayer, A., Bloem, R.: Program Repair as a Game. In: CA V

  19. [27]

    Journal of Computer and System Sciences 9(3), 256–278 (1974) 2.3

    Johnson, D.S.: Approximation Algorithms for Combinatorial Problems. Journal of Computer and System Sciences 9(3), 256–278 (1974) 2.3

    1974

  20. [28]

    In: FM 2015

    Joshi, S., Kroening, D.: Property-Driven Fence Insertion Using Reorder Bounded Model Checking. In: FM 2015. pp. 291–307. Springer (2015) 3.2

    2015

  21. [29]

    CoRR abs/1403.1749 (2014) 3.2

    Joshi, S., Lal, A.: Automatically finding atomic regions for fixing bugs in Concur- rent programs. CoRR abs/1403.1749 (2014) 3.2

    2014 arXiv

  22. [30]

    In: VMCAI 2021

    Joshi, S., Muduganti, G.: GPURepair: Automated Repair of GPU Kernels. In: VMCAI 2021. pp. 401–414. Springer (2021) 3.2, 3.3

    2021

  23. [31]

    In: IPDPS 2012

    Joshi, S., Shyamasundar, R.K., Aggarwal, S.K.: A New Method of MHP Anal- ysis for Languages with Dynamic Barriers. In: IPDPS 2012. pp. 519–528. IEEE Computer Society (2012) 3.1

    2012

  24. [32]

    https://github.com/ParRes/Kernels, [Online; accessed 30-September-2024] 4.1

    Kernels, P.R.: Parallel Research Kernels. https://github.com/ParRes/Kernels, [Online; accessed 30-September-2024] 4.1

    2024

  25. [33]

    Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21(7), 558–565 (1978) 3.1

    1978

  26. [34]

    In: CGO 2004

    Lattner, C., Adve, V.S.: LL VM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: CGO 2004. pp. 75–88. IEEE Computer Society (2004) 2.1, 3.1

    2004

  27. [35]

    In: FSE 2010

    Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel func- tions. In: FSE 2010. pp. 187–196. ACM (2010) 3.1

    2010

  28. [36]

    In: PPOPP 2012

    Li, G., Li, P., Sawaya, G., Gopalakrishnan, G., Ghosh, I., Rajan, S.P.: GKLEE: concolic verification and test generation for GPUs. In: PPOPP 2012. pp. 215–224. ACM (2012) 3.1

    2012

  29. [37]

    In: SC 2017

    Liao, C., Lin, P., Asplund, J., Schordan, M., Karlin, I.: DataRaceBench: A Bench- mark Suite for Systematic Evaluation of Data Race Detection Tools. In: SC 2017. p. 11. ACM (2017) 4.1

    2017

  30. [38]

    https://github.com/cs17resch01003/llor, [Online; accessed 30-September-2024] 4, A.3, A.3 16 Bora, Joshi, Muduganti et al

    LLOR: LLOR Github Repository. https://github.com/cs17resch01003/llor, [Online; accessed 30-September-2024] 4, A.3, A.3 16 Bora, Joshi, Muduganti et al

    2024

  31. [39]

    https://doi.org/10.5281/zenodo

    LLOR: LLOR VMCAI 2025 Artifacts. https://doi.org/10.5281/zenodo. 13886253, [Online; accessed 30-September-2024] 4

    2025 doi

  32. [40]

    In: ICST 2011

    Malik, M.Z., Siddiqui, J.H., Khurshid, S.: Constraint-Based Program Debugging Using Data Structure Repair. In: ICST 2011. pp. 190–199. IEEE Computer Society (2011) 3.2

    2011

  33. [41]

    CoRR abs/0712.1097 (2007) 2.4

    Marques-Silva, J., Planes, J.: On Using Unsatisfiability for Solving Maximum Sat- isfiability. CoRR abs/0712.1097 (2007) 2.4

    2007 arXiv

  34. [42]

    In: SC 1991

    Mellor-Crummey, J.M.: On-the-fly Detection of Data Races for Programs with Nested Fork-Join Parallelism. In: SC 1991. pp. 24–33. ACM (1991) 3.1

    1991

  35. [43]

    https://docs

    Microsoft: Microsoft Azure Fsv2-Series Virtual Machine Sizes. https://docs. microsoft.com/en-us/azure/virtual-machines/fsv2-series , [Online; accessed 30-September-2024] 4.1

    2024

  36. [44]

    Alves, E.H., da Silva, I., Ismail, H., Cordeiro, L.C., de Lima Filho, E.B.: ESBMC-GPU A context-bounded model checking tool to verify CUDA programs

    Monteiro, F.R., da S. Alves, E.H., da Silva, I., Ismail, H., Cordeiro, L.C., de Lima Filho, E.B.: ESBMC-GPU A context-bounded model checking tool to verify CUDA programs. Science of Computer Programming 152, 63–69 (2018) 3.1

    2018

  37. [45]

    In: TACAS 2008

    de Moura, L.M., Bjørner, N.: Z3: An Efficient SMT Solver. In: TACAS 2008. pp. 337–340. Springer (2008) 4.1, A.4

    2008

  38. [46]

    In: MICRO 2010

    Muzahid, A., Otsuki, N., Torrellas, J.: AtomTracker: A Comprehensive Approach to Atomic Region Inference and Violation Detection. In: MICRO 2010. pp. 287–

    2010

  39. [47]

    Nethercote, N., Seward, J.: Valgrind: A Program Supervision Framework. In: R V

  40. [48]

    Netzer, R.: Race Condition Detection for Debugging Shared-Memory Parallel Pro- grams. Ph.D. thesis, University of Wisconsin Madison (1991) 3.1

    1991

  41. [49]

    In: OSDI 1996

    Perkovic, D., Keleher, P.J.: Online Data-Race Detection via Coherency Guarantees. In: OSDI 1996. pp. 47–57. ACM (1996) 3.1

    1996

  42. [50]

    TOPLAS 33(1), 3:1–3:55 (2011) 3.1

    Pratikakis, P., Foster, J.S., Hicks, M.: LOCKSMITH: Practical Static Race Detec- tion for C. TOPLAS 33(1), 3:1–3:55 (2011) 3.1

    2011

  43. [51]

    https://proxyapps.exascaleproject

    Project, E.C.: ECP Proxy Applications. https://proxyapps.exascaleproject. org/, [Online; accessed 30-September-2024] 4.1

    2024

  44. [52]

    In: PACT 2011

    Quinlan, D., Liao, C.: The ROSE source-to-source compiler infrastructure. In: PACT 2011. vol. 2011, p. 1 (2011) A.4

    2011

  45. [53]

    ACM Trans

    Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: A Dynamic Data Race Detector for Multithreaded Programs. ACM Trans. Comput. Syst. 15(4), 391–411 (1997) 3.1

    1997

  46. [54]

    In: JMLC 2003

    Schordan, M., Quinlan, D.J.: A Source-to-Source Architecture for User-Defined Optimizations. In: JMLC 2003. pp. 214–223. Springer (2003) A.4

    2003

  47. [55]

    In: WBIA 2009

    Serebryany, K., Iskhodzhanov, T.: ThreadSanitizer: Data race detection in practice. In: WBIA 2009. pp. 62–71 (2009) A.4

    2009

  48. [56]

    In: R V 2011

    Serebryany, K., Potapenko, A., Iskhodzhanov, T., Vyukov, D.: Dynamic Race De- tection with LL VM Compiler - Compile-Time Instrumentation for ThreadSanitizer. In: R V 2011. pp. 110–114. Springer (2011) A.4

    2011

  49. [57]

    http://valgrind.org/docs/ manual/drd-manual.html, [Online; accessed 30-September-2024] A.4

    Valgrind-project: DRD: A Thread Error Detector. http://valgrind.org/docs/ manual/drd-manual.html, [Online; accessed 30-September-2024] A.4

    2024

  50. [58]

    http://valgrind.org/ docs/manual/hg-manual.html, [Online; accessed 30-September-2024] 2.1, 3.1, A.4

    Valgrind-project: Helgrind: A Thread Error Detector. http://valgrind.org/ docs/manual/hg-manual.html, [Online; accessed 30-September-2024] 2.1, 3.1, A.4

    2024

  51. [59]

    In: POPL 2010

    Vechev, M.T., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchroniza- tion. In: POPL 2010. pp. 327–338. ACM (2010) 3.2

    2010

  52. [60]

    In: FSE 2007

    Voung, J.W., Jhala, R., Lerner, S.: RELAY: Static Race Detection on Millions of Lines of Code. In: FSE 2007. pp. 205–214. ACM (2007) 3.1 LLOR: Automated Repair of OpenMP Programs 17

    2007

  53. [61]

    In: CORRECTNESS

    Ye, F., Schordan, M., Liao, C., Lin, P., Karlin, I., Sarkar, V.: Using Polyhedral Analysis to Verify OpenMP Applications are Data Race Free. In: CORRECTNESS

  54. [62]

    omp . h

    Yuki, T., Gupta, G., Kim, D., Pathan, T., Rajopadhye, S.V.: AlphaZ: A System for Design Space Exploration in the Polyhedral Model. In: LCPC 2012. pp. 17–31. Springer (2012) A.4 Appendix A More Experiments and Results A.1 Source Code Size Fig. 3 shows the size of the programs i...

    2012

  55. [67]

    The thread num is retrieved

  56. [68]

    The data array is read

  57. [69]

    3 and Tab

    The data array is written into Tab. 3 and Tab. 4 illustrate the LL VM IR instructions generated for these three steps for Listing 1.8 and Listing 1.9, respectively. The LL VM IR generated byClang and Flang for the first two steps are similar. However, the third step (writing i...

  58. [297]

    IEEE Computer Society (2010) 3.2

    2010

  59. [2003]

    pp. 44–66. Elsevier (2003) A.4

    2003

  60. [2005]

    pp. 226–238. Springer (2005) 3.2

    2005

  61. [2018]

    pp. 42–50. IEEE (2018) 2.1, 3.1, A.4

    2018

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.