Numerical Power
Analysis
Anna Achilli
Diego Bellantuono
Excursus
Introduzione alla NPA
Classe di domini P(B,E)
P(B,E) come reticolo completo: astrazione di (B )
Proprietà: ACC, Elementi Meet-Irriducible
Combinazione con altri domini astratti
Calcolo della semantica astratta e concreta in esempi
pratici
Il problema di Collatz e sua risoluzione tramite l’NPA
Programmi in linguaggio PCCP
Osservazioni conclusive.
2
Introduzione alla NPA
NPA è la Power Analysis di valori numerici
interi o razionali.
La Power Analysis è un strumento importante
per prevedere risultati statistici significativi in
un determinato esperimento scientifico prima
che l’esperimento sia effettuato
Come funziona la PA:
E’ necessario avere in mente una ipotesi
alternativa a quella che si vuole dimostrare
Utilizzata in particolare assieme ai metodi
statistici
3
Power Analisys: Esempio
Scopo: Effettuare un Sondaggio di Marketing
Sia π ( chiamato parametro di interesse )la porzione
di persone favorevoli all’oggetto del sondaggio
E’ interrogato un campione casuale di persone. Sia N
questo campione:
generalmente N sarà un valore molto piccolo rispetto
alla popolazione in generale. Il calcolo delle persone
interrogate è una statistica chiamata P.
Già prima di eseguire lo studio si sa che P π
di una quantità chiamata errore di campionamento
La PA è utilizzata per rispondere a domande relative
a velocità, semplicità, accuratezza ( dimensione
del campione per minimizzare l’errore )
4
Alternative alla PA:
Intervalli di confidenza
In alternativa alla PA, esiste un approccio
basato su intervalli di confidenza.
se lo scopo è solo di illustrare i risultati è
sufficiente questa tecnica,
se invece si vuole approfondire uno studio è
più utile la PA
5
Scopo: Costruire domini astratti
Progettare domini astratti per l’analisi delle potenze
numeriche
Questi domini
sono dimostrati corretti nel framework adjoint
dell’interpretazione astratta
Il progettista di domini è facilitato a dimostrare la
correttezza e l‘ottimalità dell’analisi
Altre proprietà rilevanti:
Possono avere infinite catene discendenti ma soddisfano
l’ACC ( “Ascending Chain Condition” )
Non sono permesse infinite catene ascendenti
Importante nell’analisi statica perché dimostra che
non ci possono essere cicli infiniti nella semantica
astratta
Domini visti come reticoli con elementi meet-irriducible
6
Analisi
Consideriamo la nostra analisi come la soluzione di un sistema
di equazioni di punti fissi associate alla semantica concreta del
programma
Ogni equazione è interpretata nel dominio astratto che
restituisce una trasformazione approssimata
dell’invarianza del programma in ogni suo punto
Perché questa analisi sia effettiva
La soluzione iterativa del sistema di equazioni approssimato
deve terminare.
Condizione di terminazione raggiunta
Staticamente disegnando domini astratti senza catene
ascendenti
Dinamicamente calcolando i punti fissi tramite operazioni di
widening/narrowing per velocizzare la convergenza
7
Domini e proprietà
Questi domini sono ideati per scoprire
proprietà del tipo:
la variabile x, con x N , Z ,
è la potenza numerica di c k ,
con k che gode della
proprietà :
c
proprietà di n i
dove c, sono
determinat e automatica mente
Esempio
PROBLEMA DI COLLATZ: applicando la NPA a questo
problema è possibile individuare automaticamente delle
proprietà
8
Campi di applicazione
Combinazione di domini
NPA è molto utile se combinata con altre tecniche di analisi di valori
numerici
Analisi di Congruenza di Granger, Interval Analysis
La combinazione avviene tramite ad esempio
Prodotto ridotto
Studiato per superare le limitazioni del prodotto diretto ( è il dominio
ottenuto dal prodotto cartesiano dei due domini astratti )
Mancanza di precisione perché manca l’interazione tra le
componenti
Prodotto cartesiano + riduzione ( processo che trasforma una GC una
GI )
Prodotto di Granger
Definisce due nuove operazioni sul prodotto cartesiano dei domini, che
riducono rispettivamente ogni componente
Vantaggi
Costruzione di analisi più sofisticate
Riutilizzo di implementazioni esistenti
9
Campi di Applicazione
Probabilistic Concurrent Constraint Program
NPA usata nell’analisi statica di linguaggi di
programmazione probabilistica a scelta casuale
Si è la traccia di stati intermedi con probabilità Pi 0,1
dove
s0 , p0 ... si , pi
pstato f inale pi
i
pstato f inale spesso è la potenza numerica di una frazione
NPA approssima in modo accurato prodotti razionali
Posso usare NPA per approssimare la probabilità
risultante in computazioni casuali
Caso studio: programmi in linguaggio PCCP
10
Il dominio delle potenze numeriche
Consideriamo tipi numerici standard:
Naturali, Interi, Razionali
Identifichiamo gli elementi utili alla nostra analisi
come collezioni di insiemi ognuno dei quali
contiene potenze numeriche di un particolare
valore intero o razionale
base B Ζ, Q, l' esponente E E x ( X ) | X N , Z ,
a B, X E : si definiscon o X - POWERS ax a k | k X
11
Il dominio concreto
Le variabili assumono valore in Z o Q, quindi i
possibili valori che assumono durante l’esecuzione
del programma appartengono al (Z ) o al(Q)
( X ), , Z ,0,, con X Z , Q
è un reticolo booleano che rappresenta il dominio
concreto dell’interpretazione
Un reticolo booleano è un reticolo distributivo
complementato
12
Classe di domini con X-Powers
Introduciamo la classe di domini che include tutte le X-
Powers di valori interi o razionali
P( B, E ) , B a | a B and X E
X
con la condizione che se E E
allora B Q
In P( B, E ) consideriamo all’inizio solo insiemi di potenze di
Z
elementi atomici e poi assegnamo i risultati ottenuti alla
stessa P( B, E )
Atomo esponenziale di A ( a ) è il più piccolo elemento b X
tale che a b k con k N e X N , Z , Q e a X
a è atomico se a a allora a a con X E , a B , k N ,
In particolare quando B Q e E E lavoriamo solo con
insiemi di potenze con valori maggiori di 1 e quindi
possiamo estendere i risultati agli insiemi delle potenze di
tutti i valori razionali
0
X
kX
Z
13
Domino delle potenze degli interi
Dominio delle potenze degli interi
14
Analisi della Base
Introduciamo due domini astratti:
X N , Z
P( B, X ) con
P( B, X ) formano RETICOLI COMPLETI:
PB, X è un RETICOLO
Definire lub e glb
PB, X è un reticolo COMPLETO
GI tra (B ) e PB, X
Consideriamo domini EXPONENTIAL-CLOSED
Proprietà: ACC e elementi MEET-IRRIDUCIBLE
PB, X è un’ASTRAZIONE DI (B )
PB, X è una MOORE – FAMILY
15
Fase 1:dimostrazione RETICOLO
Individuiamo Least Upper Bound - lub (e Greatest Lower Bound
- glb)
k
h
Sia a, b B tale che a a , b b con k , h N
Consideriamo X N , Z
gcd(k , h ) X
d
se a b d
X
X
a b
B
altrimenti
Idea della dimostrazione:
a b d
Caso
Visto che a ak , b bh
allora ak bh d gcd(k ,h )
X
Quindi sappiamo che aX , bX d gcd(k ,h)
Dimostriamo che
d gcd(k ,h) X è contenuto nell’insieme c
X
X
X
con c a , b
e cB
X
16
Fase 1: dimostrazione RETICOLO
In altri termini d gcd(k ,h ) cX d gcd(k ,h)
X
Se a b d
, aX bX d lcm( k ,h)
Sappiamo che d è atomico ( d = d ) e c d
Quindi l’intersezione esiste
X
X
Per dimostrarlo considero e
tale che
X
X
a, b d gcd(k , h ) c eX
con c B
X
X
X
Ciò implica che a , b
c
X
e quindi e d
Ma al tempo stesso per le proprietà dell’intersezione
eX d gcd(k ,h) X e quindi e d gcd(k ,h )
Possiamo concludere che e d gcd(k ,h )
cioè
gcd(k , h )
cX
d gcd(k ,h )
X
17
Esempio 1: calcolo lub con B=Z
Consideriamo
a, b Z , a 312 56
e
b 316 58
Troviamo il lub= a b
Calcoliamo il gcd per definire k e h
2
k gcd( 6,12) 6 quindi a 3 5 d
h gcd( 8,16) 8
quindi b 32 5 d
6
Allora a d
e b d8
Usando la notazione del teorema per il calcolo del lub
per cui
m gcd( 6,8) 2
N
Lub =
3
4
N
52
N
18
Esempio 2: calcolo lub
con B=Q e X={N,Z}
Consideriamo
p
2 4
54
23
58
58
4
e
546
2 33
q 12
5
512
6
Calcoliamo k e h come gcd degli esponenti:
k gcd( 4,8) 4
2 33
52
quindi
h gcd( 6,12) 6
quindi q p
Calcoliamo il gcd tra k e h
m=gcd(4,6)=2
X
2 2
Allora il lub è: r 2 2 3
p
r
2
5
19
Domini Exponential-Closed
Finora abbiamo visto che P ( B, E ) è un reticolo ordinato per
inclusione
Consideriamo ora un tipo particolare di dominio chiamato
exponential-closed
Tale assunzione è imposta dalla caratterizzazione di E:
consideriamo E come collezione di insiemi di interi o naturali
In particolare E può essere visto come una astrazione
di (N ) e (Z)
Questa generalizzazione permette di analizzare le potenze
combinando P( B, X ) con altri domini astratti
ma pone un problema che può essere superato
introducendo questo tipo di domini
20
Domini Exponential-Closed
Problema:
Dati
E N e E z domini astratti
con E N uco N , EZ uco Z e
E E X | X N , Z
Dove una funzione è UCO se è estensiva, monotona e
idempotente
Un UCO identifica un’inserzione di Galois
Se
E e k N o kZ
in generale non è detto che kχ E
e quindi, nell' ambito della Moore - Family,
non è detto che a b sia nella forma
X
cZ con Z E
Y
21
Domini Exponential-Closed
Se C è un reticolo completo allora X C è una
Moore-Family di C ( M ( X ) ) se X glb S | S X
Un dominio exponential-closed assicura che
l’astrazione dell’esponente in un dominio E sia una
Moore-Family ( e quindi una astrazione del (B ) )
Una Moore-Family E X è un dominio exponentialclosed se per ogni
, Y E X e k , h X : z X ,W E x
| kχ hY zW
E x è infinitame nte esponential - closed
se tale proprietà vale anche con infinite
intersezioni
22
E: dominio exponential-closed
Noi assumiamo che E Ex uco ( X ) | X N , Z
Visto che
X N , Z allora X è un dominio esponentia l - closed
perchè kX hY lcm(k , h) X , quindi
E è un dominio esponentia l - closed
I domini così costruiti (con E che soddisfa ACC)
non possono avere infinite catene ascedenti ( ma
le possono avere infinite discedeti )
23
Ascending Chain Condition (ACC)
Consideriamo un poset P:
P soddisfa ACC se per ogni
x1 ... xn ...
Aumentando la sequenza degli elementi di P
k N | xk xk 1 ...
Se X N , Z allora P(B,X ) rispetta ACC
Diamo ora una caratterizzazione degli elementi
meet-irriducible di P(B,E).
24
Elementi Meet-Irriducible
Sia C un reticolo con Mirr(C) è l’insieme degli
elementi meet-irriducible in un reticolo C.
P C e P T P si chiama
meet - irriducible se P x glb c y
implica che P x o P y, cioè non può
essere ottenuto come glb di x o y
C è definito meet-generated dai suoi elementi meetirriducible se e solo se C=M(Mirr(C))
Sia A un insieme e
XA
allora X
è meet-irriducible in ( A) a A | x A \ 0
( A) M ( Mirr (( A))
P( B, E ) M(Mirr(P(B , E)))
25
P(B,E): Reticolo Completo
Dimostriamo ora che P(B,E) con E dominio
esponential-closed è un reticolo completo.
Per far ciò bisogna trovare una G.I. tra P(B,E) e il
powerset di B
Sia :(B) P(B,E) e : P( B, E ) ( B), con , monotone
GI di P(B,E) in(B) :
1) x ( ( x))
P( B, E ) , , ,( B) Adjunction(( B), P( B, E ))
2) ( ( x)) x
3) x.x
Sia Y E
Y ax | x E e Y ax
ax ax
Se E N , Z oppure se E è un dominio infinitame nte esponential - closed
allora P(B,E), α, γ,(B) è una GI
P(B,E) e (B) sono reticoli completi
26
P(B,E): astrazione di (B )
Finora abbiamo dimostrato che P( B, E ) e (B)
sono reticoli completi.
Osserviamo che P ( B, E )
è una astrazione di (B )
cioè che P ( B, E ) è una Moore-Family del (B )
Una GI può essere caratterizzata nei termini di una MooreFamily (Ward):
( P( B, E ), , ,( B)) è una GI P(B,E) è isomorfo
ad una Moore - Family di( B)
P( B, E ) è una astrazione di( B)
27
Operazioni astratte
Dopo aver descritto P(B,E) consideriamo il linguaggio di
programmazione con operazioni aritmetiche standard su N o Q
e ne definiamo l’interpretazione astratta
Queste operazioni sono corrette e in particolare
è un’operazione astratta che rappresenta una astrazione
ottimale della corrispondente operazione concreta del (B )
28
Domini infinitamente exponential-closed
I domini conosciuti nell’ambito della NPA di interi o
razionali sono infinitamente exponential-closed
Quindi sono utilizzabili per approssimare le
proprietà dell’insieme esponente
1. Dominio di congruenza di Granger:
2.
Consente di analizzare potenze numeriche nella
forma mZ+n con n,m Z
Dominio di intervalli di Cousot:
Utilizzato per analizzare la dimensione dell’insieme
esponente in N o Z
Considereremo la restrizione a N:
29
C(Z), Int(Z), Int(N), P(Z,{N})
3.
Dominio per NPA: P(B,E)
C(Z), Int(Z), P(Z, {N}) uco(Z) e Int(N) uco(N)
sono domini infinitamente exponential-closed
Per analizzare le proprietà dell’insieme esponente di
essere un power-set in P(Z,{N})
sono cioè nella forma kX∩hX=zW
per infinite intersezioni
Consideriamo alcuni esempi di intersezioni e lub nei
domini considerati per dimostrare che sono
infinitamente exponential-closed
30
Esempio con E = Int(N)
Dati B=Z, E=Int(N) determiniamo l’intersezione:
Dove:
e
Calcoliamo i valori di k e h:
quindi
quindi
Gli e-atomi di a e b sono uguali quindi l’intersezione esiste
Possiamo trovare l’intersezione come:
Dove: 6N=2N 3N, 4,20 k2,10; 12,45 h4,15
Cioè c=
e
31
Esempio con E = C(Z)
Dati B=Q e E=C(Z),
Trovare
Si noti che
Calcoliamo k e h:
quindi
quindi
Anche in questo caso i 2 e-atomi sono uguali perciò:
Perché
Concludendo
([
=
e
] /6)
32
Esempio con E = Int(Z)
Dati B=Q, E=Int(Z)
Troviamo
Consideriamo gli elementi nella forma
Quindi
e
Gli e-atomi di a e b sono pari a 2
Determiniamo il lub:
Perché
33
Programma per NPA con PN , Z
Applichiamo i domini per
le potenze numeriche
all’analisi statica dei
programmi tramite
l’interpretazione astratta
Questo frammento di
programma ci illustra
l’analisi statica di potenze
numeriche in PN , Z
34
Semantica concreta e astratta
Semantica concreta S:
con π che indica un determinato
punto del programma e
rappresenta
uno stato concreto
Vogliamo calcolare la semantica concreta del
programma P al punto
è l’estensione point-wise alle funzioni dell’insieme
unione
35
Soluzione del sistema
Semantica astratta
È il minimo punto fisso dell’equazione:
Otteniamo la soluzione in 3 passi:
36
Il problema di Collatz
Si presta bene ad essere usato dalla NPA
si può esprimere come iterazione della seguente
funzione
n
se n è pari
S ( n) 2
3n 1 se n è dispari
37
Il grafo di Collatz
I risultati delle iterazioni possono essere
rappresentati con un grafo chiamato grafo di
Collatz della funzione S(n)
38
P termina sempre con 1
È facilmente osservabile che il risultato finale
è sempre 1
Esempio: partiamo da 7
E' dispari, quindi faccio 3x7+1=22.
Pari, 22:2=11.
Dispari, 11x3+1=34.
Pari, 34:2=17.
Dispari, 17x3+1=52.
Pari, 26.
Pari, 13.
Dispari, 40.
Pari, 20.
Pari, 10.
Pari, 5.
Dispari, 16.
Pari, 8.
Pari, 4.
Pari, 2.
Pari, 1.
Da questo punto in poi : 4,2,1,4,2,1,4,2,1.....
39
Formalizziamo
Ciò equivale a dire che
è una tripla di Hoare valida, con:
c può essere ogni potenza di 2
Cioè il programma P termina con n=1 ogni qual volta
Consideriamo le seguenti operazioni astratte:
40
Calcolo della semantica astratta
La semantica astratta per il programma P al punto
Quindi se
Allora
con
è un punto fisso dell’equazione
41
Analisi statica di PCCP casuali
La NPA dei razionali è adatta ad approssimare la
probabilità dei programmi casuali
Gli oggetti astratti in PQ, E si prestano ad
approssimare le componenti di probabilità delle
computazioni riguardanti scelte casuali
Inoltre il dominio E N può caratterizzare le proprietà
degli esponenti della probabilità elaborata
N
Consideriamo l’operazione prodotto astratto con
E N, E
N
N
Int ( N ), a b d
, g gcd(k, h)
42
Linguaggio PCCP
Per modellare questa situazione come un
programma di analisi statica consideriamo
una versione probabilistica del calcolo
constraint concorrente (PCCP)
PCCP si basa sul paradigma ask-tell che fa
riferimento alla nozione di bloking-ask
Un processo è sospeso quando lo store non
comporta l’ask-constraint e rimane sospeso
fino a quando ciò accade
43
Sintassi PCCP
Basata sulla nozione di constraint system C
Reticolo algebrico completo
C= insieme di constraint
= relazione d’implicazione che ordina C
= lub
True= bottom di C
False= top di C
Un programma PCCP chiamato P è un oggetto nella
forma D.A
D= insieme di dichiarazioni di procedure nella forma p(x)
A= agente PCCP
44
Sintassi agenti PCCP
45
Semantica PCCP
Semantica operazionale
Sistema di transizioni + probabilità (per ogni transizione)
Significato operazionale del costrutto scelta probabilistica
Controlla se i constranit ci sono implicati nello store
Normalizza le distribuzioni di probabilità considerando solo gli agenti
abilitati
Ciò significa che abbiamo ridefinito le distribuzioni di probabilità
solo con agenti aventi probabilità diversa da 0 e somma delle
probabilità pari a 1
Con
=probabilità di transizione normalizzata
=somma su tutti gli agenti abilitati
46
Semantica: idea di base
Associare ad ogni agente una descrizione
matematica del suo funzionamento computazionale
Spesso la computazione è influenzata dal
funzionamento I/O
Ciò viene descritto da un insieme di constraint che
rappresentano i possibili store finali dopo l’esecuzione
di un agent
L’I/O è rappresentabile con la distribuzione di
probabilità su un sistema constraint:
Cioè su un insieme di coppie (c,p) dove
c= risultato
p= probabilità della computazione risultante
47
Semantica e punti fissi
Semantica
Ottenuta tramite applicazione iterativa dell’operatore di
punto fisso
(sull’insieme dell’interpretazione) partendo
dall’interpretazione iniziale
che assegna ad ogni agente
l’insieme {true}
Interpretazione: agenti → sottoinsieme di C (descrive i
risultati della computazione agente)
Operatore di punto fisso
Con
(per gli insiemi di constraint
) così definito:
48
Spazio vettoriale su C
Restrizione sintattica
Consideriamo PCCP libero da sincronizzazioni
Così ignoriamo gli aspetti relativi alla concorrenza che
richiedono strutture più complicate
Distribuzione di probabilità
Rappresentata da vettori nello spazio vettoriale reale libero
V(C) sul sistema constraint C
Spazio costruito come insieme di tutte le combinazioni
lineari di constraint
O equivalentemente
49
Equazioni ricorsive su spazio vettoriale
Semantica di PCCP
Costruita definendo il significato degli agenti tramite un
insieme di equazioni ricorsive su uno spazio vettoriale
libero
Esempi
Agente stop può solo produrre uno store vuoto con
probabilità pari a 1
Agente tell aggiunge sempre c allo store con
probabilità 1
50
Semantica relazionale
Semantica relazionale I/O di un programma P
Dove
Constraint c=
= lub dei constraint prodotti da ogni
agente Ai
Probabilità p=
= prodotto delle probabilità associate
ad ogni constraint
Semantica astratta su GI PQ, N, , ,(Q)
51
Soundness
Processo di astrazione
Introduce una perdita di informazioni
L’importante è che ciò che mantengo nel concreto lo
sia anche nel’astratto
Soundness del dominio astratto importante
allora esiste
Tale che
cioè p A p #
Sia
quindi
52
Utilizzo di NPA in PCCP
Consideriamo questo algoritmo di calcolo casuale in PCCP
Il programma P genera una sequenza infinita di numeri casuali
con probabilità decrescente:
Questa informazione può essere ottenuta automaticamente
tramite interpretazione astratta in PQ, N
Dominio concreto: ( N Q)
53
Conclusioni
Abbiamo visto come progettare una famiglia di domini
astratti, utili per l’analisi delle potenze numeriche
Questo studio consente di creare nuovi domini astratti
per NPA considerando astrazioni sull’insieme
esponente
Si può generalizzare questa costruzione con le strutture
algebriche dell’insieme base B
Gli anelli eucludei offrono strutture algebriche che
consentono la fattorizzazione dei loro elementi
Perciò si possono trovare strutture algebriche astratte
per B tale che P(B,E) sia un’astrazione di (B )
Importante per generalizzare la NPA alle potenze di altri
oggetti non numerici
54
Bibliografia
Isabella Mastroeni, Numerical Power Analysis, Univ. degli Studi
di Verona,2005
Isabella Mastroeni, Abstract Non-Interference -An Abstract
Interpretation-based approach to Secure Information Flow,
Ph.D. Thesis, Univ. Degli Studi di Verona
Isabella Mastroeni, Algebric Power Analysis by Abstract
Interpretation, Univ. Degli Sutdi di Verona, 2004, Kluwer
Academic Publishers
A.Di Pierro and H.Wiklicky. An operational semantics for
probabilistic concurrent constraint programming. In Proc. Of the
1998 IEEE Internat. Conf. On Computer Languages (ICCL ’98).
IEEE Computer Society Press, Los Alamitos, Calif., 1998
Tino Cortesi, Manipulating Abstract Domains and Abstract
Operations for Static Analysis of (Declarative) Programs, Univ.
degli Studi di Venezia Ca’ Foscari
L'algoritmo di Collatz, Gianfranco Bo,
http://utenti.quipo.it/base5/numeri/collaz.htm
55