Pregled bibliografske jedinice broj: 1278903
Specification and verification of GPGPU programs
Specification and verification of GPGPU programs // Science of computer programming, 95 (2014), 376-388 doi:10.1016/j.scico.2014.03.013 (međunarodna recenzija, članak, znanstveni)
CROSBI ID: 1278903 Za ispravke kontaktirajte CROSBI podršku putem web obrasca
Naslov
Specification and verification of GPGPU programs
Autori
Blom, Stefan ; Huisman, Marieke ; Mihelčić, Matej
Izvornik
Science of computer programming (0167-6423) 95
(2014);
376-388
Vrsta, podvrsta i kategorija rada
Radovi u časopisima, članak, znanstveni
Ključne riječi
formal verification ; separation logic ; permissions ; GPU programming
Sažetak
Graphics Processing Units (GPUs) are increasingly used for general-purpose applications because of their low price, energy efficiency and enormous computing power. Considering the importance of GPU applications, it is vital that the behaviour of GPU programs can be specified and proven correct formally. This paper presents a logic to verify GPU kernels written in OpenCL, a platform- independent low-level programming language. The logic can be used to prove both data-race-freedom and functional correctness of kernels. The verification is modular, based on ideas from permission-based separation logic. We present the logic and its soundness proof, and then discuss tool support and illustrate its use on a complex example kernel.
Izvorni jezik
Engleski
Znanstvena područja
Računarstvo, Informacijske i komunikacijske znanosti
Citiraj ovu publikaciju:
Časopis indeksira:
- Current Contents Connect (CCC)
- Web of Science Core Collection (WoSCC)
- Science Citation Index Expanded (SCI-EXP)
- SCI-EXP, SSCI i/ili A&HCI
- Scopus
