Theorie et pratique de la concurrence

Master 1 Ingénierie Informatique de Paris 7

La présentation officielle du cours dans la maquette du Master1.

Une présentation résumée et actualisée :

Pré-requis :

système, logique

Objectif :

raisonner sur des programmes concurrents
construire des programmes concurrents corrects
connaître quelques solutions classiques (exclusion mutuelle, sémaphores, régions critiques, moniteurs)

Plan du cours (voir aussi le calendrier) :

Abstraction des programmes concurrents
Propriétés et sémantique des programmes concurrents
Exclusion mutuelle : problème, algorithmes (Dekker, Petterson, Lamport), applications, implémentation.
Sémaphores : notations, sémantique, implémentation, utilisation pour l'exclusion mutuelle, les producteurs/consommateurs, le dîner des philosophes, le lecteurs/écrivains.
Moniteurs : notations, sémantique, implémentation, utilisation pour le barbier endormi, ordonnancement.
Concurrence dans les systèmes distribues : échange de messages asynchrones, rendez-vous, RPC.
Langages dédiés : Java, Occam, Ada, Linda.

Bibliographie et liens :

M. Ben-Ari, Principles of Concurrent and Distributed Programming, Addison-Wesley 2005
(version incomplete en francais : M. Ben-Ari, Processus concurrents --- introduction à la programmation parallèle, Masson 1986)
G. Andrews, Concurrent Programming --- Principles and Practice, The Benjamin-Cummings 1991
G. Andrews, Fondations of Multithread, Parallel, and Distributed Programming, Addison Wesley 2000
M. Raynal, Algorithms for Mutual Exclusion, MIT Press 1986
G. Roussel et E. Duris, Java et Internet, Vuibert 2000.
Spin Model Checker (Xspin installé sur nivose et lenteja), promela mode pour emacs.
CADP Model Checker.

La responsable du cours est Mihaela Sighireanu
Le responsable des TD est Daniele Varacca
L'enseignement a lieu le 2eme semestre. Le premier cours a lieu la semaine du 22 janvier, le premier TD la semaine du 29 janvier. L'horaire du cours et des TD est le suivant :

jour heure salle

cours vendredi 10h30 J5

TD mercredi 14h30 J4 ou 56-66 108
Évaluation : La note finale est calculée comme (2*Ex + CC)/3 ou Ex est la note de l'examen et CC est la note pour le contrôle continu.

	jour	heure	salle
cours	vendredi	10h30	J5
TD	mercredi	14h30	J4 ou 56-66 108

Attention, ce calendrier est sujet à des modification. Consultez-le régulièrement!

Semaine du	Cours	TD	Observations
22 jan.	C-1 (introduction, abstraction des programmes concurrents)	-
29 jan.	C-2 (algorithmes d'exclusion mutuelle)	TD-1 (proprietes et preuve de programmes)	exemples en Spin
5 fev.	C-3 (exclusion mutuelle cont.)	TP-2 (introduction à Spin/Promela)	exemples en Spin
12 fev.	C-4 (sémaphores - sémantique, exemples, implémentation)	TD-3 (verification de l'exclusion mutuelle) (correction corrigée)	-
19 fev.	C-5 (sémaphores cont.)	TD-4 (sémaphores) (correction, philosophes1, philosophes2, broadcast)	-
26 fevr.	C-6 (moniteurs, Java)	TD-5 (vérification avec sémaphores) (correction)	-
5 mars	C-7 (exemple moniteurs)	TD-6 (moniteurs en Java)	-
12 mars	C-8 (communication par messages, rendez-vous, RPC) et exemples	controle continu en TP	-
19 mars	C-9 (Linda, temps-reel et automates temporises)	TD-8 (protocoles et Spin)	-
26 mars	-	TP-9 (Linda)	-
2 avr.	C-10 (introduction a l'algorithmique distribuee, exclusion mutuelle)	TD-10 (automates temporises et Uppaal)	-
23 avr.	C-11 (algorithmique distribuee)	TD-11 (automates temporises, Uppaal)	inversion couirs et TD

Dernière modification : Fri Apr 6 09:07:27 CEST 2007
URL: http://www.liafa.jussieu.fr/~sighirea/cours/concur/index.html