PaPDAS - Parallel Program Development with Algorithmic Skeletons

In the PaPDAS project we are interested at providing a framework to ease the development of parallel programs in a systematic way using constructive algorithmics, and to either execute very efficiently the obtained programs or to compile these programs with a verified optimizing parallel compiler.

Team

• Frédéric Dabrowski (co-PI), ​LIFO, ​Université d'Orléans
• Kiminori Matsuzaki (co-PI), ​Kochi University of Technology
• Frédéric Loulergue (co-Investigator), ​LIFO, ​Université d'Orléans

• Wadoud Bousdira, ​LIFO, ​Université d'Orléans
• Sylvain Dailler, ​LIFO, ​Université d'Orléans and ​Kochi University of Technology
• Kento Emoto, ​IPL, The University of Tokyo
• Zhenjiang Hu, ​National Institute of Informatics
• Noman Javed, ​LIFO, ​Université d'Orléans / Namal College, Pakistan
• Yiu Liu, ​The Graduate University for Avanced Studies
• Thomas Pinsard, ​LIFO, ​Université d'Orléans
• Simon Robillard, ​LIFO, ​Université d'Orléans
• Vitor Rodrigues, ​LIFO, ​Université d'Orléans
• Yoshiaki Takata, ​Kochi University of Technology
• Julien Tesson, ​LIFO, ​Université d'Orléans and ​Kochi University of Technology

Support

PaPDAS is a project supported by ​ANR (project ANR- 2010-INTB-0205-02) and ​JST (project 10102704) from 2011 to 2014.

Events

• July 1-2, 2014, the PaPDAS workshop (workshop)
• October, 2013, the 3rd workshop on Frameworks for the Development of Correct (parallel) Programs (FraDeCoPP-3)
• November 26, 2012, the 2nd workshop on Frameworks for the Development of Correct (parallel) Programs (FraDeCoPP-2)
• May 15, 2012, the 1st workshop on Frameworks for the Development of Correct (parallel) Programs (FraDeCoPP2012)
• Jeudi 22 mars 2012 l'atelier Conception et implantation de squelettes algorithmiques / Thursday March 22, 2012 workshop Design and Implementation of Algorithmic Skeletons

Software

The new developments of the following software is now supported by the PaPDAS project:

• The ​OSL Library
• The ​SkeTo Library
• The ​SyDPaCC Library
• The SyDRec module for Coq

Publications

International refeered journals

1. Kiminori Matsuzaki. “Functional Models of Hadoop MapReduce? with Application to Scan”. In: Int J Parallel Prog (2015). To appear.
2. Frédéric Loulergue, Wadoud Bousdira, and Julien Tesson. “Calculating Parallel Programs in Coq using List Homomorphisms”. In: Int J Parallel Prog (2015). To appear.
3. Frédéric Dabrowski, Frédéric Loulergue, and Thomas Pinsard. “A Formal Semantics of Nested Atomic Sections with Thread Escape”. In: Comput Lang Syst Str (2015). DOI: ​10.1016/j.cl.2015.04.001.
4. Kiminori Matsuzaki and Reina Miyazaki. “Parallel Tree Accumulations on MapReduce”. In: Int J Parallel Prog (2015). DOI: ​10.1007/s10766-015-0355-8.
5. Shigeyuki Sato and Kiminori Matsuzaki. “A Generic Implementation of Tree Skeletons”. In: Int J Parallel Prog (2015). DOI: ​10.1007/s10766-015-0355-6.
6. K. Emoto and K. Matsuzaki. “An Automatic Fusion Mechanism for Variable-Length List Skeletons in SkeTo”. In: Int J Parallel Prog (2013). DOI: ​/s10766-013-0263-8.

Book chapter

1. Frédéric Loulergue, Wadoud Bousdira, and Julien Tesson. Calcul de programmes parallèles avec Coq. In Nicolas Ollinger, editor, Informatique Mathématique une photographie en 2015, collection Alpha, pages 87-134. CNRS Éditions, 2015.

International refereed conferences

