{"id":25,"date":"2019-06-21T00:58:33","date_gmt":"2019-06-20T22:58:33","guid":{"rendered":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/?p=25"},"modified":"2022-03-16T19:37:55","modified_gmt":"2022-03-16T18:37:55","slug":"soutenance-de-these","status":"publish","type":"post","link":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/2019\/06\/21\/soutenance-de-these\/","title":{"rendered":"[Jun. 2019] Phd Defense: Arvid Jakobsson, June 28th 2019"},"content":{"rendered":"\n<pre class=\"wp-block-preformatted\"> La soutenance aura lieu le Vendredi\n28 juin 2019 \u00e0 10h en salle Soutenance de Th\u00e8se (Salle 101), 1er Etage\nau B\u00e2timent S (Facult\u00e9 Des Sciences), Orl\u00e9ans.<\/pre>\n\n\n\n<pre class=\"wp-block-preformatted\">R\u00e9sum\u00e9 de la th\u00e8se :\n\nLa programmation parall\u00e8le consiste \u00e0 utiliser des architectures \u00e0\nmultiples unit\u00e9s de traitement, de mani\u00e8re \u00e0 ce que le temps de calcul\nsoit inversement proportionnel au nombre d'unit\u00e9s mat\u00e9rielles.  Le\nmod\u00e8le de BSP (Bulk Synchronous Parallel) permet de rendre le temps de\ncalcul pr\u00e9visible.  BSPlib est une biblioth\u00e8que pour la programmation\nBSP en langage C.  En BSPlib on entrelace des instructions de contr\u00f4le\nde la structure parall\u00e8le globale, et des instructions locales pour\nchaque unit\u00e9 de traitement.  Cela permet des optimisations fines de la\nsynchronisation, mais permet aussi l'\u00e9criture de programmes dont les\ncalculs locaux divergent et masquent ainsi l'\u00e9volution globale du\ncalcul BSP.\n\nToutefois, les programmes BSPlib r\u00e9alistes sont syntaxiquement\nalign\u00e9s, une propri\u00e9t\u00e9 qui garantit la convergence du flot de contr\u00f4le\nparall\u00e8le.  Dans ce m\u00e9moire nous \u00e9tudions les trois dimensions\nprincipales des programmes BSPlib du point de vue de l'alignement\nsyntaxique: la synchronisation, le temps de calcul et la\ncommunication.  D'abord nous pr\u00e9sentons une analyse statique qui\nidentifie les instructions syntaxiquement align\u00e9es et les utilise pour\nv\u00e9rifier la s\u00fbret\u00e9 de la synchronisation globale.  Cette analyse a \u00e9t\u00e9\nimpl\u00e9ment\u00e9e en Frama-C et certifi\u00e9e en Coq.  Ensuite nous utilisons\nl'alignement syntaxique comme base d'une analyse statique du temps de\ncalcul.  Elle est fond\u00e9e sur une analyse classique du co\u00fbt pour les\nprogrammes s\u00e9quentiels.  Enfin nous d\u00e9finissons une condition\nsuffisante pour la s\u00fbret\u00e9 de l'enregistrement des variables.\nL'enregistrement en BSPlib permet la communication par acc\u00e8s al\u00e9atoire\n\u00e0 la m\u00e9moire distante (DRMA) mais est sujet \u00e0 des erreurs de\nprogrammation.  Notre d\u00e9veloppement technique est la base d'une future\nanalyse statique de ce m\u00e9canisme.\n\nMots cl\u00e9s : Programmation parall\u00e8le, Bulk Synchronous Parallelism,\nSPMD, Analyse statique, Synchronisation, Analyse de co\u00fbt,\nCommunication\n\n===== English version =====\n\nDear all,\n\nIt is my pleasure to invite you to my Ph.D. defense titled\n\"Static Analysis for BSPlib Programs\"\n \nThe defense will take place on Friday, June 28th 2019 at 10:00 AM (UTC+02:00) at\n\n     Universit\u00e9 d\u2019Orl\u00e9ans, Salle Soutenance de Th\u00e8se (Salle 101), 1er\n     Etage au B\u00e2timent S (Facult\u00e9 Des Sciences), Rue de Chartres,\n     45100 Orl\u00e9ans\n\nYou are also welcome to join us to a small cocktail in the afternoon\naround 16:00-16:30, which will take place in 'Salle de r\u00e9union 3',\nfirst floor of LIFO, B\u00e2timent IIIA Rue L\u00e9onard de Vinci B.P. 6759\nF-45067 ORLEANS Cedex 2.\n\n\nThe committee will be composed of:\n KUCHEN, Herbert \u2013 Professor, WWU M\u00fcnster\n BARTHOU, Denis \u2013 Professor, Universit\u00e9 de Bordeaux\n BOUSDIRA-SEMMAR, Wadoud \u2013 Associate Professor, Universit\u00e9 d\u2019Orl\u00e9ans\n DABROWSKI, Fr\u00e9d\u00e9ric \u2013 Associate Professor, Universit\u00e9 d\u2019Orl\u00e9ans\n HAINS, Ga\u00e9tan  \u2013 Research-Engineer, Huawei Technologies\n SUIJLEN, Wijnand \u2013 Research-Engineer, Huawei Technologies\n LOULERGUE, Fr\u00e9d\u00e9ric \u2013 Professor, Northern Arizona University et Universit\u00e9 d\u2019Orl\u00e9ans\n CHAILLOUX, Emmanuel \u2013 Professor, Sorbonne Universit\u00e9\n\n\nAbstract: The goal of scalable parallel programming is to program\ncomputer architectures composed of multiple processing units so that\nincreasing the number of processing units leads to an increase in\nperformance.  Bulk Synchronous Parallel (BSP) is a widely used model\nfor scalable parallel programming with predictable performance. BSPlib\nis a library for BSP programming in C.  In BSPlib, parallel algorithms\nare expressed by intermingling instructions that control the global\nparallel structure, and instructions that express the local\ncomputation of each processing unit. This lets the programmer\nfine-tune synchronization, but also implement programs whose diverging\nparallel control flow obscures the underlying BSP structure.  In\npractice however, the majority of BSPlib program are textually\naligned, a property that ensures parallel control flow convergence.\n\nWe examine three core aspects of BSPlib programs through the lens of\ntextual alignment: synchronization, performance and communication.\nFirst, we present a static analysis that identifies textually aligned\nstatements and use it to verify safe synchronization. This analysis\nhas been implemented in Frama-C and certified in Coq.  Second, we\nexploit textual alignment to develop a static performance analysis for\nBSPlib programs, based on classic cost analysis for sequential\nprograms.  Third, we develop a textual alignment-based sufficient\ncondition for safe registration.  Registration in BSPlib enables\ncommunication by Direct Remote Memory Access but is error prone.  This\ndevelopment forms the basis for a future static analysis of\nregistration.<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>La soutenance aura lieu le Vendredi 28 juin 2019 \u00e0 10h en salle Soutenance de Th\u00e8se (Salle 101), 1er Etage au B\u00e2timent S (Facult\u00e9 Des Sciences), Orl\u00e9ans. R\u00e9sum\u00e9 de la th\u00e8se : La programmation parall\u00e8le consiste \u00e0 utiliser des architectures \u00e0 multiples unit\u00e9s de traitement, de mani\u00e8re \u00e0 ce que le temps de calcul soit &hellip; <a href=\"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/2019\/06\/21\/soutenance-de-these\/\" class=\"more-link\">Continue reading<span class=\"screen-reader-text\"> &#8220;[Jun. 2019] Phd Defense: Arvid Jakobsson, June 28th 2019&#8221;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1],"tags":[],"class_list":["post-25","post","type-post","status-publish","format-standard","hentry","category-non-classe"],"_links":{"self":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts\/25","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/comments?post=25"}],"version-history":[{"count":6,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts\/25\/revisions"}],"predecessor-version":[{"id":287,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts\/25\/revisions\/287"}],"wp:attachment":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/media?parent=25"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/categories?post=25"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/tags?post=25"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}