Safe Asynchronous Multicore Memory Operations (CROSBI ID 579524)
Prilog sa skupa u zborniku | izvorni znanstveni rad | međunarodna recenzija
Podaci o odgovornosti
Botinčan, Matko ; Dodds, Mike ; Donaldson, Alastair F. ; Parkinson, Matthew J.
engleski
Safe Asynchronous Multicore Memory Operations
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.
software verification; concurrent programs; abstract interpretation; automated theorem proving
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
2011.
objavljeno
Podaci o matičnoj publikaciji
Washington (MD): IEEE CS
Podaci o skupu
The 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011)
predavanje
06.11.2011-12.11.2011
Lawrence (KS), Sjedinjene Američke Države