1. Por qué un simulador de exclusión mutua
Las condiciones de carrera son no deterministas: dependen del intercalado exacto, que cambia en cada ejecución. Un programa puede pasar mil pruebas y fallar en la mil uno. Por eso, la verificación por pruebas no es suficiente: hay que verificar todos los intercalados posibles.
El simulador de este tema hace exactamente eso: explora todos los estados posibles de cada algoritmo y verifica si cumple los tres requisitos (exclusión mutua, progreso, espera acotada). Si encuentra un estado que viola un requisito, lo muestra.
Este enfoque se llama verificación por exploración de estados (state space exploration) o model checking. Es la técnica que usan las herramientas profesionales (Spin, TLA+) para verificar protocolos de concurrencia.
Las pruebas ejecutan el programa con entradas específicas y verifican el resultado. La verificación formal explora todos los estados posibles y verifica que los requisitos se cumplen en todos. Las pruebas pueden pasar y el programa aún tener errores; la verificación formal es concluyente.
2. El modelo: estados y transiciones
El simulador modela cada algoritmo como una máquina de estados. Un estado es una configuración completa del sistema en un instante dado. Una transición es el cambio de un estado a otro cuando un hilo ejecuta una instrucción.
El simulador explora todos los estados alcanzables desde el estado inicial, siguiendo todas las transiciones posibles. Si encuentra un estado que viola un requisito, lo reporta.
El modelo simplifica el algoritmo a sus operaciones esenciales: leer, escribir y evaluar variables compartidas. No modela el código de la sección crítica (se asume que es arbitrario).
3. Qué es un estado
Un estado incluye:
- Valores de las variables compartidas: bandera[0], bandera[1], turno, etc.
- Estado de cada hilo: qué instrucción está a punto de ejecutar (PC).
- Región crítica: qué hilo(s) están en la sección crítica.
Por ejemplo, para Peterson con dos hilos, un estado podría ser:
bandera[0] = 1, bandera[1] = 1, turno = 1
Hilo 0: en el while (esperando)
Hilo 1: en la sección crítica
Región crítica: Hilo 1El número de estados crece exponencialmente con el número de hilos y variables, por eso el simulador se limita a dos hilos.
4. Cómo se verifica un algoritmo
El verificador explora todos los estados y verifica tres propiedades:
- Exclusión mutua: en ningún estado hay dos hilos en la sección crítica. seguridad
- Progreso: si ningún hilo está en la sección crítica y hay hilos que quieren entrar, existe al menos una transición que lleva a un hilo a la sección crítica. vivacidad
- Espera acotada: para cada hilo que quiere entrar, existe un límite finito de transiciones antes de que entre. equidad
Si alguna propiedad se viola, el verificador muestra el estado y la transición que la violan.
5. Los algoritmos a verificar
El simulador verifica cuatro algoritmos:
| Algoritmo | Variables | Requisitos que cumple |
|---|---|---|
| Variable de turno | turno | Exclusión mutua ✓, Progreso ✗, Espera acotada ✗ |
| Bandera de intención | bandera[0], bandera[1] | Exclusión mutua ✗, Progreso ✓, Espera acotada ✓ |
| Turno + bandera | turno, bandera[0], bandera[1] | Exclusión mutua ✓, Progreso ✓, Espera acotada ✗ |
| Peterson | turno, bandera[0], bandera[1] | Exclusión mutua ✓, Progreso ✓, Espera acotada ✓ |
6. Verificación del intento 1: variable de turno
La variable de turno cumple la exclusión mutua pero viola el progreso y la espera acotada. El verificador encuentra un estado donde el hilo 1 quiere entrar pero no puede porque el turno es del hilo 0, y el hilo 0 no quiere entrar.
Estado que viola el progreso:
turno = 0
Hilo 0: en sección no crítica (no quiere entrar)
Hilo 1: quiere entrar (en protocolo de entrada)
Región crítica: vacía
→ El hilo 1 no puede entrar porque turno != 1, aunque la sección crítica esté libre.
→ Violación del progreso.7. Verificación del intento 2: bandera de intención
La bandera de intención cumple el progreso y la espera acotada pero viola la exclusión mutua. El verificador encuentra un estado donde ambos hilos están en la sección crítica a la vez.
Estado que viola la exclusión mutua:
bandera[0] = 1, bandera[1] = 1
Hilo 0: en la sección crítica
Hilo 1: en la sección crítica
→ Ambos hilos levantaron sus banderas a la vez y pasaron el while.
→ Violación de la exclusión mutua.8. Verificación del intento 3: turno + bandera
La combinación cumple la exclusión mutua y el progreso pero viola la espera acotada. El verificador encuentra un estado donde un hilo espera indefinidamente.
Estado que viola la espera acotada:
turno = 1, bandera[0] = 1, bandera[1] = 1
Hilo 0: quiere entrar, espera (turno == 1)
Hilo 1: entra y sale repetidamente
→ El hilo 1 puede entrar y salir indefinidamente, mientras el hilo 0 espera.
→ Violación de la espera acotada.9. Verificación de Peterson
Peterson cumple los tres requisitos. El verificador explora todos los estados y no encuentra ninguna violación:
- Exclusión mutua: en ningún estado hay dos hilos en la sección crítica.
- Progreso: si nadie está en la sección crítica y alguien quiere entrar, existe una transición que lleva a un hilo a la sección crítica.
- Espera acotada: para cada hilo que quiere entrar, el número de veces que el otro puede entrar antes es acotado (a lo sumo 1).
El verificador confirma que Peterson es correcto para dos hilos.
10. Simulador interactivo
Este simulador verifica los cuatro algoritmos y muestra los resultados:
Simulador · verificador de exclusión mutua
| Requisito | Resultado | Explicación |
|---|
11. Extensiones posibles
- Más hilos: extender el verificador para 3 o más hilos.
- Otros algoritmos: verificar el algoritmo de Lamport, Eisenberg-McGuire, etc.
- Visualización de estados: mostrar el grafo de estados y las transiciones.
- Verificación de propiedades adicionales: ausencia de deadlock, ausencia de livelock.
- Model checking: implementar un model checker básico (como Spin).
12. Resumen
- El simulador explora todos los estados posibles de cada algoritmo.
- Verifica los tres requisitos: exclusión mutua, progreso, espera acotada.
- La variable de turno cumple exclusión mutua pero viola progreso y espera acotada.
- La bandera de intención cumple progreso y espera acotada pero viola exclusión mutua.
- La combinación cumple exclusión mutua y progreso pero viola espera acotada.
- Peterson cumple los tres requisitos para dos hilos.
- La verificación por exploración de estados es concluyente, a diferencia de las pruebas.
13. Preguntas de repaso
Intenta responder cada una antes de abrir la respuesta.
1. ¿Qué es la verificación por exploración de estados?
Explorar todos los estados posibles de un algoritmo y verificar que los requisitos se cumplen en todos.
2. ¿Qué es un estado en el simulador?
Una configuración completa del sistema: valores de variables compartidas, estado de cada hilo y región crítica.
3. ¿Qué es una transición?
El cambio de un estado a otro cuando un hilo ejecuta una instrucción.
4. ¿Qué algoritmos verifica el simulador?
Variable de turno, bandera de intención, turno + bandera, y Peterson.
5. ¿Qué algoritmo cumple los tres requisitos?
Peterson (para dos hilos).
6. ¿Qué viola la variable de turno?
El progreso y la espera acotada.
7. ¿Qué viola la bandera de intención?
La exclusión mutua.
8. ¿Qué viola la combinación de turno y bandera?
La espera acotada.
9. ¿Por qué la verificación formal es mejor que las pruebas?
Porque explora todos los estados, no solo los que se prueban. Las pruebas pueden pasar y el programa aún tener errores.
10. ¿Qué es model checking?
Una técnica de verificación formal que explora el espacio de estados de un sistema para verificar propiedades.
Para practicar
- Ejecuta el simulador para cada algoritmo y verifica los resultados.
- Dibuja el grafo de estados de la variable de turno.
- Explica por qué la verificación por exploración de estados es concluyente.
- Investiga qué es Spin y cómo se usa para verificar protocolos.
- Modifica el simulador para verificar un algoritmo de Lamport.
- Implementa la visualización del grafo de estados.