nach oben

Formal Methods in System Design

26.05.2023

Memory access protocols: certified data-race freedom for GPU kernels

verfasst von: Tiago Cogumbreiro, Julien Lange, Dennis Liew, Hannah Zicarelli

Erschienen in: Formal Methods in System Design

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

GPUs offer parallelism as a commodity, but they are difficult to program correctly. Static analyzers that guarantee data-race freedom (DRF) are essential to help programmers establish the correctness of their programs (kernels). However, existing approaches produce too many false alarms and struggle to handle larger programs. To address these limitations we formalize a novel compositional analysis for DRF, based on memory access protocols. These protocols are behavioral types that codify the way threads interact over shared memory. Our work includes fully mechanized proofs of our theoretical results, the first mechanized proofs in the field of DRF analysis for GPU kernels. Our theory is implemented in Faial, a tool that outperforms the state-of-the-art. Notably, it can correctly verify at least \(1.42\times \) more real-world kernels, and it exhibits a linear growth in 4 out of 5 experiments, while others grow exponentially in all 5 experiments.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

The acronym DRF should not be confused with acronyms used in memory models, such as DRF0 [21], DRF1 [22], or DRFX [23].

https://github.com/mc-imperial/gpuverify/releases/tag/2018-03-22.

http://formalverification.cs.utah.edu/PUG/distributions/pug-v0.2_x64.tar.gz.

https://github.com/Geof23/Gklee/tree/77214669c83ac2f20802299df61940f2dd91360c.

Nguyen G, Dlugolinsky S, Bobák M, Tran V, López García Á, Heredia I, Malík P, Hluchý L (2019) Machine learning and deep learning frameworks and libraries for large-scale data mining: a survey. Artif Intell Rev 52(1):77–124. https://doi.org/10.1007/s10462-018-09679-zCrossRef

Stone JE, Hardy DJ, Ufimtsev IS, Schulten K (2010) GPU-accelerated molecular modeling coming of age. J Mol Graph Model 29(2):116–125. https://doi.org/10.1016/j.jmgm.2010.06.010CrossRef

Dematté L, Prandi D (2010) GPU computing for systems biology. Brief Bioinform 11(3):323–333. https://doi.org/10.1093/bib/bbq006CrossRef

Shi L, Liu W, Zhang H, Xie Y, Wang D (2012) A survey of GPU-based medical image computing techniques. Quant Imaging Med Surg 2:188–206. https://doi.org/10.3978/j.issn.2223-4292.2012.08.02CrossRef

Chajan E, Schulte-Tigges J, Reke M, Ferrein A, Matheis D, Walter T (2021) GPU based model-predictive path control for self-driving vehicles. In: Proceedings of IV. IEEE, Piscataway, NJ, USA, pp 1243–1248. https://doi.org/10.1109/IV48863.2021.9575619

Kalaiselvi T, Sriramakrishnan P, Somasundaram K (2017) Survey of using GPU CUDA programming model in medical image analysis. Inform Med Unlocked 9:133–144. https://doi.org/10.1016/j.imu.2017.08.001CrossRef

Li G, Li P, Sawaya G, Gopalakrishnan G, Ghosh I, Rajan SP (2012) GKLEE: concolic verification and test generation for GPUs. In: Proceedings of the PPoPP, vol 47. ACM, New York, NY, USA, pp 215–224. https://doi.org/10.1145/2370036.2145844

Li P, Li G, Gopalakrishnan G (2014) Practical symbolic race checking of GPU programs. In: Proceedings of the SC. IEEE, Piscataway, NJ, USA, pp 179–190. https://doi.org/10.1109/SC.2014.20

Pereira P, Albuquerque H, Marques H, Silva I, Carvalho C, Cordeiro L, Santos V, Ferreira R (2016) Verifying CUDA programs using SMT-based context-bounded model checking. In: Proceedings of SAC. ACM, New York, NY, USA, pp 1648–1653. https://doi.org/10.1145/2851613.2851830

10.

Betts A, Chong N, Donaldson AF, Ketema J, Qadeer S, Thomson P, Wickerson J (2015) The design and implementation of a verification technique for GPU kernels. Trans Program Lang Syst 37(3):1–49. https://doi.org/10.1145/2743017CrossRef

11.

