MYX: MUST correctness checking for YML and XMP programs

Exascale挑战程序员编写多级并行程序，这意味着使用不同的范式来处理系统中的多级并行性。在针对千万亿级后系统的多级编程范式FP3C中，用户能够用YML工作流语言表达高级并行性，并使用用XcalableMP范式编写的并行组件。XcalableMP （XMP）旨在结合生产力和性能，是日本PC集群联盟指定的一种基于指令的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.