Corrección
Que un programa haga lo que tiene que hacer (que no tenga bugs):
- En procesos (programas secuenciales) es suficiente con debuggear para encontrar errores, ya que ante una misma entrada se obtiene siempre la misma salida.
- En programas concurrentes, la salida puede depender del escenario que resultó en la ejecución.
Propiedades de Corrección
- Safety: debe ser verdadera siempre.
- Liveness: debe volverse verdadera eventualmente.
Propiedades tipo Safety
- Exclusión mutua: dos procesos no deben intercalar ciertas (sub)secuencias de instrucciones.
- Ej: incremento de variable global.
- Ausencia de deadlock: un sistema que aún no finalizó debe poder continuar realizando su tarea, es decir, avanzar productivamente.
Propiedades tipo Liveness
- Ausencia de starvation: todo proceso que esté listo para utilizar un recurso debe recibir dicho recurso eventualmente.
- Fairness: equidad o justicia
- Un escenario es débilmente fair, si en algún estado en el escenario, una instrucción que está continuamente habilitada, eventualmente aparece en el escenario.
Sección Crítica
Modelización de la Sección Crítica
- Cada proceso se ejecuta en un loop infinito cuyo código puede dividirse en parte crítica y parte no-crítica.
- Especificaciones de corrección:
- Exclusión mutua: no deben intercalarse instrucciones de la sección crítica.
- Ausencia de deadlock: si dos procesos están tratando de entrar a la sección crítica, eventualmente alguno de ellos debe tener éxito.
- Ausencia de starvation: si un proceso trata de entrar a la sección crítica, eventualmente debe tener éxito.
- La sección crítica debe progresar (finalizar eventualmente)
- La sección no-crítica no requiere progreso (el proceso puede terminar o entrar en un loop infinito)
Locks