FSP - dichiarazione di costanti e di intervalli
in.1.1
L’uso di indici serve
per modellare calcoli
in.1.0
in.0.1
in.0.0
0
out.0
const N = 1
intervallo T = 0..N
intervallo R = 0..2*N
1
2
3
out.1
out.2
SUM
= (in[a:T][b:T]->TOTAL[a+b]),
TOTAL[s:R] = (out[s]->SUM).
Concurrency: concurrent execution
1
©Magee/Kramer
SOMMA CON RETI DI PETRI
Leggo 0,0
Stampo 0
Leggo 0,1
Leggo 1,0
Stampo 1
Leggo 1,1
Stampo 2
Se l’ordine di lettura viene considerato nella definizione degli stati
la coppia (1,0) è diversa dalla coppia (0,1):
Leggo 0,0
Concurrency: concurrent execution
Stampo 0
Leggo 0,1
Stampo 1
Leggo 1,0 Leggo 1,1
Stampo 1
Stampo 2
2
©Magee/Kramer
Capitolo 3
Processi concorrenti
Concurrency: concurrent execution
3
©Magee/Kramer
Esecuzione concorrente
Concetti: processi - esecuzione concorrente e
alternanza (interleaving).
Interazione di processi.
Modelli: composizione parellela di processi asincroni
- interleaving
interazione - azioni condivise
labeling di processi, relabeling di azioni e hiding
structure diagrams
Pratica: programmi Java con Multithread
Concurrency: concurrent execution
4
©Magee/Kramer
Definizioni
 Concorrenza
 computazioni logicamente
simultanee.
Non implica multipli processori
Richiede esecuzione “alternata”
su un singolo processore
 Parallelismo
A
B
C
Tempo
Processore condiviso da tre processi
 computazioni fisicamente
simultanee.
Richiede multipli processori
Sia la concorrenza sia il parallelismo richiedono un accesso
controllato a risorse condivise. Nel libro di testo i termini
parallelo e concorrente sono utilizzati come sinonimi.
Un azione
è concorrente a un’azione b se il loro ordine di
Concurrency:
concurrentaexecution
esecuzione è indifferente
5
©Magee/Kramer
Modellare la concorrenza
 Si riesce a modellare la velocità di esecuzione?
 Velocità arbitraria
(il tempo NON è modellato)
 Come si modella la concorrenza?
 Ordine relativo delle azioni di processi differenti è arbitrario
(alternanza dei processi MA conservazione della sequenza di
azioni in ogni processo)
 Qual’è il risultato?
 Modello generale indipendente dallo scheduling
(modello di esecuzione asincrona)
Concurrency: concurrent execution
6
©Magee/Kramer
Composizione parallela - alternanza di azioni
Se P e Q sono processi allora (P||Q) rappresenta
l’esecuzione concorrente di P e Q. L’operatore || è
denominato operatore di composizione parallela.
ITCH = (scratch->STOP).
CONVERSE = (think->talk->STOP).
||CONVERSE_ITCH = (ITCH || CONVERSE).
thinktalkscratch
thinkscratchtalk
scratchthinktalk
Concurrency: concurrent execution
Possibili sequenze
di azioni risultanti
da un’alternanza
dei processi.
7
©Magee/Kramer
Composizione parallela - alternanza di azioni
Modello LTS
scratch
think
ITCH
talk
CONVERSE
0
1
0
2 stati
1
2
3 stati
scratch
scratch
think
talk
Descrizione del
“comportamento”
scratch
CONVERSE_ITCH
0
(0,0)
1
(0,1)
2
(0,2)
from
ITCHconcurrent executionfrom CONVERSE
Concurrency:
3
(1,2)
4
talk
5
(1,1)
think
(1,0)
2  3 stati
8
©Magee/Kramer
Composizione parallela - alternanza di azioni
Modello Reti SA
fork
think
think
talk
CONVERSE
scratch
ITCH
scratch
talk
join
CONVERSE-ITCH ?
Concurrency: concurrent execution
9
©Magee/Kramer
Composizione parallela - proprietà algebriche
Commutativa:
Associativa:
Concurrency: concurrent execution
(P||Q) = (Q||P)
(P||(Q||R)) = ((P||Q)||R)
= (P||Q||R).
10
©Magee/Kramer
Modellare l’interazione - azioni condivise
Se due processi che devono essere composti hanno delle
azioni in comune, queste azioni sono dette condivise. Per
mezzo di azioni condivise si modella l’interazione tra
processi. Mentre le azioni non condivise possono essere
alternate in modo arbitrario, un’azione condivisa deve
essere eseguita nello stesso istante da tutti i processi
che vi partecipano
MAKER = (make->ready->MAKER).
USER = (ready->use->USER).
||MAKER_USER = (MAKER || USER).
Concurrency: concurrent execution
MAKER si
sincronizza
con USER
quando
ready.
11
©Magee/Kramer
Modelli
make
LTS
0
use
make
ready
1
2
3
use
use
used
make
make
RETI SA
ready
MAKER
Concurrency: concurrent execution
ready
use
USER
Ready
use
12
©Magee/Kramer
MAKER-USER
labeling di processi
a:P pone il prefisso a ad ogni etichetta di azione
dell’alfabeto del processo P.
Due istanze di un processo “switch”:
SWITCH = (on->off->SWITCH).
||DOPPIO_SWITCH = (a:SWITCH || b:SWITCH).
a.on
b.on
a:SWITCH
b:SWITCH
0
1
a.off
0
1
b.off
Un array di istanze del processo switch :
||SWITCHES(N=3) = (forall[i:1..N] s[i]:SWITCH).
||SWITCHES(N=3) = (s[i:1..N]:SWITCH).
Concurrency: concurrent execution
13
©Magee/Kramer
process labeling by a set of prefix labels
{a1,..,ax}::P sostituisce ogni etichetta n di azione
nell’alfabeto di P con le etichette a1.n,…,ax.n. Inoltre,
ogni transizione (n->X) nella definizione di P è
sostituita dalle transizioni ({a1.n,…,ax.n} ->X).
Il prefisso di processi è utile per modellare risorse condivise:
RISORSA = (riserva->rilascia->RISORSA).
UTENTE = (riserva->usa->rilascia->UTENTE).
||CONDIVISIONE DI RISORSE = (a:UTENTE || b:UTENTE
|| {a,b}::RISORSA).
Concurrency: concurrent execution
14
©Magee/Kramer
Prefissi di processi per risorse condivise
a.acquire
a:riserva
a:UTENTE
a:USER
0
a.use
a:usa
b:riserva
b.acquire
b:UTENTE
b:USER
1
2
0
a.release
a:rilascia
b:usa
b.use
1
2
b:rilascia
b.release
b.acquire
a:riserva
b:riserva
a.acquire
{a,b}::RESOURCE
RISORSA
0
1
a:riserva
a.acquire
b:riserva
b.acquire
b:usa
b.use
a:rilascia
a.release
b:rilascia
b.release
a:usa
a.use
CONDIVISIONE DI
RESOURCE_SHARE
RISORSE
0
1
2
3
4
b:rilascia
b.release
Concurrency: concurrent execution
15
a:rilascia
a.release
©Magee/Kramer
Prefissi di processi per risorse condivise
disponibile
riserva
riserva
non
disponibile
usa
rilascia
disponibile
rilascia



