Modelos de Consistencia de Memoria

Un modelo de consistencia de memoria especifica qué valores pueden observar las lecturas cuando hilos concurrentes acceden a memoria compartida, definiendo las garantías de ordenamiento en las que los programadores pueden confiar.

Definition

Un modelo de consistencia de memoria es una especificación formal de los valores que las operaciones de lectura pueden devolver en una ejecución concurrente, fijando los ordenamientos de los accesos a memoria que el lenguaje, el compilador y el hardware deben respetar.

Scope

Este tema abarca el espectro de modelos de consistencia, desde la consistencia secuencial hasta los modelos relajados y débiles, la relación "happens-before" y las garantías "data-race-free", los ordenamientos de memoria de hardware (como el orden total de almacenamiento), y los modelos de memoria a nivel de lenguaje para C++ y Java. Aborda por qué existen los modelos relajados, cómo las barreras de memoria ("fences") y las operaciones atómicas restauran el ordenamiento, y cómo razonar de manera sólida sobre la memoria concurrente.

Core questions

• ¿Qué ordenamientos de operaciones de memoria puede observar legalmente un programa?
• ¿Por qué existen los modelos de memoria relajados y qué permiten?
• ¿Cómo simplifica el razonamiento la garantía "data-race-free"?
• ¿Cómo imponen el ordenamiento las barreras de memoria ("fences") y las operaciones atómicas?

Key theories

Consistencia secuencial

Lamport definió la consistencia secuencial, en la que una ejecución multiprocesador debe aparecer como una única intercalación de operaciones que respeta el orden del programa de cada procesador, el modelo de línea de base intuitivo más fuerte.

Consistencia relajada y la garantía SC-for-DRF

Adve y Gharachorloo explican los modelos relajados y el principio de que los programas "data-race-free" se comportan como si fueran secuencialmente consistentes, conciliando el rendimiento con la programabilidad.

Modelos de memoria a nivel de lenguaje

Manson, Pugh y Adve formalizaron el modelo de memoria de Java utilizando una relación "happens-before", definiendo qué optimizaciones son legales y qué garantías reciben incluso los programas con condiciones de carrera ("racy programs").

Clinical relevance

Dado que los procesadores multinúcleo y los compiladores optimizadores reordenan las operaciones de memoria, los modelos de memoria del lenguaje son esenciales para escribir código concurrente correcto y portable. Indican a los programadores cuándo se requiere sincronización y definen las garantías que las bibliotecas y los entornos de ejecución pueden ofrecer.

History

Lamport formalizó la consistencia secuencial en 1979. A medida que el hardware adoptó ordenamientos relajados para el rendimiento, el tutorial de Adve y Gharachorloo de 1996 codificó el panorama de los modelos de consistencia y el marco "data-race-free". Los diseñadores de lenguajes luego incorporaron modelos de memoria en las especificaciones, con el modelo de memoria de Java (2005) y el modelo de memoria C++11 estableciendo el enfoque moderno.

Debates

Semántica de los programas con condiciones de carrera ("racy programs")

Una pregunta difícil es qué garantías, si las hay, dar a los programas que contienen condiciones de carrera; los modelos de lenguaje deben evitar valores "de la nada" ("out-of-thin-air") al mismo tiempo que permiten optimizaciones agresivas del compilador y del hardware.

Key figures

• Leslie Lamport
• Sarita Adve
• Kourosh Gharachorloo
• William Pugh
• Jeremy Manson

Seminal works

• lamport1979
• adve1996
• manson2005

Frequently asked questions

¿Por qué no todos los sistemas simplemente usan consistencia secuencial?

La consistencia secuencial prohíbe muchas optimizaciones de compilador y hardware que mejoran el rendimiento, por lo que la mayoría de los sistemas reales adoptan modelos relajados y proporcionan primitivas de sincronización para recuperar un ordenamiento más fuerte solo donde sea necesario.

¿Qué es la garantía "data-race-free"?

Bajo muchos modelos de memoria de lenguaje, se garantiza que un programa que no contiene condiciones de carrera (todos los accesos conflictivos están correctamente sincronizados) se comporta como si la memoria fuera secuencialmente consistente.