Linealizabilidad

En la programación concurrente , una operación (o conjunto de operaciones) es linealizable si consiste en una lista ordenada de eventos de invocación y respuesta , que puede extenderse agregando eventos de respuesta de tal manera que:

1. La lista extendida se puede expresar nuevamente como un historial secuencial (es serializable ).
2. Esa historia secuencial es un subconjunto de la lista original sin extender.

De manera informal, esto significa que la lista de eventos sin modificar es linealizable si y solo si sus invocaciones fueron serializables, pero algunas de las respuestas del cronograma serial aún no han regresado. ^{[ 1 ]}

En un sistema concurrente, los procesos pueden acceder a un objeto compartido simultáneamente. Dado que varios procesos acceden a un mismo objeto, puede darse la situación de que, mientras un proceso accede al objeto, otro modifica su contenido. Una solución a este problema es hacer que un sistema sea linealizable. En un sistema linealizable, aunque las operaciones se superponen en un objeto compartido, cada operación parece ejecutarse instantáneamente. La linealizabilidad es una condición de corrección estricta que restringe las posibles salidas cuando varios procesos acceden a un objeto concurrentemente. Es una propiedad de seguridad que garantiza que las operaciones no finalicen de forma inesperada o impredecible. Si un sistema es linealizable, permite al programador razonar sobre él. ^{[ 2 ]}

La linealizabilidad fue introducida por primera vez como un modelo de consistencia por Herlihy y Wing en 1987. Incluía definiciones más restrictivas de atómico, como "una operación atómica es aquella que no puede ser (o no es) interrumpida por operaciones concurrentes", que suelen ser vagas en cuanto a cuándo se considera que una operación comienza y termina.

Un objeto atómico puede comprenderse de forma inmediata y completa a partir de su definición secuencial, como un conjunto de operaciones que se ejecutan en paralelo y que siempre parecen ocurrir una tras otra; no pueden surgir inconsistencias. En concreto, la linealizabilidad garantiza que los invariantes de un sistema se observen y se conserven en todas las operaciones: si todas las operaciones conservan individualmente un invariante, el sistema en su conjunto también lo hará.

Un sistema concurrente consiste en un conjunto de procesos que se comunican mediante estructuras de datos u objetos compartidos. La linealización es importante en estos sistemas, donde varios procesos pueden acceder a los objetos simultáneamente y el programador necesita prever los resultados esperados. La ejecución de un sistema concurrente genera un historial , una secuencia ordenada de operaciones completadas.

Un historial es una secuencia de invocaciones y respuestas que un conjunto de hilos o procesos realizan sobre un objeto. Una invocación puede considerarse como el inicio de una operación, y la respuesta como la señal de finalización de dicha operación. Cada invocación de una función tendrá una respuesta posterior. Esto puede utilizarse para modelar cualquier uso de un objeto. Supongamos, por ejemplo, que dos hilos, A y B, intentan obtener un bloqueo, desistiendo si ya está ocupado. Esto se modelaría como la invocación de la operación de bloqueo por ambos hilos, seguida de la recepción de una respuesta por cada hilo, uno exitoso y otro no.

Un historial secuencial es aquel en el que todas las invocaciones tienen respuestas inmediatas; es decir, se considera que la invocación y la respuesta ocurren instantáneamente. Un historial secuencial debería ser fácil de comprender, ya que no presenta concurrencia real; el ejemplo anterior no era secuencial y, por lo tanto, resulta difícil de analizar. Aquí es donde entra en juego la linealización.

Una historia es linealizable si existe un orden lineal.${\displaystyle \sigma }$de las operaciones completadas de tal manera que:

1. Por cada operación completada en${\displaystyle \sigma }$La operación devuelve el mismo resultado en la ejecución que si cada operación se completara una por una en orden.${\displaystyle \sigma }$.
2. Si una operación op ₁ se completa (recibe una respuesta) antes de que op ₂ comience (se invoque), entonces op ₁ precede a op ₂ en${\displaystyle \sigma }$. ^{[ 1 ]}

En otras palabras:

• Sus invocaciones y respuestas pueden reordenarse para generar una historia secuencial;
• que la historia secuencial es correcta según la definición secuencial del objeto;
• Si una respuesta precedió a una invocación en el historial original, aún debe precederla en la reordenación secuencial.

Nótese que los dos primeros puntos coinciden con la serializabilidad : las operaciones parecen ocurrir en algún orden. Es el último punto el que es exclusivo de la linealizabilidad y, por lo tanto, constituye la principal contribución de Herlihy y Wing. ^{[ 1 ]}

Consideremos dos maneras de reordenar el ejemplo de bloqueo anterior.

Reordenar la invocación de B tras la respuesta de A da como resultado un historial secuencial. Esto es fácil de comprender, ya que todas las operaciones se suceden en un orden obvio. Sin embargo, no coincide con la definición secuencial del objeto (no coincide con la semántica del programa): A debería haber obtenido el bloqueo correctamente y B debería haber abortado posteriormente.

Esta es otra historia secuencial correcta. También es una linealización, ya que coincide con la definición secuencial. Cabe señalar que la definición de linealizabilidad solo impide que las respuestas que preceden a las invocaciones se reordenen; dado que la historia original no tenía respuestas antes de las invocaciones, estas pueden reordenarse. Por lo tanto, la historia original es, en efecto, linealizable.

Un objeto (a diferencia de un historial) es linealizable si todos los historiales válidos de su uso pueden linealizarse. Esta afirmación es mucho más difícil de demostrar.

Los procesadores cuentan con instrucciones que permiten implementar algoritmos de bloqueo , sin bloqueo y sin espera . La capacidad de inhibir temporalmente las interrupciones , asegurando que el proceso en ejecución no pueda cambiar de contexto , también es suficiente en un monoprocesador . Estas instrucciones son utilizadas directamente por los desarrolladores de compiladores y sistemas operativos , pero también se abstraen y se exponen como bytecodes y funciones de biblioteca en lenguajes de alto nivel.

• lectura/escritura atómica;
• intercambio atómico (la instrucción RDLK en algunos mainframes Burroughs y la instrucción XCHG x86 );
• prueba y configuración ;
• obtener-y-agregar ;
• comparar e intercambiar ;
• cargar-enlace/almacenar-condicional .

La mayoría de los procesadores incluyen operaciones de escritura que no son atómicas con respecto a la memoria. Estas incluyen escrituras de varias palabras y operaciones con cadenas de caracteres. Si se produce una interrupción de alta prioridad cuando se completa una parte de la escritura, la operación debe finalizar cuando se devuelve el nivel de interrupción. La rutina que procesa la interrupción no debe modificar la memoria que se está modificando. Es importante tener esto en cuenta al escribir rutinas de interrupción.

Cuando hay varias instrucciones que deben completarse sin interrupción, se utiliza una instrucción de la CPU que desactiva temporalmente las interrupciones. Esto debe limitarse a unas pocas instrucciones y las interrupciones deben reactivarse para evitar tiempos de respuesta inaceptables o incluso la pérdida de interrupciones. Este mecanismo no es suficiente en un entorno multiprocesador, ya que cada CPU puede interferir con el proceso independientemente de si se producen interrupciones o no. Además, en presencia de una segmentación de instrucciones , las operaciones ininterrumpibles presentan un riesgo de seguridad, ya que potencialmente pueden encadenarse en un bucle infinito para crear un ataque de denegación de servicio , como en el caso del error de coma de Cyrix .

El estándar C y SUSv3 permiten sig_atomic_tlecturas y escrituras atómicas simples; no se garantiza que el incremento o decremento sea atómico. ^{[ 3 ]} En C11 se encuentran disponibles operaciones atómicas más complejas stdatomic.h. Los compiladores utilizan las características del hardware o métodos más complejos para implementar las operaciones; un ejemplo es libatomic de GCC.

El conjunto de instrucciones ARM proporciona LDREXinstrucciones STREXque se pueden usar para implementar el acceso atómico a la memoria mediante el uso de monitores exclusivos implementados en el procesador para rastrear los accesos a la memoria para una dirección específica. ^{[ 4 ]} Sin embargo, si se produce un cambio de contexto entre las llamadas a LDREXy STREX, la documentación indica que STREXfallará, lo que indica que la operación debe reintentarse. En el caso de la arquitectura ARMv8-A de 64 bits, proporciona LDXRinstrucciones STXRpara tamaños de byte, media palabra, palabra y doble palabra. ^{[ 5 ]}

