problème des philosophes



On suppose que quatre philosophes sont assis à des emplacements fixes autour d'une table, à tout instant un philosophe est soit en train de manger, soit il a decidé de manger mais il manque de(s) fourchette(s), il attend que les deux fourchettes dont il a besoin soient libres, soit il pense et n'utilise aucune fourchette.

soient P1,P2,P3,P4 les philosophes et F1,F2,F3,F4 les fourchettes

on a quatre fourchettes F1,F2,F3,F4 : ⊢F1,F2,F3,F4

on introduit les ressources (les fourchettes).



le philosophe P1 utilise les fourchettes F1 et F2: F1,F2⊢P1 le philosophe P1 a besoin d'utiliser les ressources F1 et F2 pour pouvoir manger.



le philosophe P3 utilise les fourchettes F3 et F4: F3,F4⊢P3 le philosophe P3 consomme les ressources F3 et F4 pour se nourrir.



le philosophe P2 utilise les fourchettes F2 et F3:F2,F3⊢P2 le philosophe P2 consomme les ressources F2 et F3



le philosophe P4 utilise les fourchettes F1 et F4: F1,F4⊢P4 le philosophe P4 consomme les ressources F1 et F4



On se rend compte qu'au maximum deux philosophes n'utilisant pas les mêmes fourchettes peuvent se nourrir simultanément, voici une table qui permet de se rendre compte des blocages.

philosophes/ fourchettes	F1	F2	F3	F4
P1	X	X
P2		X	X
P3			X	X
P4	X			X

on a donc les incompatibilités suivantes:

	P1	P2	P3	P4
P1	X	Blocage		Blocage
P2	Blocage	X	Blocage
P3		Blocage	X	Blocage
P4	Blocage		Blocage	X

P1 et P3 peuvent donc manger en même temps, ils n'utilisent pas les mêmes fourchettes



ainsi que P2 et P4, toute autre combinaison de philosophes entrainerait un blocage.



P2 et P4 peuvent manger simultanément donc on a les deux processus (philosophes) qui consomment les ressources F1,F2,F3,F4 (ils utilisent donc toutes les fourchettes) on le note: F1,F2,F3,F4⊢P2⊗P4

il en est de même pour P1 et P3 : F1,F2,F3,F4⊢P1⊗P3



Les philosophes P1 et P3 peuvent manger ensembles, ou P2 et P4 peuvent manger ensembles mais pas les quatre ensembles (il s'agit donc d'un 'ou' exclusif que l'on note &).

Ce qui donne: F1,F2,F3,F4⊢(P1⊗P3)&(P2⊗P4).

On a donc finalement le réseau de preuves suivant:

⊢F1,F2,F3,F4
F1,F2⊢P1 F3,F4⊢P3			F2,F3⊢P2 F1,F4⊢P4
F1,F2,F3,F4⊢P1⊗P3			F1,F2,F3,F4⊢P2⊗P4
	F1,F2,F3,F4⊢(P1 ⊗ P3)&(P2 ⊗P4)

-- BenychouSabrina - 28 Apr 2005
to top