Vai alla Home Page About me Courseware Federica Living Library Federica Federica Podstudio Virtual Campus 3D Le Miniguide all'orientamento Gli eBook di Federica La Corte in Rete
 
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

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 c0 k c1:
  • c::= skip | X:=a |c0;c1| if b then c0 else c1| while b do c | c0 k c1
  • Semantica informale:
    • Dati c0 e c1, l’esecuzione della loro composizione parallela c0 k c1 avverrà come se c0 e c1 fossero eseguiti contemporaneamente!

Osservazioni:

  • Cosa succede se c0 e c1 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.

Semantica dell’operazione parallela

  • La semantica operazionale della composizione parallela è data dalle regole in figura.
  • La relazione di esecuzione rappresenta singoli passi non interrompibili in modo da permettere ad un comando di modi-ficare lo stato di un altro comando con cui è posto in parallelo.
  • Le prime due regole si riferiscono al caso in cui c0 sia eseguita prima di c1 e le ultime due al caso simmetrico (c1 prima di c0).
  • La prima e la terza regola si riferiscono al caso in cui l’esecuzione di c0 e c1 siano terminate, mentre la seconda e la quarta al caso che esse non lo siano.

Comunicazione e nondeterminismo

  • In una operazione di composizione parallela c0 k c1, se c0 e c1 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 c0 else c1
  • non possiamo sapere se questo si comporterà come c0 o come c1
  • 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à.

Vantaggi del nondeterminismo

  • Spesso il raggiungimento di un certo risultato non dipende da quale strada viene utilizzata, fra quelle disponibili.
  • Un utilizzo “disciplinato” del nondeterminismo può portare allo sviluppo di algoritmi più efficienti.
  • Il linguaggio dei comandi con guardia di Dijkstra è basato su questa filosofia: non è richiesto al programmatore di specificare nei dettali il metodo di soluzione.
  • Edsger Wybe Dijkstra (1930–2002) was a Dutch computer scientist.
  • He received the 1972 A. M. Turing Award for fundamental contributions in the area of programming languages (ALGOL, late 1950’s ).
  • Dijkstra’s algorithm: an algorithm that solves the single-source shortest path problem for a directed graph with nonnegative edge weights.
Edsger Wybe Dijkstra

Edsger Wybe Dijkstra


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| c0;c1 | if gc fi | do gc od
  • La sintassi dei comandi con guardia è data dalle seguenti regole:
    • gc::= b ! c | gc0 Y gc1
  • Y è l’operatore alternativo. Un comando con guardia solitamente ha la forma:
    • (b1 ! c1) Y … Y (bn ! cn)
  • In questo caso le bi sono chiamate guardie. Se bi è true allora ci può essere eseguito. Se nessuna guardia è valutata true il comando fallisce. Altrimenti non deterministicamente viene eseguito uno tra i ci abilitati ad essere eseguiti.

Significato degli altri comandi

  • Sintassi dei comandi e dei comandi con guardia:
    • c::= skip | abort | X:=a| c0;c1 | if gc fi | do gc od
    • gc::= b ! c | gc0 Y gc1
  • 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 di derivazione per c e gc

  • Una configurazione di un comando è <c, σ> oppure solo σ. Si raggiunge la configurazione σ solo quando uno stato è stato completamento eseguito.
  • Una configurazione iniziale di un comando con guardia è <gc, σ> e un solo passo di esecuzione può portare a una configurazione di comando o ad una configurazione di fallimento (fail).
Regole per i comandi

Regole per i comandi


Regole per i comandi con guardia

Si noti come i comandi alternativi introducano il nondeterminismo

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 c0 else c1 ´ if b ! c0 Y :b ! C1 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”.

Esempio (1)

L’esempio in figura mostra un utilizzo efficiente del comando if del linguaggio IMPCG per calcolare il massimo tra due locazioni.


Esempio (2)

Il seguente esempio mostra un modo elegante dell’applicazione dell’algoritmo di Euclide per il calcolo del massimo comun divisore di due numeri, utilizzo il comando do del linguaggio IMPCG.


Osservazioni sulla terminazione

  • For every IMP command c and for every state σ there exists a configuration <c’, σ’> (or σ’) such that <c, σ>!1 <c’, σ’> (or <c, σ>!1 σ’, 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, σ>!1 <c’, σ’> (<c, σ>!1 σ’).

Esercizio 1

  • Si dimostri che per ogni espressione booleana b e comando c, i comandi in figura sono semanticamente equivalenti.
  • La valutazione di :b è semplicemente data dall’opposto della valutazione di b.

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
  • Contenuti protetti da Creative Commons
  • Feed RSS
  • Condividi su FriendFeed
  • Condividi su Facebook
  • Segnala su Twitter
  • Condividi su LinkedIn
Progetto "Campus Virtuale" dell'Università degli Studi di Napoli Federico II, realizzato con il cofinanziamento dell'Unione europea. Asse V - Società dell'informazione - Obiettivo Operativo 5.1 e-Government ed e-Inclusion