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

Généralités[modifier | modifier le code]

Structure d'un programme[modifier | modifier le code]

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 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[modifier | modifier le code]

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[modifier | modifier le code]

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 des affectations du type (x, y) := (y, x).

Détails sur les commandes[modifier | modifier le code]

La commande parallèle[modifier | modifier le code]

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[modifier | modifier le code]

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 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[modifier | modifier le code]

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 effectuer 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 choix sélectionnent la même communication, aucun problème n'est soulevé. Par contre, si chacun sélectionne 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.

Ainsi, on évite bien le problème décrit.

La commande répétitive[modifier | modifier le code]

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[modifier | modifier le code]

Définition de processus[modifier | modifier le code]

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 exécutée au lancement du programme.

Commande d'affichage (print)[modifier | modifier le code]

Pour afficher un message à l'écran, on utilise usuellement la commande :

print (message)

Commande aléatoire (random)[modifier | modifier le code]

x := random (debut, fin)

Permet de prendre un nombre au hasard compris dans l'intervalle [début, fin]

Commande sleep[modifier | modifier le code]

sleep (tps)

Stoppe le processus qui l'exécute pendant tps millisecondes. Permet de simuler des temps d'attente, etc.

Définition de constantes[modifier | modifier le code]

On utilise communément la syntaxe :

define CONSTANTE valeur

Exemple :

define PI 3.1415

Exemple de programmes de type producteur/consommateur[modifier | modifier le code]

Un producteur, deux consommateurs[modifier | modifier le code]

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[modifier | modifier le code]

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 ("producteur " + 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[modifier | modifier le code]

↑ (en) A. W. Roscoe, The Theory and Practice of Concurrency, New York, Prentice Hall, 1997, 565 p., poche (ISBN 978-0-13-674409-2, LCCN 97031217)
↑ (en) C. A. R. Hoare, « Communicating sequential processes », Communications of the ACM, vol. 21, n^o 8,‎ 1978, p. 666–677 (DOI 10.1145/359576.359585)
↑ (en) G. Barrett, « Model checking in practice: The T9000 Virtual Channel Processor », IEEE Transactions on Software Engineering, vol. 21, n^o 2,‎ 1995, p. 69–78 (DOI 10.1109/32.345823).
↑ (en) A Hall et R. Chapman, « Correctness by construction: Developing a commercial secure system », IEEE Software, vol. 19, n^o 1,‎ 2002, p. 18–25 (DOI 10.1109/52.976937, lire en ligne [PDF])

Liens externes[modifier | modifier le code]

Général

[PDF] Article originel dans lequel C.A.R. Hoare définit CSP
Une archive en ligne sur ce sujet
WoTUG, un forum destiné aux utilisateurs 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 la programmation informatique

[roscoe-1] (en) A. W. Roscoe, The Theory and Practice of Concurrency, New York, Prentice Hall, 1997, 565 p., poche (ISBN 978-0-13-674409-2, LCCN 97031217)

[hoare1978-2] (en) C. A. R. Hoare, « Communicating sequential processes », Communications of the ACM, vol. 21, n^o 8,‎ 1978, p. 666–677 (DOI 10.1145/359576.359585)

[barrett-3] (en) G. Barrett, « Model checking in practice: The T9000 Virtual Channel Processor », IEEE Transactions on Software Engineering, vol. 21, n^o 2,‎ 1995, p. 69–78 (DOI 10.1109/32.345823).

[hall-4] (en) A Hall et R. Chapman, « Correctness by construction: Developing a commercial secure system », IEEE Software, vol. 19, n^o 1,‎ 2002, p. 18–25 (DOI 10.1109/52.976937, lire en ligne [PDF])

[1]

[2]

[3]

[4]