3.13.9 PD/Modelos y semántica formal

Temas:
Electivo

• Modelos formales de procesos y paso de mensajes, incluyendo algebras como Procesos Secuenciales de Comunicación (CSP) y Pi-Calculus
• Modelos formales de computación paralela, incluyendo la Máquina de Acesso Aleatorio Paralelo (PRAM) y alternativas como Bulk Synchronous Parallel (BSP)
• Modelos formales de dependencias computacionales.
• Modelos de consistencia (relajado) de memoria compartida y su relación con las especificaciones del lenguaje de programación.
• Criterios de corrección de algoritmos incluyendo (linearizability).
• Modelos de progreso algorítmic, incluyendo garantias de no bloqueo y equidad.
• Técnicas para especificar y comprobar las propiedades de corrección tales como atomicidad y la libertad de las carreras de datos.

Objetivos de Aprendizaje (Learning Outcomes):
Elective:

1. Modelar un proceso concurrente usando un modelo formal, por ejemplo, cálculo pi [Usar (Usage)]
2. Explicar las caracteristicas de un particular modelo paralelo formal [Familiarizarse (Familiarity)]
3. Formalmente modelar un sistema de memoria compartida para mostrar y éste es consistente [Usar (Usage)]
4. Usar un modelo para mostrar las garantias de progreso en un algoritmo paralelo [Usar (Usage)]
5. Usar técnicas formales para mostrar que un algoritmo paralelo es correcto con respecto a la seguridad o la propiedad liveness [Usar (Usage)]
6. Decidir si una ejecución específica es linealizable o no [Usar (Usage)]