Next: Propriedades de programas concurrentes
Up: Abstracción
Previous: Regiones críticas
  Índice General
Generalmente se dice que un programa es correcto si dado una entrada
el programa produce los resultados deseados.
Más formalmente:
Sea P(x) una propriedad de una variable x de entrada
(aquí el símbolo x refleja cualquier conjunto de variables de entradas).
Sea Q(x, y) una propriedad de una variable x de entrada y de una
variable y de salida.
Se define dos tipos de funcionamiento correcto de un programa:
- funcionamiento correcto parcial:
- dado una entrada a,
si P(a) es verdadero, y si se
lanza el programa con la entrada a, entonces si el programa termina
habrá calculado b y Q(a, b) también es verdadero.
- funcionamiento correcto total:
- dado una entrada a,
si P(a) es verdadero, y si se
lanza el programa con la entrada a, entonces el programa termina
y habrá calculado b con Q(a, b) siendo también verdadero.
Se distingue los dos casos sobre todo porque el problema si un
programa, dado una entrada, se para, no es calculable.
Para un programa secuencial existe solamente un orden total de
las instrucciones atómicas (en el sentido que un procesador
secuencial siempre sigue el mismo orden de las instrucciones),
mientras que para un programa concurrente
puedan existir varios órdenes.
Por eso se tiene que exigir:
- funcionamiento correcto concurrente:
- un programa concurrente funciona correctamente si el resultado Q(x, y)
no depende del orden de las instrucciones atómicas entre todos
los órdenes posibles.
Entonces:
- Se debe asumir que los hilos oueden intercalarse en cualquier punto en
cualquier momento.
- Los programas no deben estar basados en la suposición de que vaya a haber
un intercalado especifico entre los hilos de parte del planificador.
Next: Propriedades de programas concurrentes
Up: Abstracción
Previous: Regiones críticas
  Índice General
© 2004, Dr. Arno Formella, Universidad de Vigo, Departamento de Informática