Kojima K, Imanishi A, Igarashi A (2018) Automated verification of functional correctness of race-free GPU programs. J Autom Reason 60(3):279–298. https://doi.org/10.1007/s10817-017-9428-2MathSciNetCrossRefMATH

12.

Blom S, Huisman M, Mihelčić M (2014) Specification and verification of GPGPU programs. Sci Comput Program 95(P3):376–388. https://doi.org/10.1016/j.scico.2014.03.013CrossRef

13.

Li G, Gopalakrishnan G (2010) Scalable SMT-based verification of GPU kernel functions. In: Proceedings of the FSE. ACM, New York, NY, USA, pp 187–196. https://doi.org/10.1145/1882291.1882320

14.

Wu M, Ouyang Y, Zhou H, Zhang L, Liu C, Zhang Y (2020) Simulee: detecting CUDA synchronization bugs via memory-access modeling. In: Proceedings of the ICSE. ACM, New York, NY, USA, pp 937–948. https://doi.org/10.1145/3377811.3380358

15.

Ancona D, Bono V, Bravetti M, Campos J, Castagna G, Deniélou P-M, Gay SJ, Gesbert N, Giachino E, Hu R, Johnsen EB, Martins F, Mascardi V, Montesi F, Neykova R, Ng N, Padovani L, Vasconcelos VT, Yoshida N (2016) Behavioral types in programming languages. Found Trends Program Lang 3(2–3):95–230. https://doi.org/10.1561/2500000031CrossRef

16.

Cogumbreiro T, Lange J, Liew Zhen Rong D, Zicarelli H (2021) Memory access protocols: certified data-race freedom for GPU kernels (artifact). GitLab. https://gitlab.com/umb-svl/faial-artifact-journal

17.

Cogumbreiro T, Lange J, Rong DLZ, Zicarelli (2021) Checking data-race freedom of GPU kernels, compositionally. In: Proceedings of CAV, LNCS, vol 12759. ACM, New York, NY, USA, pp 403–426. https://doi.org/10.1007/978-3-030-81685-8_19

18.

ul Hassan Khan Khan A, Al-Mouhamed M, Fatayer A, Almousa A, Baqais A, Assayony M (2014) Padding free bank conflict resolution for CUDA-based matrix transpose algorithm. In: Proceedings of the SNPD. IEEE, Piscataway, NJ, USA, pp 1–6. https://doi.org/10.1109/SNPD.2014.6888709

19.

Ruetsch G, Micikevicius P (2009) Optimizing matrix transpose in CUDA. NVIDIA CUDA SDK Application Note 18

20.

Betts A, Chong N, Donaldson AF, Qadeer S, Thomson P (2012) GPUVerify: a verifier for GPU kernels. In: Proceedings of OOPSLA. ACM, New York, NY, USA, pp 113–132. https://doi.org/10.1145/2384616.2384625

21.

Adve SV, Hill MD (1990) Weak ordering—a new definition. In: Proceedings of ISCA. ACM, New York, NY, USA, pp 2–14. https://doi.org/10.1145/325164.325100

22.

Adve SV, Hill MD (1993) A unified formalization of four shared-memory models. IEEE Trans Distrib Syst 4(6):613–624. https://doi.org/10.1109/71.242161CrossRef

23.

Marino D, Singh A, Millstein T, Musuvathi M, Narayanasamy S (2010) DRFX: a simple and efficient memory model for concurrent programming languages. In: Proceedings of the PLDI. ACM, New York, NY, USA, pp 351–362. https://doi.org/10.1145/1806596.1806636

24.

Li G, Gopalakrishnan G (2012) Parameterized verification of GPU kernel programs. In: Proceedings of the IPDPSW. IEEE, Piscataway, NJ, USA, pp 2450–2459. https://doi.org/10.1109/IPDPSW.2012.302

25.

Ma H, Diersen SR, Wang L, Liao C, Quinlan D, Yang Z (2013) Symbolic analysis of concurrency errors in OpenMP programs. In: Proceedings of the ICPP. IEEE, Piscataway, NJ, USA, pp 510–516. https://doi.org/10.1109/ICPP.2013.63

26.

Lattner C, Adve V (2004) LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the CGO. IEEE, Piscataway, NJ, USA, pp 75–88. https://doi.org/10.1109/CGO.2004.1281665

27.

De Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Proceedings of the TACAS. Springer, Berlin, pp 337–340

28.

