MYX: MUST correctness checking for YML and XMP programs

Exascale挑战程序员编写多级并行程序，这意味着采用不同的范例来解决系统中的多级并行性。在面向后千万亿次系统的多级编程范式FP3C中，用户能够用YML工作流语言表达高级并行性，并采用用XcalableMP范式编写的并行组件。XcalableMP（XMP）旨在将生产力和性能联合收割机结合起来，是日本PC Cluster Consortium指定的基于指令的PGAS（分区全局地址空间）语言。在那里，它是研究后千万亿次编程模型的主要工具。XMP提供了全局视图模型和局部视图模型，前者针对节点级并行性，后者提供了完整的PGAS编程模型。XMP的实现采用MPI作为通信接口，YML采用YvetteML工作流语言在很高的层次上描述应用程序的并行性。YML提供了一个编译器来将YvetteML符号转换为XMP并行程序，以及一个实时调度器来管理并行程序的执行。它允许对程序员隐藏底层的通信细节，特别是在耦合复杂的应用程序时。通过利用MPI分析接口，MUST正确性检查器目前可以检测MPI以及OpenMP和混合程序中的各种问题。该项目的总体目标是通过提高编程生产力来简化未来Exascale系统的编程。为此，我们将研究应用可扩展的正确性检查方法，以支持YML工作流语言，XMP编程模型和MPI的选定功能，如单边通信。这包括研究如何编程语言和并行化范式可以扩展，以提高自动正确性检查分析的有效性和可扩展性。总之，我们将解决两个开放的研究问题：第一，需要哪些属性的语言或并行化范式，以实现有效的自动正确性检查，并可能避免错误摆在首位，第二，如何可以扩展现有的规范或API，以提供必要的语义信息的正确性检查工具。XMP正确性检查支持的开发将显著提高Exascale系统XMP编程的生产力。该项目延续了法国和日本10多年的合作，并增加了可扩展的正确性检查支持作为一个新的组件，由德国合作伙伴提供。该项目将导致联合研究、出版物和软件开发，因此预计将为今后的研究活动积累重要的资产。

Exascale challenges the programmer to write multi-level parallel programs, which means employing different paradigms to address multiple levels of parallelism in the system. In the multi-level programming paradigm FP3C targeting post-petascale systems, users are able to express high-level parallelism in the YML workflow language and employ parallel components written in the XcalableMP paradigm.XcalableMP (XMP) aims to combine productivity and performance and is a directive-based PGAS (partitioned global address space) language specified by Japan's PC Cluster Consortium. There it is the main vehicle for research in post-petascale programming models. XMP provides both, a global-view model and a local-view model - the first targeting node-level parallelism, and the latter offering a complete PGAS programming model. The XMP implementation employs MPI as its communication interface.In YML, the YvetteML workflow language is used to describe the parallelism of an application at a very high level. YML provides a compiler to translate the YvetteML notation into XMP-parallel programs, and a just-in-time scheduler managing the execution of parallel programs. It allows to hide low-level communication details from the programmer, particularly when coupling complex applications.Runtime error detection is the most practical approach for correctness checking. By exploiting the MPI profiling interface, the MUST correctness checker currently can detect a wide range of issues in MPI, as well as OpenMP and hybrid programs.The overall goal of this project is to ease programming of future Exascale systems by increasing the programming productivity. To this end we will investigate the application of scalable correctness checking methods to support the YML workflow language, the XMP programming model and selected features of MPI, such as one-sided communication. This includes research on how programming languages and parallelization paradigms could be extended to increase the validity and scalability of automatic correctness checking analyses. In summary, we will address two open research questions: first, which properties of a language or parallelization paradigm are required to enable effective automatic correctness checking and possibly to avoid errors in the first place, and second, how can existing specifications or APIs be extended to provide the necessary semantic information for the correctness checking tool. The development of correctness checking support for XMP will significantly improve the productivity in programming with XMP for Exascale systems.This project continues a French-Japanese collaboration existing for over 10 years and adds the scalable correctness checking support as a new component, delivered by the German partner. The project will result in joint research, publications and software development and consequently is expected to build important assets for future research activities.