Pi-calcul

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.

Sommaire

1 La problématique

2 Définition informelle

2.1 Les entités du π-calcul

2.2 Les constructions du π-calcul

2.2.1 Processus terminé

2.2.2 Émission

2.2.3 Réception

2.2.4 Composition parallèle

2.2.5 Création d'un nom

2.2.6 Test d'égalité

2.2.7 Processus dual

2.2.8 Infinité de processus

3 Exemple : Un gestionnaire d'impression

3.1 Informellement

3.2 Formellement

3.3 Exécution du gestionnaire d'impression

3.4 Propriétés du gestionnaire d'impression

3.4.1 Format des messages

3.4.2 Autorisations de lecture/d'écriture

3.4.3 Gestion des ressources

3.4.4 Équivalence avec un autre gestionnaire d'impression

4 Implémentations

La problématique

En tant que langage de programmation théorique (ou langage formel), 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)

politique 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 en anglais : 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, 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.

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. 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.

Processus dual

La notation P + Q dénote un processus qui se comporte tout aussi bien comme P que comme Q.

Infinité de processus

Il est possible de faire référence à une infinité de copies d'un processus P par la notation !P. Cette syntaxe n'a donc pas la signification usuelle not P utilisée par la plupart des langages de programmation !

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{array}{rcl} 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{array}$

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 :

$\begin{array}{rcl} CLIENT|SPOOLER|PRINTERS & = & (\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{array}$

$\begin{array}{rcl} CLIENT|SPOOLER|PRINTERS & \longrightarrow & (\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{array}$

$\begin{array}{rcl} CLIENT|SPOOLER|PRINTERS & \longrightarrow & (\nu cb)( \\ & & \ \ cb().P | (\nu spool)( \\ & & \ \ \ \ 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{array}$

$\begin{array}{rcl} CLIENT|SPOOLER|PRINTERS & \longrightarrow^* & (\nu cb)( \\ & & \ \ cb().P | (\nu spool)( \\ & & \ \ \ \ 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{array}$

$\begin{array}{rcl} CLIENT|SPOOLER|PRINTERS & \longrightarrow & P | (\nu spool)( \\ & & \ \ 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{array}$

$\begin{array}{rcl}CLIENT|SPOOLER|PRINTERS & \equiv & P | SPOOLER | PRINTERS\end{array}$

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/mise en œuvre 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.

Gestion des ressources

Cette section est vide, insuffisamment détaillée ou incomplète. Votre aide est la bienvenue !

Équivalence avec un autre gestionnaire d'impression

Cette section est vide, insuffisamment détaillée ou incomplète. Votre aide est la bienvenue !

Implémentations

Les langages de programmation suivants sont des implémentations du π-calcul ou de ses variantes :

Acute

Business Process Modeling Language (BPML)

Nomadic Pict

jumel : un compilateur pour un dialecte de ML assorti de primitives du π-calcul pour le passage de messages

occam-π

Pict

JoCaml (basé sur le Join-calcul)

Funnel (une implémentation du join-calcul compatible avec JRE)

CubeVM (une implementation sans pile)

Le langage SpiCO : un π-calcul stochastique pour les objets concurents

BioSPI et SPiM: simulateurs pour le π-calcul stochastique

Ateji PX: une extension de Java avec des primitives de parallèlisme inspirées du π-calcul

Portail de l'informatique théorique

Catégories :
Langage de programmation théorique
Méthode formelle

Contenu soumis à la licence CC-BY-SA. Source : Article Pi-calcul de Wikipédia en français (auteurs)

Игры ⚽ Поможем сделать НИР

Regardez d'autres dictionnaires:

CALCUL INFINITÉSIMAL - Histoire — L’expression «calcul infinitésimal» désigne habituellement l’ensemble des notations et des méthodes fondamentales du calcul différentiel, du calcul intégral et du calcul des variations, tel qu’il a été mis au point au cours des XVIIe et XVIIIe… … Encyclopédie Universelle
Calcul (Mathématiques) — En mathématiques, un calcul est une opération ou un ensemble d opérations effectuées sur des grandeurs[1]. Initialement ces grandeurs étaient des nombres mais le développement des outils mathématiques et de l abstraction permet maintenant d… … Wikipédia en Français
Calcul (mathematiques) — Calcul (mathématiques) En mathématiques, un calcul est une opération ou un ensemble d opérations effectuées sur des grandeurs[1]. Initialement ces grandeurs étaient des nombres mais le développement des outils mathématiques et de l abstraction… … Wikipédia en Français
Calcul Des Prédicats — Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens de la fin du XIXe siècle et … Wikipédia en Français
Calcul des predicats — Calcul des prédicats Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens de la fin… … Wikipédia en Français
Calcul des prédicats du premier ordre — Calcul des prédicats Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens de la fin… … Wikipédia en Français
Calcul des relations — Calcul des prédicats Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens de la fin… … Wikipédia en Français
Calcul littéral — Calcul (mathématiques) En mathématiques, un calcul est une opération ou un ensemble d opérations effectuées sur des grandeurs[1]. Initialement ces grandeurs étaient des nombres mais le développement des outils mathématiques et de l abstraction… … Wikipédia en Français
Calcul mathématique — Calcul (mathématiques) En mathématiques, un calcul est une opération ou un ensemble d opérations effectuées sur des grandeurs[1]. Initialement ces grandeurs étaient des nombres mais le développement des outils mathématiques et de l abstraction… … Wikipédia en Français
Calcul scientifique — Calcul (mathématiques) En mathématiques, un calcul est une opération ou un ensemble d opérations effectuées sur des grandeurs[1]. Initialement ces grandeurs étaient des nombres mais le développement des outils mathématiques et de l abstraction… … Wikipédia en Français
Calcul Des Propositions — Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C est aussi la première… … Wikipédia en Français

Dictionnaires et Encyclopédies sur 'Academic'

Pi-calcul

Sommaire

La problématique

Définition informelle

Les entités du π-calcul

Les constructions du π-calcul

Processus terminé

Émission

Réception

Composition parallèle

Création d'un nom

Test d'égalité

Processus dual

Infinité de processus

Exemple : Un gestionnaire d'impression

Informellement

Formellement

Exécution du gestionnaire d'impression

Propriétés du gestionnaire d'impression

Format des messages

Autorisations de lecture/d'écriture

Gestion des ressources

Équivalence avec un autre gestionnaire d'impression

Implémentations

Regardez d'autres dictionnaires:

Share the article and excerpts

Dictionnaires et Encyclopédies sur 'Academic'

Wikipédia en Français

Pi-calcul

Sommaire

La problématique

Définition informelle

Les entités du π-calcul

Les constructions du π-calcul

Processus terminé

Émission

Réception

Composition parallèle

Création d'un nom

Test d'égalité

Processus dual

Infinité de processus

Exemple : Un gestionnaire d'impression

Informellement

Formellement

Exécution du gestionnaire d'impression

Propriétés du gestionnaire d'impression

Format des messages

Autorisations de lecture/d'écriture

Gestion des ressources

Équivalence avec un autre gestionnaire d'impression

Implémentations

Regardez d'autres dictionnaires:

Share the article and excerpts

Direct link