Vivacidad
En computación concurrente , la 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 después. 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 limitado, la violación de las propiedades de vida puede ser más difícil de establecer, ya que ningún testigo limitado puede usarse como prueba. [5]
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 ejecución final de la sección crítica.
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.
La distinción entre seguridad y vitalidad se puede establecer formalmente a través de un predicado , donde se refiere al tiempo. Sea el instante de tiempo a partir del cual se evalúan las propiedades de vida y seguridad. En los ejemplos a continuación, sea un proceso (o subproceso) que uno quiere asegurar que está libre de interbloqueo.
La seguridad:
