Esta preparación de examen está patrocinada por el gran salvador Bocata.

Un mismo ejercicio donde hay que hacer:

• Especificación LTL
• Máquinas de estados
• Promela
• Código C
• Tablas, para calcular tiempos

LTL

• [] Define que es global
• <> Esto es eventualmente, por ejemplo como consecuencia de. La consecuencia es aposteriori, no inmediata (para preguntas de tests).
• U until, hasta
• x siguiente estado, no se ve apenas
• || or
• && and
• ! or
• = asignar
• == comprobar
• -> implicar

Algunos ejemplos:

• Si el pedido está terminado, los LEDS de recogida se enciende: [] ((pedido==1) -> <> (leds = 1))
• Si el nivel de bateria es menor de 10%, el LED de batería baja se encienden: [] ((bat < 10) -> <> (led_bat = 1))
• La detección de distancia demasiado cercana sigue funcionando siempre: si se producen violaciones de la distancia de seguridad infinitamente a menudo, se seguirán generando las alarmas infinitamente a menudo: [] ((alarma = 1) U (distancia==0))
• El sistema continúa enviando la temperatura mientras la bateria esté por encima del 10% (si la batería se mantiene encima del 10%, se envía la temperatura infinitamente a menudo): [] ((enviarTemp = 1) U (bateria < 10))
• El coche eléctrico no puede estar cargando si está en moviento: [] (!cargando || !movimiento)

Máquinas de estados

Hay que tener en cuenta:

• El estado inicial
• El periodo de reloj

Las cosas periódicas se hacen con las siguientes sentencias:

• timer = now Para actualizar el timer
• next = timer + 1 seg Asigno el tiempo de comprobación
• timer >= next Compruebo si salta el timer

Los estados tienen condición barra consecuencia, son máquinas meeley, cambian en la transición.

Un ejercicio de ejemplo:

Preguntar periódicamente (cada segundo) si el pedido está finalizado. De ser así, debe hacer parpadear los LEDs (un cambio cada 250ms) hasta que el dispositivo se lleve al punto de recogida.

• La variable pedido_terminado se pone a 1 si el pedido está listo y pueden pasar a recogerlo al punto de recogida.
• La variable punto_recogida se pone a 1 si el dispositivo está en el punto de recogida.
• La variable leds_recogida permite poner a 1 o 0 los LEDS que indican que el pedido está listo para recoger.

Promela

Te piden hacer promela para la máquina de estados. Es bastante probable que al final del examen den una hoja con ejemplos de promela.

active proctype pedido () {
    timer = now;
    next = timer + 4;
    
    state = A;
    do
    ::(state == A) -> atomic {
        if
        ::(pedido == 1) -> led = 1; state = B;
        ::(pedido != 1) -> timer = now; next = timer + 4; state = C;
        fi
    }
    ::(state = B) -> atomi {
        if
        ::(recogida == 1) -> led_rec = 0; state = A;
        ::(recogida != 1) -> timer2 = now; leds_r!=leds_r; next2 = timer2 + 1; state = D;
        fi
    }
    ::(state = D) -> atomic {
    //STUFF
    }
    od
}

active proctype entorno(){
    // Se utiliza para inicializar variables. Todas las variables que se comprueban se les da un valor
    now = 0;
    do
    :: pedido_terminado = 1;
    :: punto_recogida = 1;
    :: skip;
    od
    now = now + 250
}

Tablas

Las tablas se pueden resolver con:

• Threads
  • Herencia de prioridad
  • Techo de prioridad inmediato
• Reactor
• Ejecutivo cíclico

Algunas definiciones:

• T = periodo de cada tarea
• C = Tiempo de ejecución en caso peor
• D = Plazo de respuesta de cada tarea
• P = Prioridad
• B = Bloqueo
• R = Tiempo de respuesta
• r1, r2, r3 = Recursos compartidos

Las tablas se hacen de la siguiente manera para threads:

• A mismos valores de D, no se dan prioridades iguales.
• El D más alto, mínima prioridad.
• El techo de prioridad se calcula como la prioridad de la tarea de máxima prioridad que utiliza el recurso.
• El bloqueo se calcula distinto dependiendo de cómo sea el ejercicio. Tenemos que mirar a las casillas de los recursos con techo de prioridad ≥ que la prioridad de la tarea, y a tareas con < prioridad.
  • Herencia de prioridad -> Contamos solo 1 bloqueo por tarea y 1 bloqueo por recurso, nos quedamos con el máximo. La última tarea siempre tiene bloque 0.
  • Techo de prioridad inmediato -> Se coje el máximo de todas las tareas y recursos.
• La R se calcula de la siguiente forma->
  • \(R_i = C_i + B_i + I_i\), donde \(I_i\) es interferencia con tareas de mayor prioridad. \(I_i = \sum_{k = i+1}^{i_{max}} ceil(R_i / T_k) \cdot C_k\). Para iniciar el bucle recursivo se empieza con \(R_i = 1\) dentro del ceil, y se consigue el resultado cuando se estabilice.
  • Se considera planificable si la fila de R’s vale menos que la fila de D’s.
  • En reactor se calcula distinto. El bloqueo se sacará mirando el mayor Ci de las tareas de menor prioridad, hay una imagen abajo que lo pone .Calculo la R, en este caso será \(R_i = W_i + F_i\) tal que \(W_i = C_i - F_i + B_i + I_i\)

