liu.seSearch for publications in DiVA
Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Software Model Checking for GPGPU Programs, Towards a Verification Tool
Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system. Linköpings universitet, Tekniska högskolan.
Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system. Linköpings universitet, Tekniska högskolan.
2011 (engelsk)Rapport (Annet vitenskapelig)
Abstract [en]

The tremendous computing power GPUs are capable of makes of them the epicenter of an unprecedented attention for applications other than graphics and gaming. Apart from the highly parallel nature of the programs to be run on GPUs, the sought after gain in computing power is only achieved with low level tuning at threads level and is therefore veryerror prone. In fact the level of intricacy involved when writing such programs is already a problem and will become a major bottleneck in spreading the technology.

Only very recent and rare works started looking into using formal methods for helping GPU programmers avoiding errors like data races, incorrect synchronizations or assertions violations. These are at their infancy and directly import techniques adapted for other (sequential) systems with simple approximations for concurrency. Besides that, theonly help we are aware of right now takes a concrete input and explores a tiny portion of the possible thread scheduling looking for such errors. This easily misses common errors and makes of GPU programming a nightmare task. There is therefore still a lot of work to do in order to come up with helpful and scalable tools for today's and tomorrow's GPGPU software.

We state in this paper our intention in building in Linköping a agship verication tool that will take CUDA code and track and report, with minimal assistance from the programmer, errors like data races, incorrect synchronizations or assertions violations. In order to achieve this ambitious and vital goal for the widespread of GPU programming, webuild on our experience using and implementing CUDA and GPU code and on our latest work in the verication of multicore and concurrent programs. In fact, GPU programs like those written in CUDA are suitable for verication as they typically neither manipulate pointer arithmetics nor allowrecursion. This restricts the focus to concurrency and array manipulation, combined with intra and inter procedural analysis. To give a avor of where we start from, we report on our experiments in automatically verifying two synchronization algorithms that appeared in a recent paper proposing effiient barriers for inter-block synchronization. Unlike any other verication approach for GPU programs,we can show that the algorithms neither deadlock nor violate the barrier condition regardless of the number of threads. We also capture bugs in case basic relations are violated between the number of blocks and the number of threads per block.

sted, utgiver, år, opplag, sider
2011. , s. 3
Emneord [en]
GPU, Software Model Checking, CUDA, Formal Verication
HSV kategori
Identifikatorer
URN: urn:nbn:se:liu:diva-76411OAI: oai:DiVA.org:liu-76411DiVA, id: diva2:514389
Prosjekter
CENIITTilgjengelig fra: 2012-04-09 Laget: 2012-04-09 Sist oppdatert: 2012-04-16bibliografisk kontrollert

Open Access i DiVA

Software Model Checking for GPGPU Programs, Towards a Verification Tool(214 kB)247 nedlastinger
Filinformasjon
Fil FULLTEXT01.pdfFilstørrelse 214 kBChecksum SHA-512
0e7d7c910057b0de59233a109da1e907f3d9c281dd179c2e0f60d1878e2cfb960dc355ad49fe714e586b645f942d6f1a1d64a68002b79468ba976b41de479fb5
Type fulltextMimetype application/pdf

Personposter BETA

Bordoloi, UnmeshRezine, Ahmed

Søk i DiVA

Av forfatter/redaktør
Bordoloi, UnmeshRezine, Ahmed
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar
Totalt: 247 nedlastinger
Antall nedlastinger er summen av alle nedlastinger av alle fulltekster. Det kan for eksempel være tidligere versjoner som er ikke lenger tilgjengelige

urn-nbn

Altmetric

urn-nbn
Totalt: 264 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf