OpenMP竞争分析的操作语义基础
An Operational Semantic Basis for OpenMP Race Analysis
摘要：
OpenMP是利用新一代超级计算机中的节点上并行性的事实标准。尽管其总体上易于使用，但即使是专家用户也知道创建隐藏并发错误的OpenMP程序，其中最隐蔽的错误之一是{ \em数据竞争}。OpenMP也是一个快速发展的标准，一个简单而严格的操作语义可以帮助建立可靠的竞争检查器，并通过程序员教育和更好地避免未来的错误。本文的主要贡献是为OpenMP提供了一个简单的操作语义，其中的原始事件与当今流行的OpenMP运行时和跟踪方法（如OMPT）所生成的事件相匹配，这使得我们的操作语义不仅仅是一个理论文档，更是一个智力启迪;它可以作为OpenMP事件捕获和工具构建的蓝图。我们通过总结新的数据竞争检查器的工作原理来支持这一说法，我们的语义所服务的更大的目的是服务于OpenMP社区关于他们对OpenMP的预期扩展以及未来的工具工作的需求。
英文摘要：
OpenMP is the de facto standard to exploit the on-node parallelism in new generation supercomputers.Despite its overall ease of use, even expert users are known to create OpenMP programs that harbor concurrency errors, of which one of the most insidious of errors are {\em data races}.OpenMP is also a rapidly evolving standard, which means that future data races may be introduced within unfamiliar contexts.A simple and rigorous operational semantics for OpenMP can help build reliable race checkers and ward off future errors through programmer education and better tooling.This paper's key contribution is a simple operational semantics for OpenMP, with primitive events matching those generated by today's popular OpenMP runtimes and tracing methods such as OMPT.This makes our operational semantics more than a theoretical document for intellectual edification; it can serve as a blueprint for OpenMP event capture and tool building.We back this statement by summarizing the workings of a new data race checker for OpenMP being built based on this semantics.The larger purpose served by our semantics is to serve the needs of the OpenMP community with regard to their contemplated extensions to OpenMP, as well as future tooling efforts.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
