Calcul de processus

En informatique , les calculs de processus (ou algèbres de processus ) sont une famille diversifiée d'approches connexes pour la modélisation formelle des systèmes concurrents . Les calculs de processus fournissent un outil pour la description de haut niveau des interactions, des communications et des synchronisations entre un ensemble d'agents ou de processus indépendants. Ils fournissent également des lois algébriques qui permettent de manipuler et d'analyser les descriptions de processus, et permettent un raisonnement formel sur les équivalences entre les processus (par exemple, en utilisant la bisimulation ). Les principaux exemples de calculs de processus incluent CSP , CCS , ACP et LOTOS . Les ajouts plus récents à la famille incluent le π-calcul , le calcul ambiant , PEPA , le calcul de fusion et le calcul de jointure .

Bien que la variété des calculs de processus existants soit très grande (y compris des variantes qui intègrent le comportement stochastique , les informations temporelles et les spécialisations pour l'étude des interactions moléculaires), il existe plusieurs caractéristiques que tous les calculs de processus ont en commun :

• Représenter les interactions entre des processus indépendants comme une communication ( transmission de messages ), plutôt que comme une modification de variables partagées.
• Décrire les processus et les systèmes à l'aide d'une petite collection de primitives et d'opérateurs permettant de combiner ces primitives.
• Définition de lois algébriques pour les opérateurs de processus, qui permettent de manipuler les expressions de processus à l'aide du raisonnement équationnel .

Pour définir un calcul de processus , on commence par un ensemble de noms (ou canaux ) dont le but est de fournir des moyens de communication. Dans de nombreuses implémentations, les canaux ont une structure interne riche pour améliorer l'efficacité, mais cela est abstrait dans la plupart des modèles théoriques. En plus des noms, il faut un moyen de former de nouveaux processus à partir d'anciens. Les opérateurs de base, toujours présents sous une forme ou une autre, permettent :

• composition parallèle des processus
• spécification des canaux à utiliser pour envoyer et recevoir des données
• séquentialisation des interactions
• masquage des points d'interaction
• récursivité ou réplication de processus

La composition parallèle de deux processus et , généralement écrite , est la primitive clé qui distingue les calculs de processus des modèles séquentiels de calcul. La composition parallèle permet aux calculs dans et de se dérouler simultanément et indépendamment. Mais elle permet également l'interaction, c'est-à-dire la synchronisation et le flux d'informations de vers (ou vice versa) sur un canal partagé par les deux. Il est essentiel qu'un agent ou un processus puisse être connecté à plusieurs canaux à la fois.

Les canaux peuvent être synchrones ou asynchrones. Dans le cas d'un canal synchrone, l'agent qui envoie un message attend qu'un autre agent ait reçu le message. Les canaux asynchrones ne nécessitent pas une telle synchronisation. Dans certains calculs de processus (notamment le calcul π ), les canaux eux-mêmes peuvent être envoyés dans des messages via (d'autres) canaux, ce qui permet de modifier la topologie des interconnexions de processus. Certains calculs de processus permettent également de créer des canaux pendant l'exécution d'un calcul.

L'interaction peut être (mais n'est pas toujours) un flux d'informations dirigé . Autrement dit, l'entrée et la sortie peuvent être distinguées comme des primitives d'interaction duales. Les calculs de processus qui font de telles distinctions définissent généralement un opérateur d'entrée ( eg ) et un opérateur de sortie ( eg ), qui désignent tous deux un point d'interaction (ici ) qui est utilisé pour se synchroniser avec une primitive d'interaction duale.

Si des informations doivent être échangées, elles circuleront du processus de sortie vers le processus d'entrée. La primitive de sortie spécifiera les données à envoyer. Dans , ces données sont . De même, si une entrée s'attend à recevoir des données, une ou plusieurs variables liées serviront de paramètres fictifs à remplacer par des données, lorsqu'elles arriveront. Dans , joue ce rôle. Le choix du type de données pouvant être échangées dans une interaction est l'une des caractéristiques clés qui distinguent les différents calculs de processus.

