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.

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.

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

Ejemplos de propiedades de seguridad:

• el algoritmo usado es correcto
• la exclusión mutua de regiones críticas

Ejemplos de propiedades de vivacidad:

• ningún proceso muere por inanición
• 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 (p.ej., en Java, cada stop() es razonable)
• un proceso no se queda dormido (p.ej. en Java, cada suspend() tiene su resume() correspondiente)
• la conexión entre procesos es fiable