More Web Proxy on the site http://driver.im/

research-article

Verifying GPU kernels by test amplification

Authors:

Yuvraj Agarwal,

Sorin LernerAuthors Info & Claims

ACM SIGPLAN Notices, Volume 47, Issue 6

Pages 383 - 394

https://doi.org/10.1145/2345156.2254110

Published: 11 June 2012 Publication History

Abstract

We present a novel technique for verifying properties of data parallel GPU programs via test amplification. The key insight behind our work is that we can use the technique of static information flow to amplify the result of a single test execution over the set of all inputs and interleavings that affect the property being verified. We empirically demonstrate the effectiveness of test amplification for verifying race-freedom and determinism over a large number of standard GPU kernels, by showing that the result of verifying a single dynamic execution can be amplified over the massive space of possible data inputs and thread interleavings.

References

[1]

L. Andersen. Program analysis and specialization for the C programming language. PhD thesis, 1994.

[2]

A. Aviram, S.-C. Weng, S. Hu, and B. Ford. Efficient system-enforced deterministic parallelism. In OSDI, pages 193--206, 2010.

Digital Library

[3]

T. Bergan, O. Anderson, J. Devietti, L. Ceze, and D. Grossman. CoreDet: a compiler and runtime system for deterministic multithreaded execution. In ASPLOS, pages 53--64, 2010.

Digital Library

[4]

M. Boyer, K. Skadron, and W. Weimer. Automated dynamic analysis of CUDA programs. In STMC, 2008.

[5]

C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: automatically generating inputs of death. In CCS, pages 322--335, 2006.

Digital Library

[6]

C. Cadar, P. Godefroid, S. Khurshid, C. S. Păsăreanu, K. Sen, N. Tillmann, and W. Visser. Symbolic execution for software testing in practice: preliminary assessment. In ICSE, pages 1066--1071, 2011.

Digital Library

[7]

F. Chen and G. Roşu. Parametric and sliced causality. In CAV, pages 240--253, 2007.

Digital Library

[8]

A. Dinning and E. Schonberg. Detecting access anomalies in programs with critical sections. In Workshop on Parallel and Distributed Debugging, pages 85--96, 1991.

Digital Library

[9]

P. A. Emrath and D. A. Padua. Automatic detection of nondeterminacy in parallel programs. In PADD, pages 89--99, 1988.

Digital Library

[10]

D. Engler and K. Ashcraft. RacerX: Effective, static detection of race conditions and deadlocks. In SOSP, pages 237--252, 2003.

Digital Library

[11]

C. Flanagan and S. Freund. Type-based race detection for Java. In PLDI, pages 219--232, 2000.

Digital Library

[12]

C. Flanagan and S. N. Freund. Atomizer: a dynamic atomicity checker for multithreaded programs. In POPL, pages 256--267, 2004.

Digital Library

[13]

C. Flanagan and S. Qadeer. A type and effect system for atomicity. In PLDI, pages 191--202, 2003.

Digital Library

[14]

P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1996.

[15]

P. Godefroid and J. Kinder. Proving memory safety of floating-point computations by combining static and dynamic program analysis. In ISSTA, pages 1--12, 2010.

Digital Library

[16]

P. Godefroid, N. Klarlund, and K. Sen. DART: directed automated random testing. In PLDI, pages 213--223, 2005.

Digital Library

[17]

P. Godefroid, M. Y. Levin, and D. A. Molnar. Active property checking. In EMSOFT, pages 207--216, 2008.

Digital Library

[18]

J. A. Goguen and J. Meseguer. Security policies and security models. IEEE Symposium on Security and Privacy, pages 11--20, 1982.

[19]

P. Joshi, K. Sen, and M. Shlimovich. Predictive testing: amplifying the effectiveness of software testing. In ESEC/FSE, pages 561--564, 2007.

Digital Library

[20]

L. Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558--565, 1978.

Digital Library

[21]

E. Larson and T. Austin. High coverage detection of input-related security faults. In USENIX Security, 2003.

