Accueil🇫🇷Chercher

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

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

  1. l'une soit une commande d'entrée, l'autre une commande de sortie ;
  2. les deux processus se nomment mutuellement ;
  3. 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 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

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 exécuté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 compris dans l'intervalle [début, 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 ("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

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

Liens externes

Général
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.
Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.