Deriving Specialized Program
Analyses for Certifying
Component- Client Conformance
Elisabetta Bozzo 804279
Claudio Modanese 804278
Prof. : Agostino Cortesi
Indice
 Overview dell’articolo:


Cosa?
Come?
 CMP (Concurrent Modification Problem)
 Processo di certificazione generica
 Processo di astrazione


Staged Abstraction
Specialized Abstraction
 Conclusioni
Elisabetta Bozzo, Claudio Modanese
2
Overview dell’articolo: COSA?
 Problema
certifica/verifica statica di quando un
programma client, risulta conforme ai
vincoli del componente per un corretto uso.
usa
Libreria
usa
Componente
CLIENT

Assicurare che il codice cliente soddisfi i vincoli
imposti dal componente/libreria per garantire un
corretto uso.
Elisabetta Bozzo, Claudio Modanese
3
Overview dell’articolo: COME?

Usando un modello a passi per problemi che fanno parte di una
classe di specifiche (First Order Safety).

Il processo di certificazione prevede i seguenti passi:
1.
2.
3.
Si deriva un’astrazione per modellare lo stato del client;
L’astrazione generata viene incorporata in un motore di
analisi statica per produrre un certificatore;
Il certificatore viene applicato al client per determinare
quando il client viola i vincoli del componente;
Elisabetta Bozzo, Claudio Modanese
4
CMP (Concurrent Modification
Problem)
 Tipico problema di conformità dei vincoli;
 Si sviluppa nel contesto del Java Collections Framework;
 Consiste nel determinare staticamente quanto un client causa
un’eccezione CME (ConcurrentModificationException);
 Una eccezione CME viene lanciata da una componente quando
utilizzando un iteratore oi su una collezione oc.questa viene
modificata attraverso:

iteratori differenti;

un aggiornamento diretto della collezione.
Elisabetta Bozzo, Claudio Modanese
5
Astrazione di programmi come
specifica: linguaggio Easl
 Per la specifica di CMP useremo un linguaggio che traduce le
proprietà FOS in un programma astratto.
 Easl è costituito da:

una restrizione di statement Java (assegnamento, if, while,
allocazione dello heap);

una restrizione di tipi primitivi (booleani e indirizzi di
oggetti);

Built-in Set;

Require statement: descrivono un vincolo che deve essere
soddisfatto in un particolare punto dell’esecuzione;
Elisabetta Bozzo, Claudio Modanese
6
La specifica di CMP
class Version { /* represents distinct versions of a
Set */ }
class Set {
Version ver;
Set() { ver = new Version(); }
boolean add(Object o) { ver = new Version(); }
Iterator iterator() { return new Iterator(this); }
}
class Iterator {
Set set;
Version defVer;
Iterator (Set s){ defVer = s.ver; set = s; }
void remove() {
requires (defVer == set.ver);
set.ver = new Version();
defVer = set.ver;
}
Object next() { requires (defVer == set.ver); }
}

Ogni modifica della collezione
crea una versione distinta
della collezione identificata
dall’oggetto versione;

Ogni iteratore registra quale
versione di quale collezione è
associato ad esso;

Ad ogni uso dell’ iteratore
viene controllata la correttezza
comparando la versione della
collezione definita dall’iteratore
con la versione della
collezione presa in
considerazione.
Elisabetta Bozzo, Claudio Modanese
7
Esempio
/* 0 */ Set v = new Set();
/* 1 */ Iterator i1 = v.iterator();
/* 2 */ Iterator i2 = v.iterator();
/* 3 */ Iterator i3 = i1;
/* 4 */ i1.next();
// The following update via i1 invalidates the
// iterator referred to by i2.
/* 5 */ i1.remove();
/* 6 */ if (...) { i2.next(); /* CME thrown */ }

Come si può vedere dal
codice una CME può essere
lanciata durante l’esecuzione
delle linee 6 e 9, ma non
durante l’esecuzione della
linea 7.

Una analisi che non rileva gli
errori nelle linee 6 e 9 è
// i3 refers to the same, valid, iterator as i1
/* 7 */ if (...) { i3.next(); /* CME not thrown */
}
// The following invalidates all iterators over v
/* 8 */ v.add("...");
unsound.

/* 9 */ if (...) { i1.next(); /* CME thrown */ }
Elisabetta Bozzo, Claudio Modanese
Un report di un possibile
errore nella linea 7
costituisce un falso allarme.
8
Processo di certificazione generica…
Il comportamento delle
componenti è modellato
attraverso uno HEAP
astratto
Perché non usare un’analisi
generica dello heap per
risolvere il CMP?
Elisabetta Bozzo, Claudio Modanese
9
…processo di certificazione generica
 In generale un processo di certificazione generica
è composto dalle seguenti fasi:
1. Creare un programma composto combinando:
a.Il codice cliente;
b.La specifica delle componenti trattandola
come una implementazione della
componente;
2. Applicare un adeguato algoritmo di analisi al
programma composto precedente e verificare che,
quando una clausola “requires” è in esecuzione,
venga valutata a true.
Elisabetta Bozzo, Claudio Modanese
10
Generic Certification for CMP
 Nel caso del CMP potremmo realizzare la clausola 2 utilizzando un
algoritmo per analisi must-alias.
 Prendiamo ad esempio una analisi del tipo “allocation site” che non è in
grado di distinguere oggetti allocati da un programma nello stesso
punto. Una analisi di questo tipo applicata al CMP non è in grado di
certificare se il seguente frammento di codice è privo di errori CMP.
Set s = new HashSet();
while (...) {
s.add(...);
for (Iterator i = s.iterator(); i.hasNext(); ) {
Object o = i.next();
}
}
 L’analisi infatti non è in grado di distinguere tra le differenti versioni di
set s all’interno del loop.
 Quindi non è possibile utilizzare analisi generiche per risolvere il CMP.
Elisabetta Bozzo, Claudio Modanese
11
Staged Certification
 Problema:

 Soluzione:

un’analizzatore generico utilizza
un’astrazione basata su proprietà che non
sono collegate ai vincoli di conformità della
componente.
usare una specifica dei vincoli di conformità
delle componenti per ottenere un’astrazione
specializzata dello stato della componente.
 In questo modo si ottengono certificatori precisi ed efficienti.
Elisabetta Bozzo, Claudio Modanese
12
Caso di analisi: SCMP
 Per illustrare il nostro processo di staged abstraction
utilizzeremo una restrizione del CMP: SCMP.
 SCMP:

riferimenti a collezioni e iteratori sono
contenuti in variabili locali o statiche (non in
campi di un oggetto);

nel client non ci sono chiamate a metodi di
altri client.
Elisabetta Bozzo, Claudio Modanese
13
Processo di astrazione
 Il nostro processo di astrazione consiste di un:

Astrazione dello stato delle componenti: la quale caratterizza
gli aspetti dello stato delle componenti che sono rilevanti per
il processo di certificazione.

Astrazione dei metodi delle componenti: identifica come
l’astrazione dello stato delle componenti viene aggiornata in
seguito alla chiamata di un metodo.
Elisabetta Bozzo, Claudio Modanese
14
Staged Certification: ottenere
l’astrazione dello stato
 Lo stato viene rappresentato attraverso predicati strumentali .
 I predicati strumentali vengono generati iterando una
computazione simbolica e backward weakest-precondition su
ogni possibile sequenza di chiamate di metodi secondo le
seguenti regole:
 Se ogni metodo ha una clausola requires φ all’entrata del
metodo allora ¬ φ è una possibile formula strumentale;
 Se φ1 OR … OR φk è una possibile forma strumentale (dove
nessuna delle φi è una disgiunzione della forma α OR β )
allora ogni φi è un possibile predicato strumentale;
 Se φ è un possibile predicato strumentale e S è il corpo di
un metodo allora la weakest precondition di φ rispetto a S,
WP (S, φ) è una possibile formula strumentale.
Elisabetta Bozzo, Claudio Modanese
15
Esempio: astrazione dello stato delle
componenti per CMP
 Step 1: determinare ad ogni
chiamata ai metodi
 Iterator::next()
 Iterator::remove()
 se la precondizione del metodo
è vera o falsa
(i.defver != i.set.ver)
Stalei=true
Iterator::next()
Iterator::remove()
CME
TRUE
FALSE
 Stalei ≡ i.defver != i.set.ver;
Elisabetta Bozzo, Claudio Modanese
16
Esempio: astrazione dello stato delle
componenti per CMP
 Step 2: Consideriamo come
l’esecuzione di differenti
metodi di set e iterator
modificano il valore del
predicato stalei
 Esempio v.add()
 stalei è vero dopo
l’esecuzione di
v.add() sse la
condizione stalei ||
(i.set==v ) è vera
prima dell’esecuzione
dell’istruzione;
 Iterofi,v ≡ i.set = v
