Skip to main content

Remote-scope Promotion: Clarified, Rectified, and Verified

Wickerson, John and Batty, Mark and Beckmann, Bradford M. and Donaldson, Alastair F. (2015) Remote-scope Promotion: Clarified, Rectified, and Verified. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. SPLASH Systems, Programming, and Applications . ACM, New York, USA, pp. 731-747. ISBN 978-1-4503-3689-5. (doi:10.1145/2814270.2814283) (KAR id:51384)

PDF Publisher pdf
Language: English
Download (325kB) Preview
[thumbnail of OOPSLA.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL


Modern accelerator programming frameworks, such as OpenCL, organise threads into work-groups. Remote-scope 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.

Item Type: Book section
DOI/Identification number: 10.1145/2814270.2814283
Uncontrolled keywords: Formal methods, Isabelle, OpenCL, graphics processing unit (GPU), programming language implementation, weak memory models, work stealing
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Batty
Date Deposited: 02 Nov 2015 23:59 UTC
Last Modified: 16 Feb 2021 13:29 UTC
Resource URI: (The current URI for this page, for reference purposes)
Batty, Mark:
  • Depositors only (login required):