Title
An Operational Semantic Basis for Building an OpenMP Data Race Checker
Abstract
Despite the popularity and growing importance of OpenMP, a formal characterization of its concurrency is lacking. In this paper, we provide such a characterization through an operational semantics. Semantic descriptions of languages are written to serve specific end goals, and hence are abstractions of fully detailed implementations. We have developed our semantics to help with the construction of a novel OpenMP data race checker called Sword that collects execution traces efficiently, and subjects the traces to offline analysis: the semantics are used in the latter phase. Key contributions of this paper are: (1) defining OpenMP's concurrency rigorously through a precise set of rules, (2) helping systematically design Sword's offline analysis phase by ensuring that the OpenMP events mentioned in our semantics are exactly those that can also be collected through OMPT, a standard event collection mechanism for OpenMP, and (3) characterizing the benefits of this design. We conclude with the message that developing formal semantics for concurrent languages must not be viewed as an esoteric diversion, but as standard practice, as such semantics can help clearly define the language, help rigorously analyze proposed future extensions to it, and also help reveal lurking pitfalls, especially in this era where multiple concurrency formalisms are often used together.
Year
DOI
Venue
2018
10.1109/IPDPSW.2018.00074
2018 IEEE International Parallel and Distributed Processing Symposium Workshops (IPDPSW)
Keywords
Field
DocType
High Performance Computing,OpenMP,Operational Semantics of OpenMP,Data Race Checking
Operational semantics,Programming language,Supercomputer,Concurrency,Instruction set,Computer science,Implementation,Concurrent computing,Rotation formalisms in three dimensions,Semantics,Distributed computing
Conference
ISSN
ISBN
Citations 
2164-7062
978-1-5386-5556-6
1
PageRank 
References 
Authors
0.36
9
2
Name
Order
Citations
PageRank
Simone Atzeni1322.68
Ganesh Gopalakrishnan21619130.11