Aniello Murano » 15.Nondeterminismo e Parallelismo (Concorrenza)

Prefazione

• In questa lezione introduciamo l’ultimo argomento del corso: Sistemi e Programmi Nondeterministici e Paralleli (Concorrenti) e alla loro semantica.
• Inizieremo mostrando un semplice linguaggio parallelo (IMPP) ottenuto estendendo il linguaggio IMP.
• Poi analizzeremo modelli di comunicazione tra sistemi che condividono variabili. Saranno trattati i seguenti argomenti:
  • Linguaggio di Dijkstra dei comandi con guardia (IMPCG);
  • Communicating Sequential Processes (CSP) di Tony Hoare
  • Calculus of Communicating system (CCS) di Robin Milner
• Infine, in riferimento alla verifica di sistemi introdotta nella lezione precedente, brevemente mostreremo:
  • Una Logica modale da utilizzare come linguaggio di specifica.
  • Un algoritmo per la verifica del soddisfacimento di una specifica da parte di un processo a stati finiti.
• Tutti questi strumenti sono alla base dello studio degli strumenti di verifica formale dei sistemi paralleli !!!

Linguaggio IMP parallelo

• Un semplice linguaggio parallelo può essere introdotto estendo l’insieme dei comandi del linguaggio imperativo IMP con una operazione di composizione parallela c₀ k c₁:
• c::= skip | X:=a |c₀;c₁| if b then c₀ else c₁| while b do c | c₀ k c₁
• Semantica informale:
  • Dati c₀ e c₁, l’esecuzione della loro composizione parallela c₀ k c₁ avverrà come se c₀ e c₁ fossero eseguiti contemporaneamente!

Osservazioni:

• Cosa succede se c₀ e c₁ accedono alla stessa variabile (per esempio due nuovi assegnamenti alla stessa variabile?
• Uno dei due comandi eseguirà con successo l’assegnamento eventualmente seguito dall’altro assegnamento;
• Questo significa che:
  • L’interpretazione dei comandi non è certa !
  • Non possiamo descrivere l’esecuzione di comandi paralleli utilizzando la stessa relazione fra configurazioni di comandi e stati finali finora utilizzata per IMP.

Comunicazione e nondeterminismo

• In una operazione di composizione parallela c₀ k c₁, se c₀ e c₁ hanno locazioni in comune, allora le loro esecuzioni possono risultare reciprocamente influenzate.
• Si può pensare che i due comandi comunichino tramite queste locazioni (comunicazione tramite variabili condivise).
• Come si vede dalle regole semantiche date per la composizione parallela, l’interpretazione di IMPP non è certa. Per esempio, per il seguente comando:
  • c ´ (X:=0 k X:=1); if X:=0 then c₀ else c₁
• non possiamo sapere se questo si comporterà come c₀ o come c₁
• Questa incertezza viene chiamata nondeterminismo.
• È importante sapere che nella programmazione parallela il nondeterminismo è un elemento ineliminabile. Questo vale non solo per i programmi semplici presentati in questo corso, ma anche per i complessi sistemi utilizzati nella realtà.

Sintassi del linguaggio di Dijkstra

• Questo linguaggio contiene le stesse espressioni aritmetiche e booleane di IMP, (Aexp e Bexp). Inoltre, possiede due nuove categorie sintattiche: i comandi (c) e i comandi con guardia (gc).
• La sintassi dei comandi è data dalle seguenti regole:
  • c::= skip | abort | X:=a| c₀;c₁ | if gc fi | do gc od
• La sintassi dei comandi con guardia è data dalle seguenti regole:
  • gc::= b ! c | gc₀ Y gc₁
• Y è l’operatore alternativo. Un comando con guardia solitamente ha la forma:
  • (b₁ ! c₁) Y … Y (b_n ! c_n)
• In questo caso le b_i sono chiamate guardie. Se b_i è true allora ci può essere eseguito. Se nessuna guardia è valutata true il comando fallisce. Altrimenti non deterministicamente viene eseguito uno tra i c_i abilitati ad essere eseguiti.

Significato degli altri comandi

• Sintassi dei comandi e dei comandi con guardia:
  • c::= skip | abort | X:=a| c₀;c₁ | if gc fi | do gc od
  • gc::= b ! c | gc₀ Y gc₁
• Skip, assegnamento e composizione sequenziale hanno lo stesso significato dato in IMP.
• Abort non produce uno stato finale a partire da qualsiasi stat.
• Il comando if gc fi si comporta come il comando di guardia gc se gc non fallisce, altrimenti si comporta come abort.
• Il comando do gc od si comporta come l’esecuzione ripetuta del comando di guardia gc fino a che gc non fallisce. Esso si comporta come skip quando gc fallisce.

Regole per i comandi con guardia

Si noti come i comandi alternativi introducano il nondeterminismo

Equivalenza di IMPG con gli altri comandi di IMP

• Conditionals and while-loops of IMP can easily be modeled in IMPGC.
• We reintroduce them as abbreviations of IMPGC commands:
  • if b then c₀ else c₁ ´ if b ! c₀ Y :b ! C₁ fi and
  • while b do c ´ do b ! c od

Come utilizzare IMPGC

Given an expression in pseudocodice:

if a ¸ b then print “More or equal”;
else if a < b then print “Less”;

The equivalent in guarded commands is:

if
a ¸ b ! print “More or equal” Y
a < b ! print “Less”
fi

The power of guarded commands is illustrated in the following expression:

if
a ¸ b ! print “More or equal” Y
a · b ! print “Less or equal”
fi

When a = b, the result of command can be one “More or equal” or “Less or equal”.

Osservazioni sulla terminazione

• For every IMP command c and for every state σ there exists a configuration <c’, σ’> (or σ’) such that <c, σ>!₁ <c’, σ’> (or <c, σ>!₁ σ’, respect.)
  • The proof is a straightforward induction on the structure of c.
• In IMP, every command c has, from every state _, precisely one computation.
  • The prof follows by structural induction on commands.
• Le precedenti proprietà non valgono per IMPGC. La seconda è stata già discussa in precedenza. Per mostrare la non validità della prima è sufficiente utilizzare il seguente comando
• c ´<if false ! skip, σ> . Infatti, per le regole date, non esiste una configurazione <c’, σ’> (o uno stato σ) tale che <c, σ>!₁ <c’, σ’> (<c, σ>!₁ σ’).

Esercizio 2

Si dimostri la terminazione del programma in figura dove:

• 2|X significa 2 divide X
• ( 5 x X)/3 significa (5 moltiplicato X) diviso 3