PaPDAS Workshop

July 1-2, 2014

Orléans, France

Date and Location

Tuesday and Wednesday, July 1-2, 2014

Université d'Orléans, LIFO, Orléans, France

Rooms: SR1 and SR2

Organised by Frédéric Loulergue, Thomas Pinsard and Isabelle Renard


Registration is free (without dinner) but mandatory. The deadline for registration is June 21, 2014.

Program (schedule may change)

Tuesday, July 1

Welcome and introduction (9h00-9h30)

  • 9h00-9h15: Welcome
  • 9h15-9h30: Introduction

Session: Constructive algorithms (9h30-12h30)

Session Chair: Julien Tesson

  • 9h30-10h10: Kiminori Matsuzaki, Functional Models of Hadoop MapReduce and Their Application to Scan
    MapReduce, first proposed by Google, is a remarkable programming model for processing very large data. An open-source Java implementation of Google’s MapReduce, Hadoop, is now widely used for developing wide-range of applications. Under these situations, functional models for the MapReduce computation play important roles in for example understanding the computation, proving the correctness of programs, and even optimization. In this study, we develop five functional models that capture semantics of the MapReduce computation. In addition, we develop MapReduce algorithms for the list scan (prefix sums) on the proposed models. With the most concrete model of MapReduce, we can successfully define the BSP-based scan algorithm.
  • 10h10-10h50: Kento Emoto, Frédéric Loulergue, and Julien Tesson, A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
    The integration of the generate-and-test paradigm and semi-rings for the aggregation of results provides a parallel programming framework for large scale data-intensive applications. The so-called GTA framework allows a user to define an inefficient specification of his/her problem as a composition of a generator of all the candidate solutions, a tester of valid solutions, and an aggregator to combine the solutions. Through two calculation theorems a GTA specification is transformed into a divide-and-conquer efficient program that can be implemented in parallel. In this talk we present a verified implementation of this framework in the Coq proof assistant: efficient bulk synchronous parallel functional programs can be extracted from naive GTA specifications. We show how to apply this framework on an example, including performance experiments on parallel machines.
  • 10h50-11h10: Coffee Break

Session Chair: Kiminori Matsuzaki

  • 11h10-11h50: Reina Miyazaki and Kiminori Matsuzaki, Parallel Tree Accumulations on MapReduce
    MapReduce is a remarkable parallel programming model as well as a parallel processing infrastructure for large-scale data processing. MapReduce is now widely available on cloud environments, developing methodology or patterns of MapReduce programming is important. In particular, XML is the de facto standard for representing data, processing semi-structured data is involved in many applications. The target computational pattern in this paper are tree accumulations. Tree accumulations are shape-preserving computations over trees in which values are updated through flows over the tree. We develop BSP algorithms for two tree accumulations as extensions of the BSP algorithm for tree reduction by Kakehi et al. (2006). We also implemented the two-superstep algorithms by a single MapReduce execution. Experimental results on 16-node PC cluster show good speedups with factors of 10.9-12.7.
  • 11h50-12h30: Frédéric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Legaux, and Zhenjiang Hu. Formal Derivation and Extraction of a Parallel Program for the All Nearest Smaller Values Problem
    The All Nearest Smaller Values (ANSV) problem is an important problem for parallel programming as it can be used to solve several problems and is one of the phases of several other parallel algorithms. We formally develop by construction a functional parallel program for solving the ANSV problem using the theory of Bulk Synchronous Parallel (BSP) homomorphisms within the Coq proof assistant. The performances of the Bulk Synchronous Parallel ML program obtained from Coq is compared to a version derived without software support (pen-and-paper) and implemented using the Orléans Skeleton Library of algorithmic skeletons, and to a (unproved correct) direct implementation of the BSP algorithm of He and Huang.

Lunch (12h30-14h00)

Session: Algorithmic skeleton libraries (14h00-18h00)

