proposition de stage de M2 :
Typage statique de Cython en vue de sa parallélisation
Encadrant : Emmanuel Chailloux (APR-LIP6-UPMC) - Emmanuel.Chailloux@lip6.fr
Lieu : LIP6 - Campus Jussieu - 4, place Jussieu 75005 Paris
Durée et dates : 5 à 6 mois à partir de février 2018
Rémunération : standard

Description

Une des principales difficultés de paralléliser le code Python provient du gil (global interactive lock ou verrou global interactif) ne permettant qu’à un seul fil d’exécution (thread) de s’exécuter à un moment donné. Cela facilite l’implantation du gestionnaire automatique de mémoire. L’extension Cython [CYTHON] ajoute un sous-ensemble de C/C++ à Python ce qui permet une compilation plus efficace et une facilité de s’interfacer avec des bibliothèques C existantes. Mais même dans ce cas là il est nécessaire de supporter le “gil” de Python car il peut avoir des structures hétérogènes faisant cohabiter les deux mondes. Et même pour des structures homogènes, issues uniquement du monde Cython, les difficultés apparaissant avec l’aliasing et la modification physique de memoire empêchent de paralléliser le code Cython.

Contexte

  1. généralités sur le verrou global (gil)

    On rencontre plusieurs implantations de langages de haut niveau qui possèdent au niveau de leur bibliothèque d’exécution (runtime library) un verrou global. Ce qui garantit que seul le fil d’exécution (thread) possédant ce verrou peut s’exécuter. Ce verrou global rend alors l’exécution séquentielle, même s’il existe dans le langage une bibliothèque de thread, y compris de thread POSIX. L’intérêt de ce verrou global est de simplifier le runtime, en particulier au niveau de la gestion automatique de mémoire, tout en garantissant le bon déroulement du programme, en évitant des "data races" où plusieurs instructions de threads différents accèdent à la même location mémoire pouvant alors impliquer un comportement incohérent du programme via des "race conditions" [WIKIPEDIA-RACE-CONDITION] (situations de compétition [WIKIPEDIA-SITUATION-DE-COMPETITION]). Un tel verrou global permet d’avoir l’expressivité de la concurrence dans son langage, mais ne peut prétendre au parallélisme physique et ne peut pas profiter de la puissance des différents coeurs d’un processeur. C’est par exemple le cas des langages Python ou OCaml.
    On peut noter que ces "race conditions" ne peuvent survenir que de la combinaison de mécanisme d’aliasing [WIKIPEDIA-ALIASING] et de mutation à la même location mémoire. Un système dont les ressources sont immuables (dont l’état ne peut pas changer) est immunisé contre ce problème.

  2. Différents systèmes de types apportent des éléments de réponse pour traiter cette limitation :

    On retrouve cette technique de manière plus concrète dans les permission à la Mezzo (formel) [TOPLAS2016] [MEZZO] ou dans les propriétés/prêts à la Rust (pratique, sans GC) [SIGADA2014] [RUST].

  3. Rust

    L’idée essentielle du système de types de Rust est de garantir que l’aliasing et la modification (mutation) ne peuvent pas se produire en même temps sur un emplacement donné, ce qui pourra être vérifié en laissant les types représenter la propriété (qui a la possession).

    Pour cela deux cas de figure sont envisagés :

    Au final on obtient des types de la forme "&’a mut T" (référence mutable) ou "&’a T"(référence partagée). Le paramètre de type "’a" indique alors la durée de vie, pour déterminer la durée des prêts, nécessaire en Rust pour la libération mémoire.

Objectif

Dans le cadre du langage Python, il n’est pas possible d’avoir un mécanisme à la thread Posix, profitant des performances des architectures multi-coeurs, sans devoir modifier le runtime de Python. Mais cela peut avoir des conséquences sur les programmes purement séquentiels, comme une baisse de performances, ce qui semble difficilement acceptable par la communauté. Par contre pour une extension du langage, à la Cython, on peut apporter des garanties sur la partie exécutée hors du moteur classique Python.

Dans ce cas là on peut procéder en plusieurs étapes :

Bibliographie

[WIKIPEDIA-RACE-CONDITION] : https://en.wikipedia.org/wiki/Race_condition

[WIKIPEDIA-SITUATION-DE-COMPETITION] : https://fr.wikipedia.org/wiki/Situation_de_comp

[WIKIPEDIA-ALIASING] : https://en.wikipedia.org/wiki/Aliasing_(computing)

[LNCS1710] Flemming Nielson, Hanne Riis Nielson. Type and Effect Systems. 1999. In Correct System Design: Recent Insight and Advances. LNCS. Springer-Verlag. vol 1710: pp 114–136

[WIKIPEDIA-EFFECT] Systèmes de types pour les effets : https://en.wikipedia.org/wiki/Effect_system

[PCM1990] Philip Wadler. Linear types can change the world. 1990. In Programming Concepts and Methods , M Broy and C B Jones (Eds.). North-Holland

[WIKIPEDIA-LINEAR-TYPE] Wikipedia sur types linéaires : https://en.wikipedia.org/wiki/Substructural_type_system

[SIGADA2014] Nicholas D. Matsakis and Felix S. Klock II. 2014. The Rust language. In SIGAda Ada Letters, Vol. 34. https://doi.org/10.1145/ 2663171.2663188

[RUST] Site du langage Rust : https://www.rust-lang.org/en-US/

[MRPYTHON] https://github.com/nohtyprm/MrPython

[PYRE] https://github.com/facebook/pyre-check

[MYPY] http://mypy-lang.org/

[TOPLAS2016] Thibaut Balabonski, Fraançois Pottier, and Jonathan Protzenko. 2016. The design and formalization of Mezzo, a permission- based programming language. TOPLAS 38, 4 (2016). https://doi.org/10.1145/2837022

[MEZZO] Les permissions avec Mezzo : http://protz.github.io/mezzo/

[POPL2017-TUTORIAL] Jeremy G. Siek. The State of the Art in Gradual Typing. Tutorial in Symposium on Principles of Programming Languages (POPL). ACM, January 2017. https://www.dropbox.com/s/tphnkvb56tal7ab/popl-2017-tutorial-slides.pdf?dl=0


Ce document a été traduit de LATEX par HEVEA