vivacidad
En computación concurrente , vivacidad se refiere a un conjunto de propiedades de sistemas concurrentes , que requieren que un sistema progrese a pesar del hecho de que sus componentes ("procesos") que se ejecutan concurrentemente pueden tener que "tomar turnos" en secciones críticas , partes del programa. que no puede ser ejecutado simultáneamente por múltiples procesos. [1] Las garantías de vida son propiedades importantes en los sistemas operativos y los sistemas distribuidos . [2]
De manera más general, una propiedad de vitalidad establece que "algo bueno eventualmente ocurrirá", 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 (ocurriendo el evento "malo"), pero una propiedad de vitalidad no se puede violar en una ejecución finita de un sistema distribuido porque el evento "bueno" aún podría ocurrir en algún tiempo más tarde. La consistencia eventual es un ejemplo de una propiedad de vitalidad. [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 vitalidad puede ser más difícil de establecer ya que ningún testigo finito 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 avance se define como la finalización de la ejecución del tramo crítico.
Según B. Alpern, la libertad de interbloqueo es una propiedad de seguridad . [7] Alpern supone que los estados del sistema se pueden dividir entre estados en los que hay interbloqueo (estados rojos) y estados en los que no hay interbloqueo (estados verdes). La propiedad que establece que el sistema permanece para siempre en estados verdes (o, alternativamente, que el sistema nunca alcanza estados rojos) es una propiedad de seguridad. Sin embargo, si uno no puede distinguir entre los estados verde y rojo, la propiedad que dice que eventualmente uno de los procesos en el sistema evolucionará es una propiedad de vida.
La distinción entre seguridad y vivacidad puede establecerse 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 asegurarse de que esté libre de interbloqueos.
La seguridad:
