Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude?

Yehia Abd Arrahman; Marina Andric; Alessandro Beggiato; Alberto Lluch Lafuente

doi:10.1007/978-3-319-12904-4_2

Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude?

Yehia Abd Arrahman, Marina Andric, Alessandro Beggiato, Alberto Lluch Lafuente

Department of Applied Mathematics and Computer Science

IMT Institute for Advanced Studies Lucca

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

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.

Original language	English
Title of host publication	Revised Selected Papers of the 10th International Workshop on Rewriting Logic and Its Applications, WRLA 2014
Editors	Santiago Escobar
Publisher	Springer
Publication date	2014
Pages	21-41
ISBN (Print)	978-3-319-12903-7
ISBN (Electronic)	978-3-319-12904-4
DOIs	https://doi.org/10.1007/978-3-319-12904-4_2
Publication status	Published - 2014
Event	10th International Workshop on Rewriting Logic and its Applications (WRLA 2014) - Grenoble, France Duration: 5 Apr 2014 → 6 Apr 2014 Conference number: 10 http://users.dsic.upv.es/workshops/wrla2014/#main

Workshop

Workshop	10th International Workshop on Rewriting Logic and its Applications (WRLA 2014)
Number	10
Country/Territory	France
City	Grenoble
Period	05/04/2014 → 06/04/2014
Internet address	http://users.dsic.upv.es/workshops/wrla2014/#main

Series	Lecture Notes in Computer Science
Volume	8663
ISSN	0302-9743

Access to Document

10.1007/978-3-319-12904-4_2

OpenUrl availability

Full text

Cite this

@inproceedings{b1571a64fa6f4913b370070b22ce8140,

title = "Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude?",

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.",

author = "Arrahman, {Yehia Abd} and Marina Andric and Alessandro Beggiato and {Lluch Lafuente}, Alberto",

year = "2014",

doi = "10.1007/978-3-319-12904-4_2",

language = "English",

isbn = "978-3-319-12903-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "21--41",

editor = "Escobar, {Santiago }",

booktitle = "Revised Selected Papers of the 10th International Workshop on Rewriting Logic and Its Applications, WRLA 2014",

note = "10th International Workshop on Rewriting Logic and its Applications (WRLA 2014), WRLA ; Conference date: 05-04-2014 Through 06-04-2014",

url = "http://users.dsic.upv.es/workshops/wrla2014/#main",

}

Arrahman, YA, Andric, M, Beggiato, A & Lluch Lafuente, A 2014, Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude? in S Escobar (ed.), Revised Selected Papers of the 10th International Workshop on Rewriting Logic and Its Applications, WRLA 2014. Springer, Lecture Notes in Computer Science, vol. 8663, pp. 21-41, 10th International Workshop on Rewriting Logic and its Applications (WRLA 2014), Grenoble, France, 05/04/2014. https://doi.org/10.1007/978-3-319-12904-4_2

Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude? / Arrahman, Yehia Abd; Andric, Marina; Beggiato, Alessandro et al.
Revised Selected Papers of the 10th International Workshop on Rewriting Logic and Its Applications, WRLA 2014. ed. / Santiago Escobar. Springer, 2014. p. 21-41 (Lecture Notes in Computer Science, Vol. 8663).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review