PDF de programación - Análisis amortizado de consumo de recursos

Análisis amortizado de consumo de recursos

M. Hofmann

S. Jost

J. Hoffmann K. Aehlig

Análisis y Transformación de Programas

Máster en Investigación en Informática, 2012

Hofmann et al.

Análisis amortizado de consumo de recursos

1/54
1/54

M. HofmannS. JostPOPL'03B. CampbellESOP'09M. Hofmannet al.ESOP'06S. Jostet al.FM'09J. HoffmannM. HofmannESOP'10J. HoffmannM. HofmannAPLAS'10J. HoffmannK. AehligM. HofmannPOPL'11S. Jostet al.POPL'10 M. HofmannS. JostPOPL'03B. CampbellESOP'09M. Hofmannet al.ESOP'06S. Jostet al.FM'09J. HoffmannM. HofmannESOP'10J. HoffmannM. HofmannAPLAS'10J. HoffmannK. AehligM. HofmannPOPL'11S. Jostet al.POPL'10 Introducción

• Objetivo: Dado un programa escrito en un lenguaje funcional,

determinar una cota superior de la cantidad de recursos necesarios
(celdas de memoria) para su ejecución.

• Esta cota vendrá dada en forma de función sobre los argumentos.

◦ POPL’03: Funcion lineal.
◦ ESOP’10: Función polinómica sobre una variable.
◦ POPL’11: Función polinómica sobre varias variables.

• Se utilizan técnicas de análisis amortizado.

Hofmann et al.

Análisis amortizado de consumo de recursos

3/54
3/54

Análisis amortizado

• Técnica introducida formalmente por Robert Tarjan (1985):

Amortized Computational Complexity.

• Es un método de analisis de algoritmos que considera el coste

global (en el caso peor) una secuencia de operaciones.
◦ Más preciso que considerar la suma de los costes individuales en el
◦ El hecho de que algunas operaciones sean demasiado costosas viene

caso peor.

compensado por tener operaciones menos costosas, pero más
frecuentes.

Hofmann et al.

Análisis amortizado de consumo de recursos

4/54
4/54

Análisis amortizado
Método del potencial

• Existe una función potencial φ(s) asociada a cada estado posible s

del programa.

s C s0

• Operaciones menos costosas acumulan potencial en el estado.
• El potencial se usa para pagar operaciones costosas.

Camortizado = C +φ(s0)− φ(s)

Hofmann et al.

Análisis amortizado de consumo de recursos

5/54
5/54

Lenguaje RAML
Resource-Aware ML

Sintaxis

e

::= () | True | False | n | x | x1 ⊕ x2
f (x1, . . . ,xn) | letx1 = e1 in e2
if x thenet else ef

| nil | (x1 :: x2) | (x1,x2)
|
|
| match x with (x1,x2) → e
| match x withnil → e1
(x :: xx ) → e2

Hofmann et al.

Análisis amortizado de consumo de recursos

6/54
6/54

Lenguaje RAML
Resource-Aware ML

Sintaxis

e

::= () | True | False | n | x | x1 ⊕ x2
f (x1, . . . ,xn) | letx1 = e1 in e2
if x thenet else ef

| nil | (x1 :: x2) | (x1,x2)
|
|
| match x with (x1,x2) → e
| match x withnil → e1
(x :: xx ) → e2

Sistema de tipos básico

A ::= unit | bool | int | L(A) | (A,A)
F ::= (A,A, . . . ,A) → A

Hofmann et al.

Análisis amortizado de consumo de recursos

6/54
6/54

Lenguaje RAML
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → let x1 = append(xx ,ys)

in (x :: x1)

append : (L(A),L(A)) → L(A)

Hofmann et al.

Análisis amortizado de consumo de recursos

7/54
7/54

123546789 Lenguaje RAML
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → let x1 = append(xx ,ys)

in (x :: x1)

append : (L(A),L(A)) → L(A)

Hofmann et al.

Análisis amortizado de consumo de recursos

7/54
7/54

123546789 Lenguaje RAML
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → let x1 = append(xx ,ys)

in (x :: x1)

append : (L(A),L(A)) → L(A)

Hofmann et al.

Análisis amortizado de consumo de recursos

7/54
7/54

1235467891234 Sistema de tipos
Análisis amortizado

• Asociar un potencial a cada elemento de la estructura de datos.
• El potencial total de la estructura de datos es lineal con respecto

su tamaño.

Hofmann et al.

Análisis amortizado de consumo de recursos

8/54
8/54

...x1x2x3xnaaaa…......... Sistema de tipos
Análisis amortizado

• Asociar un potencial a cada elemento de la estructura de datos.
• El potencial total de la estructura de datos es lineal con respecto

su tamaño.

• El potencial se refleja en el tipo de la estructura de datos.

xs : L(a)(int)

=⇒

φ(xs) = a∗|xs|

Hofmann et al.

Análisis amortizado de consumo de recursos

8/54
8/54

...x1x2x3xnaaaa…......... Sistema de tipos
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → x :: append(xx ,ys)

Hofmann et al.

Análisis amortizado de consumo de recursos

9/54
9/54

1235467891111 Sistema de tipos
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → x :: append(xx ,ys)

Hofmann et al.

Análisis amortizado de consumo de recursos

9/54
9/54

1235467891111 Sistema de tipos
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → x :: append(xx ,ys)

Hofmann et al.

Análisis amortizado de consumo de recursos

9/54
9/54

12354678941111Coste construcción1 Sistema de tipos
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → x :: append(xx ,ys)

Hofmann et al.

Análisis amortizado de consumo de recursos

9/54
9/54

12354678912341111 Sistema de tipos
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → x :: append(xx ,ys)

