Download CSP: Sintaxis y semántica

Communicating Sequential
Processes
Presentación realizada por :
Alberto Calixto Simon
Ivan Olmos Pineda
CSP
• Fue descrito por primera vez en un
documento presentado por C. A. R. Hoare.
• La idea del nombre fue tratar de describir
sistemas como un número de componentes
(procesos) que operan independientemente
y se comunican entre si por un número bien
definido de canales.
• Influenciado por Ada
CSP: Características
• Enfocado a desarrollar sistemas paralelos.
• Comunicación por medio de paso de
mensajes mediante memoria compartida.
• Sintaxis y semántica enfocada a desarrollar
sistemas paralelos con naturalidad.
• Sincronización entre procesos,
comunicación síncrona.
CSP: Características
• Facilidad para implementar programas con
múltiples entradas y salidas.
• Se especifican claramente el número de
procesos concurrentes, variables, etc.
• Se dice que más que un lenguaje, es una
filosofía de programación.
CSP: Sintaxis, Semántica
Comando asignación: :=
x := x +1;
(x, y) := (y, x);
• En caso que las variables que intervienen en
una asignación sean de distintos tipos, esta
no se realiza.
CSP: Sintaxis, Semántica
Instrucción ||:
X(1) :: CL1 || X(2) :: CL2;
user :: USER || sort(i: 1 .. 1000) :: SORT ||...
• No hay almacenamiento de variables
• Termina el procesamiento paralelo cuando
terminan todos los procesos paralelos.
• Como cada proceso se define explícitamente, no
hay creación dinámica de procesos.
CSP: Sintaxis y semántica
Comandos de entrada / salida
procl ? l
lpr ! l
La primera operación indica que del canal
procl entra algo a l.
La segunda operación indica que del canal b
sale el valor de l.
CSP: Sintaxis y semántica
• Existen operadores básicos: +, -, <, >,...
[ coutn < 100 ; xyz < 20 -> count:=count+1
[] count = 100 -> xyz := 34;
[] xyz >= 20 -> xyz := 0
]
CSP: Sintaxis y semántica
• En el ejemplo anterior, ; significa la
conjunción lógica.
• Se pueden realizar programas simples como
el siguiente, el cual solo recibe un conjunto
de 100 caracteres desde el teclado e
imprime los que sean caracteres
imprimibles.
CSP: Sintaxis y semántica
[ c: character;
(i: 1.. 100) continue(i); keyboard(i) ? c ->
[ c = LINEFEED -> console(i) ! RETURN;
console(i) ! LINEFEED
[] c <> LINEFEED -> console(i) ! C
]
]
CSP: Sintaxis y semántica
• Para crear una iteración de un conjunto de
instrucciones, se coloca un asterisco al inicio de
estas.
*[ (i: 1.. 5) A(i) > A(i+1)
(A(i),A(i+1)) := (A(i+1), A(i))
]
En este ejemplo, A es un arreglo de 1000 enteros.
En este ejemplo, se ordena el arreglo en orden
ascendente.
FDR
Failures Divergence Refinement
Refinamiento Divergente de Fallas
¿Qué es FDR ?
FDR es un modelo de chequeo para
maquinas de estados, con base en la teoría
de concurrencia establecida alrededor de
CSP desarrollado en la Universidad de
Oxford.
Capacidad
La versión FDR2 mejora la ejecución de su
antecesor, e incorpora una jerarquía
abstracta y mecanismos de compresión que
permiten al sistema analizar una gran
cantidad de estados (7^(2^1024)) en
minutos.
Aplicaciones
• Desarrollo y verificación de comunicaciones de
hardware (en el Transputer T9000 y el chip C104 de
ruteadores)
• Protocolos de Seguridad
- Propiedades
- Defectos en el intercambio de llaves
- Autentificación, confidencialidad,...
¿Que ofrece FDR2?
• Soporte de operadores fuera del núcleo de
CSP y completamente diferente al lenguaje.
• Todos
los
procesos
pueden
ser
parametrizados.
• Mejorar el manejo de la sincronización
múltiple, con la representación de reglas de
disparo basadas en los eventos los cuales
integran.
• Proveer de un lenguaje poderoso para los
tipos de datos y expresiones.
• La habilidad de construir un sistema
convergente gradualmente, en cada etapa
comprime al subsistema a producir un
proceso equivalente con menos estados.
FDR Soporta Directamente Tres
Modelos
• El modelo de trazos
• El modelo de fallos estables
• El modelo de fallos divergentes
Entorno
FDR requiere un sistema workstation y se aconseja
usar FDR en un sistema con almenos 32Mb de
memoria física, y al menos 64Mb de memoria
virtual.
Las plataformas de soporte son:
Sun Sparc systems (Solaris 2.3 o superiores)
HP PA-RISC systems (HP-UX 9.0.5)
IBM RS/6000 systems (AIX 3.2.5)
Procesos
•
•
•
•
•
•
•
c -> p
prefijo simple
c ?x ?x':a !y -> p prefijo complejo
p;q
composición secuencial
p [[ c <- c' ]]
re-etiquetar
!x
salida
?x:a
entrada obligada
?x
entrada espontanea
Ejemplos
BUFF(in,out) = in?x -> out!x -> BUFF(in, out)
square(n) = n * n
P = in ? x -> out ! square(x) -> P
Ejemplos
-- First, the set of values to be communicated
datatype FRUIT = apples | oranges | pears
channel left,right,mid : FRUIT
channel ack
COPY = left ? x -> right ! x -> COPY
SEND = left ? x -> mid ! x -> ack -> SEND
REC = mid ? x -> right ! x -> ack -> REC
SYSTEM = (SEND [| {| mid, ack |} |] REC) \ {| mid, ack |}
assert COPY [FD= SYSTEM
assert SYSTEM [FD= COPY
Referencias
• http://cswww.vuse.vanderbilt.edu/~raghavan/cs38
1/csplect/index.htm
• http://archive.comlab.ox.ac.uk/csp.html
• http://www.formal.demon.co.uk/CSP.html
• http://research.cem.itesm.mx/jesus/csp/csp.html