Name
Abstract | ||
|---|---|---|
With the widespread use of graphical processing units (GPUs), it is important to ensure that programmers have a clear understanding of their shared memory consistency model, i.e. what values can be read when issued concurrently with writes. Compared to CPUs, GPUs present different shared memory behavior, and we know of no published formal consistency model for them. To fill this void, we establish a formal state transition model of GPU loads, stores, and fences in the language Murphi, and check properties -- captured in litmus tests that pertain to ordering and visibility properties -- over executions using the Murphi model checker. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1145/2464996.2467280 | I4CS |
Keywords | Field | DocType |
graphical processing unit,shared memory consistency model,language murphi,litmus test,formal consistency model,clear understanding,present different shared memory,formal state transition model,visibility property,murphi model checker | Programming language,Uniform memory access,Shared memory,Computer science,Parallel computing,Distributed memory,Memory model,Consistency model,Distributed shared memory,Cache coherence,CUDA Pinned memory | Conference |
Citations | PageRank | References |
7 | 0.54 | 17 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tyler Sorensen | 1 | 109 | 9.42 |
| Ganesh Gopalakrishnan | 2 | 1619 | 130.11 |
| Vinod Grover | 3 | 261 | 13.61 |