Dos cajeros y un saldo de 100 euros
Una condición de carrera ocurre cuando dos procesos leen y escriben el mismo dato y el resultado depende del orden de sus pasos. Es difícil de ver porque casi siempre el orden es inofensivo.
Dos cajeros automáticos consultan el mismo saldo de 100 euros. Cada uno entrega 80. Si los dos leen el saldo antes de que cualquiera lo cambie, el banco paga 160 euros con un saldo de 100.
Al final de esta lección
Nota
Puedo encontrar una condición de carrera leyendo la traza que muestra SPIN.
Palabras clave
| Palabra | Qué significa | Ejemplo |
|---|---|---|
| Proceso | un programa que avanza paso a paso a su ritmo | |
| Entrelazado | un orden posible de los pasos de varios procesos | |
| Condición de carrera | un fallo que depende del orden de los pasos | |
| Aserción | una condición que debe ser cierta en un punto del programa | paid <= 100 |
| Traza | la lista de pasos que lleva hasta un error | |
| Promela | el lenguaje en que SPIN describe un modelo |
Las celdas que rellenan los estudiantes quedan en blanco en esta vista previa.
Dos procesos pueden entrelazarse de muchas formas
Cada cajero hace dos pasos: leer el saldo y escribir el nuevo. El sistema operativo puede intercalar esos cuatro pasos de varias maneras.
Una prueba normal ve un orden, el que le toca ese día. Un model checker, que es un programa que recorre todos los estados de un modelo, ve todos los órdenes.
Ejemplo: los seis órdenes de cuatro pasos
| Orden de los pasos | Qué pasa |
|---|---|
| A lee, A escribe, B lee, B escribe | Sano: B ve el saldo ya cambiado |
| B lee, B escribe, A lee, A escribe | Sano: A ve el saldo ya cambiado |
| A lee, B lee, A escribe, B escribe | Fallo: los dos leyeron 100 |
| A lee, B lee, B escribe, A escribe | Fallo: los dos leyeron 100 |
| B lee, A lee, A escribe, B escribe | Fallo: los dos leyeron 100 |
| B lee, A lee, B escribe, A escribe | Fallo: los dos leyeron 100 |
Las celdas que rellenan los estudiantes quedan en blanco en esta vista previa.
Un modelo en Promela es un programa pequeño
Un modelo deja fuera los detalles y se queda con lo que importa: aquí, el saldo, lo entregado y los dos pasos de cada cajero.
La aserción es la regla que el banco quiere cumplir. SPIN la comprueba en cada orden posible y, si una la rompe, guarda la traza que lleva hasta ella.
El modelo de los dos cajeros
byte balance = 100; // saldo de la cuenta
byte paid = 0; // euros que el banco ha entregado
active [2] proctype atm() { // dos cajeros, dos procesos
byte seen;
seen = balance; // paso 1: lee el saldo
if
:: seen >= 80 -> balance = seen - 80; paid = paid + 80 // paso 2: paga y escribe
:: else -> skip
fi;
assert(paid <= 100) // el banco nunca paga más de 100
}Crea una carpeta para el modelo
mkdir -p ~/atmSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Escribe el modelo en un archivo
printf '%s\n' 'byte balance = 100;' 'byte paid = 0;' '' 'active [2] proctype atm() {' ' byte seen;' ' seen = balance;' ' if' ' :: seen >= 80 -> balance = seen - 80; paid = paid + 80' ' :: else -> skip' ' fi;' ' assert(paid <= 100)' '}' > ~/atm/atm.pmlSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Comprueba todos los órdenes
spinrun ~/atm/atm.pml | grep -E 'assertion violated|errors:'Se muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
La traza muestra el orden que falla
Cuando SPIN encuentra un error, guarda la traza: la lista de pasos, uno por línea, que lleva desde el inicio hasta la aserción rota. Es el contraejemplo del modelo.
Leerla es la parte útil. Fíjate en qué paso aparece cada proceso y en qué valores tiene el saldo cuando escribe.
Reproduce la traza paso a paso
spin -t -p ~/atm/atm.pml | grep -E '^ *[0-9]+:'Se muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Mira los valores finales
spin -t -p ~/atm/atm.pml | grep -E 'balance = [0-9]|paid = [0-9]'Se muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Un error frecuente
Advertencia
Mucha gente cree que una condición de carrera solo ocurre si los procesos van muy rápido. No depende de la velocidad, sino del orden. Basta un orden malo entre todos los posibles para que el fallo exista, y SPIN lo encuentra aunque sea raro.
Con un solo cajero no hay carrera
Una carrera necesita al menos dos procesos que compartan un dato. Si dejas un solo cajero, solo hay un orden posible y la aserción se cumple.
El Run siguiente cambia en una copia del modelo los dos cajeros por uno, y SPIN responde con cero errores.
Cambia a un solo cajero
sed 's/active \[2\]/active [1]/' ~/atm/atm.pml > ~/atm/one.pmlSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Comprueba el modelo de un cajero
spinrun ~/atm/one.pml | grep -E 'errors:'Se muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.