- Communicating Sequential Processes
-
Communicating sequential processes
En programmation concurrente[1], Communicating sequential processes (CSP) est une algèbre de processus permettant de modéliser l'interaction de systèmes.
CSP intègre un mécanisme de synchronisation basé sur le principe du rendez-vous (détaillé plus loin au travers de la commande d'entrée/sortie). Combinant ce mécanisme à une syntaxe simple et concise, CSP permet alors l'implémentation rapide des paradigmes classiques de la concurrence, tels que producteurs/consommateurs ou lecteurs/écrivains. Ce n'est pas un langage de programmation complet.
CSP fut décrit en premier par C. A. R. Hoare dans un article de 1978[2] , mais a depuis évolué de façon substantielle. CSP a été mis en pratique industriellement comme un outil de spécification formelle de l'exécution concurrente de systèmes variés — tels que le T9000 Transputer,[3] ou un système informatique de transaction commerciale sécurisé. [4]. C'est un champ de recherche toujours actif.
Sommaire
Généralités
Structure d'un programme
Un programme CSP se présente sous la forme d'une suite de commandes et de déclarations de variable séparées par des points-virgule :
x : integer; y : integer; x := 4; ...
Hoare distingue alors deux types de commandes :
- les commandes simples : commande nulle (skip), commande d'affectation et commande d'entrée/sortie ;
- les commandes structurées : commande parallèle, commande répétitive et commande alternative.
Les commandes d'entrée/sortie, parallèle, répétitive et alternative seront détaillées par la suite. La commande nulle, par définition, ne fait rien. Elle permet juste de combler les blocs d'instructions vides. La commande d'affectation a quant à elle une syntaxe classique variable := valeur :
x := 5
Échec de commande, terminaison de programme
L'échec d'une commande (par exemple, dans le cas d'une commande d'entrée/sortie, si le processus visé n'existe pas) entraîne l'échec du processus ou de la commande structurée qui la contient (l'échec d'une commande peut donc entraîner la fin du programme). Notons le cas particulier d'une répétitive dont l'échec d'une commande interne entraîne la terminaison et non la faillite (cf. partie La commande répétitive).
Un échec n'est donc pas une erreur en soi.
Les signaux
Une notion de signal a aussi été introduite en CSP. Un signal est en quelque sorte une variable complexe (ou structurée) composé d'un constructeur (un identifiant libre) ainsi que d'un ensemble de valeurs. Les valeurs peuvent être soit de type élémentaire (entier, chaîne de caractères, etc.) soit d'autres signaux.
Exemples :
- p(3,5) (le constructeur est p et contient les valeurs 3 et 5)
- p(q(3), 5)
- p() (ici, on dit que p() est un signal pur puisqu'il ne contient aucune valeur)
Notons aussi qu'un signal peut être affecté à une variable (exemple : x := p (4)), et peut aussi être la cible d'une affectation. Cela permet alors des affectations du type (x, y) := (y, x).
Détails sur les commandes
La commande parallèle
Elle permet la mise en concurrence de processus par la syntaxe suivante :
[ proc1 :: liste de commandes || proc2 :: liste de commandes || ... ]
Une telle commande ne se termine que lorsque tous les processus qu'elle définit sont terminés, l'échec d'un seul entraînant l'échec de la commande parallèle. Précisons qu'une variable définie avant une commande parallèle est visible par les processus qu'elle contient. Ceci implique nécessairement que tous les processus définis devront avoir accès aux variables déclarées avant la commande parallèle. On assiste donc ici à un partage de ressources, dont les contraintes soulevées (accès exclusif, etc.) sont à la charge du programmeur.
On note aussi la possibilité de déclarer plusieurs processus pour une même liste de commandes, comme le montre l'exemple suivant :
proc1 [i:1..10] :: liste de commandes
Ici, dix processus ayant la même liste de commandes seront mis en concurrence.
La commande d'entrée/sortie
Les communications entre processus reposent sur cette commande. Pour expliciter son fonctionnement, partons du cas simple de deux processus producteur et consommateur, le premier voulant transmettre une variable x au second. Une telle communication s'effectuera alors au travers des commandes suivantes :
consommateur!x
permettra au processus producteur d'envoyer x au processus consommateur
producteur?x
permettra au processus consommateur de recevoir x depuis le processus producteur
Du point de vue de la syntaxe, on remarque que le ! indique une commande de sortie, tandis que le ? indique une commande d'entrée. Plus formellement, une commande d'entrée se présentera sous la forme :
processus_source?variable_cible
et une commande de sortie sous la forme :
processus_cible!expression_source.
De plus, pour que la communication soit possible entre deux commandes d'e/s, CSP impose que :
- l'une soit une commande d'entrée, l'autre une commande de sortie ;
- les deux processus se nomment mutuellement ;
- les typages de la variable cible et de l'expression source soient identiques.
Dans ces conditions, la transmission peut avoir lieu, et le contenu de l'expression source est copié vers la variable cible. Si l'une de ces conditions n'est pas respectée, les processus sont mis en attente, entraînant par conséquent un interblocage. Si l'un des processus est mort, alors toute commande d'entrée/sortie impliquant ce processus doit échouer. Enfin, le premier processus demandant la communication doit être mis en attente jusqu'à ce que le second le rejoigne. On retrouve ici le principe du rendez-vous. Notons aussi le cas particulier d'une synchronisation simple, c'est-à-dire sans transmission de valeur, possible grâce à l'utilisation d'un signal pur. Exemple :
[ producteur :: ... consommateur?p(); ... || consommateur :: ... producteur!p(); ... ]
La commande alternative
Une commande alternative se présente sous la forme d'un ensemble de sélectives, chacune étant composée d'une garde ainsi que d'une liste de commandes. Une garde est quant à elle composée d'une partie expression booléenne et d'une partie commande d'entrée, l'une ou l'autre pouvant être omise. Syntaxiquement, une commande alternative se présente sous la forme suivante :
[ garde1 -> liste de commandes [] garde2 -> liste de commandes [] ... ]
Où garde1 et garde2 sont de la forme :
expression_booleenne ; commande_entrée
Ce qui donne par exemple :
[ i < 5 ; processus?p(x) -> ... [] console!write(msg) -> ... [] i > 5 -> ... ]Lors de l'exécution d'une commande alternative, chacune de ses gardes est testée, afin de déterminer sa valeur selon une logique trivaluée (c'est-à-dire qu'une garde peut être vraie, fausse, ou neutre) :
- Une expression booléenne peut évidemment prendre les valeurs vrai ou faux
- Une commande d' entrée prend la valeur :
- vrai si la communication est possible immédiatement ;
- neutre si le processus nommé par la commande n'est pas encore prêt ;
- faux si le processus nommé par la commande est mort (i.e. a fini son exécution).
- Dans le cas d'une garde contenant à la fois une partie expression booléenne et une partie commande entrée, l'expression booléenne est d'abord évaluée. Si elle est à faux, la garde est évaluée à faux. Si elle est à vrai, la commande d'entrée est alors évaluée, et donne la valeur à la garde.
Ainsi, si une ou plusieurs commandes gardées sont vraies, un choix indéterministe (i.e. aléatoire) doit être effectué pour n'en sélectionner qu'une. Si aucune n'est vraie mais que certaines sont neutres, le processus se met en attente des commandes d'entrées correspondantes. Et si toutes les commandes gardées sont fausses, la commande alternative échoue.
Si une garde est sélectionnée, la liste de commande correspondante doit alors être exécutée.
Il est aussi important de noter que la contrainte d'ordre syntaxique limitant les commandes d'e/s dans les gardes aux simples commandes d'entrée, provient d'un choix fait par HOARE dans le but d'éviter les incohérences.
Pour illustrer ce propos, partons de l'exemple suivant (qui suppose possible l'utilisation de commande de sortie dans les gardes) :
[ proc1 :: [ proc2?p() -> ... [] proc2?q() -> ... ] || proc2 :: [ proc1!p() -> ... [] proc1!q() -> ... ] ]Supposons que les deux processus soient chacun arrivés sur leur commande alternative. Les deux commandes vont donc être évaluées parallèlement :
- le premier processus va évaluer chacune des gardes de l'alternative, puis, les deux étant vraies, il va effectué un choix aléatoire entre l'une ou l'autre ;
- de même, le second processus va se retrouver à devoir faire un choix entre l'une ou l'autre des gardes de son alternative.
Si les deux alternatives sélectionnent la même communication, aucun problème n'est soulevé. Par contre, si chacune choisie une communication différente, on assiste à un cas d'incohérence entraînant nécessairement un interblocage.
Ainsi, la communication entre commandes d'entrée/sortie gardées posant des problèmes, HOARE a décidé de l'empêcher en autorisant uniquement les commandes d'entrée dans les gardes.
Précisons cependant que le compilateur proposé en fin de cet article autorise les commandes de sortie dans les gardes, mais ajoute en contrepartie la condition suivante :
- Pour qu'une communication soit établie entre deux processus, il faut qu'au moins une des deux commandes d'e/s soit hors-garde.
On évite alors bien le problème cité ci-dessus.
La commande répétitive
La commande répétitive est composée d'une unique commande alternative, dont l'échec entraîne la fin de la répétition. On peut donc considérer qu'une répétitive ne peut se terminer qu'avec succès. Syntaxiquement, elle se présente sous la forme d'une étoile suivie d'une alternative :
*commande alternative
Par exemple :
i := 0; *[ i < 10 -> i := i + 1 ]
Ici, la commande répétitive se terminera lorsque i aura atteint la valeur 10.
Conventions, pratiques usuelles
Définition de processus
On retrouve souvent la syntaxe PROCESSUS == liste d'instructions pour définir un processus à l'extérieur d'une commande parallèle, dans le seul but de clarifier le code. Exemple :
PREMIER == x : integer := 5; ... SECOND == msg : string; ... MAIN == [ premier :: PREMIER || second :: SECOND ]La liste d'instructions MAIN est alors celle executée au lancement du programme.
Commande d'affichage (print)
Pour afficher un message à l'écran, on utilise usuellement la commande :
print (message)
Commande aléatoire (random)
x := random (debut, fin)
Permet de prendre un nombre au hasard compri dans l'intervalle [debut, fin]
Commande sleep
sleep (tps)
Stoppe le processus qui l'exécute pendant tps millisecondes. Permet de simuler des temps d'attente, etc.
Définition de constantes
On utilise communément la syntaxe :
define CONSTANTE valeur
Exemple :
define PI 3.1415
Exemple de programmes de type producteur/consommateur
Un producteur, deux consommateurs
PRODUCTEUR == nb : integer := 0; *[ nb < 100 -> delegueur!nb; nb := nb + 1 ] DELEGUEUR == nb : integer; *[ true -> producteur?nb; [ consommateur[1]!nb -> skip [] consommateur[2]!nb -> skip ] ] CONSOMMATEUR == nb : integer; *[ true -> delegueur?nb; print (nb) ] MAIN == [ producteur :: PRODUCTEUR || consommateur[i:1..2] :: CONSOMMATEUR || delegueur :: DELEGUEUR ]
Un producteur envoie une suite de nombre à un processus délégueur qui les transmet à deux consommateurs. L'utilisation d'une commande alternative dans le délégueur permet :
- de se mettre en attente si aucun des deux consommateurs n'est prêt ;
- d'envoyer le nombre à l'un s'il est le seul prêt ;
- de choisir aléatoirement entre les 2 consommateurs si les deux sont prêts.
Plusieurs producteurs, plusieurs consommateurs
define NP 10 // Nombre de producteurs define NC 10 // Nombre de consommateurs define TL 5 // Taille du tampon intermédiaire CONSOLE == msg : string; *[ true-> [ (i:1..NP) producteur[i]?write (msg) -> print (msg) [] (i:1..NC) consommateur[i]?write (msg) -> print (msg) ] ] PRODUCTEUR == nb : integer := 0; message : string; *[ true -> message := "objet num " + nb; liste!prod(message); console!write ("production " + i + " : " + message + "\n"); nb := nb + 1 ] LISTE == tab : [0..TL-1] string := [0..TL-1] ""; used,mark : integer := 0; message : string := ""; *[ (i:1..NP) used < TL; producteur[i]?prod(tab[(mark + used) mod TL]) -> used := used + 1 [] (i:1..NC) used > 0; consommateur[i]!cons(tab[mark]) -> mark := (mark + 1) mod TL; used := used - 1 ] CONSOMMATEUR == message : string; *[ true -> liste?cons(message); console!write ("consommateur " + i + " : " + message + "\n") ] MAIN == [ producteur[i:1..NP] :: PRODUCTEUR || consommateur[i:1..NC] :: CONSOMMATEUR || liste :: LISTE || console :: CONSOLE ]Références
- ↑ (en) A. W. Roscoe, The Theory and Practice of Concurrency, Prentice Hall, 1997 (ISBN 0-13-674409-5)
- ↑ C. A. R. Hoare, « Communicating sequential processes », dans Communications of the ACM, vol. 21, no 8, 1978, p. 666–677 [lien DOI]
- ↑ G. Barrett, « Model checking in practice: The T9000 Virtual Channel Processor », dans IEEE Transactions on Software Engineering, vol. 21, no 2, 1995, p. 69–78 [lien DOI]
- ↑ A Hall, « Correctness by construction: Developing a commercial secure system », dans IEEE Software, vol. 19, no 1, 2002, p. 18–25 [[pdf] texte intégral lien DOI]
Liens externes
- Général
- [pdf] Article originel dans lequel C.A.R. Hoare définit CSP
- Une archive en ligne sur ce sujet
- WoTUG, est un forum dédié aux utilisateur du langage CSP.
- Citations référencées par le portail CiteSeer
- Outils d'analyse
- Formal Systems Europe, Ltd. développe des outils CSP, dont certains sont en téléchargement libre .
- ARC, propose un outil de vérification.
- ProB est un animateur et vérificateur de modèle pour la Méthode B, mais permet aussi la vérification de programmes CSP.
- PAT est un vérificateur et simulateur de modèle CSP, plus diverses extensions du langage (par exemple, variables partagées, tableaux, équité).
- Aide à l'implémentation
- CTJ est une implémentation en Java de CSP avec support réseau/distribué.
- C++CSP est une implémentation des idées de CSP/occam/JCSP en C++, d'un style semblable à JCSP.
- Jibu (connu précédemment sous le nom CSP.NET) est une bibliothèque Microsoft .NET de style CSP.
- CSP++ est un outil de synthèse logicielle qui rend les spécifications écrite en CSPm exécutable via C++.
- csp est une bibliothèque Common Lisp qui utilise un modèle d'exécution concurrente inspiré de CSP.
- CHP est une bibliothèque Haskell implémentant un modèle de concurrence inspiré de CSP.
- CTJ (CSP to JAVA), un compilateur de CSP avec interface graphique, ce compilateur accepte toutes les conventions définies précédemment. Les exemples cités ci-dessus fonctionnent correctement avec ce compilateur.
Portail de l’informatique
Catégories : Langage de programmation | Méthode formelle
Wikimedia Foundation. 2010.