1. Frédéric Dabrowski, Frédéric Loulergue, and Thomas Pinsard. “Nested Atomic Sections with Thread Escape: Compilation to Threads and Locks”. In: ACM Symposium on Applied Computing (SAC). Salamanca, Spain: ACM, 2015, pp. 2099–2106. DOI: ​10.1145/2695664.2695870.
2. Kento Emoto, Frédéric Loulergue, and Julien Tesson. “A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction”. In ITP, number 8558 in LNAI, pages 258-274. Springer, 2014. DOI: ​10.1007/978-3-319-08970-6_17.
3. Frédéric Dabrowski, Frédéric Loulergue, and Thomas Pinsard. “Nested Atomic Sections with Thread Escape: A Formal Definition”. In ACM Symposium on Applied Computing (SAC), pages 1585-1592. ACM Press, 2014. DOI: ​10.1145/2554850.2554996.
4. Frédéric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Légaux, and Zhenjiang Hu. “Formal Derivation and Extraction of a Parallel Program for the All Nearest Smaller Values Problem”. In: ACM Symposium on Applied Computing (SAC). Gyeongju, Korea: ACM, 2014, pp. 1577–1584. DOI: ​10.1145/2554850.2554912.
5. Joeffrey Légaux, Sylvain Jubertie, and Frédéric Loulergue. “Development Effort and Performance Trade-off in High-Level Parallel Programming”. In: International Conference on High Performance Computing and Simulation (HPCS). Bologna, Italy: IEEE, 2014, pp. 162–169. DOI: ​10.1109/HPCSim.2014.6903682.
6. Frédéric Loulergue, Virginia Niculescu, and Julien Tesson. “Implementing Powerlists with Bulk Synchronous Parallel ML”. In: Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). Timisoara, Romania: IEEE, 2014, pp. 325–332. DOI: ​10.1109/SYNASC.2014.51.
7. Joeffrey Légaux, Frédéric Loulergue, and Sylvain Jubertie. “OSL: an algorithmic skeleton library with exceptions”. In: International Conference on Computational Science (ICCS). Barcelona, Spain: Elsevier, 2013, pp. 260–269. DOI: ​10.1016/j.procs.2013.05.189.
8. Joeffrey Légaux, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, and Julien Tesson. “Programming with BSP Homomorphisms”. In: Euro-Par Parallel Processing. LNCS 8097. Aachen, Germany: Springer, 2013, pp. 446–457. DOI: ​10.1007/978-3-642-40047-6_46.
9. Joeffrey Légaux, Frédéric Loulergue, and Sylvain Jubertie. “Managing Arbitrary Distributions of Arrays in Orléans Skeleton Library”. In: International Conference on High Performance Computing and Simulation (HPCS). Helsinki, Finland: IEEE, 2013, pp. 437–444. DOI: ​10.1109/HPCSim.2013.6641451.
10. Frédéric Loulergue, Virginia Niculescu, and Simon Robillard. “Powerlists in Coq: Programming and Reasoning”. In: First International Symposium on Computing and Networking (CANDAR). Matsuyama, Japan: IEEE Computer Society, 2013, pp. 57–65. DOI: ​10.1109/CANDAR.2013.17.
11. Frédéric Dabrowski, Frédéric Loulergue, and Thomas Pinsard. “Nested Atomic Sections with Thread Escape: An Operational Semantics”. In: Parallel and Distributed Computing, Applications and Technologies (PDCAT). Taiwan: IEEE, 2013, pp. 29–35. DOI: ​10.1109/PDCAT.2013.12.
12. Wadoud Bousdira, Frédéric Loulergue, and Julien Tesson. “A Verified Library of Algorithmic Skeletons on Evenly Distributed Arrays”. In: Algorithms and Architectures for Parallel Processing (ICA3PP). LNCS 7439. Fukuoka, Japan: Springer, 2012, pp. 218–232. DOI: ​10.1007/978-3-642-33078-0_16.
13. Yu Liu, Zhenjiang Hu, and Kiminori Matsuzaki. “Towards Systematic Parallel Programming over MapReduce?”. In: Euro-Par 2011 Parallel Processing. Ed. by Emmanuel Jeannot, Raymond Namyst, and Jean Roman. Vol. 6853. LNCS. Springer, 2011, pp. 39–50. DOI: ​10.1007/978-3-642-23397-5_5.
14. Noman Javed and Frédéric Loulergue. “Verification of a Heat Diffusion Simulation written with Orléans Skeleton Library”. In: 9th International Conference on Parallel Processing and Applied Mathematics (PPAM 2011). LNCS 7204. Torun, Poland: Springer, 2012, pp. 91–100. DOI: ​10.1007/978-3-642-31500-8_10.
15. Noman Javed and Frédéric Loulergue. “Parallel Programming and Performance Predictability with Orléans Skeleton Library”. In: International Conference on High Performance Computing and Simulation (HPCS). Istanbul, Turkey: IEEE, 2011, pp. 257–263. DOI: ​10.1109/HPCSim.2011.5999832.
16. Noman Javed and Frédéric Loulergue. “A Formal Programming Model of Orléans Skeleton Library”. In: 11th International Conference on Parallel Computing Technologies (PaCT). Ed. by Victor Malyshkin. LNCS 6873. Kazan, Russia: Springer, 2011, pp. 40–52. DOI: ​10.1007/978-3-642-23178-0_4.

National refereed conferences

1. Kento Emoto, Kiminori Matsuzaki, ​Implementing a Fusion-equipped Library with boost::proto, IPSJ SIG-PRO Meeting, Februray 2013
2. Takayuki Kawamura and Kiminori Matsuzaki. ​Evaluation of Tree Processing based on the m-bridge Technique over Hadoop (in Japanese). In 29th Conference of the Japan Society for Software Science and Technology, August 2012.

Tutorials

1. Frédéric Loulergue, Wadoud Bousdira, Julien Tesson, Calcul de programmes parallèles en Coq, Course at the Spring School "Ecole des Jeunes Chercheurs en Informatique Mathématique", Orléans, France, 2015.
2. Frédéric Loulergue and Julien Tesson, Certified Parallel Program Calculation in Coq: A Tutorial, International Conference in High Performance Computing and Simulation (HPCS), Bologna, Italy, July 2014. DOI: ​10.1109/HPCSim.2014.6903655
3. Frédéric Loulergue. “Systematic Development of Correct Programs for Parallel and Cloud Computing”, Faculty of Mathematics and Informatics, Babes-Bolyai University of Cluj-Napoca, Romania, February 2014.
4. Frédéric Loulergue. “Systematic Development of Correct Programs for Parallel and Cloud Computing”, NII International advanced lectures series on ICT, Tokyo, Japan, October-November 2013 (7 lectures).

Thesis

1. Thomas Pinsard, Nested Atomic Sections with Thread Espace: Semantics and Compilation, PhD Thesis, LIFO, University of Orléans, December 2014
2. Joeffrey Légaux, ​Squelettes algorithmiques pour la programmation et l’exécution efficaces de codes parallèles, LIFO, University of Orléans, December 2013
3. Julien Tesson, ​Environnement pour le développement et la preuve de correction systématiques de programmes parallèles fonctionnels. PhD Thesis, LIFO, University of Orléans, November 2011
4. Noman Javed, ​Metaprogrammed Algorithmic Skeletons: Implementations, Performances and Semantics, PhD Thesis, LIFO, University of Orléans, October 2011

Deliverables