No determinismo
El no determinismo es una propiedad inherente a la concurrencia.
Por culpa del no determinismo, es más difícil analizar y verificar un algoritmo concurrente.
Ojo, que existan varias posibilidades de salida NO significa necesariamente que un programa concurrente sea incorrecto.
Acciones atómicas
Por culpa del no determinismo, la ejecución del programa puede ser incorrecta e inesperada.
Surge la conveniencia de imponer que ciertas piezas de código se ejecuten de forma atómica.
cobegin
x := 2;
x := 65536;
coend;
¡¡el resultado podría ser x=65538!!
Acciones atómicas (2)
En el análisis de algoritmos concurrentes, se permite declarar que una sentencia se ejecuta de forma atómica.
cobegin < x:=x+1> < x:=x+2> coend
Así se facilita el análisis y verificación de estos algoritmos.
No nos incumbe (por ahora) cómo se consigue la ejecución atómica.
Historias / secuencias de ejecución
Una historia o la secuencia de ejecución es una secuencia temporal de acciones que ocurren durante la ejecución de un programa.
Un programa concurrente puede tener múltiples secuencias de ejecución (y todas ellas pueden ser correctas)
a -> b -> c
c -> a -> b
…
Verificación de programas
¿Cuándo un programa (secuencial) se considera correcto?
Parcialmente correcto. Dadas unas precondiciones correctas, si el programa termina se cumplen las postcondiciones previstas.
Totalmente correcto. Dadas unas precondiciones correctas, el programa termina y se cumplen las postcondiciones.
Peculiaridades de los programas concurrentes
Los programas concurrentes pueden no terminar nunca y al mismo tiempo ser correctos.
Un pr.c. puede tener múltiples secuencias de ejecución.
Cuando se dice que un pr.c. es correcto, se entiende que se refiere a todas sus posibles secuencias de ejecución.
Seguridad y progreso(safety and liveness)
Dos tipos de propiedades útiles en los sistemas concurrentes
Propiedades de seguridad (safety)
una propiedad que debe ser cierta siempre
ejs. exclusión mutua, no interbloqueo
Propiedades de progreso (liveness)
una propiedad que se cumplirá con toda seguridad en algún momento de la ejecución
ejs. propiedades de justicia (fairness), evitación de inanición
Ejemplos de justicia (fairness)
Justicia débil. Si un proceso realiza continuamente una petición, terminará siendo atendido.
Justicia fuerte. Si un proceso realiza una petición con frecuencia infinita, terminará siendo atendido.
Espera lineal. Si un proceso realiza una petición, ningún otro proceso puede ser atendido dos veces antes que él.
Espera FIFO. Si un proceso realiza una petición, será atendido antes que cualquier otra solicitud posterior.
Análisis de algoritmos concurrentes
Usar invariantes y lógica proposicional
Usar métodos inductivos
Usar historias de ejecución (a->b)
Usar predicados posicionales: at(I), in(I), after(I)
Usar lógica temporal
…
 Página anterior | Volver al principio del trabajo | Página siguiente  |