zbMATH — the first resource for mathematics

Can we efficiently check concurrent programs under relaxed memory models in Maude? (English) Zbl 1367.68057
Escobar, Santiago (ed.), 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. Cham: Springer (ISBN 978-3-319-12903-7/pbk; 978-3-319-12904-4/ebook). Lecture Notes in Computer Science 8663, 21-41 (2014).
Summary: 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.
For the entire collection see [Zbl 1318.68016].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q42 Grammars and rewriting systems
Full Text: DOI