Specification and Verification of Atomic Operations in GPGPU Programs
| Autor: | Amighi, A., Darabi, Saeed, Blom, Stefan, Huisman, Marieke, Calinescu, Radu, Rumpe, Bernhard |
|---|---|
| Rok vydání: | 2015 |
| Předmět: |
Soundness
Correctness Theoretical computer science METIS-312673 Exploit Computer science EWI-26147 020207 software engineering 02 engineering and technology Separation logic EC Grant Agreement nr.: FP7/258405 IR-97701 Kernel (image processing) EC Grant Agreement nr.: FP7/2007-2013 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing SIMD Invariant (mathematics) General-purpose computing on graphics processing units EC Grant Agreement nr.: FP7/287767 |
| Zdroj: | Software Engineering and Formal Methods ISBN: 9783319229683 SEFM Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015), 69-83 STARTPAGE=69;ENDPAGE=83;TITLE=Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015) |
| DOI: | 10.1007/978-3-319-22969-0_5 |
| Popis: | We propose a specification and verification technique based on separation logic to reason about data race freedom and functional correctness of GPU kernels that use atomic operations as synchronisation mechanism. Our approach exploits the notion of resource invariant from Concurrent Separation Logic (CSL) to capture the behaviour of atomic operations. However, because of the different memory levels in the GPU architecture, we adapt this notion of resource invariant to these memory levels, i.e., group resource invariants capture the behaviour of atomic operations that access locations in local memory, while kernel resource invariants capture the behaviour of atomic operations that access locations in global memory. We show soundness of our approach and we provide tool support that enables us to verify kernels from standard benchmarks suites. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|