Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude?. Abd Alrahman, Y., Andric, M., Beggiato, A., & Lluch-Lafuente, A. In Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014, Revised Selected Papers, volume 8663, of Lecture Notes in Computer Science, pages 21-41, 2014. Springer.
Paper doi abstract bibtex Relaxed memory models offer suitable abstractions of the actual optimizations offered by multi-core architectures and by compilers of concurrent programming languages. Using such abstractions for verification purposes is challenging in part due to their inherent non-determinism which contributes to the state space explosion. Several techniques have been proposed to mitigate those problems so to make verification under relaxed memory models feasible. We discuss how to adopt some of those techniques in a Maude-based approach to language prototyping, and suggest the use of other techniques that have been shown successful for similar verification purposes.
@inproceedings{DBLP:conf/wrla/AlrahmanABL14,
author = {Yehia {Abd Alrahman} and
Marina Andric and
Alessandro Beggiato and
Alberto Lluch{-}Lafuente},
editor = {Santiago Escobar},
title = {Can We Efficiently Check Concurrent Programs Under Relaxed Memory
Models in Maude?},
booktitle = {Rewriting Logic and Its Applications - 10th International Workshop,
{WRLA} 2014, Held as a Satellite Event of ETAPS, Grenoble, France,
April 5-6, 2014, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {8663},
pages = {21-41},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-12904-4\_2},
doi = {10.1007/978-3-319-12904-4\_2},
abstract = {Relaxed memory models offer suitable abstractions of the actual optimizations offered by multi-core architectures and by compilers of concurrent programming languages. Using such abstractions for verification purposes is challenging in part due to their inherent non-determinism which contributes to the state space explosion. Several techniques have been proposed to mitigate those problems so to make verification under relaxed memory models feasible. We discuss how to adopt some of those techniques in a Maude-based approach to language prototyping, and suggest the use of other techniques that have been shown successful for similar verification purposes.}
}
Downloads: 0
{"_id":"XFG82B5E3mB55geoH","bibbaseid":"abdalrahman-andric-beggiato-lluchlafuente-canweefficientlycheckconcurrentprogramsunderrelaxedmemorymodelsinmaude-2014","author_short":["Abd Alrahman, Y.","Andric, M.","Beggiato, A.","Lluch-Lafuente, A."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Yehia"],"propositions":[],"lastnames":["Abd Alrahman"],"suffixes":[]},{"firstnames":["Marina"],"propositions":[],"lastnames":["Andric"],"suffixes":[]},{"firstnames":["Alessandro"],"propositions":[],"lastnames":["Beggiato"],"suffixes":[]},{"firstnames":["Alberto"],"propositions":[],"lastnames":["Lluch-Lafuente"],"suffixes":[]}],"editor":[{"firstnames":["Santiago"],"propositions":[],"lastnames":["Escobar"],"suffixes":[]}],"title":"Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude?","booktitle":"Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014, Revised Selected Papers","series":"Lecture Notes in Computer Science","volume":"8663","pages":"21-41","publisher":"Springer","year":"2014","url":"https://doi.org/10.1007/978-3-319-12904-4\\_2","doi":"10.1007/978-3-319-12904-4_2","abstract":"Relaxed memory models offer suitable abstractions of the actual optimizations offered by multi-core architectures and by compilers of concurrent programming languages. Using such abstractions for verification purposes is challenging in part due to their inherent non-determinism which contributes to the state space explosion. Several techniques have been proposed to mitigate those problems so to make verification under relaxed memory models feasible. We discuss how to adopt some of those techniques in a Maude-based approach to language prototyping, and suggest the use of other techniques that have been shown successful for similar verification purposes.","bibtex":"@inproceedings{DBLP:conf/wrla/AlrahmanABL14,\n author = {Yehia {Abd Alrahman} and\n Marina Andric and\n Alessandro Beggiato and\n Alberto Lluch{-}Lafuente},\n editor = {Santiago Escobar},\n title = {Can We Efficiently Check Concurrent Programs Under Relaxed Memory\n Models in Maude?},\n booktitle = {Rewriting Logic and Its Applications - 10th International Workshop,\n {WRLA} 2014, Held as a Satellite Event of ETAPS, Grenoble, France,\n April 5-6, 2014, Revised Selected Papers},\n series = {Lecture Notes in Computer Science},\n volume = {8663},\n pages = {21-41},\n publisher = {Springer},\n year = {2014},\n url = {https://doi.org/10.1007/978-3-319-12904-4\\_2},\n doi = {10.1007/978-3-319-12904-4\\_2},\n abstract = {Relaxed memory models offer suitable abstractions of the actual optimizations offered by multi-core architectures and by compilers of concurrent programming languages. Using such abstractions for verification purposes is challenging in part due to their inherent non-determinism which contributes to the state space explosion. Several techniques have been proposed to mitigate those problems so to make verification under relaxed memory models feasible. We discuss how to adopt some of those techniques in a Maude-based approach to language prototyping, and suggest the use of other techniques that have been shown successful for similar verification purposes.}\n}\n","author_short":["Abd Alrahman, Y.","Andric, M.","Beggiato, A.","Lluch-Lafuente, A."],"editor_short":["Escobar, S."],"key":"DBLP:conf/wrla/AlrahmanABL14","id":"DBLP:conf/wrla/AlrahmanABL14","bibbaseid":"abdalrahman-andric-beggiato-lluchlafuente-canweefficientlycheckconcurrentprogramsunderrelaxedmemorymodelsinmaude-2014","role":"author","urls":{"Paper":"https://doi.org/10.1007/978-3-319-12904-4\\_2"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://lazkany.bitbucket.io/publication.bib","dataSources":["9BWFRLuir5vrfREwa"],"keywords":[],"search_terms":["efficiently","check","concurrent","programs","under","relaxed","memory","models","maude","abd alrahman","andric","beggiato","lluch-lafuente"],"title":"Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude?","year":2014}