Laurea Specialistica in Informatica
Analisi e Verifica dei Programmi
docente: prof. Cortesi Agostino
ANALISI DEI RUOLI
Visentini Diego mat.814702
De Martin Andrea mat. 810091
AA 2006/2007
Analisi dei Ruoli
1
OBIETTIVI

Nuovo “sistema di Ruoli”

Funzionalità dei ruoli

Algoritmi che implementano varie analisi dei ruoli
AA 2006/2007
Analisi dei Ruoli
2
EXCURSUS

Introduzione generale

Definizione e Proprietà dei ruoli

Modello di programmazione

Analisi intraprocedurale

Analisi interprocedurale

Estensioni del sistema di ruoli

Lavoro correlato

Conclusioni
AA 2006/2007
Analisi dei Ruoli
3
TIPO vs RUOLO



Tipo di una variabile: int, bool, float, ecc…
Ruolo: estensione del concetto di tipo inteso come relazione di
referenza tra oggetti; incrementa sia sicurezza che leggibilità del
programma
Esempio ideologico, non basato su codice, che chiarisce la
distinzione tra ruolo e tipo:
Carta Postepay


Il tipo dell’oggetto è “carta ricaricabile”
Il ruolo dipende dall’ambito in cui viene usata:


AA 2006/2007
carta di credito in operazioni di acquisto su internet con Paypal
Bancomat allo sportello delle poste
Analisi dei Ruoli
4
INTRODUZIONE (1)



Sistemi di ruoli tradizionali mantengono proprietà
“invarianti”, finchè l’oggetto esiste
Ruoli di un oggetto cambiano a seconda di come
cambiano i valori memorizzati nei propri campi oppure
mentre i programmi invocano operazioni su tale oggetto
Soluzione: integrazione tra cambiamento di stati e
sistema di ruoli
AA 2006/2007
Analisi dei Ruoli
5
INTRODUZIONE (2)

Role Concept: lo stato di un oggetto dipende dalle sue

Linguaggio per definire un ruolo: per esprimere invarianti

Modello di Programmazione: set di regole che

Linguaggio delle specifiche per l’interfaccia procedurale:

Algoritmi di analisi dei ruoli: controllano se i vincoli
relazioni di referenza con gli altri oggetti
e strutture dati
permettono o meno la violazione dei vincoli
contesto iniziale ed effetti su procedure
vengono violati e in questo caso controllano se la regola
applicata ne consentiva la violazione
AA 2006/2007
Analisi dei Ruoli
6
ESEMPIO
Diagramma delle referenze dei ruoli per un process scheduler
AA 2006/2007
Analisi dei Ruoli
7
DEFINIZIONE DEI RUOLI (1)
Esempio di definizione dei ruoli del grafo precedente scritto in pseudocodice
Ruolo dei processi in
esecuzione: notare il vincolo
acyclic
Ruolo dei processi in
esecuzione: notare il
vincolo identities
AA 2006/2007
Analisi dei Ruoli
8
DEFINIZIONE DEI RUOLI (2)

Vincoli di identità

Vincoli di aciclicità

Nell’esempio: il vincolo di identità next.prev nel ruolo
RunningProc specifica il vincolo della lista ciclica
doppiamente linkata che segue il next, poi il campo
prev riconduce sempre all’oggetto iniziale. Il vincolo
aciclico left e il right nel ruolo SleepingProc specifica
che non ci sono cicli nello heap inglobando solo gli archi
left e right. Dall’altro lato, la lista dei processi attivi
deve essere ciclica, perché i suoi nodi non possono mai
puntare a null
AA 2006/2007
Analisi dei Ruoli
9
PROPRIETA’ DEI RUOLI

Proprietà di consistenza: i ruoli sono in grado di assicurare
che il programma rispetti le proprietà di consistenza della struttura
dati a livello applicazione. I ruoli nel nostro process scheduler, per
esempio, assicurano che un processo non può essere
contemporaneamente attivo e sleeping

