Pretražite po imenu i prezimenu autora, mentora, urednika, prevoditelja

Napredna pretraga

Pregled bibliografske jedinice broj: 543318

Safe Asynchronous Multicore Memory Operations


Botinčan, Matko; Dodds, Mike; Donaldson, Alastair F.; Parkinson, Matthew J.
Safe Asynchronous Multicore Memory Operations // Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011)
Washington DC: IEEE CS, 2011. (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)


CROSBI ID: 543318 Za ispravke kontaktirajte CROSBI podršku putem web obrasca

Naslov
Safe Asynchronous Multicore Memory Operations

Autori
Botinčan, Matko ; Dodds, Mike ; Donaldson, Alastair F. ; Parkinson, Matthew J.

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011) / - Washington DC : IEEE CS, 2011

Skup
The 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011)

Mjesto i datum
Lawrence, Kansas, SAD, 06-12.11.2011

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
software verification; concurrent programs; abstract interpretation; automated theorem proving

Sažetak
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.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Računarstvo



POVEZANOST RADA


Projekti:
037-0362980-2774 - Distribuirani algoritmi za pronalaženje optimalnih putova u grafovima (Manger, Robert, MZOS ) ( POIROT)

Ustanove:
Prirodoslovno-matematički fakultet, Matematički odjel, Zagreb

Profili:

Avatar Url Matko Botinčan (autor)


Citiraj ovu publikaciju:

Botinčan, Matko; Dodds, Mike; Donaldson, Alastair F.; Parkinson, Matthew J.
Safe Asynchronous Multicore Memory Operations // Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011)
Washington DC: IEEE CS, 2011. (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)
Botinčan, M., Dodds, M., Donaldson, A. & Parkinson, M. (2011) Safe Asynchronous Multicore Memory Operations. U: Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011).
@article{article, author = {Botin\v{c}an, Matko and Dodds, Mike and Donaldson, Alastair F. and Parkinson, Matthew J.}, year = {2011}, keywords = {software verification, concurrent programs, abstract interpretation, automated theorem proving}, title = {Safe Asynchronous Multicore Memory Operations}, keyword = {software verification, concurrent programs, abstract interpretation, automated theorem proving}, publisher = {IEEE CS}, publisherplace = {Lawrence, Kansas, SAD} }
@article{article, author = {Botin\v{c}an, Matko and Dodds, Mike and Donaldson, Alastair F. and Parkinson, Matthew J.}, year = {2011}, keywords = {software verification, concurrent programs, abstract interpretation, automated theorem proving}, title = {Safe Asynchronous Multicore Memory Operations}, keyword = {software verification, concurrent programs, abstract interpretation, automated theorem proving}, publisher = {IEEE CS}, publisherplace = {Lawrence, Kansas, SAD} }




Contrast
Increase Font
Decrease Font
Dyslexic Font