Parfois, les interactions doivent être ordonnées temporellement. Par exemple, il peut être souhaitable de spécifier des algorithmes tels que : d'abord recevoir des données sur puis envoyer ces données sur . La composition séquentielle peut être utilisée à ces fins. Elle est bien connue dans d'autres modèles de calcul. Dans les calculs de processus, l'opérateur de séquentialisation est généralement intégré à l'entrée ou à la sortie, ou aux deux. Par exemple, le processus attendra une entrée sur . Ce n'est que lorsque cette entrée aura eu lieu que le processus sera activé, les données reçues via substituées à l'identifiant .

La règle de réduction opérationnelle clé, contenant l'essence computationnelle des calculs de processus, peut être donnée uniquement en termes de composition parallèle, de séquentialisation, d'entrée et de sortie. Les détails de cette réduction varient selon les calculs, mais l'essence reste à peu près la même. La règle de réduction est la suivante :

L'interprétation de cette règle de réduction est la suivante :

1. Le processus envoie un message, ici , le long du canal . De même, le processus reçoit ce message sur le canal .
2. Une fois le message envoyé, devient le processus , tandis que devient le processus , qui est avec l'espace réservé substitué par , les données reçues sur .

La classe de processus qui est autorisée à s'étendre comme continuation de l'opération de sortie influence considérablement les propriétés du calcul.

Les processus ne limitent pas le nombre de connexions qui peuvent être faites à un point d'interaction donné. Mais les points d'interaction permettent l'interférence (c'est-à-dire l'interaction). Pour la synthèse de systèmes compacts, minimaux et compositionnels, la capacité à restreindre l'interférence est cruciale. Les opérations de masquage permettent de contrôler les connexions faites entre les points d'interaction lors de la composition d'agents en parallèle. Le masquage peut être noté de diverses manières. Par exemple, dans le π-calcul, le masquage d'un nom dans peut être exprimé comme , tandis que dans CSP, il peut être écrit comme .

Les opérations présentées jusqu'ici ne décrivent que des interactions finies et sont par conséquent insuffisantes pour une calculabilité complète, qui inclut un comportement non terminal. La récursivité et la réplication sont des opérations qui permettent des descriptions finies de comportements infinis. La récursivité est bien connue du monde séquentiel. La réplication peut être comprise comme une abréviation de la composition parallèle d'un nombre dénombrable infini de processus :

Les calculs de processus incluent généralement également un processus nul (diversement désigné par , , , ou tout autre symbole approprié) qui n'a aucun point d'interaction. Il est totalement inactif et son seul but est d'agir comme l'ancre inductive sur laquelle des processus plus intéressants peuvent être générés.

L'algèbre de processus a été étudiée pour le temps discret et le temps continu (temps réel ou temps dense).

Dans la première moitié du XXe siècle, divers formalismes ont été proposés pour saisir le concept informel de fonction calculable , les fonctions μ-récursives , les machines de Turing et le calcul lambda étant probablement les exemples les plus connus aujourd'hui. Le fait surprenant qu'ils soient essentiellement équivalents, dans le sens où ils sont tous encodables les uns dans les autres, soutient la thèse de Church-Turing . Une autre caractéristique commune est plus rarement commentée : ils sont tous plus facilement compris comme des modèles de calcul séquentiel . La consolidation ultérieure de l'informatique a nécessité une formulation plus subtile de la notion de calcul, en particulier des représentations explicites de la concurrence et de la communication. Des modèles de concurrence tels que les calculs de processus, les réseaux de Petri en 1962 et le modèle d'acteur en 1973 ont émergé de cette ligne de recherche.

Les recherches sur les calculs de processus ont commencé sérieusement avec le travail fondateur de Robin Milner sur le calcul des systèmes communicants (CCS) au cours de la période de 1973 à 1980. Les processus séquentiels communicants (CSP) de CAR Hoare sont apparus pour la première fois en 1978 et ont ensuite été développés en un calcul de processus à part entière au début des années 1980. Il y a eu beaucoup de fertilisation croisée des idées entre CCS et CSP au fur et à mesure de leur développement. En 1982, Jan Bergstra et Jan Willem Klop ont commencé à travailler sur ce qui est devenu connu sous le nom d' algèbre des processus communicants (ACP) et ont introduit le terme d'algèbre de processus pour décrire leur travail. CCS, CSP et ACP constituent les trois principales branches de la famille des calculs de processus : la majorité des autres calculs de processus peuvent faire remonter leurs racines à l'un de ces trois calculs.

Différents calculs de processus ont été étudiés et tous ne correspondent pas au paradigme esquissé ici. L'exemple le plus frappant est peut-être le calcul ambiant . Cela est prévisible car les calculs de processus sont un domaine d'étude actif. Actuellement, la recherche sur les calculs de processus se concentre sur les problèmes suivants.

• Développer de nouveaux calculs de processus pour une meilleure modélisation des phénomènes informatiques.
• Trouver des sous-calculs bien conçus d'un calcul de processus donné. Ceci est utile car (1) la plupart des calculs sont assez sauvages dans le sens où ils sont plutôt généraux et on ne peut pas dire grand-chose sur les processus arbitraires ; et (2) les applications informatiques épuisent rarement l'intégralité d'un calcul. Elles utilisent plutôt uniquement des processus dont la forme est très limitée. La contrainte de la forme des processus est principalement étudiée au moyen de systèmes de types .
• Logiques pour les processus qui permettent de raisonner sur des propriétés (essentiellement) arbitraires des processus, en suivant les idées de la logique de Hoare .
• Théorie comportementale : que signifie que deux processus soient identiques ? Comment pouvons-nous décider si deux processus sont différents ou non ? Peut-on trouver des représentants pour les classes d'équivalence de processus ? En général, les processus sont considérés comme identiques si aucun contexte, c'est-à-dire d'autres processus exécutés en parallèle, ne peut détecter une différence. Malheureusement, préciser cette intuition est subtil et conduit généralement à des caractérisations peu maniables de l'égalité (qui dans la plupart des cas doivent également être indécidables, en conséquence du problème d'arrêt ). Les bisimulations sont un outil technique qui aide au raisonnement sur les équivalences de processus.
• Expressivité des calculs. L'expérience de programmation montre que certains problèmes sont plus faciles à résoudre dans certains langages que dans d'autres. Ce phénomène nécessite une caractérisation plus précise de l'expressivité des calculs modélisant le calcul que celle offerte par la thèse de Church-Turing . Une façon de procéder consiste à considérer les codages entre deux formalismes et à voir quelles propriétés les codages peuvent potentiellement préserver. Plus les propriétés peuvent être préservées, plus la cible du codage est dite expressive. Pour les calculs de processus, les résultats célèbres sont que le π-calcul synchrone est plus expressif que sa variante asynchrone, a le même pouvoir expressif que le π-calcul d'ordre supérieur , mais est inférieur au calcul ambiant .
• Utilisation du calcul des processus pour modéliser les systèmes biologiques (π-calcul stochastique, BioAmbients, Beta Binders, BioPEPA, calcul des branes). Certains pensent que la compositionnalité offerte par les outils de la théorie des processus peut aider les biologistes à organiser leurs connaissances de manière plus formelle.

Les idées derrière l’algèbre de processus ont donné naissance à plusieurs outils, notamment :

• PCA
• Atelier de concurrence
• Ensemble d'outils mCRL2

Le monoïde d'histoire est l' objet libre qui est génériquement capable de représenter les histoires de processus de communication individuels. Un calcul de processus est alors un langage formel imposé à un monoïde d'histoire de manière cohérente. C'est-à-dire qu'un monoïde d'histoire ne peut qu'enregistrer une séquence d'événements, avec synchronisation, mais ne spécifie pas les transitions d'état autorisées. Ainsi, un calcul de processus est à un monoïde d'histoire ce qu'un langage formel est à un monoïde libre (un langage formel est un sous-ensemble de l'ensemble de toutes les chaînes de longueur finie possibles d'un alphabet généré par l' étoile de Kleene ).

L'utilisation de canaux pour la communication est l'une des caractéristiques qui distinguent les calculs de processus des autres modèles de concurrence , tels que les réseaux de Petri et le modèle d'acteur (voir Modèle d'acteur et calculs de processus ). L'une des motivations fondamentales de l'inclusion de canaux dans les calculs de processus était de permettre certaines techniques algébriques, facilitant ainsi le raisonnement algébrique sur les processus.