Modifiche dell’ interfaccia:
l’interfaccia cambia mentre
cambiano le sue relazioni di referenza

Relazioni correlate:
gruppi di oggetti cooperano per
implementare una parte di una funzionalità
AA 2006/2007
Analisi dei Ruoli
10
SINTASSI E SEMANTICA DEI RUOLI (1)

Rappresentazione di uno Heap:

grafo HC

oggetti nodes(HC)

archi (O1, ƒ,O2) є HC
AA 2006/2007
Analisi dei Ruoli
11
SINTASSI E SEMANTICA DEI RUOLI (2)

R set usati nelle definizioni di ruoli

nullR, nullc, R0=R U{nullR}

Ogni ruolo è rappresentato come la congiunzione di 4
vincoli:




Campi:per ogni campo c è associata una funzione
fieldƒ(): R 2R0
Slots: slotno(r): un oggetto di ruolo r può avere un numero di
alias pari a slot(r)
Identità: identities(r) C ƒ є F. Le identità sono coppie di campi
(ƒ,g) dove ogni referenza ƒ su un oggetto o poi ritorna su
referenze g che portano nuovamente ad o
Aciclicità:setAcyclic(r) C ƒ di campi lungo la quale i cicli sono
proibiti
AA 2006/2007
Analisi dei Ruoli
12
SINTASSI E SEMANTICA DEI RUOLI (3)

REFERENCE ROLE DIAGRAM

DEFINIZIONE FORMALE:
RRD={(r,ƒ, r’) | r’ є fieldƒ (r) e эi (r,ƒ) є sloti (r’ )} U {(r,ƒ, nullR)\ nullR є fieldƒ (r) }

Come si può notare, cattura alcuni ma non tutti i tipi di
vincoli definiti in precedenza
AA 2006/2007
Analisi dei Ruoli
13
MODELLO DI PROGRAMMAZIONE (1)



1.
2.
Scopo di questa tecnica: violare temporaneamente i vincoli
durante la modifica di strutture dati
Linguaggio imperativo (ogni programma è un insieme di
procedure proc) con allocazione di oggetti dinamica
Oggetti onstage e offstage nello heap
onstage(Hc) : referenziato da una variabile locale o da un
parametro di qualche attivazione di record
offstage(Hc) : mai referenziati da variabili locali o parametri
AA 2006/2007
Analisi dei Ruoli
14
MODELLO DI PROGRAMMAZIONE (2)

Consistenza locale

Consistenza dei nodi offstage e onstage

Consistenza rimozione referenze

Consistenza chiamate a procedura
AA 2006/2007
Analisi dei Ruoli
15
ANALISI INTRAPROCEDURALE DEI RUOLI

Rappresentazione grafica (Heap,nodi, archi)

Algoritmo: generare casualmente più nodi offstage


Scopo: Verificare che oggetti che hanno lo stesso ruolo
ma sono rappresentati da nodi offstage diversi, hanno
diversa raggiungibilità
Verifica globale tramite verifica progressiva di nodi che
passano a offstage
AA 2006/2007
Analisi dei Ruoli
16
ANALISI INTERPROCEDURALE DEI RUOLI
Approssimiamo la funzione di trasferimento nelle semantiche concrete
con interfacce procedurali consistenti in:
1.
un contesto iniziale
2.
un insieme di effetti
Assumiamo che queste interfacce procedurali siano concepite:
1.
2.
verificando che approssimino in modo sommario il comportamento
della procedura
istanziando le interfacce di procedura ai call sites
AA 2006/2007
Analisi dei Ruoli
17
INTERFACCE DI PROCEDURA (1)
CONTESTO INIZIALE
Il grafo di tipo iniziale assegna:

un insieme di heaps concreti ai campi della
procedura

i nomi per gli insiemi di oggetti in questi heaps
Denotiamo il grafo di ruolo iniziale come <HIC, ρIC, KIC>
Il grafo di tipo iniziale potrebbe contenere due tipi di
archi:

arco di parametro p  pn è interpretato come
<proc, p, pn>  HIC

