Bulk Synchronous Parallel ML or BSML is a functional data-parallel language for programming bulk synchronous parallel (BSP) algorithms. The execution time can be estimated and dead-locks and indeterminism are avoided. For large scale applications where parallel processing is helpful and where the total amount of data often exceeds the total main memory available, parallel disk I/O becomes a necessity. We present here a library of I/O features for BSML and its cost model.
Bulk Synchronous Parallel ML or BSML is a functional data-parallel language for programming bulk synchronous parallel (BSP) algorithms. The execution time can be estimated and dead-locks and indeterminism are avoided. For large scale applications, more than one parallel machine is needed. We consider here the design and cost-model of a BSML-like language devoted to the programming of such applications: Departmental Metacomputing ML or DMML.
BSML (Bulk-Synchronous Parallel ML) et DMML (Departmental Metacomputing ML) sont deux extensions ML pour la programmation fonctionnelle d'algorithmes parallèles.C'est autour de ces extensions que mon stage fût axé. Tout d'abord, mon travail était d'enrichir les implémentations proposées par la BSMLlib. La prévision de performance est un élément important dans l'élaboration de programmes, il était nécessaire d'avoir un programme écrit en BSML permettant d'obtenir les paramètres BSP de la machine parallèle. En plus de ces paramètres, le programme permet aussi d'obtenir la puissance de calcul de cette même machine. Enfin, une expérimentation a mis en évidence cette prévision de performance.
The Bulk Synchronous Parallel ML (BSML) is a functional language for BSP programming, a model of computing which allows parallel programs to be ported to a wide range of architectures. It is based on an extension of the ML language by parallel operations on a parallel data structure called parallel vector, which is given by intention. We present a new approach to certifying BSML programs in the context of type theory. Given a specification and a program, an incomplete proof of the specification (of which algorithmic contents corresponds to the given program) is built in the type theory, in which gaps would correspond to the proof obligation. This development demonstrates the usefulness of higher-order logic in the process of software certification of parallel applications. It also shows that the proof of rather complex parallel algorithms may be done with inductive types without great difficulty by using existing certified programs. This work has been implemented in the Coq Proof Assistant, applied on non-trivial examples and is the basis of a certified library of BSML programs.
The BSML (Bulk Synchronous ML) language is a data-parallel functional language for programming BSP (Bulk Synchronous algorithms) algorithms in so-called direct mode. In a direct mode BSP algorithm, the physical structure of processes is made explicit. The execution time can then be estimated and dead-locks and indeterminism are avoided. The BSMLlib library, the current implementation of the BSML language, permits, as an extension of Objective Caml, the use of the exceptions handling mechanism that comes with this language. However, the interaction of Objective Caml exceptions with the BSλ-calculus (the theoretical model underlying the BSML language) has not yet been studied and yields some safety issues. In particular, the use of collective synchronization operations needs the participation of all processes during the call to one of these operation, should the opposite occur, processes involved in this call are locked. The BSML language, without exceptions, ensures that all processes participate to such a call and thus that dead-locks are avoided (except for process failure). When one introduces Objective Caml exceptions, this safety property does not hold any more. Thus it is needed to study a new semantics, suitable to exceptions handling, to recover this property. The present work introduces such a semantics in which the participation of all processes is ensured and dead-lock issues are avoided. We will also introduce a semantics allowing the pattern-matching of BSML parallel vectors. This semantics has been studied in the framework of a previous work on exceptions handling which has not been retained here but its functionalities will be nethertheless add to the BSML language.
The BSMLlib library is a library for Bulk Synchronous Parallel (BSP) programming with the functional language Objective Caml. It is based on an extension of the λ-calculus by parallel operations on a data structure named parallel vector, which is given by intention. In order to have an execution that follows the BSP model, and to have a simple cost model, nesting of parallel vectors is not allowed. The novelty of this work is a type system which prevents such nesting. This system is correct w.r.t. the dynamic semantics which is also presented. An inference algorithm is given.
This file was generated by bibtex2html 1.96.