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

Napredna pretraga

Pregled bibliografske jedinice broj: 543562

Resource-Sensitive Synchronization Inference by Abduction


Botincan, Matko; Dodds, Mike; Jagannathan, Suresh
Resource-Sensitive Synchronization Inference by Abduction // Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012)
New York: ACM, 2012. (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)


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

Naslov
Resource-Sensitive Synchronization Inference by Abduction

Autori
Botincan, Matko ; Dodds, Mike ; Jagannathan, Suresh

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

Izvornik
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012) / - New York : ACM, 2012

Skup
The 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012)

Mjesto i datum
Philadelphia, SAD, 25-27.01.2012

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
separation logic; abduction; frame inference; deterministic parallelism

Sažetak
We present an analysis which takes as its input a sequential program, augmented with annotations indicating potential parallelization opportunities, and a sequential proof, written in separation logic, and produces a correctly-synchronized parallelized program and proof of that program. Unlike previous work, ours is not an independence analysis ; we insert synchronization constructs to preserve relevant dependencies found in the sequential program that may otherwise be violated by a naive translation. Separation logic allows us to parallelize fine-grained patterns of resource-usage, moving beyond straightforward points-to analysis. Our analysis works by using the sequential proof to discover dependencies between different parts of the program. It leverages these discovered dependencies to guide the insertion of synchronization primitives into the parallelized program, and to ensure that the resulting parallelized program satisfies the same specification as the original sequential program, and exhibits the same sequential behaviour. Our analysis is built using frame inference and abduction, two techniques supported by an increasing number of separation logic tools.

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:

Botincan, Matko; Dodds, Mike; Jagannathan, Suresh
Resource-Sensitive Synchronization Inference by Abduction // Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012)
New York: ACM, 2012. (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)
Botincan, M., Dodds, M. & Jagannathan, S. (2012) Resource-Sensitive Synchronization Inference by Abduction. U: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012).
@article{article, author = {Botincan, Matko and Dodds, Mike and Jagannathan, Suresh}, year = {2012}, keywords = {separation logic, abduction, frame inference, deterministic parallelism}, title = {Resource-Sensitive Synchronization Inference by Abduction}, keyword = {separation logic, abduction, frame inference, deterministic parallelism}, publisher = {ACM}, publisherplace = {Philadelphia, SAD} }
@article{article, author = {Botincan, Matko and Dodds, Mike and Jagannathan, Suresh}, year = {2012}, keywords = {separation logic, abduction, frame inference, deterministic parallelism}, title = {Resource-Sensitive Synchronization Inference by Abduction}, keyword = {separation logic, abduction, frame inference, deterministic parallelism}, publisher = {ACM}, publisherplace = {Philadelphia, SAD} }




Contrast
Increase Font
Decrease Font
Dyslexic Font