La forma más sencilla de lograr la linealización es ejecutar grupos de operaciones primitivas en una sección crítica . Estrictamente hablando, se puede permitir cuidadosamente que las operaciones independientes se solapen en sus secciones críticas, siempre que esto no viole la linealización. Este enfoque debe equilibrar el costo de un gran número de bloqueos con los beneficios de un mayor paralelismo.

Otro enfoque, preferido por los investigadores (aunque todavía no muy extendido en la industria del software), consiste en diseñar un objeto linealizable utilizando las primitivas atómicas nativas que proporciona el hardware. Esto tiene el potencial de maximizar el paralelismo disponible y minimizar los costes de sincronización, pero requiere demostraciones matemáticas que muestren que los objetos se comportan correctamente.

Una prometedora combinación de estas dos técnicas consiste en proporcionar una abstracción de memoria transaccional . Al igual que con las secciones críticas, el usuario marca el código secuencial que debe ejecutarse de forma aislada de otros hilos. La implementación garantiza entonces que el código se ejecute de forma atómica. Este estilo de abstracción es común al interactuar con bases de datos; por ejemplo, al usar el Spring Framework , anotar un método con @Transactional garantiza que todas las interacciones con la base de datos se produzcan dentro de una única transacción . La memoria transaccional va un paso más allá, asegurando que todas las interacciones con la memoria se produzcan de forma atómica. Al igual que con las transacciones de base de datos, surgen problemas con respecto a la composición de transacciones, especialmente entre las transacciones de base de datos y las transacciones en memoria.

Un tema común al diseñar objetos linealizables es proporcionar una interfaz de todo o nada: o una operación se completa con éxito o falla y no hace nada. ( Las bases de datos ACID se refieren a este principio como atomicidad ). Si la operación falla (generalmente debido a operaciones concurrentes), el usuario debe volver a intentarlo, normalmente realizando una operación diferente. Por ejemplo:

• La operación de comparación e intercambio escribe un nuevo valor en una ubicación solo si el contenido de esta coincide con un valor anterior proporcionado. Esto se usa comúnmente en una secuencia de lectura-modificación-CAS: el usuario lee la ubicación, calcula un nuevo valor para escribir y lo escribe con una operación CAS (comparación e intercambio); si el valor cambia simultáneamente, la operación CAS fallará y el usuario lo intentará de nuevo.
• El patrón Load-link/Store-conditional se codifica de forma más directa: el usuario lee la ubicación con load-link, calcula un nuevo valor para escribir y lo escribe con store-conditional; si el valor ha cambiado simultáneamente, el SC (store-conditional) fallará y el usuario lo intentará de nuevo.
• En una transacción de base de datos , si la transacción no se puede completar debido a una operación concurrente (por ejemplo, en un interbloqueo ), la transacción se abortará y el usuario deberá intentarlo de nuevo.

• ÁCIDO
• transacción atómica
• Tipo de datos replicados sin conflictos (CRDT)
• Modelo de consistencia
• Actualización de copia de lectura (RCU)
• Leer, modificar, escribir
• Hora de verificación a hora de uso

• Herlihy, Maurice P.; Wing, Jeannette M. (1987). «Axiomas para objetos concurrentes». Actas del 14.º simposio ACM SIGACT-SIGPLAN sobre principios de lenguajes de programación - POPL '87 . págs. 13-26 . doi : 10.1145/41625.41627 . ISBN  978-0-89791-215-0. S2CID 16017451 . 
• Herlihy, Maurice P. (1990). Una metodología para implementar estructuras de datos altamente concurrentes . Vol.  25. pp. 197–206 . CiteSeerX 10.1.1.186.6400 . doi : 10.1145/99164.99185 . ISBN   978-0-89791-350-8.{{cite book}}: |journal=ignorado ( ayuda )
• Herlihy, Maurice P.; Wing, Jeannette M. (1990). "Linearizabilidad: una condición de corrección para objetos concurrentes". ACM Transactions on Programming Languages ​​and Systems . 12 (3): 463– 492. CiteSeerX 10.1.1.142.5315 . doi : 10.1145/78969.78972 . S2CID 228785 .  
• Aphyr. "Modelos de consistencia fuerte" . aphyr.com . Aphyr . Consultado el 13 de abril de 2018 .