En computación concurrente , vivacidad se refiere a un conjunto de propiedades de sistemas concurrentes , que requieren que un sistema avance a pesar de que sus componentes ("procesos") que se ejecutan simultáneamente pueden tener que "turnarse" en secciones críticas , partes del programa. que no pueden ser ejecutados simultáneamente por múltiples procesos. [1] Las garantías de vida son propiedades importantes en los sistemas operativos y sistemas distribuidos . [2]
De manera más general, una propiedad de vitalidad establece que "eventualmente ocurrirá algo bueno", en contraste con una propiedad de seguridad que establece que "algo malo no ocurre". Si se viola una propiedad de seguridad, siempre hay una ejecución finita que muestra la violación (el evento "malo" que ocurre), pero una propiedad de vida no se puede violar en una ejecución finita de un sistema distribuido porque el evento "bueno" aún puede ocurrir en algún tiempo más tarde. La consistencia eventual es un ejemplo de una propiedad de vivacidad. [3] Todas las propiedades de tiempo lineal se pueden expresar como la intersección de las propiedades de seguridad y vitalidad. [4]Mientras que la violación de una propiedad de seguridad dada admite un testigo finito, la violación de las propiedades de vida puede ser más difícil de establecer, ya que ningún testigo finito puede usarse como prueba. [5]
Formas de vitalidad
Se reconocen varias formas de vitalidad. Los siguientes se definen en términos de un sistema multiproceso que tiene una sección crítica, protegida por algún dispositivo de exclusión mutua (mutex). Se supone que todos los procesos utilizan correctamente el mutex; El progreso se define como la finalización de la ejecución de la sección crítica.
- Liberarse del estancamiento es una forma de vitalidad, aunque débil. Considere un sistema con múltiples procesos y una sola sección crítica, protegido por algún dispositivo de exclusión mutua . Se dice que un sistema de este tipo está libre de interbloqueo si, cuando un grupo de procesos compite por el acceso a la sección crítica en algún momento, algún proceso finalmente avanza en un momento posterior. Ese proceso no tiene por qué pertenecer al grupo antes mencionado; podría haber obtenido acceso en un momento anterior o incluso posterior. [6]
- La libertad de pasar hambre (o "desvío finito") es una garantía de vitalidad más fuerte que la libertad de estancamiento. Afirma que todos los procesos que compiten por el acceso a la región crítica eventualmente progresan. Cualquier sistema libre de inanición también está libre de interbloqueos. [6]
- Más fuerte aún es el requisito de bypass limitado. Esto significa que, si n procesos compiten por el acceso a la región crítica, entonces cada proceso avanza después de haber sido pasado por alto como máximo f ( n ) veces por otros procesos para alguna función f . [6]
Vivacidad y seguridad
Según B. Alpern, la libertad de punto muerto es una propiedad de seguridad . [7] Alpern supone que los estados del sistema se pueden dividir entre estados en los que está presente un punto muerto (estados rojos) y estados en los que no hay ningún punto muerto (estados verdes). La propiedad que establece que el sistema permanece para siempre en estados verdes (o, alternativamente, que el sistema nunca llega a estados rojos) es una propiedad de seguridad. Sin embargo, si uno no puede distinguir entre estados verde y rojo, la propiedad que dice que eventualmente uno de los procesos en el sistema evolucionará es una propiedad de vitalidad.
Distinción formal
La distinción entre seguridad y vitalidad puede establecerse formalmente mediante un predicado , dónde se refiere al tiempo. Dejarser el instante de tiempo a partir del cual se evalúan las propiedades de vida y seguridad. En los ejemplos siguientes, deje ser un proceso (o hilo) que uno quiere asegurar que está libre de interbloqueo.
Seguridad:
Ejemplo: medio " está en un estado de punto muerto en el momento ".
Vivacidad:
Ejemplo: medio " deja de esperar a la hora ".
Bypass acotado y adelantamiento acotado
También vale la pena señalar que la distinción entre la propiedad de vivacidad de la derivación limitada y la propiedad de seguridad de los adelantamientos limitados es sutil. La libertad de hambre junto con el adelantamiento limitado implica un desvío limitado (es decir, aunque el desvío limitado se clasifica como una propiedad de vida, en realidad es una mezcla de una propiedad de vida y una propiedad de seguridad). El adelantamiento limitado significa que después de que un proceso etiquetado declara el interés en ingresar a la sección crítica, cada uno de los otros procesos superará al proceso etiquetado un número limitado de veces antes de que el proceso etiquetado ingrese a la sección crítica. Tenga en cuenta que si al proceso etiquetado nunca se le otorga el permiso para ingresar a su sección crítica, los adelantamientos limitados aún pueden mantenerse. Por lo tanto, el adelantamiento limitado, en sí mismo, no es una propiedad de vitalidad. En un sistema en punto muerto, los adelantamientos limitados se mantienen trivialmente, ya que ningún proceso supera al otro, pero el bypass limitado no lo hace. [8]
Ver también
Referencias
- ^ Lamport, L. (1977). "Comprobación de la exactitud de los programas multiproceso". Transacciones IEEE sobre ingeniería de software (2): 125–143. CiteSeerX 10.1.1.137.9454 . doi : 10.1109 / TSE.1977.229904 .
- ^ Luís Rodrigues, Christian Cachin; Rachid Guerraoui (2010). Introducción a la programación distribuida confiable y segura (2. ed.). Berlín: Springer Berlín. págs. 22-24. ISBN 978-3-642-15259-7.
- ^ Bailis, P .; Ghodsi, A. (2013). "Coherencia eventual hoy: limitaciones, extensiones y más allá" . Cola . 11 (3): 20. doi : 10.1145 / 2460276.2462076 .
- ^ Alpern, B .; Schneider, FB (1987). "Reconociendo la seguridad y la vitalidad". Computación distribuida . 2 (3): 117. CiteSeerX 10.1.1.20.5470 . doi : 10.1007 / BF01782772 .
- ^ Gouda, Mohamed G. (1993). "Verificación de protocolo simplificada: un tutorial". Redes informáticas y sistemas RDSI . 25 (9): 969–980. doi : 10.1016 / 0169-7552 (93) 90094-k .
- ^ a b c Raynal, Michel (2012). Programación concurrente: algoritmos, principios y fundamentos . Springer Science & Business Media. págs. 10-11. ISBN 978-3642320262.
- ^ Alpern, B. (1985). "Definición de vivacidad". Cartas de procesamiento de información . 21 (4): 181-185. doi : 10.1016 / 0020-0190 (85) 90056-0 .
- ^ Fang, Y. (2006). Vivacidad por invariantes invisibles . Conferencia internacional sobre técnicas formales para sistemas en red y distribuidos . Apuntes de conferencias en informática. 4229 . págs. 356–371. doi : 10.1007 / 11888116_26 . ISBN 978-3-540-46219-4.