Un probador y dos clientes a la vez
La exclusión mutua es la regla de que un solo proceso a la vez toque un dato compartido. Un cerrojo hace cumplir esa regla. Uno mal escrito falla en un solo orden entre muchos.
Una tienda tiene un probador con una luz que indica que está ocupado. Dos clientes miran la luz a la vez, la ven apagada y entran. Los dos comprobaron antes de que cualquiera la encendiera.
Al final de esta lección
Nota
Puedo escribir un cerrojo y comprobar con SPIN que no tiene errores.
Palabras clave
| Palabra | Qué significa | Ejemplo |
|---|---|---|
| Exclusión mutua | solo un proceso a la vez dentro de la sección crítica | |
| Sección crítica | la parte del programa que toca el dato compartido | |
| Cerrojo | una variable que impide que entren dos procesos a la vez | busy |
| Bloqueo mutuo | dos procesos esperan para siempre uno al otro | |
| Aserción | una condición que debe ser cierta en un punto | inside == 1 |
| Algoritmo de Peterson | un cerrojo para dos procesos hecho solo con variables |
Las celdas que rellenan los estudiantes quedan en blanco en esta vista previa.
Un cerrojo ingenuo: mirar y luego cerrar
La idea parece buena: el cliente espera a que la luz esté apagada y después la enciende. Son dos pasos, y entre ellos puede colarse el otro cliente.
Mira el modelo. Cada cliente espera con busy == false, enciende con busy = true, entra, comprueba con la aserción y sale.
El probador con un cerrojo ingenuo
bool busy = false; // la luz del probador
byte inside = 0; // cuántos clientes hay dentro
active [2] proctype client() {
busy == false; // paso 1: espera a que la luz esté apagada
busy = true; // paso 2: enciende la luz
inside++; // entra
assert(inside == 1); // dentro no puede haber dos
inside--;
busy = false // sale y apaga la luz
}Crea una carpeta para los modelos
mkdir -p ~/doorSe 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 ingenuo
printf '%s\n' 'bool busy = false;' 'byte inside = 0;' '' 'active [2] proctype client() {' ' busy == false;' ' busy = true;' ' inside++;' ' assert(inside == 1);' ' inside--;' ' busy = false' '}' > ~/door/naive.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 cerrojo ingenuo
spinrun ~/door/naive.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.
Mira dónde aparece la luz en la traza
spin -t -p ~/door/naive.pml | grep -E '^ *[0-9]+:.*busy'Se muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
El algoritmo de Peterson usa dos variables
Hay otra forma de hacer el cerrojo: que comprobar y cerrar sean un solo paso que nada interrumpe. El laboratorio te pide que la escribas tú.
El algoritmo de Peterson no la necesita. Cada cliente dice que quiere entrar y, justo después, cede el turno al otro. Solo entra cuando el otro no quiere o cuando el turno es suyo.
El cerrojo de Peterson
bool wants[2]; // wants[i]: el cliente i quiere entrar
byte turn = 0; // a quién le toca ceder
byte inside = 0;
active [2] proctype client() {
byte other = 1 - _pid;
wants[_pid] = true; // quiero entrar
turn = other; // pero cedo el turno al otro
(wants[other] == false || turn == _pid); // espero a que no quiera o a que me toque
inside++;
assert(inside == 1);
inside--;
wants[_pid] = false
}Escribe el modelo de Peterson
printf '%s\n' 'bool wants[2];' 'byte turn = 0;' 'byte inside = 0;' '' 'active [2] proctype client() {' ' byte other = 1 - _pid;' ' wants[_pid] = true;' ' turn = other;' ' (wants[other] == false || turn == _pid);' ' inside++;' ' assert(inside == 1);' ' inside--;' ' wants[_pid] = false' '}' > ~/door/peterson.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 cerrojo de Peterson
spinrun ~/door/peterson.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.
Un error frecuente
Advertencia
Mucha gente cree que un cerrojo sin aserciones rotas ya es correcto. No siempre. Puede dejar a los dos procesos esperando para siempre. Eso no rompe la aserción, pero SPIN lo avisa como invalid end state: un estado en que nadie puede avanzar y no todos han terminado.
Quitar el turno provoca un bloqueo mutuo
Prueba a quitar el turno al modelo de Peterson. Ahora cada cliente dice que quiere entrar y espera a que el otro no quiera.
Si los dos lo dicen a la vez, cada uno espera al otro. Ninguno entra y ninguno sale. Los dos siguientes Runs hacen el cambio con sed y lo comprueban.
Quita el turno al modelo
sed '/turn = other/d; s/ || turn == _pid//' ~/door/peterson.pml > ~/door/stuck.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 sin turno
spinrun ~/door/stuck.pml | grep -E 'invalid end state|errors:'Se muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.