Book chapter ยท Conference paper
Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude?
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.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2014 |
Pages: | 21-41 |
Proceedings: | 10th International Workshop on Rewriting Logic and its Applications (WRLA 2014)International Workshop on Rewriting Logic and Its Applications |
Series: | Lecture Notes in Computer Science |
ISBN: | 3319129031 , 331912904X , 331912904x , 9783319129037 and 9783319129044 |
ISSN: | 16113349 and 03029743 |
Types: | Book chapter and Conference paper |
DOI: | 10.1007/978-3-319-12904-4_2 |
ORCIDs: | Lluch Lafuente, Alberto |