Digital Library

[22]

C. Lattner and V. Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In CGO, 2004.

Digital Library

[23]

G. Li and G. Gopalakrishnan. Scalable smt-based verification of gpu kernel functions. In FSE, pages 187--196, 2010.

Digital Library

[24]

R. J. Lipton. Reduction: a method of proving properties of parallel programs. Commun. ACM, 18:717--721, December 1975.

Digital Library

[25]

T. Liu, C. Curtsinger, and E. D. Berger. Dthreads: Efficient deterministic multithreading. In SOSP, pages 327--336, 2011.

Digital Library

[26]

F. Masdupuy. Semantic analysis of interval congruences. In Formal Methods in Programming and Their Applications, LNCS 735. 1993.

Digital Library

[27]

A. Myers. JFlow: Practical mostly-static information flow control. In POPL, pages 228--241, 1999.

Digital Library

[28]

NVIDIA. CUDA toolkit 3.0. http://developer.nvidia.com/cuda-toolkit-30-downloads, 2010.

[29]

NVIDIA. CUDA accelerated applications. http://www.nvidia.com/object/cuda_app_tesla.html, 2011.

[30]

M. Raza, C. Calcagno, and P. Gardner. Automatic parallelization with separation logic. In ESOP, pages 348--362, 2009.

Digital Library

[31]

C. Sadowski, S. N. Freund, and C. Flanagan. SingleTrack: A dynamic determinism checker for multithreaded programs. In ESOP, pages 394--409, 2009.

Digital Library

[32]

S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: A dynamic data race detector for multi-threaded programs. ACM Transactions on Computer Systems, 15:391--411, 1997.

Digital Library

[33]

K. Sen, D. Marinov, and G. Agha. CUTE: a concolic unit testing engine for c. In ESEC/FSE, pages 263--272, 2005.

Digital Library

[34]

T. Terauchi. A type system for observational determinism. In CSF, pages 287--300, 2008.

Digital Library

[35]

M. T. Vechev, E. Yahav, R. Raman, and V. Sarkar. Automatic verification of determinism for structured parallel programs. In SAS, pages 455--471, 2010.

Digital Library

[36]

L. Wang and S. D. Stoller. Runtime analysis of atomicity for multithreaded programs. IEEE Trans. Softw. Eng., 32:93--110, February 2006.

Digital Library

[37]

S. Zdancewic and A. C. Myers. Observational determinism for concurrent program security. In CSFW, pages 29--43, 2003.

Cited By

Luz HSouza PSouza S(2024)Structural testing for CUDA programming modelConcurrency and Computation: Practice and Experience10.1002/cpe.810536:14Online publication date: 9-Apr-2024
https://doi.org/10.1002/cpe.8105
Peng CRajan AJog AKayiran OPattnaik A(2020)Automated test generation for OpenCL kernels using fuzzing and constraint solvingProceedings of the 13th Annual Workshop on General Purpose Processing using Graphics Processing Unit10.1145/3366428.3380768(61-70)Online publication date: 23-Feb-2020
https://dl.acm.org/doi/10.1145/3366428.3380768
Zhu QZaidman A(2020)Massively Parallel, Highly Efficient, but What About the Test Suite Quality? Applying Mutation Testing to GPU Programs2020 IEEE 13th International Conference on Software Testing, Validation and Verification (ICST)10.1109/ICST46399.2020.00030(209-219)Online publication date: Oct-2020
https://doi.org/10.1109/ICST46399.2020.00030
Show More Cited By

Index Terms

Verifying GPU kernels by test amplification

Recommendations

Verifying GPU kernels by test amplification
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation

We present a novel technique for verifying properties of data parallel GPU programs via test amplification. The key insight behind our work is that we can use the technique of static information flow to amplify the result of a single test execution over ...
Lock-based synchronization for GPU architectures
CF '16: Proceedings of the ACM International Conference on Computing Frontiers

