Dado un programa que consta de variables e instrucciones que modifican estas variables, y una primitiva de sincronización (un monitor, mutex, Java sincronizado o bloqueo de C #), ¿es posible demostrar que dicho programa es seguro para subprocesos?
¿Existe incluso un modelo formal para describir cosas como la seguridad del hilo o las condiciones de carrera?
Respuestas:
Probar que un programa es "seguro para subprocesos" es difícil. Sin embargo, es posible definir concreta y formalmente el término "carrera de datos". Y es posible determinar si una traza de ejecución de una ejecución específica de un programa tiene o no una carrera de datos en el tiempo proporcional al tamaño de la traza. Este tipo de análisis se remonta al menos a 1988: Barton P. Miller, Jong-Deok Choi, "Un mecanismo para la depuración eficiente de programas paralelos", Conf. en Prog. Lang. Dsgn. e Impl. (PLDI-1988): 135-144 .
Dada una traza de una ejecución, primero definimos un orden parcial antes de que suceda entre los eventos en la traza. Dados dos eventos y que ocurren en el mismo hilo, entonces o . (Los eventos en el mismo subproceso forman un orden total dado por la semántica secuencial del lenguaje de programación). Los eventos de sincronización (estos pueden ser mutex adquiere y libera, por ejemplo), dan un paso adicional entre subprocesos antes del orden parcial. (Si el hilo libera un mutex y luego el hilo adquiere ese mutex, decimos que el lanzamiento ocurre antes de la adquisición).a b a<b b<a S T
Luego, dado dos accesos a datos (lecturas o escrituras en variables que no son variables de sincronización) y que están en la misma ubicación de memoria, pero por diferentes subprocesos y donde o es una operación de escritura, decimos que hay un dato- carrera entre y si ni ni .a b a b a b a<b b<a
El estándar C ++ 11 es un buen ejemplo. (La sección relevante es 1.10 en el borrador de especificaciones que están disponibles en línea.) C ++ 11 distingue entre objetos de sincronización (mutexes y variables declaradas con un
atomic<>tipo) y todos los demás datos. La especificación C ++ 11 dice que el programador puede razonar acerca de los accesos a los datos en un rastro de un programa multiproceso como si fuera secuencialmente consistente si los accesos a los datos están libres de carrera de datos.La herramienta Helgrind (parte de Valgrind) realiza este tipo de detección basada en datos que sucede antes que otras herramientas comerciales (por ejemplo, Intel Inspector XE). Los algoritmos en las herramientas modernas se basan en mantener relojes vectoriales asociados con cada hilo y sincronización objeto. Creo que esta técnica de usar relojes vectoriales para la detección de la carrera de datos fue desarrollada por Michiel Ronsse; Koen De Bosschere: "RecPlay: un sistema de grabación / reproducción práctica totalmente integrado", ACM Trans. Comput Syst. 17 (2): 133-152, 1999 .
fuente
Desde el punto de vista práctico, existe un sistema de verificación VCC que se puede utilizar para probar formalmente la seguridad de subprocesos de los programas en C.
Esta es una cita del sitio web:
fuente
Esta es un área muy difícil para garantizar la corrección del programa en cuanto a descartar las condiciones de carrera, una especie de "talón de Aquiles" de procesamiento paralelo. El mejor enfoque para la corrección del programa es generalmente evitar las primitivas de bajo nivel y trabajar con patrones de diseño de alto nivel (por ejemplo, de bibliotecas) que garanticen la sincronización de subprocesos. Hay un modelo CSP, que comunica procesos secuenciales de Hoare, que tiene algunas pruebas de corrección dado que los desarrolladores se limitan al "marco". Tiene cierta similitud conceptual y origen / superposición cronológica con los "tubos y filtros" de Unix, aunque no ha encontrado (¿todavía?) Un vínculo directo entre los dos.
Otros dos marcos que intentan mejorar la corrección de paralelización a través de patrones de diseño y que tienen la mayoría de los algoritmos / patrones de diseño estándar / conocidos para este propósito:
fuente