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 ax  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:
 PB, X  è un RETICOLO
 Definire lub e glb
 PB, X  è un reticolo COMPLETO
 GI tra (B ) e PB, X 
 Consideriamo domini EXPONENTIAL-CLOSED
 Proprietà: ACC e elementi MEET-IRRIDUCIBLE
 PB, X  è un’ASTRAZIONE DI (B )
 PB, 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  ak , b  bh
allora ak  bh  d gcd(k ,h )
X
 Quindi sappiamo che aX , bX  d gcd(k ,h) 
 Dimostriamo che
d gcd(k ,h) X è contenuto nell’insieme c
X
X
X
 con c  a , b
e cB


X
16
Fase 1: dimostrazione RETICOLO
 In altri termini d gcd(k ,h )   cX  d gcd(k ,h) 
X
 Se a  b  d
, aX  bX  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 eX
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
eX  d gcd(k ,h) X e quindi e  d gcd(k ,h )
 Possiamo concludere che e  d gcd(k ,h )
cioè
gcd(k , h )
cX

 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
23

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 kZ

in generale non è detto che kχ  E
e quindi, nell' ambito della Moore - Family,
non è detto che a  b sia nella forma
X
cZ 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
XA
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    ax | x  E e Y  ax
 
 ax  ax

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  k2,10; 12,45  h4,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 PN , 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 PN , 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 PQ, 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 PQ, 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 PQ, 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
Scarica

Document