Aniello Murano » 18.Calculus of Communicating Systems (CCS)

CCS: un’introduzione

• Il CCS (Calculus of Communicating System), fu introdotto da Robin Milner intorno al 1980.
• Il CCS ha avuto un forte impatto sullo studio teorico del parallelismo.
• Il CCS, insieme al CSP ed a IMPGC, fa parte dei modelli di comunicazione tra sistemi che condividono variabili.
• Il linguaggio formale CCS è dotato di primitive per la descrizione della composizione parallela, scelte tra azioni e restrizioni di ambito.

Rappresentazione dei processi CCS

• Un processo CCS comunica con il suo ambiente attraverso i canali connessi alle sue porte, proprio come avviene con CSP.
• Un processo p, disposto ad eseguire un input dai canali α e β e un output sui canali α e γ può essere visualizzato come indicato in figura, con le sue porte etichettate nel modo opportuno.

Operazione di restrizione sui processi CCS

• La composizione parallela di p con q, un processo che sia disposto ad eseguire un input da α e un output su β e δ, può essa stessa essere vista come un processo p||q, con porte α?, α!, β?, β!, γ!, γ!.
• L’operazione di restrizione nasconde un determinato insieme di porte.
• Ad esempio, effettuando una restrizione sulle porte specificato dall’insieme di etichette {α, γ} del processo p, si ottiene un processo p{α γ} disposto solamente ad eseguire input sul canale β. La rappresentazione del processo p sarà quindi differente dalla precedente:

Ridenominazione dei canali

• Spesso può risultare utile generare più copie di uno stesso processo, ridenominando, però, alcuni canali.
• Una funzione di ridenominazione è una funzione sui nomi dei canali.
• Dopo essere stato dalla funzione f, con f(α)= γ, f(β)=δ e f(γ)=γ, il processo p diventa il processo p[f].

CCS: sintassi (2)

La sintassi dei processi p, p₀,p₁,… è quella indicata in figura.

dove:

• a e b sono rispettivamente espressioni aritmetiche e booleane;
• x è una variabile che indica un generico valore;
• L è un sottoinsieme dei nomi di canale;
• f è una funzione di ridenominazione;
• P sta per un processo con parametri a₁, …, a_k (quando la lista dei parametri è vuota si scrive solo P).

CCS: sintassi (3)

•  Formalmente, α?x→p è come una lambda astrazione su x, ed ogni occorrenza della variabile x in p è legata da α?x, a condizione che tali variabili non siano presenti in sottotermini della forma β?x→q:
  • le variabili che non sono in questo senso legate vengono dette libere.
• Agli identificatori di processo P sono associate definizioni, scritte come indicato in figura; dove tutte le variabili libere di p compaiono nella lista x₁, …, x_k di variabili distinte.
• Il comportamento di un processo viene determinato dalle definizioni associate agli identificatori di processo che esso contiene.

CCS: semantica

Di seguito viene utilizzato λ che assume valori nell’insieme delle azioni α?n, α!n e τ.