Session Chair: Frédéric Loulergue

  • 14h15-15h30 Invited Talk: Joel Falcou, Costless Software Abstractions for Parallel Architectures
    Performing large, intensive or non-trivial computing on array like data structures is one of the most common task in scientific computing, video game development and other fields. This matter of fact is backed up by the large number of tools, languages and libraries to perform such tasks. If we restrict ourselves to C++ based solutions, more than a dozen such libraries exists from BLAS/LAPACK C++ binding to template meta-programming based Blitz++ or Eigen. If all of these libraries provide good performance or good abstraction, none of them seems to fit the need of so many different user types. Moreover, as parallel system complexity grows, the need to maintain all those components quickly become unwieldy. This talk explores various software design techniques and their application to the implementation of a parallel computing librariy in such a way that:
    - abstraction and expressiveness are maximized through the use of Parallel Skeletons
    - cost over efficiency is minimized thanks to Generative Programming
    - architecture specific hints are used throughout the whole library thanks to architecture aware tag dispatching
    We'll skim over various applications and see how they can benefit from such tools. We will conclude by discussing what lessons were learnt from this kind of implementation and how those lessons can translate into new directions for the C++ language itself and for the design of future Parallel Skeletons.
  • 15h30-16h00: Coffee Break

Session Chair: Julien Tesson

  • 16h00-16h40: Kento Emoto, Kiminori Matsuzaki, The SkeTo Library
    The SkeTo (Skeletons in Tokyo) library is a library of algorithmic skeletons, which was originally designed to allow users to describe parallel computations in a sequential manner and implemented in C++ on top of MPI. It provides three distributed data structures for lists (1D-arrays), matrices (2D-arrays) and trees, as well as skeletons for their manipulation. Recent works on the SkeTo library have been done for its automatic optimization mechanism by using the meta-programming technique with C++ templates. In this talk, we will introduce the outline of our SkeTo library and show how we integrated the optimization mechanism on the algorithmic skeletons.
  • 16h40-17h20: Joeffrey Légaux, Noman Javed, Sylvain Jubertie, and Frédéric Loulergue, OSL: The Orléans Skeleton Library
    Structured parallel models such as algorithmic skeletons offer a global view of the parallel program in contrast with the fragmented view of the SPMD style. This makes program easier to write and to read for users, and offer additional opportunities for optimisation done by the libraries, compilers and/or run-time systems. Algorithmic skeletons are or can be seen as patterns or higher-order functions implemented in parallel, often manipulating distributed data structures. Orléans Skeleton Library (OSL) is a library of parallel algorithmic skeletons, written in C++ on top of MPI, which uses meta-programming techniques for optimisation. This talk will present the recent work on OSL: skeletons used to manage arbitrary distributions of distributed arrays, support for BSP homomorphisms, an exception mechanism that ensures the global coherence of the system after exceptions are caught.
  • 17h20-10h00: Shigeyuki Sato, Kiminori Matsuzaki, A Generic Implementation of Tree Skeletons
    In data-parallel skeleton libraries, the implementation of skeletons is usually tightly-coupled with that of data structures. However, a loose coupling between both like C++ STL will improve modularity and flexibility of skeletons and data structures. This flexibility is particularly valuable for tree skeletons. To achieve such a loose coupling, we present an iterator-based interface of trees for tree skeletons. We have implemented tree skeletons on the basis of our interface; we present their design and implementation. This paper also reports the results of preliminary experiments.


Wednesday, July 2

Session: Verified compilation (10h00-12h10)

Session Chair: Frédéric Loulergue

  • 10h00-11h10: Invited Speaker Francesco Zappa Nardelli, We can't get memory models right.
  • 11h10-11h30: Coffee Break
  • 11h30-12h10: Thomas Pinsard, Frédéric Dabrowski, Frédéric Loulergue, Nested Atomic Sections with Thread Escape: From a Formal Definition to Verified Compilation
    We consider a simple imperative language with fork/join parallelism and lexically scoped nested atomic sections from which threads can escape. In this context, our contribution is the precise definition of atomicity, well-synchronisation on execution traces and the proof that the latter implies the strong form of the former. Then we define the formal operational semantics of this language that satisfies these specifications.



The Symposium on High Level Parallel Programming and Applications (HLPP) is held in Amsterdam on July 3-4.

Trains from Orléans to Amsterdam on July, 2:

  • 13h28 - 18h42
  • 15h28 - 20h42
  • 17h28 - 22h42
Last modified 3 years ago Last modified on Jul 3, 2014, 10:06:28 AM