Elisabetta Bozzo, Claudio Modanese
(Stalei|| (i.set==v))=true
v.add()
Stalei=true
17
Esempio: astrazione dello stato delle
componenti per CMP
 Step 3: considerare gli effetti dell’
esecuzione di j.remove() (con j
iteratore) sul predicato stalei . Si
può verificare che stalei è vero
dopo l’esecuzione di j.remove()
sse stalei || ((i.set == j.set) && (i !=
j)) è vera prima dell’esecuzione
dell’istruzione.
(Stalei||
(i.set==j.set)&&(i!=j))=true
j.remove()
Stalei=true
 Mutxi,j ≡ (i.set == j.set) && (i != j)
Elisabetta Bozzo, Claudio Modanese
18
Esempio: astrazione dello stato delle
componenti per CMP
 Step 4: si può verificare
che Iterofi,v è vero dopo
l’esecuzione di i=
w.iterator sse v == w
prima dell’esecuzione
dell’istruzione.
v=w
i=w.iterator()
Iterofi,v=true
 Samev,w ≡ v == w
Elisabetta Bozzo, Claudio Modanese
19
Raggiungimento del punto fisso
 Quando applicando le regole per identificare i
predicati strumentali non vengono prodotti ulteriori
predicati
PUNTO FISSO
Elisabetta Bozzo, Claudio Modanese
20
Come ottenere l’astrazione dei
metodi delle componenti
 Ogni metodo astratto definisce come la
chiamata a quel metodo cambia i valori
dei predicati strumentali, compreso
l’astrazione dello stato
 L’astrazione del metodo M consiste in
una formula di aggiornamento per ogni
predicato strumentale che viene visto
come una precondizione per il metodo
Elisabetta Bozzo, Claudio Modanese
21
Astrazione dei metodi per CMP
 Ogni chiamata a
funzione del codice
cliente (colonna a sx)
viene rimpiazzato dalla
corrispondente
astrazione del metodo
(colonna a dx).
Elisabetta Bozzo, Claudio Modanese
22
Specialized Certification
 Come si utilizzano le componenti e
l’astrazione dei metodi nella certificazione di
un client?
 Step 1: trasformazione
 sostituire le variabili nel programma con
delle variabili booleane corrispondenti ai
predicati strumentali identificati;
 sostituire le chiamate ai metodi con una
corrispondente istanza dell’astrazione del
metodo.
Elisabetta Bozzo, Claudio Modanese
23
Specialized Certification: esempio
// variables representing values of nullary predicate abstraction
// used for certification
boolean stalei1, stalei2, stalei3;
boolean iterof i1,v, iterof i2,v, iterof i3,v;
boolean mutxi1,i1, mutxi1,i2, mutxi1,i3, mutxi2,i1, mutxi2,i2;
boolean mutxi2,i3, mutxi3,i1, mutxi3,i2, mutxi3,i3;
boolean samev,v;
...
// 0: Set v = new Set();
samev,v := 1;
iterof i1,v := 0;
iterof i2,v := 0;
iterof i3,v := 0;
// 1: Iterator i1 = v.iterator();
iterof i1,v := samev,v;
mutxi1,i1 := 0;
mutxi1,i3 := iterof i3,v; mutxi3,i1 := iterof i3,v;
mutxi1,i2 := iterof i2,v; mutxi2,i1 := iterof i2,v;
stalei1 := 0;
// 2: Iterator i2 = v.iterator();
iterof i2,v := samev,v;
mutxi2,i2 := 0;
mutxi2,i1 := iterof i1,v; mutxi1,i2 := iterof i1,v;
mutxi2,i3 := iterof i3,v; mutxi3,i2 := iterof i3,v;
stalei2 := 0;
...
// 5: i1.remove();
requires ￢stalei1; //requires statement is satisfied
stalei1 := stalei1 ∨ mutxi1,i1;
stalei2 := stalei2 ∨ mutxi2,i1; // stalei2 becomes 1
stalei3 := stalei3 ∨ mutxi3,i1;
.
 Le dichiarazioni delle
variabili Iterator e Set sono
state sostituite con
l’astrazione dei metodi e
degli stati della componente
(vedi tabella precedente)
 Notiamo la trasformazione
dell’istruzione 5:


La clausola requires
che controlla la
validità dell’iteratore
i1 è soddisfatta.
il valore della
variabile stalei2
diventa 1
Elisabetta Bozzo, Claudio Modanese
24
Specialized Certification
 Step 2: analizzare il programma trasformato
