- Renseignements pratiques
- Enseignement
Contact
LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2
Tel: +33 (0)2 38 41 70 11
Fax: +33 (0)2 38 41 71 37
Accéder aux Rapports de l'année : 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013
RR-2013-01 Parallel Programming with BSP Homomorphisms
Joeffrey Legaux, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, Julien Tesson
Résumé : Les squelettes algorithmiques combinés aux homomorphismes de listes jouent un rôle important dans le développement formel d'algorithmiques parallèle. Nous avons conçu une notion d'homomorphisme adapté au parallélisme quasi synchrone (BSP). Dans cet article nous dérivons deux applications en nous basant sur cette théorie: une multiplication matrice creuse par vecteur, et le problème de des plus petites valeurs les plus proches (ANSV). Nous décrivons l'implantation d'un squelette algorithmique dédié dans la bibliothèque OSL et des expériences avec les deux applications.
Mot(s) Clé(s) :
RR-2013-02 Programming and Reasonning with PowerLists in Coq
Frédéric Loulergue, Virginia Niculescu
Résumé : Le développement de programmes parallèles corrects par construction est activité importante puisque, pour les programmes parallèles, la vérification a posteriori est très complexe, et le déboggage extrêmement difficile. Construire des programmes corrects n'est pas une tâche aisée et les méthodologies usuelles pour le faire sont souvent théoriques et non outillées. Une meilleure approche serait de concevoir des outils logiciels basés sur ces théories. Un utilisateur pourrait alors développer des application en implantant des programmes simples satisfaisants certaines conditions facilement, ou idéalement automatiquement, prouvées, à partir desquels un environnement de développement générerait des programmes parallèles efficaces. La théorie des PowerLists et ses variantes est une bonne base théorique pour une telle approche. Par ailleurs l'assistant de preuve Coq est un outil logiciel permettant la modélisation, la preuve, et dans une certaines mesure l'automatisation des preuves, et est à ce titre un bon point de départ pour un tel environnement de développement. Le but de cet article est de modéliser les PowerLists in Coq, d'utiliser cette modélisation pour programmer et raisonner sur des programmes parallèles en Coq. C'est un première étape indispensable à la réalisation d'un environnement pour le développement de programmes parallèles corrects et vérifiables.
Mot(s) Clé(s) :
RR-2013-03 A Constraint Programming Approach for Constrained Clustering
Thi-Bich-Hanh Dao, Khanh-Chuong Duong, Christel Vrain
Résumé : Clustering is an important task in Data Mining and many algorithms have been designed for it. It has been extended to semi-supervised clustering, so as to integrate some previous knowledge on objects that must be or cannot be in the same cluster, and many classical algorithms have been extended to handle such constraints. Other kinds of constraints could be specified by the user, as for instance the sizes of the clusters or their diameters, but adding such constraints generally requires to develop new algorithms. We propose a declarative and generic framework, based on Constraint Programming, which enables to design a clustering task by specifying an optimization criterion and some constraints either on the clusters or on pairs of objects. In our framework, several classical optimization criteria are considered and they can be coupled with different kinds of constraints. Relying on Constraint Programming has two main advantages: the declarativity, which enables to easily add new constraints and the ability to find an optimal solution satisfying all the constraints (when there exists one). On the other hand, computation time depends on the constraints and on their ability to reduce the domain of variables, thus avoiding an exhaustive search.
Mot(s) Clé(s) :
RR-2013-04 Over-approximating Descendants by Synchronized Tree Languages
Yohan Boichut, Jacques Chabin, Pierre Réty
Résumé : Over-approximating the descendants (successors) of a initial set of terms by a rewrite system is used in verification. The success of such verification methods depends on the quality of the approximation. To get better approximations, we are going to use non-regular languages. We present a procedure that always terminates and that computes an over-approximation of descen- dants, using synchronized tree-(tuple) languages expressed by logic programs.
Mot(s) Clé(s) : Rewriting, descendants, tree languages, logic programming
RR-2013-05 Nested Atomic Sections with Thread Escape: A Formal Definition
Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard
Résumé : Nous considérons un langage impératif parallèle simple avec lancement/attente de processus légers et des sections atomiques emboîtées dont les processus légers peuvent s'échapper. Dans ce contexte notre contribution est une définition précise d'atomicité, de bonne synchronisation et une preuve que cette dernière implique la forme forte de la première. Une formalisation de nos résultats dans l'assistant de preuve Coq est disponible.
Mot(s) Clé(s) : sections atomiques, bonne synchronisation, traces de programmes, sémantiques formelles, assistant de preuve
Les rapports de recherche du LIFO en 2013
RR-2013-01
Parallel Programming with BSP Homomorphisms
Joeffrey Legaux, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, Julien Tesson
Date : 2013-03-22
Résumé Télécharger
RR-2013-02
Programming and Reasonning with PowerLists in Coq
Frédéric Loulergue, Virginia Niculescu
Date : 2013-03-26
Résumé Télécharger
RR-2013-03
A Constraint Programming Approach for Constrained Clustering
Thi-Bich-Hanh Dao, Khanh-Chuong Duong, Christel Vrain
Date : 2013-05-07
Résumé Télécharger
RR-2013-04
Over-approximating Descendants by Synchronized Tree Languages
Yohan Boichut, Jacques Chabin, Pierre Réty
Date : 2013-04-19
Résumé Télécharger
RR-2013-05
Nested Atomic Sections with Thread Escape: A Formal Definition
Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard
Date : 2013-06-24
Résumé Télécharger
Résumés des rapports de recherche
RR-2013-01 Parallel Programming with BSP Homomorphisms
Joeffrey Legaux, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, Julien Tesson
Résumé : Les squelettes algorithmiques combinés aux homomorphismes de listes jouent un rôle important dans le développement formel d'algorithmiques parallèle. Nous avons conçu une notion d'homomorphisme adapté au parallélisme quasi synchrone (BSP). Dans cet article nous dérivons deux applications en nous basant sur cette théorie: une multiplication matrice creuse par vecteur, et le problème de des plus petites valeurs les plus proches (ANSV). Nous décrivons l'implantation d'un squelette algorithmique dédié dans la bibliothèque OSL et des expériences avec les deux applications.
Mot(s) Clé(s) :
RR-2013-02 Programming and Reasonning with PowerLists in Coq
Frédéric Loulergue, Virginia Niculescu
Résumé : Le développement de programmes parallèles corrects par construction est activité importante puisque, pour les programmes parallèles, la vérification a posteriori est très complexe, et le déboggage extrêmement difficile. Construire des programmes corrects n'est pas une tâche aisée et les méthodologies usuelles pour le faire sont souvent théoriques et non outillées. Une meilleure approche serait de concevoir des outils logiciels basés sur ces théories. Un utilisateur pourrait alors développer des application en implantant des programmes simples satisfaisants certaines conditions facilement, ou idéalement automatiquement, prouvées, à partir desquels un environnement de développement générerait des programmes parallèles efficaces. La théorie des PowerLists et ses variantes est une bonne base théorique pour une telle approche. Par ailleurs l'assistant de preuve Coq est un outil logiciel permettant la modélisation, la preuve, et dans une certaines mesure l'automatisation des preuves, et est à ce titre un bon point de départ pour un tel environnement de développement. Le but de cet article est de modéliser les PowerLists in Coq, d'utiliser cette modélisation pour programmer et raisonner sur des programmes parallèles en Coq. C'est un première étape indispensable à la réalisation d'un environnement pour le développement de programmes parallèles corrects et vérifiables.
Mot(s) Clé(s) :
RR-2013-03 A Constraint Programming Approach for Constrained Clustering
Thi-Bich-Hanh Dao, Khanh-Chuong Duong, Christel Vrain
Résumé : Clustering is an important task in Data Mining and many algorithms have been designed for it. It has been extended to semi-supervised clustering, so as to integrate some previous knowledge on objects that must be or cannot be in the same cluster, and many classical algorithms have been extended to handle such constraints. Other kinds of constraints could be specified by the user, as for instance the sizes of the clusters or their diameters, but adding such constraints generally requires to develop new algorithms. We propose a declarative and generic framework, based on Constraint Programming, which enables to design a clustering task by specifying an optimization criterion and some constraints either on the clusters or on pairs of objects. In our framework, several classical optimization criteria are considered and they can be coupled with different kinds of constraints. Relying on Constraint Programming has two main advantages: the declarativity, which enables to easily add new constraints and the ability to find an optimal solution satisfying all the constraints (when there exists one). On the other hand, computation time depends on the constraints and on their ability to reduce the domain of variables, thus avoiding an exhaustive search.
Mot(s) Clé(s) :
RR-2013-04 Over-approximating Descendants by Synchronized Tree Languages
Yohan Boichut, Jacques Chabin, Pierre Réty
Résumé : Over-approximating the descendants (successors) of a initial set of terms by a rewrite system is used in verification. The success of such verification methods depends on the quality of the approximation. To get better approximations, we are going to use non-regular languages. We present a procedure that always terminates and that computes an over-approximation of descen- dants, using synchronized tree-(tuple) languages expressed by logic programs.
Mot(s) Clé(s) : Rewriting, descendants, tree languages, logic programming
RR-2013-05 Nested Atomic Sections with Thread Escape: A Formal Definition
Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard
Résumé : Nous considérons un langage impératif parallèle simple avec lancement/attente de processus légers et des sections atomiques emboîtées dont les processus légers peuvent s'échapper. Dans ce contexte notre contribution est une définition précise d'atomicité, de bonne synchronisation et une preuve que cette dernière implique la forme forte de la première. Une formalisation de nos résultats dans l'assistant de preuve Coq est disponible.
Mot(s) Clé(s) : sections atomiques, bonne synchronisation, traces de programmes, sémantiques formelles, assistant de preuve
