Safe asynchronous multicore memory operations

M. Bontincan; Mike Dodds; A.F. Donaldson; Matthew J. Parkinson

doi:10.1109/ASE.2011.6100049

Safe asynchronous multicore memory operations

M. Bontincan, Mike Dodds, A.F. Donaldson, Matthew J. Parkinson

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Asynchronous memory operations provide a means for coping with the memory wall problem in multicore processors, and are available in many platforms and languages, e.g., the Cell Broadband Engine, CUDA and OpenCL. Reasoning about the correct usage of such operations involves complex analysis of memory accesses to check for races. We present a method and tool for proving memory-safety and race-freedom of multicore programs that use asynchronous memory operations. Our approach uses separation logic with permissions, and our tool automates this method, targeting a C-like core language. We describe our solutions to several challenges that arose in the course of this research. These include: syntactic reasoning about permissions and arrays, integration of numerical abstract domains, and utilization of an SMT solver. We demonstrate the feasibility of our approach experimentally by checking absence of DMA races on a set of programs drawn from the IBM Cell SDK.

Original language	English
Title of host publication	Automated Software Engineering (ASE), 2011 26th IEEE/ACM International Conference on
Publisher	IEEE
Pages	153-162
Number of pages	10
ISBN (Print)	978-1-4577-1638-6
DOIs	https://doi.org/10.1109/ASE.2011.6100049
Publication status	Published - 2011
Event	26th IEEE/ACM International Conference On Automated Software Engineering (ASE 2011) - Kansas, Lawrence, United Kingdom Duration: 6 Nov 2011 → 12 Nov 2011

Conference

Conference	26th IEEE/ACM International Conference On Automated Software Engineering (ASE 2011)
Country/Territory	United Kingdom
City	Lawrence
Period	6/11/11 → 12/11/11

Access to Document

10.1109/ASE.2011.6100049

http://ieeexplore.ieee.org/xpl/articleDetails.jsp?tp=&arnumber=6100049

Cite this

@inproceedings{57280f154c574272830aff07db3491f3,

title = "Safe asynchronous multicore memory operations",

abstract = "Asynchronous memory operations provide a means for coping with the memory wall problem in multicore processors, and are available in many platforms and languages, e.g., the Cell Broadband Engine, CUDA and OpenCL. Reasoning about the correct usage of such operations involves complex analysis of memory accesses to check for races. We present a method and tool for proving memory-safety and race-freedom of multicore programs that use asynchronous memory operations. Our approach uses separation logic with permissions, and our tool automates this method, targeting a C-like core language. We describe our solutions to several challenges that arose in the course of this research. These include: syntactic reasoning about permissions and arrays, integration of numerical abstract domains, and utilization of an SMT solver. We demonstrate the feasibility of our approach experimentally by checking absence of DMA races on a set of programs drawn from the IBM Cell SDK.",

author = "M. Bontincan and Mike Dodds and A.F. Donaldson and Parkinson, {Matthew J.}",

year = "2011",

doi = "10.1109/ASE.2011.6100049",

language = "English",

isbn = "978-1-4577-1638-6",

pages = "153--162",

booktitle = "Automated Software Engineering (ASE), 2011 26th IEEE/ACM International Conference on",

publisher = "IEEE",

address = "United States",

note = "26th IEEE/ACM International Conference On Automated Software Engineering (ASE 2011) ; Conference date: 06-11-2011 Through 12-11-2011",

}

Bontincan, M, Dodds, M, Donaldson, AF & Parkinson, MJ 2011, Safe asynchronous multicore memory operations. in Automated Software Engineering (ASE), 2011 26th IEEE/ACM International Conference on. IEEE, pp. 153-162, 26th IEEE/ACM International Conference On Automated Software Engineering (ASE 2011), Lawrence, United Kingdom, 6/11/11. https://doi.org/10.1109/ASE.2011.6100049

TY - GEN

T1 - Safe asynchronous multicore memory operations

AU - Bontincan, M.

AU - Dodds, Mike

AU - Donaldson, A.F.

AU - Parkinson, Matthew J.

PY - 2011

Y1 - 2011

N2 - Asynchronous memory operations provide a means for coping with the memory wall problem in multicore processors, and are available in many platforms and languages, e.g., the Cell Broadband Engine, CUDA and OpenCL. Reasoning about the correct usage of such operations involves complex analysis of memory accesses to check for races. We present a method and tool for proving memory-safety and race-freedom of multicore programs that use asynchronous memory operations. Our approach uses separation logic with permissions, and our tool automates this method, targeting a C-like core language. We describe our solutions to several challenges that arose in the course of this research. These include: syntactic reasoning about permissions and arrays, integration of numerical abstract domains, and utilization of an SMT solver. We demonstrate the feasibility of our approach experimentally by checking absence of DMA races on a set of programs drawn from the IBM Cell SDK.

AB - Asynchronous memory operations provide a means for coping with the memory wall problem in multicore processors, and are available in many platforms and languages, e.g., the Cell Broadband Engine, CUDA and OpenCL. Reasoning about the correct usage of such operations involves complex analysis of memory accesses to check for races. We present a method and tool for proving memory-safety and race-freedom of multicore programs that use asynchronous memory operations. Our approach uses separation logic with permissions, and our tool automates this method, targeting a C-like core language. We describe our solutions to several challenges that arose in the course of this research. These include: syntactic reasoning about permissions and arrays, integration of numerical abstract domains, and utilization of an SMT solver. We demonstrate the feasibility of our approach experimentally by checking absence of DMA races on a set of programs drawn from the IBM Cell SDK.

U2 - 10.1109/ASE.2011.6100049

DO - 10.1109/ASE.2011.6100049

M3 - Conference contribution

SN - 978-1-4577-1638-6

SP - 153

EP - 162

BT - Automated Software Engineering (ASE), 2011 26th IEEE/ACM International Conference on

PB - IEEE

T2 - 26th IEEE/ACM International Conference On Automated Software Engineering (ASE 2011)

Y2 - 6 November 2011 through 12 November 2011

ER -