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 Atzeni | 1 | 32 | 2.68 |
Ganesh Gopalakrishnan | 2 | 1619 | 130.11 |