zbMATH — the first resource for mathematics

Automatic verification of determinism for structured parallel programs. (English) Zbl 1306.68037
Cousot, Radhia (ed.) et al., Static analysis. 17th international symposium, SAS 2010, Perpignan, France, September 14–16, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-15768-4/pbk). Lecture Notes in Computer Science 6337, 455-471 (2010).
Summary: We present a static analysis for automatically verifying determinism of structured parallel programs. The main idea is to leverage the structure of the program to reduce determinism verification to an independence property that can be proved using a simple sequential analysis. Given a task-parallel program, we identify program fragments that may execute in parallel and check that these fragments perform independent memory accesses using a sequential analysis. Since the parts that can execute in parallel are typically only a small fraction of the program, we can employ powerful numerical abstractions to establish that tasks executing in parallel only perform independent memory accesses. We have implemented our analysis in a tool called Dice and successfully applied it to verify determinism on a suite of benchmarks derived from those used in the high-performance computing community.
For the entire collection see [Zbl 1196.68004].

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