Resource Traces: A Domain for Processes Sharing
Exclusive Resources

P. Gastin, Dan Teodosiu

IBP-Litp 1996/29: Rapport de Recherche Litp / Litp research reports
25 pages - Septembre/September 1996 - French document.

PostScript : Ko /Kb

Titre / Title: Resource Traces: A Domain for Processes Sharing
Exclusive Resources

Résumé : La théorie des mots finis et infinis avec terminaison explicite est
usuellement utilisée pour donner des sémantiques dénotationnelles à des algèbres de processus séquentiels. Dans cet article, on
généralise cette théorie au cas de processus concurrents qui se
synchronisent sur un ensemble fixe de ressources partagées.
On part d'un alphabet d'actions, d'un ensemble de ressources et d'une application qui fait correspondre à chaque action le sous-ensemble non-vide des ressources qu'elle utilise. Deux actions sont déclarées indépendantes si elles ne partageny aucune ressource.
La description d'un processus (trace à ressource) comprend deux parties: une trace de Mazurkiewicz pour décrire ce qui a déjà été observé et l'ensemble des resources réservées par le processus pour terminer son exécution. On peut alors définir une concaténation
``concurrente'' des processus de telle sorte que des actions du deuxième processus puissent être exécutée avant la fin du premier processus si ces actions n'utilisent pas les ressources reservées par le premier processus pour terminer son exécution. On définit ensuite un ordre d'approximation entre les processus et on obtient un domaine de Scott cohéremment complet et premier algébrique. De plus, on définit une distance ultramétrique naturelle. La topologie induite par cette distance coïncide avec la topologie de Lawson associée à l'ordre d'approximation. Le domaine des traces à ressources est ainsi compact et la concaténation est en fait uniformément continue. L'un des principaux avantages de ce modèle est que la concaténation est continue par rapport à l'ordre d'approximation. Ceci en fait un bon candidat pour donner des sémantiques dénotationnelles, particulièrement lorsqu'on considère une spécification modulaire d'un ensemble de processus partageant des ressources exclusives. A titre d'exemple, les machines de type PRAM basées sur des registres partagés aussi bien que les algèbres de processus comme CSP où les synchronisations se font au travers de canaux devraient bénéficier de cette nouvelle approche.

The theory of finite and infinite words with explicit termination is commonly used to give denotational semantics for algebras of sequential processes. In this paper we generalize this theory to the case of partially terminated concurrent processes synchronizing on a fixed set of shared exclusive resources.

We start with an alphabet of actions, a set of resources,
and a resource map assigning to each action the non-empty subset of resources it uses. Actions that do not share common resources are declared independent. The specification we use for partially terminated processes (resource traces) is similar to failure semantics. It consists of two components: an already observed part represented as an action-labeled event structure (Mazurkiewicz trace), and a guard set containing the resources granted to the process for its further development. A process concatenation is then defined such that independent actions can be dispatched concurrently. Specification refinement leads to the definition of a natural approximation ordering between processes which generates a coherently complete prime algebraic Scott domain, where process
concatenation is continuous in both arguments. Furthermore, we define a natural ultrametric on processes based on prefix information. The induced topology is shown to be equivalent to the compact Lawson topology generated by the approximation ordering. Moreover, process concatenation is shown to be uniformly continuous with respect to the defined ultrametric. We develop a mathematical theory which perfectly extends the central properties of the domain of finite and infinte words with explicit termination and the domain of finite and infinite Mazurkiewicz traces. Its natural semantics is well suited to the design of modular denotational semantics for algebras of processes sharing exclusive resources such as programs using some set of shared registers (PRAM) or concurrent sequential processes
synchronizing over exclusive communication channels (CSP).

Abstract : The theory of finite and infinite words with explicit termination is commonly used to give denotational semantics for algebras of sequential processes. In this paper we generalize this theory to the case of partially terminated concurrent processes synchronizing on a fixed set of shared exclusive resources.

We start with an alphabet of actions, a set of resources,
and a resource map assigning to each action the non-empty subset of resources it uses. Actions that do not share common resources
are declared independent. The specification we use for partially terminated processes (resource traces) is similar to failure semantics. It consists of two components: an already observed part represented as an action-labeled event structure (Mazurkiewicz trace), and a guard set containing the resources granted to the process for its further development. A process concatenation is then defined such that independent actions can be dispatched concurrently. Specification refinement leads to the definition of a natural approximation ordering between processes which generates a coherently complete prime algebraic Scott domain, where process
concatenation is continuous in both arguments. Furthermore, we define a natural ultrametric on processes based on prefix information. The induced topology is shown to be equivalent to the compact Lawson topology generated by the approximation ordering. Moreover, process concatenation is shown to be uniformly continuous with respect to the defined ultrametric.

We develop a mathematical theory which perfectly extends the central properties of the domain of finite and infinte words with explicit termination and the domain of finite and infinite Mazurkiewicz traces. Its natural semantics is well suited to the design of modular denotational semantics for algebras of processes sharing exclusive resources such as programs using some set of shared registers (PRAM) or concurrent sequential processes
synchronizing over exclusive communication channels (CSP).

Publications internes Litp 1996 / Litp research reports 1996