Seguridad y vivacidad

Un programa concurrente puede fallar por varias razones las cuales se pueden clasificar entre dos grupos de propiedades:

seguridad:

Esa propriedad inidca que no está pasando nada malo en el programa, es decir, el programa no ejecuta instrucciones que no deba hacer (``safety property'').

vivacidad:

Esa propriedad indica que está pasando continuamente algo bueno durante la ejecución, es decir, el programa consigue algún progreso en sus tareas o en algún momento en el futuro se cumple una cierta condición (``liveness property'').

Las propiedades de seguridad suelen ser algunas de las invariantes del programa que se tienen que introducir en las comprobaciones del funcionamiento correcto (p.ej., mediante inducción).

Ejemplos de propiedades de seguridad:

• el algoritmo usado es correcto
• el acceso con exclusión mutua a regiones críticas está garantizado

Ejemplos de propiedades de vivacidad:

• ningún proceso muere por inanición (``starvation''), es decir, un proceso o unos procesos siguen con su trabajo pero otros nunca llegan a utilizar los recursos
• si un proceso pide un recurso, lo consigue en algún momento
• los procesos no se bloquean mutuamente
• no se termina un proceso desde fuera sin motivo
• un proceso no se queda dormido (p.ej. en Java, cada suspend() tiene su resume() correspondiente)
• la conexión entre procesos es fiable