riserva
riserva


usa

rilascia
Concurrency: concurrent execution
non
disponibile
usa
rilascia
16
©Magee/Kramer
relabeling di azioni
Le funzioni di relabeling sono applicate ai processi per
rinominare le azioni. La forma generale di una funzione di
relabeling è la seguente:
/{newlabel_1/oldlabel_1,… newlabel_n/oldlabel_n}.
Queste funzioni assicurano che processi
composti possano essere sincronizzati su
azioni particolari
CLIENT = (call->wait->continue->CLIENT).
SERVER = (request->service->reply->SERVER).
Concurrency: concurrent execution
17
©Magee/Kramer
relabeling di azioni
||CLIENT_SERVER = (CLIENT || SERVER)
/{call/request, reply/wait}.
call
reply
SERVER
CLIENT
0
1
call
0
2
1
call
0
2
reply
continue
CLIENT_SERVER
service
service
1
reply
2
3
continue
Concurrency: concurrent execution
18
©Magee/Kramer
relabeling di azioni
request
call
wait
service
continue
reply
call
service
reply
Concurrency: concurrent execution
continue
19
©Magee/Kramer
relabeling di azioni - etichette prefisso
Una formulazione alternativa del sistema client server è
descritta sotto per mezzo di etichette qualificate o
prefisso :
SERVERv2 = (accept.request
->service->accept.reply->SERVERv2).
CLIENTv2 = (call.request
->call.reply->continue->CLIENTv2).
||CLIENT_SERVERv2 = (CLIENTv2 || SERVERv2)
/{call/accept}.
Concurrency: concurrent execution
20
©Magee/Kramer
hiding di azioni - astrazione per ridurre la complessità
Applicato a un processo P, l’operatore di hiding \{a1..ax}
rimuove i nomi di azioni a1..ax dall’alfabeto di P e rende
queste azioni celate "silenti". Le azioni silenti sono
etichettate tau. Azioni silenti in processi distinti NON
sono condivise.
Talvolta è più appropriato specificare l’insieme di azioni
che devono essere mostrate .... (operatore complementare)
Applicato a un processo P, l’operatore di
interfaccia @{a1..ax} nasconde tutte le
azioni nell’alfabeto di P che NON appaiono
nell’insieme a1..ax.
Concurrency: concurrent execution
21
©Magee/Kramer
Hiding di azioni
Le seguenti definizioni sono equivalenti:
UTENTE = (riserva->usa->rilascia->UTENTE)
\{usa}.
UTENTE = (riserva->usa->rilascia->UTENTE)
@{riserva,rilascia}.
acquire
riserva
tau
usa
0
1
2
La minimizzazione rimuove azioni
tau nascoste per produrre un
LTS con comportamento
osservabile equivalente.
riserva
acquire
release
rilascia
0
1
rilascia
release
Concurrency: concurrent execution
22
©Magee/Kramer
structure diagrams
P
Processo P con
alfabeto {a,b}.
a
b
P
a
c
x
m
c
x
b
d
x
Composizione Parallela
(P||Q) / {m/a,m/b,c/d}
Q
S
x
P
a
Concurrency: concurrent execution
Q
y
Composite process
||S = (P||Q) @ {x,y}
23
©Magee/Kramer