[[Image(ANR07-240.gif, nolink, right, width=180)]][[Image(jst.jpg, nolink, right)]]

= 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), [http://www.univ-orleans.fr/lifo LIFO], [http://www.univ-orleans.fr Université d'Orléans]
 * Kiminori Matsuzaki (co-PI), [http://www.kochi-tech.ac.jp/gs_e/index.html Kochi University of Technology]
 * Frédéric Loulergue (co-Investigator), [http://www.univ-orleans.fr/lifo LIFO], [http://www.univ-orleans.fr Université d'Orléans]

 * Wadoud Bousdira, [http://www.univ-orleans.fr/lifo LIFO], [http://www.univ-orleans.fr Université d'Orléans] 
 * Sylvain Dailler, [http://www.univ-orleans.fr/lifo LIFO], [http://www.univ-orleans.fr Université d'Orléans] and [http://www.kochi-tech.ac.jp/gs_e/index.html Kochi University of Technology]
 * Kento Emoto, [http://www.ipl.t.u-tokyo.ac.jp IPL, The University of Tokyo]
 * Zhenjiang Hu, [http://www.nii.ac.jp National Institute of Informatics]
 * Noman Javed, [http://www.univ-orleans.fr/lifo LIFO], [http://www.univ-orleans.fr Université d'Orléans] / Namal College, Pakistan
 * Yiu Liu, [http://www.nii.ac.jp/graduate/index_e.html The Graduate University for Avanced Studies]
 * Thomas Pinsard, [http://www.univ-orleans.fr/lifo LIFO], [http://www.univ-orleans.fr Université d'Orléans]
 * Simon Robillard, [http://www.univ-orleans.fr/lifo LIFO], [http://www.univ-orleans.fr Université d'Orléans]  
 * Vitor Rodrigues, [http://www.univ-orleans.fr/lifo LIFO], [http://www.univ-orleans.fr Université d'Orléans] 
 * Yoshiaki Takata, [http://www.kochi-tech.ac.jp/gs_e/index.html Kochi University of Technology]
 * Julien Tesson, [http://www.univ-orleans.fr/lifo LIFO], [http://www.univ-orleans.fr Université d'Orléans] and [http://www.kochi-tech.ac.jp/gs_e/index.html Kochi University of Technology]

== Support == 

PaPDAS is a project supported by [http://www.agence-nationale-recherche.fr ANR] (project ANR- 2010-INTB-0205-02) and [http://www.jst.go.jp/EN/ JST]  (project 10102704)
from 2011 to 2014.

== Events ==

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

== Software == 

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

 * The [http://traclifo.univ-orleans.fr/OSL OSL] Library
 * The [http://sketo.ipl-lab.org SkeTo] Library
 * The [http://traclifo.univ-orleans.fr/SyDPaCC SyDPaCC] Library
 * The [http://traclifo.univ-orleans.fr/PaPDAS/attachment/wiki/WikiStart/SyDRec.tar.gz 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.
1. 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.
1. 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: [http://dx.doi.org/10.1016/j.cl.2015.04.001 10.1016/j.cl.2015.04.001].
1. Kiminori Matsuzaki and Reina Miyazaki. “Parallel Tree Accumulations on !MapReduce”. In: Int J Parallel Prog (2015). DOI: [http://dx.doi.org/10.1007/s10766-015-0355-8 10.1007/s10766-015-0355-8].
1. Shigeyuki Sato and Kiminori Matsuzaki. “A Generic Implementation of Tree Skeletons”. In: Int J Parallel Prog (2015). DOI: [http://dx.doi.org/10.1007/s10766-015-0355-6 10.1007/s10766-015-0355-6].
1. K. Emoto and K. Matsuzaki. “An Automatic Fusion Mechanism for Variable-Length List Skeletons in !SkeTo”. In: Int J Parallel Prog (2013). DOI: [http://dx.doi.org/10.1007/s10766-013-0263-8 /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: [http://dx.doi.org/10.1145/2695664.2695870 10.1145/2695664.2695870].
1. 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: [http://dx.doi.org/10.1007/978-3-319-08970-6_17 10.1007/978-3-319-08970-6_17].
1. 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: [http://dx.doi.org/10.1145/2554850.2554996 10.1145/2554850.2554996].
1. 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: [http://dx.doi.org/10.1145/2554850.2554912 10.1145/2554850.2554912].
1. 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: [http://dx.doi.org/10.1109/HPCSim.2014.6903682 10.1109/HPCSim.2014.6903682]. 
1. 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: [http://dx.doi.org/10.1109/SYNASC.2014.51 10.1109/SYNASC.2014.51].
1. 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: [http://dx.doi.org/10.1016/j.procs.2013.05.189 10.1016/j.procs.2013.05.189].
1. 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: [http://dx.doi.org/10.1007/978-3-642-40047-6_46 10.1007/978-3-642-40047-6_46].
1. 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: [http://dx.doi.org/10.1109/HPCSim.2013.6641451 10.1109/HPCSim.2013.6641451].
1. 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: [http://dx.doi.org/10.1109/CANDAR.2013.17 10.1109/CANDAR.2013.17].
1. 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: [http://dx.doi.org/10.1109/PDCAT.2013.12 10.1109/PDCAT.2013.12].
1. 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: [http://dx.doi.org/10.1007/978-3-642-33078-0_16 10.1007/978-3-642-33078-0_16].
1. 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: [http://dx.doi.org/10.1007/978-3-642-23397-5_5 10.1007/978-3-642-23397-5_5].
1. 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: [http://dx.doi.org/10.1007/978-3-642-31500-8_10 10.1007/978-3-642-31500-8_10].
1. 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: [http://dx.doi.org/10.1109/HPCSim.2011.5999832 10.1109/HPCSim.2011.5999832].
1. 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: [http://dx.doi.org/10.1007/978-3-642-23178-0_4 10.1007/978-3-642-23178-0_4].

=== National refereed conferences ===

1. Kento Emoto, Kiminori Matsuzaki,  [https://traclifo.univ-orleans.fr/PaPDAS/raw-attachment/wiki/WikiStart/ipsj-pro2013.pdf Implementing a Fusion-equipped Library with boost::proto], IPSJ SIG-PRO Meeting, Februray 2013
1. Takayuki Kawamura and Kiminori Matsuzaki. [http://ipl.info.kochi-tech.ac.jp/matsuzaki-lab/papers/jssst2012.pdf 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.
1. 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: [http://dx.doi.org/10.1109/HPCSim.2014.6903655 10.1109/HPCSim.2014.6903655]
1. 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.
1. 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
1. Joeffrey Légaux, [http://tel.archives-ouvertes.fr/tel-00990852 Squelettes algorithmiques pour la programmation et l’exécution efficaces de codes parallèles], LIFO, University of Orléans, December 2013
1. Julien Tesson, [ftp://ftp.univ-orleans.fr/theses/julien.tesson_2187.pdf 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
1. Noman Javed, [http://www.theses.fr/2011ORLE2021/document Metaprogrammed Algorithmic Skeletons: Implementations, Performances and Semantics], PhD Thesis, LIFO, University of Orléans, October 2011

== [wiki:Deliverables Deliverables] ==