arco di albero n - f  m denota un arco <n,f,m>
 HIC
ARCHI DI
PARAMETRO
ARCHI DI
NODO
NODO
DICHIARATO ANONIMO ALBERO
Chiamiamo i nodi dell’RRD (contenuto nel grafo di ruolo
iniziale) nodi anonimi
AA 2006/2007
Analisi dei Ruoli
18
INTERFACCE DI PROCEDURA(2)
EFFETTI DI PROCEDURA
Gli effetti di procedura:

approssimano conservativamente la zona dell’heap dove accede la
procedura

indicano cambiamenti alle relazioni di riferimento all’interno di questa zona
Ci sono due tipi di effetti:

quelli di lettura: specificano un set read(proc) di nodi del grafo di ruolo
iniziale a cui ha accesso la procedura; sono usati per assicurare che la
condizione di accessibilità sia soddisfatta

quelli di scrittura: nella forma e1.f=e2 raccoglie l’effetto di operazioni
store all’interno della chiamata; e1 denota gli oggetti scritti, f il campo
scritto e e2 gli oggetti i cui riferimenti sono scritti nel campo
AA 2006/2007
Analisi dei Ruoli
19
VERIFICA DELLE INTERFACCE
DI PROCEDURA(1)
Per verificare gli effetti ampliamo la rappresentazione dell’analisi <H,ρ,K>.

H è l’heap astratto che rappresenta gli oggetti

ρ è un assegnamento di ruolo astratto

K indica il tipo di ogni nodo
Un grafo di tipo non-error e’ ora una tupla <H,ρ,K,,E> dove:


 : nodes(H)nodes0(HIC) e’ una trasformazione di contesto iniziale
che assegna un grafo di tipo iniziale (n)  nodes(HIC) per ogni nodo n
rappresentante un oggetto che esiste a priori verso la chiamata di
procedura. Esso assegna anche NEW ad ogni nodo rappresentante un
oggetto creato durante l’esecuzione della procedura
E UimustWri(proc) e’ una lista di effetti must write che la procedura
ha performato finora
AA 2006/2007
Analisi dei Ruoli
20
VERIFICA DELLE INTERFACCE
DI PROCEDURA(2)
GRAFI DI RUOLO ALLE ENTRY DI PROCEDURA
La nostra analisi dei ruoli:
 crea l’insieme dei grafi di ruolo alle entry di procedura dal grafo di
ruolo iniziale context(proc).
 istanzia quindi i nodi nel grafo di ruolo iniziale per creare un set di
grafici di ruolo ( La figura qui sotto descrive questo processo )
L’analisi:
• prima seleziona un parametro arco per
ogni parametro
• poi usa il parametro di espansione di
relazione  per istanziare e dividere il
nodo referenziato
AA 2006/2007
Analisi dei Ruoli
21
VERIFICA DELLE INTERFACCE
DI PROCEDURA(3)
VERIFICA DELLE ASSERZIONI BASE
Per assicurare che una procedura sia conforme alla sua interfaccia, l’analisi usa
la mappa  per assegnare ogni asserzione di Load e Store ad un effetto
dichiarato
L’esecuzione simbolica di una clausola di Load x=y.f

rende certo che il Load e’ registrato in qualche effetto letto

se il caso non e’ questo, viene riportato un errore
L’esecuzione simbolica della clausola di Store x.f=y

prima reperisce i nodi (nx) e (ny) del grafo di ruolo iniziale che
corrispondono ai nodi nx e ny nel grafo di ruolo corrente

se l’effetto < (nx),f, (ny) > e’ dichiarato come un effetto di possibile
scrittura, l’esecuzione procede come al solito

altrimenti, l’effetto e’ usato per aggiornare la lista E degli effetti must-write
AA 2006/2007
Analisi dei Ruoli
22
VERIFICA DELLE INTERFACCE
DI PROCEDURA(4)
VERIFICA DELLE POSTCONDIZIONI DI PROCEDURA
Alla fine della procedura, l’analisi:


