A formal semantics of the MULTI-ML language

International audienceIn the context of high performance computing, it is important to avoid indeterminism and deadlocks. MULTI-ML is a functional parallel programming language " à la ML " , designed to program hierarchical architectures in a structured way. It is based of the MULTI-BSP bridging model. To ensure that a program " cannot go wrong " , we first need to define how a program " goes ". To do so, we propose a formal operational semantics of the MULTI-ML language to ensure the properties of the MULTI-BSP model. We first describe a core-language and then introduce the big step's semantics evaluation rules. Then, we propose a set of evaluation rules that describe the behaviour of the MULTI-ML language. The memory model is also precisely defined, as the MULTI-BSP model deals with multiple level of nested memories