Bardsley E, Donaldson AF (2014) Warps and atomics: beyond barrier synchronization in the verification of GPU kernels. In: Proceedings of the NFM. Springer, Berlin, pp 230–245. https://doi.org/10.1007/978-3-319-06200-6_18

29.

Bardsley E, Betts A, Chong N, Collingbourne P, Deligiannis P, Donaldson AF, Ketema J, Liew D, Qadeer S (2014) Engineering a static verification tool for GPU kernels. In: Proceedings of the CAV, vol 8559. Springer, Berlin, pp 226–242. https://doi.org/10.1007/978-3-319-08867-9_15

30.

Bakhoda A, Yuan GL, Fung WWL, Wong H, Aamodt TM (2009) Analyzing CUDA workloads using a detailed GPU simulator. In: Proceedings of the ISPASS. IEEE, Piscataway, NJ, USA, pp 163–174. https://doi.org/10.1109/ISPASS.2009.4919648

31.

Michalakes J, Vachharajani M (2008) GPU acceleration of numerical weather prediction. In: Proceedings of the IPDPS. IEEE, Piscataway, NJ, USA, pp 1–7. https://doi.org/10.1109/IPDPS.2008.4536351

32.

Schatz MC, Trapnell C, Delcher AL, Varshney A (2007) High-throughput sequence alignment using graphics processing units. BMC Bioinform 8:474–483. https://doi.org/10.1186/1471-2105-8-474CrossRef

33.

Manavski SA (2007) CUDA compatible GPU as an efficient hardware accelerator for AES cryptography. In: Proceedings of the ICSPC. IEEE, Piscataway, NJ, USA, pp 65–68. https://doi.org/10.1109/ICSPC.2007.4728256

34.

Chatarasi P, Shirako J, Kong M, Sarkar V (2017) An extended polyhedral model for SPMD programs and its use in static data race detection. In: Proceedings of LCPC’16. Springer, Berlin, pp 106–120. https://doi.org/10.1007/978-3-319-52709-3_10

35.

Grosser T, Ramanujam J, Pouchet L-N, Sadayappan P, Pop S (2015) Optimistic delinearization of parametrically sized arrays. In: Proceedings of the ICS. ACM, New York, NY, USA, pp 351–360. https://doi.org/10.1145/2751205.2751248

36.

Collingbourne P, Donaldson AF, Ketema J, Qadeer S (2013) Interleaving and lock-step semantics for analysis and verification of GPU kernels. In: Proceedings of ESOP. Springer, Berlin, pp 270–289. https://doi.org/10.1007/978-3-642-37036-6_16

37.

Bardsley E, Donaldson AF, Wickerson J (2014) KernelInterceptor: automating GPU kernel verification by intercepting kernels and their parameters. In: Proceedings of the IWOCL. ACM, New York, NY, USA, pp 1–5. https://doi.org/10.1145/2664666.2664673

38.

Barnett M, Chang B-YE, DeLine R, Jacobs B, Leino KRM (2005) Boogie: a modular reusable verifier for object-oriented programs. In: Proceedings of the FMCO. Springer, Berlin, pp 364–387. https://doi.org/10.1007/11804192_17

39.

Kojima K, Igarashi A (2013) A Hoare logic for SIMT programs. In: Proceedings of APLAS, vol 8301. Springer, Berlin, pp 58–73. https://doi.org/10.1007/978-3-319-03542-0_5

40.

Kojima K, Igarashi A (2017) A Hoare logic for GPU kernels. Trans Comput Logic 18(1):1–43. https://doi.org/10.1145/3001834MathSciNetCrossRefMATH

41.

Zheng M, Ravi VT, Qin F, Agrawal G (2011) GRace: a low-overhead mechanism for detecting data races in GPU programs. In: Proceedings of PPoPP. ACM, New York, NY, USA, pp 135–146. https://doi.org/10.1145/1941553.1941574

42.

Zheng M, Ravi VT, Qin F, Agrawal G (2014) GMRace: detecting data races in GPU programs via a low-overhead scheme. Trans Parallel Distrib Syst 25(1):104–115. https://doi.org/10.1109/TPDS.2013.44CrossRef

43.

Li P, Hu X, Chen D, Brock J, Luo H, Zhang EZ, Ding C (2017) LD: low-overhead GPU race detection without access monitoring. Trans Archit Code Optim 14(1):1–25. https://doi.org/10.1145/3046678CrossRef