attua una verifica di nodo su tutti i nodi in stato usando il predicato
nodeCheck(n,<H, ρ, K>, nodes(H)) per tutti i nodi nonstage(H).
verifica anche che ogni effetto apportato in E può essere attribuito ad un
esatto must-effect dichiarato.
AA 2006/2007
Analisi dei Ruoli
23
ANALISI DEI CALL SITES(1)
L’analisi aggiorna l’insieme dei grafi di ruolo dei siti alla chiamata di procedura
basati sulle interfacce del chiamato e considera una procedura proc
come un call site nella forma proc’(x1,……,xp)
La computazione della funzione di trasferimento per un call sites ha le
seguenti fasi:

Parameter check

Context Matching ( matchContext )

Effect Instantiation (FX)

Role Reconstruction(RR)
AA 2006/2007
Analisi dei Ruoli
24
ANALISI DEI CALL SITES(2)
PARAMETER CHECK
assicura che i ruoli dei parametri siano conformi ai ruoli attesi dalla chiamata
proc’ richiedendo nodeCheck(ni, G, offstage(H{nj}j) per ogni nodo
di parametro ni
CONTEXT MATCHING
assicura che i grafi di ruolo chiamati rappresentino un sottoinsieme dell’albero
concreto rappresentato da <HIC, ρIC, KIC> derivando un mapping  dal
grafo di ruolo chiamato ai nodi (HIC).
AA 2006/2007
Analisi dei Ruoli
25
ANALISI DEI CALL SITES(3)
EFFECT INSTANTIATION
usa mayWr(proc’) e mustWri(proc’) per approssimare tutti i cambiamenti al
grafo di ruolo che proc’ può effettuare
ROLE RECONSTRUCTION
usa ruoli finali per i nodi di parametro, postRi(proc’), combinata con le
definizioni di ruolo globali, per ricostruire i ruoli di ogni nodo nella parte del
grafo di ruolo che rappresenta la regione modifica dell’heap
AA 2006/2007
Analisi dei Ruoli
26
ESTENSIONI DEL SISTEMA DI
RUOLO BASE(1)
CAMBIAMENTI DI RUOLO A CASCATA
Noi usiamo la clausola setRoleCascade(x1:r1,……..,xn:rn) per effettuare un
cambiamento di ruolo a cascata su di un insieme di oggetti
Dato un grafo di ruolo <H,ρ,K,E>, un cambio di ruolo a cascata:

trova un nuovo valido assegnamento di ruolo ρ‘ nel quale l’oggetto in stato
ha i ruoli desiderati

i ruoli degli oggetti fuori stato sono aggiustati in modo appropriato
Ogni soluzione che soddisfa le costrizioni deve rispettare la semantica originale
AA 2006/2007
Analisi dei Ruoli
27
ESTENSIONI DEL SISTEMA DI
RUOLO BASE(2)
RUOLI SIMULTANEI
Questa definizione di albero specifica
che una struttura dati è un albero
con costrizioni sui campi left e
right
AA 2006/2007
Similarmente, la definizione di una
lista linkata specifica costrizioni solo
per il campo next
Analisi dei Ruoli
28
ESTENSIONI DEL SISTEMA DI
RUOLO BASE(3)
Possiamo combinare l’albero ed i tipi di lista per ottenere un tipo ad albero
threaded:
• Definizioni di ruolo per ruoli simultanei possono usare precedenti
definizioni di ruolo tramite la parola chiave extends
• Le relazioni extends sono date dall’insieme di ruoli subroles(r) per
ogni ruolo r
AA 2006/2007
Analisi dei Ruoli
29
LAVORO CORRELATO
Approcci typestate proposti recentemente usano ruoli lineari per collegamenti
ad heap per supportare i cambi di stato degli oggetti allocati
dinamicamente.
I ricercatori hanno:



sviluppato approcci typestate per verificare le proprietà di salvaguardia di
programmi di linguaggio assembly
sviluppato sistemi che usano estensioni di ruoli lineari che evitino la
pseudonimia generale e conti sul design del linguaggio per evitare
l’inferenza di tipo non locale
adottato un approccio constraint-based che caratterizza le strutture dati in
termini delle costrizioni che devono essere soddisfatte
AA 2006/2007
Analisi dei Ruoli
30
CONFRONTO
La nostra analisi:





ha un approccio constraint-based che caratterizza le strutture dati in
termini delle costrizioni che devono essere soddisfatte
è incentrata sull’aspetto globale come ad esempio la partecipazione
di oggetti in strutture dati multipli
usa un meno preciso ma più scalabile trattamento di procedure
usa un approccio composizionale che analizza ogni procedura da
sola per verificare che sia conforme alla sua interfaccia
traccia molte più informazioni dettagliate riguardo l’heap
AA 2006/2007
Analisi dei Ruoli
31
CONCLUSIONI
Questa analisi dei ruoli propone 2 idee chiave:

le relazioni di aliasing potrebbero determinare, in parte, il ruolo di ogni
oggetto

il sistema di ruolo dovrebbe usare l’oggetto risultante come sua astrazione
fondamentale per descrivere le interfacce di procedura e le relazioni di
riferimento degli oggetti
ed un algoritmo di analisi che può verificare che il programma rispetti
correttamente i vincoli di ruolo
I programmatori possono usare i ruoli per una varietà di utilizzi:

per assicurare la correttezza dell’interfaccia di procedura estesa che prende
i ruoli dei parametri negli account

per verificare importanti proprietà della consistenza delle strutture dati

per esprimere come le procedure muovono oggetti tra strutture dati

per controllare che il programma implementi correttamente le relazioni
correlate tra gli stati di oggetti multipli
Ci aspettiamo perciò che i ruoli migliorino l'affidabilità del programma e la sua
trasparenza a sviluppatori e manutentori.
AA 2006/2007
Analisi dei Ruoli
32
RIFERIMENTI(1)
[1] A. Albano, R. Bergamini, G. Ghelli and R. Orsini. An introduction to
database programming language Fibonacci. The VLDB journal, 4(3), 1995
[2] Craig Chambers. Predicate Classes. In proceedings of the 7° European
Conference on Object-Oriented Programming, pages 268-296, 1993
[3] S. Drossopoulou, F. Damiani, M. Dezani-Ciancaglini, and P. Giannini. Fickle:
Dynamic objet re-classification. In proceedings of the 15° European
Conference on Object-Oriented Programming, LNCS 2072, pages 130-149.
Springer, 2001.
[4] Rakesh Ghiya and Laurie J. Hendren. Connection analysis: A practical
interprocedural heap analysis for C. In Proceedings of the 8° Workshop on
Languages and Compilers for Parallel Computing, 1995.
[5] Laurie J. Hendren, Josep Hummel, and Alexsandru Nicolau. A general data
dependence test for dynamic, pointer-based data structures. In Proceedings
of the SIGPLAN’94 Conference on Programming Language Design and
Implementation, 1994.
AA 2006/2007
Analisi dei Ruoli
33
RIFERIMENTI(2)
[6] Jacob J. Jensen, Michael E. Joergensen, Nils Klarlund, and Michael I.
Schwartzbach. Automatic verification of pointer programs using monadic
second order logic. In Proceedings of the SIGPLAN’94 Conference on
Programming Language Design and Implementation, Las Vegas, NV, 1997.
[7] Victor Kunkak. Designing an algorithm for role analysis. Master’s thesis,
Massachusetts Institute of Tecnology, 2001.
[8] Trygve Reenskaug. Working with Objects. Prentice Hall, 1996.
[9] Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric Shape
Analysis via 3-valued logic. In Proceeding of the 26° Annual ACM
Symposium on the Principles of Programming Languages, 1999.
[10] Wolfgang Thomas. Languages, automata, and logic. In Handbook of
Formal Languages Vol.3: Beyond Words. Springer-Verlag, 1997.
AA 2006/2007
Analisi dei Ruoli
34