Para reactor:

• Se pone una columna de \(F_i\) que valdrá lo mismo que la columna C.
• No se tiene columna de bloqueos.
• \(R_i = W_i + F_i\) tal que \(W_i = C_i - F_i + B_i + I_i\). Y luego se hará también \(I_i = \sum_{k = i+1}^{i_{max}} ceil(W_i / T_k) \cdot C_k\)

Para ejecutivo cíclico. Se utiliza poco.

• Hiperperiodo \(H = mcm(T_i)\). Mínimo valor divisible por todos.
• \(H_s = mcd (T_i)\). El máximo que divida a todos.
• \(frames =\frac{H}{H_s}\)
• Si una tarea no nos entra la dividimos en 2. Tenemos que hacer que la tarea al completo se haga antes de su límite.

Del código cíclo el ejemplo siguiente:

Un ejemplo de herencia de prioridad (arriba) y techo de prioridad inmediato (abajo)

Código en C

Código de ejemplo de la tabla del ejecutivo cíclico.

int main (){
    fsm_t t1 = fsm_t_new();
    fsm_t t2 = fsm_t_new();
    fsm_t t3 = fsm_t_new();
    fsm_t t4 = fsm_t_new();
    
    int frame = 0;
    next = now + 500; // Se suma el hiperperiodo
    while(1){
        switch(frame){
            case 0:
                t1.fire();
                t2.fire();
                t3.fire();
                break;
            case 1:
                t3.fire();
                t4.fire();
                break;
            case 2:
                t2.fire();
                t3.fire();
                break;
            case 3:
                t1.fire();
                t3.fire();
                t4.fire();
                break;
            case 4:
                t2.fire();
                t3.fire();
                break;
            case 5:
                t3.fire();
                t4.fire();
                break;
        }
        next = next + 500;  // Comprobar esto que no me queda claro que sea así
        delay_until(next);
        frame = (frame+1)%6;
    }
}

Test

Algunas cosas para hacer el test:

• Las condiciones de guarda no pueden asignar variables

Ventajas y desventajas de las diferentes implementaciones:

• Ejectutivo cíclico
  • Es fácil de depurar
  • No hay exclusión mutua porque solo una tarea accede a los recursos cada vez
  • Optimiza memoria
  • Los periodos deben de ser armónicos
  • Es poco flexible y difícil de mantener
  • No hay concurrencia en la ejecución
• Reactor
  • Mejora la planificabilidad
  • Mejora la latencia y tiempos de computo
  • Mejora eficiencia
  • Consume casi lo mismo que el ejecutivo cíclico
  • Los periodos pueden no se armónicos
  • Simplifica el diseño
  • El coste de ofrecer un cambio de contexto puede ser alto, por lo que el tiempo de respuesta puede alargarse.
  • Es más dificil de depurar.
• Prioridades fijas y desalojo
  • Muy flexible
  • Usa todos los cores
  • Menor latencia en caso peor
  • Aumenta el consumo y la sobrecarga del sistema
  • Necesita mecanismo de sincronización

Orden de menor a mayor tiempo de respuesta -> Prioridades fijas y desalojo < Reactor < Ejecutivo cíclico

Orden de menor a mayor consumo (periodos armónicos) -> Ejecutivo cíclico < Reactor < Prioridades fijas y desalojo

Orden de menor a mayor tiempo de respuesta (periodos NO armónicos) -> **Reactor < Ejecutivo cíclico < Prioridades fijas y desalojo **

Orden de menor a mayor tamaño de código (periodos armónicos) -> Ejecutivo cíclico < Reactor < Prioridades fijas y desalojo

Orden de menor a mayor tamaño de código (periodos NO armónicos) -> **Reactor < Ejecutivo cíclico < Prioridades fijas y desalojo **

Para verificar que el modelo cumple la especificación se ejecuta lo siguiente:

$ spin -a model.pml
$ gcc -o pan pan.c
$ ./pan -a -f

Para simular una traza de ejecución que no cumple la propiedad:

$ spin -t model.pml

¿Qué estrategia de asignación de prioridades es óptima? -> Asignación de prioridad monótona en frecuencia: a menor periodo (D), mayor prioridad.

¿Y si los plazos (D) son mayores a los periodos (T)? -> No hay asignación óptima, debemos probar para cada caso.

Una tarea que no usa recursos compartidos ¿Puede sufrir bloqueos? -> Sí, si una tarea menor prioridad tiene un recurso compartido con otra tarea de prioridad mayor, puede heredar la mayor prioridad al acceder al recurso y bloquear la terea que no accede a recursos compartidos.

El bloque máximo con protocolo de techo de prioridad inmediato, ¿puede ser mayor que si usamos herencia de prioridad? -> No, con techo de prioridad el bloqueo máximo puede ser MENOR o IGUAL al bloque máximo con herencia de prioridad.

Si no hay recursos compartidos en todo el sistema, ¿puede haber bloqueo? -> No, solo interferencias

De manera general, ¿Cuándo es necesario añadir un estado a una máquina de estados? -> Un estado por cada forma diferente de reaccionar ante los eventos.

Las máquinad de estados extendidas (con memoria, con variables) -> Simplifican el modelado de un comportamiento, aunque no el número de estados total, puesto que las variables forman parte del estado.