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

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, cx, 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 printer1, printer2 … Effectuer une impression sur une imprimante printeri 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 spool, chacun contenant le nom d'un canal printeri. Localiser une imprimante disponible revient donc à recevoir un nom d'imprimante sur le canal spool. 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 spool sera considéré comme local, c'est-à-dire que le gestionnaire sera préfixé par spool).

Pour cet exemple, faire appel au gestionnaire d'impression consiste à envoyer un message sur le canal spooler, composé

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

La réception sur spool 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 task
  • 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 CLIENT, le processus SPOOLER et un ensemble d'imprimantes PRINTERS 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 printeri
  • 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 spool, pour des raisons de sécurité
  • pour chaque canal printeri, 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 printeri
  • 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 : spooler 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

Équivalence avec un autre gestionnaire d'impression

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



Wikimedia Foundation. 2010.

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

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”