44.

Peng Y, Grover V, Devietti J (2018) CURD: a dynamic CUDA race detector. In: Proceedings of PLDI. ACM, New York, NY, USA, pp 390–403. https://doi.org/10.1145/3192366.3192368

45.

Holey A, Mekkat V, Zhai A (2013) HAccRG: hardware-accelerated data race detection in GPUs. In: Proceedings of the ICPP. IEEE, Piscataway, NJ, USA, pp 60–69. https://doi.org/10.1109/ICPP.2013.15

46.

Eizenberg A, Peng Y, Pigli T, Mansky W, Devietti J (2017) BARRACUDA: binary-level analysis of runtime RAces in CUDA programs. In: Proceedings of PLDI. ACM, New York, NY, USA, pp 126–140. https://doi.org/10.1145/3062341.3062342

47.

Kamath AK, George AA, Basu A (2020) ScoRD: a scoped race detector for GPUs. In: Proceedings of ISCA. IEEE, Piscataway, NJ, USA, pp 1036–1049. https://doi.org/10.1109/ISCA45697.2020.00088

48.

Collingbourne P, Cadar C, Kelly PHJ (2011) Symbolic crosschecking of floating-point and SIMD code. In: Proceedings of EuroSys. ACM, New York, NY, USA, pp 315–328. https://doi.org/10.1145/1966445.1966475

49.

Collingbourne P, Cadar C, Kelly PHJ (2012) Symbolic testing of OpenCL code. In: Proceedings of HVC. Springer, Berlin, pp 203–218. https://doi.org/10.1007/978-3-642-34188-5_18

50.

Ferrell B, Duan J, Hamlen KW (2019) CUDA au Coq: a framework for machine-validating GPU assembly programs. In: Proceedings of DATE. IEEE, Piscataway, NJ, USA, pp 474–479. https://doi.org/10.23919/DATE.2019.8715160

51.

Muller SK, Hoffmann J (2021) Modeling and analyzing evaluation cost of CUDA kernels. In: Proceedings of the ACM on programming languages, vol 5 (POPL). https://doi.org/10.1145/3434306

52.

Alur R, Devietti J, Leija OSN, Singhania N (2021) Static detection of uncoalesced accesses in GPU programs. Formal Methods Syst Des. https://doi.org/10.1007/s10703-021-00362-8CrossRef

53.

Alur R, Devietti J, Leija OSN, Singhania N (2017) GPUDrano: detecting uncoalesced accesses in GPU programs. In: Proceedings of CAV, LNCS, vol 10426. Springer, Berlin, pp 507–525. https://doi.org/10.1007/978-3-319-63387-9_25

54.

Dabrowski F, Pichardie D (2009) A certified data race analysis for a Java-like language. In: Proceedings of TPHOL. Springer, Berlin, pp 212–227. https://doi.org/10.1007/978-3-642-03359-9_16

55.

Vasconcelos VT, Ravara A, Gay S (2004) Session types for functional multithreading. In: Proceedings of CONCUR. Springer, Berlin, pp 497–511. https://doi.org/10.1007/978-3-540-28644-8_32

56.

Vasconcelos VT (2009) Session types for linear multithreaded functional programming. In: Proceedings of PPDP. ACM, New York, NY, USA, pp 1–6. https://doi.org/10.1145/1599410.1599411

57.

López HA, Marques ERB, Martins F, Ng N, Santos C, Vasconcelos VT, Yoshida N (2015) Protocol-based verification of message-passing parallel programs. In: Proceedings of OOPSLA. ACM, New York, NY, USA, pp 280–298. https://doi.org/10.1145/2814270.2814302

58.

Liew D, Cogumbreiro T, Lange J (2022) Provable GPU data-races in static race detection. In: Proceedings of PLACES (EPTCS), vol 356. OPA, Waterloo, Australia, pp 36–45. https://doi.org/10.4204/EPTCS.356.4

Titel: Memory access protocols: certified data-race freedom for GPU kernels
verfasst von: Tiago Cogumbreiro
Julien Lange
Dennis Liew
Hannah Zicarelli
Publikationsdatum: 26.05.2023
Verlag: Springer US
Erschienen in: Formal Methods in System Design
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI: https://doi.org/10.1007/s10703-023-00415-0

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner