Journal : Le projet Isaac cherche un thésard (bourse de thèse)
Posté par Ontologia (page perso, ) le 02 avril 2007
Le projet Isaac et Benoit Sonntag recherche assez urgement un thésard pour septembre 2007.
Une bourse est proposée avec cette thèse.
Le texte est très vague (normal pour une thèse), mais j'en préciserai les possibilités concrètes plus bas.
Proposition de thèse (Sept. 2007) pour étudiant ayant un Master 2
d'informatique dans lequel il est particulièrement bien classé.
Directeur(s) de Thèse : Philippe Clauss, PR - Benoît Sonntag, MCF
Unité(s) d'Accueil(s) : Laboratoire LSIIT UMR CNRS 7005, Strasbourg,
équipe ICPS
Établissement de rattachement : Université Louis Pasteur, Strasbourg
Requis :
- Interêt pour le projet Isaac/Lisaac (http://isaacos.loria.fr/),
- Très bonne connaissance des concepts objets,
- Bonne connaissance des systèmes d'exploitation,
- Connaissance en Architecture et Assembleur.
Contacts :
sonntag __at __ icps.u-strasbg.fr ou
clauss__at __icps.u-strasbg.fr
Titre : Programmation des couches basses par une approche de haut niveau
Sujet (résumé) :
L'informatique embarquée impose une réutilisabilité croissante du code
existant avec de fortes contraintes matérielles. Néanmoins dans la
pratique, l'équipe de développement doit maîtriser en profondeur ce code
pour l'adapter aux différentes contraintes matérielles. Le code est
essentiellement écrit en C pour des raisons d'efficacité, de portage,
d'intégration avec le système (gestion du matériel). Ici, nous dénonçons
une réutilisabilité peu fiable, parfois hasardeuse d'un code C non
maîtrisé.
Les langages de haut niveau échappent encore à la programmation système.
Le développement des couches basses nécessite un code sensible à
l'architecture matérielle et rend difficile l'application
d'optimisations génériques et automatiques. La fiabilisation des couches
basses du système devient une priorité grandissante dans une
informatique de plus en plus hétéroclite. Une impasse est alors à
combattre: la réutilisabilité et la fiabilisation d'un code sont
grandement facilitées par l'utilisation des langages de haut niveau,
mais leurs utilisations pour les couches basses du système ne sera
possible qu'après une maîtrise des optimisations spécifiques du matériel
avec des performances au moins similaires à un programme écrit en C.
Cette thèse aura pour objectif de sortir de cette impasse en repoussant
les limites des langages de haut niveau pour l'embarqué tout en
garantissant l'efficacité.
Une des possibilités de recherche pour le futur thésard serait un projet passionnant et ambitieux : Certains savent peut être que Lisaac est un langage à contrat, comme Eiffel.
Il existe à l'heure actuelle peu de compilateur permettant de produire du code certifié, et lorsque cela existe, les performances ne sont que rarement au rendez vous.
Il s'agirait donc ici de produire un prouveur de code, qui prendrai les contrats définis dans le code et vérifierai si ces contrats sont respectés par le code écris.L'utilisation de logiciels de preuve comme coq peut être envisagée (1)
C'est une hypothèse parmi d'autres...
Les avantages du projet, permettant de disposer d'un cadre accueillant sont :
-La maîtrise du compilateur :
Lisaac est un compilateur écris par Benoit Sonntag, (dont la prochaine version totalement réécrite va être bientôt publiée), à ce titre le langage est totalement maîtrisé par l'encadrant de thèse, et les modifications nécessaires lors de cette thèse pourront être faites directement dans le compilateur.
- Lisaac est un langage minimaliste construit autour d'environ 10 primitives, en ce sens, il est moins difficile à prouver.
- Analyse de flot. Lisaac est le premier compilateur objet à intègrer de l'analyse de flot, c'est à dire une analyse de toutes les possibilités d'exécutions du code.
- Performances. Lisaac est un compilateur capable d'optimiser son code de sorte à ce qu'il soit aussi rapide (ou presque) qu'un même algorithme écrit en C.
- Lisaac est écrit en Lisaac.
N'hésitez pas à en parler autour de vous.
(1) why de Jean-Christophe Filliâtre est un logiciel qui explore une problématique similaire, dans une sorte de caml, mais il subsiste quelques trous. http://why.lri.fr/index.fr.html
Une bourse est proposée avec cette thèse.
Le texte est très vague (normal pour une thèse), mais j'en préciserai les possibilités concrètes plus bas.
Proposition de thèse (Sept. 2007) pour étudiant ayant un Master 2
d'informatique dans lequel il est particulièrement bien classé.
Directeur(s) de Thèse : Philippe Clauss, PR - Benoît Sonntag, MCF
Unité(s) d'Accueil(s) : Laboratoire LSIIT UMR CNRS 7005, Strasbourg,
équipe ICPS
Établissement de rattachement : Université Louis Pasteur, Strasbourg
Requis :
- Interêt pour le projet Isaac/Lisaac (http://isaacos.loria.fr/),
- Très bonne connaissance des concepts objets,
- Bonne connaissance des systèmes d'exploitation,
- Connaissance en Architecture et Assembleur.
Contacts :
sonntag __at __ icps.u-strasbg.fr ou
clauss__at __icps.u-strasbg.fr
Titre : Programmation des couches basses par une approche de haut niveau
Sujet (résumé) :
L'informatique embarquée impose une réutilisabilité croissante du code
existant avec de fortes contraintes matérielles. Néanmoins dans la
pratique, l'équipe de développement doit maîtriser en profondeur ce code
pour l'adapter aux différentes contraintes matérielles. Le code est
essentiellement écrit en C pour des raisons d'efficacité, de portage,
d'intégration avec le système (gestion du matériel). Ici, nous dénonçons
une réutilisabilité peu fiable, parfois hasardeuse d'un code C non
maîtrisé.
Les langages de haut niveau échappent encore à la programmation système.
Le développement des couches basses nécessite un code sensible à
l'architecture matérielle et rend difficile l'application
d'optimisations génériques et automatiques. La fiabilisation des couches
basses du système devient une priorité grandissante dans une
informatique de plus en plus hétéroclite. Une impasse est alors à
combattre: la réutilisabilité et la fiabilisation d'un code sont
grandement facilitées par l'utilisation des langages de haut niveau,
mais leurs utilisations pour les couches basses du système ne sera
possible qu'après une maîtrise des optimisations spécifiques du matériel
avec des performances au moins similaires à un programme écrit en C.
Cette thèse aura pour objectif de sortir de cette impasse en repoussant
les limites des langages de haut niveau pour l'embarqué tout en
garantissant l'efficacité.
Une des possibilités de recherche pour le futur thésard serait un projet passionnant et ambitieux : Certains savent peut être que Lisaac est un langage à contrat, comme Eiffel.
Il existe à l'heure actuelle peu de compilateur permettant de produire du code certifié, et lorsque cela existe, les performances ne sont que rarement au rendez vous.
Il s'agirait donc ici de produire un prouveur de code, qui prendrai les contrats définis dans le code et vérifierai si ces contrats sont respectés par le code écris.L'utilisation de logiciels de preuve comme coq peut être envisagée (1)
C'est une hypothèse parmi d'autres...
Les avantages du projet, permettant de disposer d'un cadre accueillant sont :
-La maîtrise du compilateur :
Lisaac est un compilateur écris par Benoit Sonntag, (dont la prochaine version totalement réécrite va être bientôt publiée), à ce titre le langage est totalement maîtrisé par l'encadrant de thèse, et les modifications nécessaires lors de cette thèse pourront être faites directement dans le compilateur.
- Lisaac est un langage minimaliste construit autour d'environ 10 primitives, en ce sens, il est moins difficile à prouver.
- Analyse de flot. Lisaac est le premier compilateur objet à intègrer de l'analyse de flot, c'est à dire une analyse de toutes les possibilités d'exécutions du code.
- Performances. Lisaac est un compilateur capable d'optimiser son code de sorte à ce qu'il soit aussi rapide (ou presque) qu'un même algorithme écrit en C.
- Lisaac est écrit en Lisaac.
N'hésitez pas à en parler autour de vous.
(1) why de Jean-Christophe Filliâtre est un logiciel qui explore une problématique similaire, dans une sorte de caml, mais il subsiste quelques trous. http://why.lri.fr/index.fr.html
> Lire le journal (16 commentaires, moyenne: 3,4).
Vous avez demandé le commentaire #817834.
Run by 
Cette page a été générée par Templeet en 0.0587s (dont 0.006 de SQL).
Cette page est peut-être conforme xhtml 1.0.
Information sur le site.
Financement?
Qu'en est-il du financement ?
J'imagine que vous ne proposez pas une thèse bénévole, et comme l'argent ne pousse pas sur les arbres...
[^]Re: Financement?
Faux : Des arbres, on peut tirer des chèques en bois.
Pan ! Pan !
Ne pas utiliser : traplinuxfrnico@univ-nantes.Fr
[^]Re: Financement?
En même temps, en lisant le titre et la deuxième phrase du billet, tu aurais une idée de la réponse ...
[^]Re: Financement?
A la vue de la première ligne, il y a une bourse avec.
Par contre, il serait bien de préciser un peu la bourse en question...
"Nobody expects the spanish inquisition"
[^]Re: Financement?
C'est à déterminer :
- Soit c'est une MENRT (bourse du ministère) -> 1400 ¤ net /mois
- Soit une bourse régionale/CNRS , compter jusqu'à 1700 ¤ net /mois
Je ne peux pas en dire plus pour le moment.
[^]Re: Financement?
Euh, tu es sur de toi là ? Car il me semble (je peux me tromper) que le montant des bourses CNRS (qui incluent CNRS, CNRS/region et CNRS/region/entreprise) est le meme pour tout le monde. Et pour moi, le montant de la bourse n'est meme pas 1200¤ net par mois...
Et ma copine, qui a une bourse MENRT ne touche pas du tout 1400 ¤ net/mois.
A moins que tu inclues le monitorat avec les bourses ? Mais meme dans ce cas, je ne crois pas qu'on atteigne les sommes données.
Les montants sont donc a vérifier (ou alors on se fait sacrément avoir, et j'aimerais savoir ou aller réclamer mon manque à gagner !)
[^]Re: Financement?
Je me suis malheureusement contenté d'écrire ce que Benoit Sonntag m'a dit quand je lui ai posé la question, je ne suis donc pas sûr de moi.
Je pense que le monitorat est compris dans ce salaire.
Tu peux aussi lui poser la question :-)
[^]Re: Financement?
Je me réponds a moi meme après etre allé sur le site du CNRS.
Les reponses sont ici :
http://www.sg.cnrs.fr/drh/emploi-nonperm/bdi.htm#cnrs
Donc 1700¤ brut, c'est CNRS/entreprise
Sinon, c'est 1400¤ brut (CNRS, CNRS/region, CNRS/Region/Entreprise).
A moins que ca ne soit pas une bourse BDI, mais un autre type de bourse ?
Je n'ai pas vérifié pour les bourses ministérielles, mais je pense qu'il faut remplacer "net" par "brut".
[^]Re: Financement?
Pour la bourse MENRT, en effet, ça correspond au brut (1417,38) sans monitorat. Net c'est plutôt 1169,21¤. Enfin, cela a normalement augmenté depuis février dernier de 8% (mais l'augmentation n'a pas encore été perçue). Faîtes le calcul :-)