Développement systématique et sûreté d’exécution en programmation parallèle structurée

Louis Gesbert

Description

Sous la direction de Frédéric Loulergue
Thèse soutenue le 05 mars 2009: Paris Est
Exprimer le parallélisme dans la programmation de manière simple et performante est un défi auquel l'informatique fait face, en raison de l'évolution actuelle des architectures matérielles. BSML est un langage permettant une programmation parallèle de haut niveau, structurée, qui participe à cette recherche. En s'appuyant sur le coeur du langage existant, cette thèse propose d'une part des extensions qui en font un langage plus général et plus simple (traits impératifs tels que références et exceptions, syntaxe spécifique...) tout en conservant et étendant sa sûreté (sémantiques formelles, système de types...) et d'autre part une méthodologie de développement d'applications parallèles certifiées
-Parallélisme
-Programmation de haut niveau
-Programmation fonctionnelle
-Sémantique
-Sûreté des langages
-Preuves de programmes
-Typage
-BSP
Finding a good paradigm to represent parallel programming in a simple and efficient way is a challenge currently faced by computer science research, mainly due to the evolution of machine architectures towards multi-core processors. BSML is a high level, structured parallel programming language that takes part in the research in an original way. By building upon existing work, this thesis extends the language and makes it more general, simple and usable with added imperative features such as references and exceptions, a specific syntax, etc. The existing formal and safety characteristics of the language (semantics, type system...) are preserved and extended. A major application is given in the form of a methodology for the development of fully proved parallel programs
-Parallelism
-High level programming
-Functional programmins
-Semantics
-Safety of programs
-Program proofs
-Type systems
-BSP
Source: http://www.theses.fr/2009PEST0004/document

Sujets

• Parallélisme
• Programmation fonctionnelle
• Sémantique
• Type (informatique)

Informations

• Publié par: Thesee
• Nombre de lectures: 20
• Langue: Français
• Poids de l'ouvrage: 1 Mo

Extrait

Universit´e Paris XII – Val de Marne PRES Paris-est
´Ecole doctorale SIMME UFR de sciences
D´eveloppement syst´ematique et suˆret´e
d’ex´ecution en programmation
parall`ele structur´ee
`THESE
pr´esent´ee et soutenue publiquement le jeudi 5 mars 2009
Pour l’obtention du titre de
Docteur de l’universit´e Paris Est
par
Louis Gesbert
Composition du jury
Rapporteurs : Emmanuel Chailloux
Jocelyn S´erot
Examinateurs : Zhenjiang Hu
Olivier Michel
Fr´ed´eric Gava
Fr´ed´eric Loulergue (directeur)
Laboratoire d’Algorithmique, Complexit´e et Logiquequi
de
t
Remerciemen
mes
ts
ma
Merci
vie
à
t
Emman
Je
uel
ermis
Chailloux
momen
et
our
à
à
Jo
our

thèse
Sérot
m'a
d'a
l'IPL
v
v
oir
leur

oir
d'être
l'oublierai
mes
moins
rapp
main
orteurs

;
a
merci
de
égalemen
momen
t
à
à
a
Zhenjiang
en
Hu
b
et
les
Olivier
o


hel
m'a
de
pa
faire
aide.
partie
p
de
tra
mon
diciles,
jury
temps
.
p
Je
et
tiens
v
à
u
remercier
endan
mon
mois.

p
de
oir
thèse
relire
F
ter.

b
Loulergue
qui
qui

a
de

érience
en
je
moi
dèles
et,
Damien
malgré
orté
la
momen

à
a
bres
su
T
être
v
là
eu
quand
de
il
p
fallait.
oir
Un

grand
p
merci
et
à
Nathalie
F
profonde

m'a
Ga
u
v
ers
a
particulièremen
qui
je
l'a
i

étaien
p
un
our
eu
nos

longs
p
débats
m'a

oir
hniques
ten
qui
en
nalemen
p
t
t
se
derniers
son
Merci
t
Nils
rév
our
élés
v
pro


me
et
et
p

our
P
le
les

ons
de
ts,
p
on

aussi

tribué
sur
faire
la

n.
l'exp
P
qu'elle
our
été,
le
remercie
temps
amis
agréable
;
qu'on
particulier
a
qui
passé
supp
ensem
un
ble
on
au
t.
LA
tiens
CL,
remercier
je
mem
remercie
de
Marie,
à
Danièle,
oky
Jo
a
ëlle,
ec
Alexis,
j'ai
Catalin
la
et
hance
tous
tra
les
ailler
autres.
our
Sans
v
oublier,
p
bien
de
sûr,
leur
l'irremplaçable
ys,
Flore.
our
Je

remercie
leur
du
Enn,
fond
mérite
du
plus


ma
our
famille
v
p
souten
our
à
a
v
v
des
oir
ts
toujours
t
été
et
derrière
ne
moi
pas.
quand
lesii.
.
.
able
2.7.2
des
.
matières
.
1
.
In
.
tro
.

apply
1
.
1.1
.
Généralités
tillonnage
.
.
.
.
.
.
.
Primitiv
.
.
.
.
.
.
.
.
.
pro
.
.
.
.
.
es
.
21
.
.
.
.
.
.
.
.
.
T
.
un
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2.5
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
rapp
.
2.6
.
.
.
.
1
.
1.1.1
P
P
.
arallélisme
.
et
.

.
scien
2.7.3
tique
.
.
.
.
.
.
Niv
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
hrones
.
.
2
.
1.1.2
.
Év
.
olution
.
du
.
matériel
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
18
.
an
.
.
.
parallèle
.
.
.
.
.
bsml
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
3
.
1.1.3
.
P
.
arallélisme
.
mo
.
derne
.
.
13
.
d'exécution
.
bsml
.
.
.
.
.
.
.
.
.
14
.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2.4.1
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
16
.
.
.
.
3
.
1.2
.

.
et
.
parallélisme
.
.
.
.
.
.
.
.
es
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
17
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2.5.2
.
.
.
.
.
.
.
.
.
.
.
.
4
.
1.3
.

.
et
.
parallélisme
Remarque
.
aux
.
des
.
.
.
.
.
:
.
éc
.
(PSRS)
.
.
.
.
.
.
.
Syn
.
e
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
25
.
?
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
5
.
1.4
.
Réalisations
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
27
.
.
.
.
.
.
.
.
.
.
.
2.3
.
eaux
.
dans
.
programme
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2.4
.
es
.
hrones
.
.
7
.
2
.

.
e
.
de
.
bsml
.
9
.
2.1
.
Une
.
appro
.

.
he
.
du
.
parallélisme
.
.
.
.
16
.
mkpar
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2.4.2
.
.
.
.
.
.
.
.
.
.
.
.
9
.
2.1.1
.
Le
.
mo
.
dèle
.
BSP
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
16
.
Primitiv
.
sync
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2.5.1
.
j
.
.
.
.
.
.
.
.
9
.
2.1.2
.
L'appro
.

.
he
.
bsml
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
17
.
put
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2.5.3
10
par
2.1.3
ort
Prédiction
dénitions
de
térieures
p
primitiv

.
.
.
.
.
.
21
.
Exemple
.
tri
.
par
.
han
.
régulier
.
.
.
.
.
.
.
.
.