append : (L(1)(A),L(0)(A)) → L(0)(A)

Hofmann et al.

Análisis amortizado de consumo de recursos

9/54
9/54

12354678912341111 Sistema de tipos
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → x :: append(xx ,ys)

Hofmann et al.

Análisis amortizado de consumo de recursos

9/54
9/54

1235467893333 Sistema de tipos
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → x :: append(xx ,ys)

Hofmann et al.

Análisis amortizado de consumo de recursos

9/54
9/54

12354678943333Coste construcción12 Sistema de tipos
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → x :: append(xx ,ys)

Hofmann et al.

Análisis amortizado de consumo de recursos

9/54
9/54

123546789123433332222 Sistema de tipos
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → x :: append(xx ,ys)

append : (L(3)(A),L(2)(A)) → L(2)(A)

Hofmann et al.

Análisis amortizado de consumo de recursos

9/54
9/54

12354678912343333222222222 Sistema de tipos
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → x :: append(xx ,ys)

Hofmann et al.

Análisis amortizado de consumo de recursos

9/54
9/54

1235467893333 Sistema de tipos
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → x :: append(xx ,ys)

Hofmann et al.

Análisis amortizado de consumo de recursos

9/54
9/54

12354678943333Coste construcción12 Sistema de tipos
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → x :: append(xx ,ys)

append : (L(3)(A),L(0)(A)) → L(0)(A)

Hofmann et al.

Análisis amortizado de consumo de recursos

9/54
9/54

12354678912343333 Sistema de tipos
Ejemplo: concatenar listas

Ejemplo

append(xs,ys) = match xs with
nil → ys
(x :: xx ) → x :: append(xx ,ys)

append : (L(q)(A),L(p)(A)) → L(p)(A)

q ≥ p +1

Hofmann et al.

Análisis amortizado de consumo de recursos

9/54
9/54

12354678912343333 Sistema de tipos
Ejemplo: función attach

Ejemplo

attach(y ,xs) = match xs with
nil → nil
(x :: xx ) → (y ,x ) :: attach(y ,xx )

Hofmann et al.

Análisis amortizado de consumo de recursos

10/54
10/54

12342222 Sistema de tipos
Ejemplo: función attach

Ejemplo

attach(y ,xs) = match xs with
nil → nil
(x :: xx ) → (y ,x ) :: attach(y ,xx )

Hofmann et al.

Análisis amortizado de consumo de recursos

10/54
10/54

1234(7,4)222211Construcción tuplaConstrucción celda de lista Sistema de tipos
Ejemplo: función attach

Ejemplo

attach(y ,xs) = match xs with
nil → nil
(x :: xx ) → (y ,x ) :: attach(y ,xx )

Hofmann et al.

Análisis amortizado de consumo de recursos

10/54
10/54

1234(7,4)2222(7,3)(7,2)(7,1) Sistema de tipos
Ejemplo: función attach

Ejemplo

attach(y ,xs) = match xs with
nil → nil
(x :: xx ) → (y ,x ) :: attach(y ,xx )

attach : (int,L(2)(int)) −→ L(0)(int,int)

Hofmann et al.

Análisis amortizado de consumo de recursos

10/54
10/54

1234(7,4)2222(7,3)(7,2)(7,1) Sistema de tipos
Ejemplo: función attach

Ejemplo

attach(y ,xs) = match xs with
nil → nil
(x :: xx ) → (y ,x ) :: attach(y ,xx )

attach : (int,L(q)(int)) −→ L(p)(int,int)

q ≥ p +2

Hofmann et al.

Análisis amortizado de consumo de recursos

10/54
10/54

1234(7,4)2222(7,3)(7,2)(7,1) Sistema de tipos
Ejemplo: Inserción ordenada

Ejemplo

insert : (int,L(int)) → L(int)

Hofmann et al.

Análisis amortizado de consumo de recursos

11/54
11/54

1234111151 Sistema de tipos
Ejemplo: Inserción ordenada

Ejemplo

insert : (int,L(int)) → L(int)

Hofmann et al.

Análisis amortizado de consumo de recursos

11/54
11/54

123411115112345 Sistema de tipos
Ejemplo: Inserción ordenada

Ejemplo

insert : (int,L(int)) → L(int)

insert : (int,L(1)(int))

1/0−→ L(0)(int)

Hofmann et al.

Análisis amortizado de consumo de recursos

11/54
11/54

123411115112345 Sistema de tipos
Ejemplo: Inserción ordenada

Ejemplo

insert : (int,L(int)) → L(int)

insert : (int,L(q)(int))

p/p0−→ L(q0)(int)

q ≥ q0 +1,p ≥ p0 +1

Hofmann et al.

Análisis amortizado de consumo de recursos

11/54
11/54

123411115112345 Sistema de tipos
¿Para qué sirve el potencial?

• Supongamos una función f de tipo:

f : (L(a)(int),L(b)(int))

q/q0−→ L(c)(int)

• Para evaluar una llamada f (xs,ys), es suficiente disponer en

memoria de a∗|xs| +b ∗|ys| +q celdas.

• Al final de la evaluación, dispondremos de c ∗|zs| +q0 celdas libres,

donde zs denota el resultado de evaluar f (xs,ys).

Hofmann et al.

Análisis amortizado de consumo de recursos

12/54
12/54

Sistema de tipos
Reglas de tipo

• Sintaxis de tipos:

A ::= unit | bool | int | L(n)(A) | (A,A)
F ::= (A,A, . . . ,A)

q/q’−→ A

• Juicios de la forma:

Σ; Γ ‘ e : A (q/q0)

◦ Σ asocia nombres de función f con signaturas de tipo F.
◦ Γ asocia variables en ámbito c