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