Download Diapositiva 1

DOCTORADO EN PROGRAMACIÓN DECLARATIVA E INGENIERÍA DE LA PROGRAMACIÓN
Especificación y verificación
de routers software
(12 Créditos)
J. Guadalupe Ramos Díaz
Tutor: Dr. Germán Vidal
DSIC-PLIS-ELP-MIST
Agenda:
1. Currículum
1.1 Formación
1.2 Materias impartidas en México
1.3 Participación en proyectos
1.4 Ponencias en Congresos Nacionales
2. Docencia
3. Investigación
3.1 Definición de router
3.2 Objetivo
3.3 Anotaciones
3.4 Especificación de circuitos
3.5 Lenguaje anfitrión
3.6 Solución
4. Conclusiones
5. Trabajos futuros
6. Plan de trabajo
2
1. Currículum: Formación
Maestría en Ciencias Computacionales
I. T. León (1998)
Adiestramiento en Investigación Tecnológica
Instituto de Investigaciones Eléctricas (Cuernavaca,
México, 1995)
Ingeniería en Sistemas Computacionales
I. T. Morelia (1994)
3
1. Currículum: Materias impartidas
Programación
Programación de sistemas
Programación para Internet
Administración de archivos
Redes de área local
Sistemas abiertos
Tópicos de redes
Teleproceso
Graficación
4
1. Currículum: Proyectos de I+D
Sistema de graficación para QNX
Instituto de Investigaciones Eléctricas
Asesor de proyectos de creatividad en
etapas nacionales
– Servidor genérico P2P
– Sistema de monitoreo y control remoto por
Internet
– Aplicaciones P2P
5
1. Currículum: Ponencias en Congresos
Nacionales
Intermediario para sistemas de información
distribuida
Congreso de Ing. en Sist. Computacionales e
Informática (I.T.Tuxtla Gutiérrez, Chiapas): CISCI’02
Propuesta de middleware para aplicaciones P2P
Simposium Intertecnológico de Ciencias
Computacionales: SICI’01
Servidor genérico para aplicaciones P2P
1er. Congreso Nacional de Calidad en la Educación
Superior Tecnológica: CNCEST’00
6
2. Etapa de Docencia
Materia
Créditos
Ingeniería de requisitos O.O.
5
Bases de datos avanzadas
4
Tecnología software para ambientes web
5
Fundamentos lógicos de la Ingeniería de
Software
Ingeniería de Software automática
4
4
7
3. Investigación: Definición
Paquete
Carga útil
cabecera
Router
Dirección
destino
Estructura de
datos de rutas
Puertos de
salida Routers extensibles
Tabla de encaminamiento
Red destino
Puerto
65.0.0.0/8
3
128.9.0.0/16
1
• Seguridad
• Políticas
149.12.0.0/19
2
+Protocolos de encaminamiento
• QoS
• Direcciones
• Evolución
8
3. Investigación: Definición
Existen dos tipos: [Spalink et al., 2001]
Ejecución en un PC:
• Enchufes [Decasper et al. 1998], ETH Zurich & U. Washington
• Scout [Peterson et al. 1999], U. Arizona, U. Princeton
• Click [Kohler et al. 1999], MIT
Ejecución en un PC + Procesador de Red:
• VHDL + FPGA [Lee et al. 1999], I.P. Virginia
• Intel IXP1200 + Ensamblador [Spalink et al. 2001], U. Princeton
• NPClick + Intel IXP1200 [Shah et al. 2003], U. Berkeley
Router Modular Click
Forma de grafos
9
3. Investigación: Objetivo
Ventajas claras de los routers extensibles
(tema actual) respecto a los routers hardware
Actividad crucial en una red  Click debería
tener un entorno para especificación y
verificación de routers software, etc. ¡No lo
tiene!
Objetivo: Desarrollar un lenguaje de
dominio específico sobre un lenguaje
declarativo (multi-paradigma) para la
especificación y verificación de routers Click
10
3. Investigación: Anotaciones
No existen antecedentes en la literatura del uso de un
lenguaje declarativo para la especificación de routers
software
Existe un campo relacionado: especificación y verificación
de hardware
Explotamos la relación circuitos <-> grafos Click
Un lenguaje declarativo empotrado es Anfitrión
una librería que se incorpora a un
Librería
lenguaje ya existente
Dominio
Librería = Lenguaje de dominio
específico
11
3. Investigación: Especificación de
circuitos
Especificación del
lenguaje
empotrado: Lava
[Claessen, 2001]
Librería
type Signal = [Bool]
and :: (Signal,Signal)->Signal
xor :: (Signal,Signal)->Signal
Apoyado por Xilinx
Inc.
halfAdd (a, b) = (sum, carry)
where
sum = xor (a, b)
carry = and (a, b)
12
3. Investigación:
Especificación de
circuitos
• Especificación del
lenguaje empotrado
Hawk [Matthews, et al.,
2000]
• Apoyado por Intel Inc.
sham1 (cmd, destReg, srcRegA, srcRegB) = (destReg’, aluOutput’)
where
(aluInputA, aluInputB) = regFile srcRegA srcRegB(destReg’,aluOutput’)
aluOutput
aluOutput’
destReg’
= alu cmd aluInputA aluInputB
= delay 0 aluOutput
= delay R0 destReg
13
3. Investigación: Lenguaje anfitrión
Curry
Curry es una extensión
conservativa de Haskell (base
de Lava / Hawk) con
características de la
programación lógica
Permitirá adaptar
inmediatamente Lava
y Hawk
Proporciona el entorno
apropiado para practicar
verificación, simulación y
análisis
Curry = lógica + funcional + concurrente + distribuida +
OO = multi-paradigma
14
3. Investigación: Solución
Caso Simple:
type Packet = [ Char ]
FromDevice(eth0)->Print (“Paq:”)->Discard
fromDevice :: Int -> Packet
fromDevice _ = newPacket
print :: (String, Packet) -> Packet
print (s, px) = let
p= s++px
in p
Conector de orden superior
(fromDevice
->-
discard) 1
discard :: Packet->Int
discard p = 0
(->-) :: (a->b) -> ( b->c) -> a -> c
(element1 ->- element2) inp = let
mid = element1 inp
in element2 mid
15
3. Investigación: Solución
Caso a modelar:
Principal problema
propio a un router:
La conexión =
¿funciones? o
¿conectores? o
¿condicionales?
16
3. Investigación: Solución
router pkin = out
where
(pk, pto) = classifier pkin
pk2
= if pto==2 then paint pk 2 else GOTO
...
Características:
•Problema de salidas múltiples y condicionales
•Poco declarativo
•En Click no hay condicionales
17
3. Investigación: Solución
type Event = (Packet, Puerto)
router:: Event -> Event
router inp = out
where
outclassif = classifier inp
out
= routerBranch outclassif
routerBranch (pk,0) = arpResponder (pk,0)
routerBranch (pk,1) = arpQuerier (pk,1)
routerBranch (pk,2) = out
where
st1 = paint (pk,2) 1111
st2 = strip st1 14
st3 = checkIPHeader st2
out = getIPAddress st3
•Escritura de router mas cercana a Click
Características:
•Incorporación de abstracción de eventos
•Se aprovecha pattern matching para dar inteligencia a los elementos
18
4. Conclusiones
Los routers extensibles son un tema de actualidad que
madurará y en el que Click sobresale
La especificación y verificación formal son de gran
importancia para las empresas de hardware y ya hay
esfuerzos basados en el uso de lenguajes declarativos.
Curry podría tener un lugar ventajoso gracias a sus
características multi-paradigma
Se han comprobado las ventajas de escribir un
lenguaje empotrado con respecto la creación de un
lenguaje nuevo (con intérprete, compilador,
herramientas de verificación . . . )
19
5. Trabajos futuros
Enlazar nuestro lenguaje con Click: Traductor de
especificaciones Curry a Click
(colaboración con E. Kohler, MIT)
Especificar los 242 elementos Click
Definir e implementar técnicas de análisis, verificación,
etc. (concretas al dominio del problema)
– Propiedades de un router:
No puede haber ciclos infinitos, verificar que a una entrada hay una
salida, excepto con paquetes vencidos
El paquete sólo puede ser modificado en ciertos campos
Para todo paquete debe haber una ruta de encaminamiento, etc.
20
6. Plan de trabajo
Publicación PROLE’03 (Terceras Jornadas
sobre Lenguajes de Programación )
TESIS: Especificación (presente) Y
verificación (futuro) de routers software
Metodología de trabajo:
– Contacto regular vía email
– Visita a la UPV
– Asistencia a congresos
Proyecto de I+D centrado en el tema
21
...
22