Abstract FR:

Le but de l'etude qualitative est d'exhiber un algorithme de gestion de memoire parallele ou les exclusions sont de longueur bornee statiquement. La notion de logique d'utilite est introduite pour prendre en compte la specificite des langages relationnels. La correction partielle de l'algorithme est prouvee a l'aide de la methode axiomatique de owicki. L'objectif de l'etude quantitative est de mettre en evidence des conditions dans lesquelles l'interpreteur de langages relationnels n'est pas suspendu pour cause de saturation de la memoire. Un premier modele simple, deterministe decrit les conditions de fonctionnement temps reel sous l'hypothese que les parametres de la dynamique des processus sont des constantes. Un second modele prend en compte les aleas de progression des processus et se montre plus exigeant que le premier modele pour les conditions temps-reel et equivalent dans les autres cas. Ce modele est une chaine de markov qui a necessite la mise au point d'un resolveur original a cause du grand nombre d'etats (de l'ordre de 10. 000. 000). Ce resolveur utilise une technique d'agregation/desagregation a un premier niveau et une technique de recurrence a un second niveau