Remote-Scope Promotion: Clarified, Rectified, and Verified
File(s)
Accepted version
Author(s)
Wickerson, J
Batty, M
Beckmann, BM
Donaldson, AF
Type
Conference Paper
Abstract
Modern accelerator programming frameworks, such as
OpenCLTM, organise threads into work-groups. Remotescope
promotion (RSP) is a language extension recently
proposed by AMD researchers that is designed to enable
applications, for the first time, both to optimise for the common
case of intra-work-group communication (using memory
scopes to provide consistency only within a work-group) and
to allow occasional inter-work-group communication (as
required, for instance, to support the popular load-balancing
idiom of work stealing).
We present the first formal, axiomatic memory model of
OpenCL extended with RSP. We have extended the HERD
memory model simulator with support for OpenCL kernels
that exploit RSP, and used it to discover bugs in several
litmus tests and a work-stealing queue, that have been used
previously in the study of RSP. We have also formalised the
proposed GPU implementation of RSP. The formalisation
process allowed us to identify bugs in the description of RSP
that could result in well-synchronised programs experiencing
memory inconsistencies. We present and prove sound a
new implementation of RSP that incorporates bug fixes
and requires less non-standard hardware than the original
implementation.
This work, a collaboration between academia and industry,
clearly demonstrates how, when designing hardware support
for a new concurrent language feature, the early application
of formal tools and techniques can help to prevent errors,
such as those we have found, from making it into silicon
OpenCLTM, organise threads into work-groups. Remotescope
promotion (RSP) is a language extension recently
proposed by AMD researchers that is designed to enable
applications, for the first time, both to optimise for the common
case of intra-work-group communication (using memory
scopes to provide consistency only within a work-group) and
to allow occasional inter-work-group communication (as
required, for instance, to support the popular load-balancing
idiom of work stealing).
We present the first formal, axiomatic memory model of
OpenCL extended with RSP. We have extended the HERD
memory model simulator with support for OpenCL kernels
that exploit RSP, and used it to discover bugs in several
litmus tests and a work-stealing queue, that have been used
previously in the study of RSP. We have also formalised the
proposed GPU implementation of RSP. The formalisation
process allowed us to identify bugs in the description of RSP
that could result in well-synchronised programs experiencing
memory inconsistencies. We present and prove sound a
new implementation of RSP that incorporates bug fixes
and requires less non-standard hardware than the original
implementation.
This work, a collaboration between academia and industry,
clearly demonstrates how, when designing hardware support
for a new concurrent language feature, the early application
of formal tools and techniques can help to prevent errors,
such as those we have found, from making it into silicon
Date Issued
2015-10-01
Date Acceptance
2015-10-01
Citation
2015, 50 (10), pp.731-747
ISSN
1523-2867
Publisher
Association for Computing Machinery (ACM)
Start Page
731
End Page
747
Journal / Book Title
ACM Sigplan Notices
Volume
50
Issue
10
Copyright Statement
© ACM, 2015. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Sigplan Notices, {VOL# 50, ISS# 10, (23 Oct 2015)} https://dx.doi.org/10.1145/2814270.2814283
Sponsor
Commission of the European Communities
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Grant Number
287767
EP/K503733/1
EP/K011499/1
Source
ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
Formal methods
graphics processing unit (GPU)
Isabelle
OpenCL
programming language implementation
weak memory models
work stealing
Publication Status
Published
Start Date
2015-10-25
Finish Date
2015-10-30
Coverage Spatial
Pittsburgh, PA, USA