Modern GPUs have shown promising results in accelerating compute-intensive and numerical workloads with limited data sharing. However, emerging GPU applications manifest ample amount of data sharing among concurrently executing threads. Often data ...
Performance of CPU/GPU compiler directives on ISO/TTI kernels

GPUs are slowly becoming ubiquitous devices in High Performance Computing, as their capabilities to enhance the performance per watt of compute intensive algorithms as compared to multicore CPUs have been identified. The primary shortcoming of a GPU is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 47, Issue 6

PLDI '12

June 2012

534 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2345156

Issue’s Table of Contents

PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2012
572 pages
ISBN:9781450312059
DOI:10.1145/2254064
General Chairs:
Jan Vitek
Purdue University
,
Haibo Lin
Microsoft China
,
Program Chair:
Frank Tip
IBM T.J. Watson Research Center

Copyright © 2012 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 June 2012

Published in SIGPLAN Volume 47, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

53
Total Citations
View Citations
401
Total Downloads

Downloads (Last 12 months)23
Downloads (Last 6 weeks)2

Reflects downloads up to 17 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Luz HSouza PSouza S(2024)Structural testing for CUDA programming modelConcurrency and Computation: Practice and Experience10.1002/cpe.810536:14Online publication date: 9-Apr-2024
https://doi.org/10.1002/cpe.8105
Peng CRajan AJog AKayiran OPattnaik A(2020)Automated test generation for OpenCL kernels using fuzzing and constraint solvingProceedings of the 13th Annual Workshop on General Purpose Processing using Graphics Processing Unit10.1145/3366428.3380768(61-70)Online publication date: 23-Feb-2020
https://dl.acm.org/doi/10.1145/3366428.3380768
Zhu QZaidman A(2020)Massively Parallel, Highly Efficient, but What About the Test Suite Quality? Applying Mutation Testing to GPU Programs2020 IEEE 13th International Conference on Software Testing, Validation and Verification (ICST)10.1109/ICST46399.2020.00030(209-219)Online publication date: Oct-2020
https://doi.org/10.1109/ICST46399.2020.00030
van den Haak LWijs Avan den Brand MHuisman M(2020)Formal Methods for GPGPU Programming: Is the Demand Met?Integrated Formal Methods10.1007/978-3-030-63461-2_9(160-177)Online publication date: 16-Nov-2020
https://dl.acm.org/doi/10.1007/978-3-030-63461-2_9
Peng CZhang DMøller A(2019)On the correctness of GPU programsProceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3293882.3338989(443-447)Online publication date: 10-Jul-2019
https://dl.acm.org/doi/10.1145/3293882.3338989
Danglot BVera-Perez OYu ZZaidman AMonperrus MBaudry B(2019)A Snowballing Literature Study on Test AmplificationJournal of Systems and Software10.1016/j.jss.2019.110398(110398)Online publication date: Aug-2019
https://doi.org/10.1016/j.jss.2019.110398
Peng CRajan A(2019)CLTestCheck: Measuring Test Effectiveness for GPU KernelsFundamental Approaches to Software Engineering10.1007/978-3-030-16722-6_19(315-331)Online publication date: 4-Apr-2019
https://doi.org/10.1007/978-3-030-16722-6_19
Taram MVenkat ATullsen D(2018)Mobilizing the micro-opsProceedings of the 45th Annual International Symposium on Computer Architecture10.1109/ISCA.2018.00058(624-637)Online publication date: 2-Jun-2018
https://dl.acm.org/doi/10.1109/ISCA.2018.00058
Celik APai SKhurshid SGligoric M(2017)Bounded exhaustive test-input generation on GPUsProceedings of the ACM on Programming Languages10.1145/31339181:OOPSLA(1-25)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3133918
Chong NDonaldson AKetema J(2014)A sound and complete abstraction for reasoning about parallel prefix sumsACM SIGPLAN Notices10.1145/2578855.253588249:1(397-409)Online publication date: 8-Jan-2014
https://dl.acm.org/doi/10.1145/2578855.2535882
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents