Pi-calcul

Le Pi-calcul (ou π-calcul) est un langage de programmation théorique inventé par Robin Milner. Ce langage occupe dans le domaine de l'informatique parallèle et distribuée un rôle similaire à celui du λ-calcul dans l'informatique classique.

La problématique

En tant que langage de programmation théorique (ou formalisme), le π-calcul ne vise pas à permettre de construire des programmes exécutables. L'objectif du π-calcul est de permettre d'étudier les concepts importants en programmation parallèle et distribuée, afin:

d'isoler les mécanismes essentiels
de reformuler les mécanismes redondants sous la forme de macros construites à partir des mécanismes essentiels
de définir des notions de haut niveau telles que
- comportement d'un programme (utile pour fournir des garanties sur l'absence de certaines erreurs)
- égalité de deux programmes (utile notamment pour écrire des compilateurs ou des ramasse-miettes)
- politiques de sécurité
- confidentialité d'une information
- ...

Afin de construire un programme exécutable, il est nécessaire de passer par un langage de programmation concret dérivé (ou inspiré) du π-calcul, tel que JoCaml, Acute ou Nomadic Pict.

Définition informelle

Les entités du π-calcul

En pratique, un programme écrit en π-calcul (ou terme) décrit systématiquement un processus, noté typiquement P, 'Q, R... Les processus représentent aussi bien les processus légers (threads) ou processus lourds et aucune hypothèse n'est faite sur l'emplacement du processus: à ce niveau d'abstraction, celui-ci peut être exécuté sur n'importe quel composant ou n'importe quel ordinateur. Un langage de programmation concret ajoutera un compilateur ou un environnement d'exécution intelligent ou nécessitera plus de précisions pour savoir où placer le processus.

Plutôt que des données explicites, les programmes écrits en π-calcul manipulent des noms, notés typiquement a, b, c... x, y, z. Un nom est une construction abstraite qui peut, à ce niveau, représenter n'importe quel type d'information. Typiquement, les noms sont utilisés comme des canaux: tout processus qui connaît le nom a peut écrire sur a ou lire depuis a. Les canaux diffèrent des variables et des constantes au sens où chaque lecture doit correspondre à une seule et unique écriture -- le processus qui écrit sur a envoie donc une information au processus qui lit sur a. Les informations, de nouveau, sont des noms. Un langage de programmation concret ajoutera des types de base (entiers, booléens) et des structures de données traditionnelles.

En particulier, il est à noter qu'un système est décrit uniquement sous la forme d'un terme: en π-calcul, il n'y a pas de différence, syntaxique ou sémantique, entre le code et les données.

Les constructions du π-calcul

Note: il existe plusieurs variantes canoniques du π-calcul. Cet article présente le π-calcul polyadique asynchrone à réplication gardée avec comparaison de noms.

Processus terminé

Le processus le plus simple est le processus nil, noté 0. Ce terme ne fait rien -- il s'agit d'un processus qui a terminé de s'exécuter.

Émission

Un terme plus compliqué est l'émission (asynchrone) d'un message: le processus $a\langle b\rangle$ émet sur le canal a l'information b. L'émission est asynchrone au sens où le processus n'attend pas de réponse et continue son exécution même si aucun processus n'a reçu l'information. Comme il est très facile d'écrire une macro pour la communication synchrone à partir de cette primitive de communication asynchrone, il ne s'agit pas d'une limitation.

Réception

La réception d'un message se note $a (x). P$ et se comporte de la manière suivante: si un processus de la forme $a\langle b\rangle$ est présent, il y a communication entre les processus. Le processus récepteur continue alors sous la forme $P\{x\leftarrow b\}$ , c'est-à-dire comme le processus P dans lequel le nom x représente le message b. Ceci est similaire à un appel de fonction dans un langage traditionnel. Les différences principales sont les suivantes:

s'il n'existe aucun processus récepteur sur le canal a, émettre sur le canal a ne constitue pas une erreur -- le message est simplement mis en attente jusqu'à ce qu'un récepteur soit prêt à écouter sur le canal a
il peut y avoir plusieurs processus récepteurs prêts à écouter sur le canal a à un moment donné -- en cas de communication, l'un d'entre eux est choisi arbitrairement (dans le π-calcul, ceci peut servir à modéliser plusieurs agents prêts à fournir le même service)
la fonction est « effacée » après avoir été appelée et ne renvoie jamais de valeur -- à ce sens, la communication ressemble plus à un goto avec paramètres ou à un join avec paramètres qu'à un appel de fonction proprement dit

Réplication

Une réception peut être répliquée. On notera alors $! a (x). P$ . Contrairement à une réception non répliquée, ce processus ne disparaît pas après avoir communiqué avec un processus émetteur $a\langle b_1\rangle$ . Ce terme peut encore communiquer autant de fois que nécessaires avec $a\langle b_2\rangle$ , $a\langle b_3\rangle$ ... Chaque communication déclenche alors un processus de la forme $P\{x\leftarrow b_i\}$ . Une fois créé, un récepteur répliqué ne peut plus être effacé -- on peut donc le considérer comme un appel asynchrone de fonction.

Composition parallèle

Si P et Q sont deux processus, $P | Q$ est la composition parallèle de P et Q, qui représente le fait que P et Q sont exécutés simultanément.

Création d'un nom

Un processus peut créer un nouveau nom. Comme tous les noms, celui-ci sera a priori un canal de communication. Ainsi, le processus $(ν x) P$ (prononcer new x P) crée un nouveau canal, qui sera désigné sous le nom x dans P. Il est à noter que, contrairement à l'opération new x ou dans de nombreux langages, $(ν x)$ produit une constante x. De plus, comme l'état entier du système est représenté dans la syntaxe du terme (sans mémoire), $(ν x) P$ représente aussi le fait que x a été créé à un moment ou à un autre et que P est susceptible d'utiliser x. Par la suite de l'exécution, si $(ν x) P$ est en parallèle avec le processus Q (ce que nous noterons $(ν x) P | Q$ ) et si P communique la valeur de x à Q, le terme deviendra $(ν x)(P | Q)$ pour représenter le fait que P et Q peuvent tous deux utiliser x.

Test d'égalité

Un processus peut tester l'égalité entre deux noms. Ainsi, si a et b représentent le même nom, $if\ a=b\ then\ P\ else\ Q$ réagira comme P, sinon comme Q.

Exemple : Un gestionnaire d'impression

Dans cet exemple, nous construisons progressivement un gestionnaire d'impression (print spooler).

Informellement

Le rôle du gestionnaire d'impression est de recevoir des requêtes d'impression, de localiser une imprimante disponible et de transmettre la requête à l'imprimante. Si aucune imprimante n'est disponible, la requête est mise en attente. Lorsqu'une imprimante a terminé un travail, elle est considérée comme de nouveau en attente.

Plus formellement, une imprimante est représentée par un canal $p r i n t e r 1$ , $p r i n t e r 2$ ... Effectuer une impression sur une imprimante $p r i n t e r i$ revient à envoyer un message sur ce canal composé

du document à imprimer
d'un canal à employer pour prévenir que l'impression est terminée (technique dite de callback, souvent employée pour la programmation asynchrone).

Pour cet exemple, la réserve d'imprimantes peut être représentée comme un ensemble de messages émis sur le canal $s p o o l$ , chacun contenant le nom d'un canal $p r i n t e r i$ . Localiser une imprimante disponible revient donc à recevoir un nom d'imprimante sur le canal $s p o o l$ . Remettre l'imprimante dans la réserve revient à réémettre le nom de l'imprimante sur ce même canal. Pour « protéger » la réserve d'imprimante, le nom du canal $s p o o l$ sera considéré comme local, c'est-à-dire que le gestionnaire sera préfixé par $(ν s p o o l)$ .

Pour cet exemple, faire appel au gestionnaire d'impression consiste à envoyer un message sur le canal $s p o o l e r$ , composé

du document à imprimer
d'un canal à employer pour prévenir que l'impression est terminée.

La réception sur $s p o o l$ est répliquée car le service peut être invoqué un nombre arbitraire de fois.

Formellement

Ainsi, le gestionnaire d'impression peut être défini par $\begin{matrix} SPOOLER = & (\nu spool)(&\\ &&spool\langle printer_1\rangle|spool\langle printer_2\rangle|spool\langle printer_3\rangle|\cdots|spool\langle printer_n\rangle\\ &&|!spooler(task, callback).spool(p).(\nu w)(p\langle task, w \rangle | w().(callback \langle\rangle | spool \langle p \rangle))\\ &) \end{matrix}$

Dans ce qui précède

$task\,$ est le nom local donné au document à imprimer
$callback\,$ est le nom local donné au canal sur lequel émettre un message pour prévenir que le gestionnaire d'impression a terminé son travail
$spool(p)\,$ attend qu'une imprimante $p$ soit disponible
$(\nu w)\,$ définit un canal sur lequel l'imprimante doit émettre un message pour prévenir le gestionnaire d'impression qu'elle a terminé son travail
$p\langle task, w \rangle$ demande à l'imprimante d'imprimer le document $t a s k$
$w()\,$ attend que l'imprimante ait émis son message de fin de travail
$callback \langle\rangle$ permet au gestionnaire d'impression d'émettre son message de fin de travail
$spool \langle p \rangle$ permet de replacer $p$ dans la liste des imprimantes disponibles

Par suite, invoquer le gestionnaire d'impression consistera à placer en présence du terme précédent un terme tel que $CLIENT = (\nu cb)(spooler\langle document, cb \rangle | cb().P)$

Ce terme émet une requête d'impression et attend que la requête soit achevée pour exécuter $P$ .

Exécution du gestionnaire d'impression

Note: cette section s'apparente à observer la trace d'un programme à l'aide d'un débogueur et est donc, de manière prévisible, peu lisible.

Mis en présence, le processus $C L I E N T$ , le processus $S P O O L E R$ et un ensemble d'imprimantes $P R I N T E R S$ réagissent de la manière suivante:

$CLIENT|SPOOLER|PRINTERS = \begin{matrix} (\nu cb) (& spooler\langle document, cb \rangle | cb().P &) |\\ (\nu spool)(&\\ &spool\langle printer_1\rangle|spool\langle printer_2\rangle|spool\langle printer_3\rangle|\cdots|spool\langle printer_n\rangle\\ &|!spooler(task, callback).spool(p).(\nu w)(p\langle task, w \rangle | w().(callback \langle\rangle | spool \langle p \rangle))\\ ) & |PRINTERS \end{matrix}$

$CLIENT|SPOOLER|PRINTERS \longrightarrow \begin{matrix} (\nu cb)(& cb().P & | \\ (\nu spool)(&\\ &spool\langle printer_1\rangle|spool\langle printer_2\rangle|spool\langle printer_3\rangle|\cdots|spool\langle printer_n\rangle\\ &|!spooler(task, callback).spool(p).(\nu w)(p\langle task, w \rangle | w().(callback \langle\rangle | spool \langle p \rangle))\\ &|spool(p).(\nu w)(p\langle document, w \rangle | w().(cb \langle\rangle | spool \langle p \rangle))\\ ))& |PRINTERS\end{matrix}$

$\longrightarrow \begin{matrix} (\nu cb)(& cb().P & | \\ (\nu spool)(&\\ &spool\langle printer_1\rangle|spool\langle printer_2\rangle|spool\langle printer_3\rangle|\cdots|spool\langle printer_n\rangle\\ &|!spooler(task, callback).spool(p).(\nu w)(p\langle task, w \rangle | w().(callback \langle\rangle | spool \langle p \rangle))\\ &|(\nu w)(printer_1\langle document, w \rangle | w().(cb \langle\rangle | spool \langle printer_1 \rangle))\\ ))& |PRINTERS\end{matrix}$

$\longrightarrow^* \begin{matrix} (\nu cb)(& cb().P & | \\ (\nu spool)(&\\ &spool\langle printer_1\rangle|spool\langle printer_2\rangle|spool\langle printer_3\rangle|\cdots|spool\langle printer_n\rangle\\ &|!spooler(task, callback).spool(p).(\nu w)(p\langle task, w \rangle | w().(callback \langle\rangle | spool \langle p \rangle))\\ &|cb \langle\rangle | spool \langle printer_1 \rangle\\ ))& |PRINTERS\end{matrix}$

$\longrightarrow \begin{matrix} &P & | \\ (\nu spool)(&\\ &spool\langle printer_1\rangle|spool\langle printer_2\rangle|spool\langle printer_3\rangle|\cdots|spool\langle printer_n\rangle\\ &|!spooler(task, callback).spool(p).(\nu w)(p\langle task, w \rangle | w().(callback \langle\rangle | spool \langle p \rangle))\\ &| spool \langle printer_1 \rangle\\ ))& |PRINTERS\end{matrix}$

$= P | SPOOLER | PRINTERS\,$

Propriétés du gestionnaire d'impression

À l'aide des divers outils du π-calcul, il est possible de caractériser le gestionnaire d'impression par ses propriétés.

Format des messages

Tout comme les fonctions et variables dans un langage de programmation traditionnel, les canaux du π-calcul peuvent être typés afin de certifier que les messages qui transitent sur ces canaux ont toujours le même format. Dans le cas du gestionnaire d'impression:

$spooler\,$ permet de communiquer des couples composés d'un document et d'un nom de canal sur lequel aucune information ne transite
chaque $printer_i\,$ permet de communiquer des couples composés d'un document et d'un nom de canal sur lequel aucune information ne transite
$spool\,$ permet de communiquer des noms de canaux qui respectent la même politique que $p r i n t e r i$
$task\,$ est un nom de document
$callback\,$ et $w$ sont des noms de canaux sur lesquels aucune information ne transite

Un système de types simple permet d'associer à chaque nom de canal le type des informations qui peuvent circuler sur ce canal. Une manière de noter cela est

$\Gamma \vdash callback : Channel()$ (soit $\Gamma\,$ , l'ensemble des informations de typage connues en ce point du programme, spécifie que $callback\,$ est un nom canal sur lequel aucune information ne transite)
$\Gamma \vdash spooler : Channel(Document, Channel())$
$\Gamma \vdash printer_i : Channel(Document, Channel())$
...

Ces informations peuvent aisément être vérifiées statiquement (i.e. au cours de la compilation) par un logiciel approprié.

Autorisations de lecture/d'écriture

Tout comme les modules et les classes dans de nombreux langages de programmation introduisent des notions de méthodes et de champs publics ou privés, les canaux du π-calcul peuvent être typés afin de certifier que seuls certains agents peuvent écrire sur un canal ou que seuls agents peuvent lire sur un canal. Ainsi, dans le cadre du gestionnaire d'impression, on souhaitera probablement s'assurer que

seul le gestionnaire d'impression est autorisé à recevoir des requêtes sur le canal $s p o o l$ , pour des raisons de sécurité
pour chaque canal $p r i n t e r i$ , seule l'imprimante correspondante est autorisée à recevoir des requêtes sur ce canal
seuls les gestionnaires d'impression sont autorisés à émettre des requêtes sur les canaux $p r i n t e r i$
le gestionnaire d'impression n'est pas autorisé à écrire sur le document
...

Typiquement, afin d'assurer le respect de cette politique de sécurité, un système de types examinera de quelle manière les noms de ces canaux sont distribués (étape assimilable à la liaison dynamique dans les langages traditionnels).

Ainsi, les informations de type du gestionnaire d'impresson pourront être complétées en $\Gamma \vdash spooler : Channel(Document[read], Channel()[write])[read, write]$ . En adoptant ce type, le gestionnaire d'impression s'engage à respecter la politique. suivante: $s p o o l e r$ est un canal qui permet d'émettre ou de recevoir. Sur le canal transitent deux informations: un Document, qui est un canal en lecture seule, et un canal, en écriture seule.

Note cette garantie de sécurité, tout comme le typage public/privé/protégé/... ou interface/implantation procède d'une analyse statique. Un composant inconnu et non-vérifié peut donc violer la politique de sécurité. Pour assurer que seuls des composants vérifiés sont exécutés sur une machine, il peut être nécessaire de faire appel à des techniques telles que le Code Porteur de Preuves ou/et des vérifications dynamiques de typage de code reçu de tierces-parties.