Fri 30 Oct 2015 13:30 - 13:52 at Grand Station 1 - 11. Programming Language Design Chair(s): Gary Leavens

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.

Conference Day
Fri 30 Oct

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 15:00
11. Programming Language DesignOOPSLA at Grand Station 1
Chair(s): Gary Leavens University of Central Florida
13:30
22m
Talk
Remote-Scope Promotion: Clarified, Rectified, and VerifiedOOPSLA Artifact
OOPSLA
John WickersonImperial College London, Mark BattyUniversity of Cambridge, Bradford M. BeckmannAdvanced Micro Devices, Inc, Alastair F. DonaldsonImperial College London
DOI Media Attached
13:52
22m
Talk
Incremental Computation with NamesOOPSLA Artifact
OOPSLA
Matthew HammerUniversity of Maryland, College Park, Jana DunfieldUniversity of British Columbia, Canada, Kyle HeadleyUniversity of Maryland, College Park, Nicholas LabichUniversity of Maryland at College Park, USA, Jeffrey S. FosterUniversity of Maryland at College Park, USA, Michael HicksUniversity of Maryland at College Park, USA, David Van HornUniversity of Maryland at College Park, USA
DOI
14:15
22m
Talk
Checks and Balances: Constraint Solving without Surprises in Object-Constraint Programming LanguagesOOPSLA Artifact
OOPSLA
Tim FelgentreffHPI, Germany, Todd MillsteinUniversity of California at Los Angeles, USA, Alan BorningUniversity of Washington, USA, Robert HirschfeldHPI
DOI
14:37
22m
Talk
Optimizing Hash-Array Mapped Tries for Fast and Lean Immutable JVM CollectionsOOPSLA Artifact
OOPSLA
Michael SteindorferCWI, Netherlands, Jurgen VinjuCWI, Netherlands
Link to publication