Paper Info
Title
Automatic Verification of Determinism for Structured Parallel Programs
Abstract
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.
Year
DOI
Venue
2010
10.1007/978-3-642-15769-1_28
SAS
Keywords
Field
DocType
sequential analysis,static analysis
Programming language,Abstraction,Suite,Computer science,Determinism,Static analysis,Theoretical computer science,Dice
Conference
Volume
ISSN
ISBN
6337
0302-9743
3-642-15768-8
Citations 
PageRank 
References 
18
0.70
24
Authors
4
Name
Order
Citations
PageRank
Martin T. Vechev187548.07
Eran Yahav2170679.49
Raghavan Raman323510.70
Vivek Sarkar44318409.41