2008-09-16 22 views
11

Los algoritmos de subprocesamiento múltiple son especialmente difíciles de diseñar/depurar/probar. El algoritmo de Dekker es un excelente ejemplo de lo difícil que puede ser diseñar un algoritmo sincronizado correcto. Los sistemas operativos modernos de Tanenbaum están llenos de ejemplos en su sección de IPC. ¿Alguien tiene una buena referencia (libros, artículos) para esto? ¡Gracias!Comprobación de la corrección de los algoritmos de subprocesamiento múltiple

+0

Prueba a elaborar. – GEOCHET

Respuesta

0

@Just in case: I is. Pero por lo que aprendí, hacerlo para un algoritmo no trivial es un gran dolor. Dejo ese tipo de cosas para las personas más inteligentes. Aprendí lo que sé de Parallel Program Design: A Foundation (1988) de KM Chandy, J Misra

13

Es imposible probar nada sin basarse en garantías, por lo que lo primero que debe hacer es familiarizarse con el modelo de memoria de su plataforma objetivo; Java y x86 tienen modelos de memoria sólidos y estandarizados: no estoy tan seguro de CLR, pero si todo lo demás falla, se basará en el modelo de memoria de la arquitectura de CPU de destino. La excepción a esta regla es si tiene la intención de utilizar un idioma que no permite ningún estado mutable compartido: he oído que Erlang es así.

El primer problema de concurrencia es el estado mutable compartido.

que se puede fijar por:

  • Haciendo estado inmutable
  • No compartir el estado
  • que guardan compartían estado mutable por el misma cerradura (dos cerraduras diferentes no pueden guardar la misma pieza de estado, a menos que siempre uso exactamente estos dos cerraduras)

El segundo prob El lem de concurrencia es una publicación segura. ¿Cómo haces que los datos estén disponibles para otros hilos? ¿Cómo se realiza una transferencia? Tendrás la solución a este problema en el modelo de memoria y (con suerte) en la API. Java, por ejemplo, tiene muchas formas de publicar estado y el paquete java.util.concurrent contiene herramientas específicamente diseñadas para manejar la comunicación entre hilos.

El tercer (y más difícil) problema de concurrencia es el bloqueo. El orden de bloqueo mal administrado es la fuente de bloqueos muertos. Puede probar analíticamente, basándose en las garantías del modelo de memoria, si los bloqueos son posibles o no en su código. Sin embargo, debe diseñar y escribir su código teniendo esto en cuenta, de lo contrario, la complejidad del código puede hacer que dicho análisis sea imposible de realizar en la práctica.

Luego, una vez que tenga, o antes de hacerlo, demuestre el uso correcto de concurrencia, tendrá que probar la corrección de un solo subproceso. El conjunto de errores que pueden ocurrir en una base de código simultáneo es igual al conjunto de errores de programa de subprocesamiento único, más todos los posibles errores de concurrencia.

2

Respuesta corta: es difícil.

Hubo un trabajo realmente bueno en DEC SRC Modula-3 y alerce de finales de los 80.

p. Ej.

Algunas de las buenas ideas de Modula - 3 lo están haciendo en el mundo de Java, p. JML, aunque "JML está actualmente limitado a la especificación secuencial", dice intro.

+0

El enlace gatekeeper.dec.com está roto, pero el informe DEC SRC sobre la comprobación estática extendida está disponible en http://research.microsoft.com/en-us/um/people/leino/papers/src-159.pdf . Estoy de acuerdo ESC fue realmente un buen trabajo. –

1

No tengo ninguna referencia concreta, pero es posible que desee examinar la teoría de Owicki-Gries (si le gusta la demostración de teoremas) o la teoría/álgebra de procesos (para la que también hay varias herramientas de verificación de modelos disponibles) .

3

"Principios de Programación Concurrente y Distribuida", M. Ben-Ari
ISBN-13: 978-0-321-31283-9
que tienen en los libros de safari en línea para la lectura:
http://my.safaribooksonline.com/9780321312839

+0

Eso era más o menos exactamente lo que estaba buscando. ¡Gracias! – Leandro

+0

@Leandro: si fue "exactamente exactamente" lo que estabas buscando, entonces puedes "aceptar" la respuesta. –

Cuestiones relacionadas