per determinare i possibili valori delle variabili
booleane presenti nelle clausole requires.
 La soluzione di questo problema può essere
calcolata in un tempo O(EB2):


B rappresenta il numero delle variabili iteratore
e collezione nel programma originale;
E rappresenta il numero di archi (edge) nel
grafico control-flow del programma;
Elisabetta Bozzo, Claudio Modanese
25
Specialized vs. Generic
Abstraction
 Le figure a lato descrivono
Stato concreto prima dell’esecuzione di i1.remove()
lo stato concreto del
programma prima e dopo
l’esecuzione di i1.remove()
 Come si può notare dopo
l’esecuzione dell’istruzione si
creano due versioni della
collezione:


i1 riferisce alla nuova
versione o5
i2 continua a riferirsi
alla vecchia versione
Stato concreto dopo l’esecuzione di i1.remove()
Elisabetta Bozzo, Claudio Modanese
26
Specialized vs. Generic
Abstraction



Stato astratto dopo l’esecuzione di i1.remove()


Questa figura rappresenta lo stato
astratto dopo l’esecuzione
dell’istruzione i1.remove()
I due nodi concreti dei due oggetti
versione o4,o5 vengono uniti perché
non ci sono variabili puntatore che
puntano a uno degli oggetti
Abbiamo in questo modo perdita di
informazione.
Nello stato astratto si ha che i1, i2 e
i3 possono essere validi o invalidi.
In tabella viene evidenziato come
variano gli stati prima e dopo
l’esecuzione dell’istruzione:

Stalei2 diventa 1 perché la versione
della collezione di i2 è diversa dalla
collezione corrente
Elisabetta Bozzo, Claudio Modanese
27
Il processo di derivazione: alcuni
dettagli
 Ogni imprecisione del certificatore che usa
l’astrazione della componente è causata
dall’imprecisione dell’astrazione degli stati del client;
 In generale non ci sono garanzie che il processo di
derivazione termini
non c’è il limite al numero
dei predicati strumentali generati da questa
procedura.
 Soluzione
uso di euristiche per fermare la
generazione di nuovi predicati strumentali le quali
verificano se quelli nuovi sono equivalenti a quelli già
generati.
Elisabetta Bozzo, Claudio Modanese
28
Relazione con l’astrazione dei
predicati
 L’approccio descritto è strettamente legato al concetto di
astrazione dei predicati.
 Astrazione dei predicati: termine utilizzato in letteratura per
rappresentare:

Lo stato dei programmi: attraverso una collezione di variabili
booleane

Le istruzioni dei programmi: attraverso altre istruzioni che si
riferiscono solo alle variabili booleane rappresentanti gli
stati.
Elisabetta Bozzo, Claudio Modanese
29
Relazione con l’astrazione dei
predicati
 L’algoritmo che permette di scoprire i predicati
necessari alla determinazione dell’astrazione viene
applicato ad una specifica di componente utilizzando
una astrazione di predicati. Questo permette di:
 Analizzare la specifica della componente prima
che un programma client sia disponibile;
 Riutilizzare i risultati ottenuti per verificare altri
programmi.



+ modularità
+ scalabilità
- analisi simboliche (molto costose) per l’analisi del
programma client
Elisabetta Bozzo, Claudio Modanese
30
…Conclusioni…
 Arrivati a questo punto è possibile estendere
la generazione delle astrazioni delle
componenti effettuata non solo al problema
dell’SCMP (che abbiamo utilizzato per ridurre
il problema ad un sotto-problema più
semplice da trattare) ma ad una classe di
problemi più complessi.
Elisabetta Bozzo, Claudio Modanese
31
…Conclusioni…
 Per questo scopo abbiamo bisogno di un linguaggio
più espressivo di EASL: TVP



imperativo;
costruito attorno a un sotto-linguaggio basato sulla logica del
primo ordine.
L’unico tipo di variabile permessa è la variabile predicato.
 E un sistema per l’interpretazione astratta  TVLA.
TVLA
TVP
Elisabetta Bozzo, Claudio Modanese
32
…Conclusioni
 L’analisi che abbiamo visto si è dimostrata
abbastanza veloce e precisa.
 Attualmente si sta studiando un modo per:



Allargare la classe di problemi a cui è
possibile applicare l’approccio descritto
Migliorare il partizionamento delle parti del
programma irrilevanti per la componente
Migliorare la rappresentazione delle strutture del
primo ordine
Elisabetta Bozzo, Claudio Modanese
33