Next: Preguntas cortas Up: Examen de Programación Concurrente Previous: Controlador de un ascensor

Subsecciones

- Notas
- Se pide:
- Solución propuesta:

#
El almacén de las vacas locas

Debido al problema de contaminación priónica en vacas, el número de sacrificios está causando escasez de recintos que puedan ser dedicados a almacenarlas. El gobierno decide autorizar el uso de salas de mataderos para almacenar reses sanas y enfermas, con la restricción de que una sala sólo debe albergar, en cada momento, vacas de una clase.

Con objeto de optimizar el uso de las salas no se hace una asignación estricta de salas a tipos de vacas, sino que cuando una sala queda vacía (porque todas las vacas que había allí ha sido llevada a cremar o a una carnicería) se puede reutilizar para guardar indistintamente vacas sanas o contaminadas (tras una desinfección de la que no tenemos que ocuparnos). Previendo la posibilidad de fallos humanos, se decide automatizar el sistema de asignación de salas con un sistema de control. El funcionamiento del sistema es el siguiente: se señala, al llegar, si se quiere depositar o retirar una vaca y si ésta está contaminada o no. El sistema asignará una sala de la que extraer o recoger. El diseño del recurso al que se ha llegado es el siguiente:

    C-TADSOL AlmacenVacas

    C-Operaciones

    ACCION DejarLoca:TipoAlm    TipoNumSala

    ACCION RetirarLoca:TipoAlm    TipoNumSala

    ACCION DejarNormal:TipoAlm    TipoNumSala

    ACCION RetirarNormal:TipoAlm    TipoNumSala

    Operaciones

    ACCION Iniciar:TipoAlm

    CONCURRENCIA:

    ninguna

    TRANSACCIONES:

    DejarLoca

    RetirarLoca

    DejarNormal

    RetirarNormal

    Dominio:

    Tipo: 		 TipoAlm = Secuencia(TipoSala)

    TipoNumSala = {1..NumSalas}

    Donde:

    TipoSala = (nvacas: TipoTam   tipo:TipoVaca)

    TipoVaca = loca  normal

    TipoTam  = {0..TamSala}

    TamSala = ...

    NumSalas = ...

    Invariante:

    CPRE: cierto

    Iniciar(alm)

    POST: Todas las salas estan inicialmente vac'ias

    POST:

    CPRE: Hay una sala de vacas locas con espacio u otra  cualquiera vac'ia

    CPRE:

    DejarLoca(alm, sala)

    POST: Se utiliza la sala de vacas locas o la sala  vac'ia

    POST:

    CPRE: Hay una sala con vacas locas

    CPRE:

    RetirarLoca(alm, sala)

    POST: Se retira una vaca de una sala con vacas locas

    POST:

    CPRE: Hay una sala de vacas normales con espacio u otra  cualquiera vac'ia

    CPRE:

    DejarNormal(alm, sala)

    POST: Se utiliza la sala de vacas normales o la sala  vac'ia

    POST:

    CPRE: Hay una sala con vacas normales

    CPRE:

    RetirarNormal(alm, sala)

    POST: Se retira una vaca de una sala con vacas normales

    POST:

## Notas

- Con objeto de agilizar la entrada y salida de vacas se impone una condición adicional, no contemplada en el recurso por razones de claridad: no se deben ocupar todas las salas con vacas de un solo tipo.

- Asimismo es necesario tener en cuenta la posibilidad de un despertar en cascada al retirar una vaca loca o normal.

- No es necesario codificar operaciones rutinarias, como buscar una sala vacía. Pueden darse nombres significativos a esas operaciones y dejar escrito en lenguaje natural (pero preciso) el significado que se le asume.

## Se pide:

- Realizar la tabla de bloqueos y desbloqueos del recurso, tal y como se ha especificado formalmente.
- Estudiar cómo se puede asegurar la vivacidad del sistema, respetando la restricción introducida en la nota anterior.
- Codificar las operaciones anteriores como procedimientos Cc Modula usando monitores, basándose en la especificación, las tablas de bloqueos y desbloqueos y las consideraciones sobre vivacidad anteriores.

## Solución propuesta:

#### Tabla de bloqueos

Operación | CPRE informal | CPRE codificada | Condition
--- | --- | --- | ---
DejarLoca(alm, sala) |
Hay una sala de vacas locas con espacio u otra cualquiera vac'ia
| `dejaresperando[loca]`
RetirarLoca(alm, sala) |
Hay una sala con vacas locas
| `retiraresperando[loca]`
DejarNormal(alm, sala) |
Hay una sala de vacas normales con espacio u otra cualquiera vac'ia
| `dejaresperando[normal]`
RetirarNormal(alm, sala) |
Hay una sala con vacas normales
| `retiraresperando[normal]`

DejarLoca(alm, sala) CPRE(DejarLoca) `dejaresperando[loca]`
DejarNormal(alm, sala) CPRE(DejarNormal) `dejaresperando[normal]`
RetirarLoca(alm, sala) CPRE(RetirarLoca) `retiraresperando[loca]`
RetirarNormal(alm, sala) CPRE(RetirarNormal) `retiraresperando[normal]`
DejarLoca(alm, sala) POST(DejarLoca)
Despertar en cascada
CPRE(DejarNormal) No aplicable
cierto
CPRE(RetirarNormal) No aplicable
DejarNormal(alm, sala) POST(DejarNormal)
CPRE(DejarLoca) No aplicable
Despertar en cascada
CPRE(RetirarLoca) No aplicable
cierto
RetirarLoca(alm, sala) POST(RetirarLoca)
cierto
CPRE(RetirarLoca) No aplicable
CPRE(RetirarNormal) No aplicable
RetirarNormal(alm, sala) POST(RetirarNormal)
cierto
CPRE(RetirarLoca) No aplicable
CPRE(RetirarNormal) No aplicable

Para asegurar la vivacidad se debe respetar en todo momento la restricción introducida en la primera nota. Esta restricción se respetará si en todo momento el número de salas dedicadas a un tipo de vaca es menor o igual a NumSalas - 1. Como el número de salas dedicadas a un tipo de vaca puede aumentar como consecuencia de ejecutar un operación Dejar, debemos modificar las CPREs de las operaciones Dejar de manera que recojan la restricción. Al modificar las CPREs, vamos a introducir dos contadores en el estado del recurso, `nosalaslocas` y `nosalasnormales`, que indicarán el número de salas dedicadas a vacas locas y a vacas normales, respectivamente. Lógicamente, estos contadores deben ser inicializados a cero. Dado que estos dos contadores deben formar parte del tipo TipoAlm, tenemos que modificar la definición del tipo TipoAlm:

Las CPREs de las operaciones Dejar quedarán así:

CPRE(DejarLoca):
  Hay una sala de vacas locas con espacio, u otra cualquiera vacía y el número de salas dedicadas a vacas locas es menor o igual que NumSalas - 2.

CPRE(DejarNormal):
  Hay una sala de vacas normales con espacio, u otra cualquiera vacía y el número de salas dedicadas a vacas normales es menor o igual que NumSalas-2.

Dado que estas operaciones pueden incrementar el número de salas dedicadas a las vacas de un tipo, debemos también modificar las postcondiciones de las operaciones Dejar:

POST(DejarLoca):
  Se utiliza la sala de vacas locas, o la sala vacía y se incrementa el número de salas dedicadas a vacas locas.

POST(DejarNormal):
  Se utiliza la sala de vacas normales, o la sala vacía y se incrementa el número de salas dedicadas a vacas normales.

Asimismo, también debemos modificar las postcondiciones de las operaciones Retirar, ya que puede suceder que tras retirar una vaca de un tipo, una sala se queda vacía, y por lo tanto se decremente el número de salas dedicadas a dicho tipo.

POST(RetirarLoca):
  Se retirar una vaca de una sala con vacas locas

POST(RetirarNormal):
  Se retirar una vaca de una sala con vacas normales

Estos cambios introducidos en las CPREs y las postcondiciones de las operaciones Dejar, y en las postcondiciones de las operaciones Retirar van a afectar a dos condiciones de desbloqueo. Si al retirar una vaca de un tipo, se queda vacía la sala, entonces para poder desbloquear una operación Dejar del otro tipo de vacas, debemos comprobar .

#### Código del programa

    CONST
      normal = 1;

    loca = 2;

    NUMSALAS = ...;

    TAMSALA = ...;

    (* Tipos de uso general *)

    TYPE

    TipoVaca = [normal..loca];

    TipoNumSala = [1..NUMSALAS];

    (***********************************************************************)
    (*      Implementacion del gestor del almacen                          *)

    (***********************************************************************)

    TYPE TipoGestorAlmacen = MONITOR

    (* Constantes, tipos y nombres de procedimientos a usar dentro del monitor *)

    IMPORT

      normal, loca, TipoVaca, TipoNumSala, NUMSALAS, TAMSALA;

    (* Procedimientos p'ublicos *)

    PUBLIC

    DejarNormal,

    DejarLoca,

    RetirarNormal,

    RetirarLoca;

    (*  Tipos y variables privadas del monitor. *)

    TYPE

    TipoTamSala = [0..TAMSALA];

    TipoSala = RECORD
      npiezas : TipoTamSala;

    tipo : TipoVaca;

    END;

    VAR (* Estas variables se utilizan en la inicializaci'on *)

    i: TipoNumSala;

    j: TipoVaca;

    (* Variables que definen el estado interno del recurso *)

    STATE

    almacen: ARRAY TipoNumSala OF TipoSala;

    nodejaresperando: ARRAY TipoVaca OF CARDINAL;

    dejaresperando: ARRAY TipoVaca OF CONDITION;

    retiraresperando: ARRAY TipoVaca OF CONDITION;

    saladisponible: TipoNumSala;

    nosalas: ARRAY TipoVaca OF CARDINAL;

    (* Implementaci'on de las operaciones del recurso *)

    PROCEDURE BuscarSalaNoLlena (tipo: TipoVaca) : CARDINAL;
    (**
      * PRE: nosalas(tipo)  NUMSALAS - 1
      BuscarSalaNoLlena (almacen, sala, nosalas)
      POST: Devuelve la sala no llena que contiene m'as vacas de la clase "tipo".
     * 		 Si no existe ninguna sala con vacas de la clase "tipo",
     * 		 se devuelve cualquier sala vac'ia siempre que el n'umero de salas asignadas a

     * 		 las vacas de la clase "tipo" no supere el tope NUMSALAS-1. Si tampoco
     * 		 existe una sala vac'ia que satisfaga el requisito anterior, se devuelve
     * 		 cero.
     * POST:
     *   resultado =
      **)

    END BuscarSalaNoLlena;

    PROCEDURE BuscarSalaOcupada (tipo: TipoVaca): CARDINAL;
    (**
      * PRE: cierto
      BuscarSalaOcupada (almacen, sala)
      POST: Devuelve la sala que contenga un menor numero de vacas de la clase

     *  SPMgt;"tipo". Si no existe ninguna sala con vacas de la clase "tipo",
      * 		 se devuelve cero.
     * POST: 		 resultado =
      **)

    END BuscarSalaOcupada;

    PROCEDURE ElOtro(tipo: TipoVaca):TipoVaca;
    (**
      * PRE: cierto
     * ElOtro (tipo)
     * POST: resultado =
      **)

    END ElOtro;

    PROCEDURE Dejar (tipo : TipoVaca; sala:TipoNumSala);(**
      * PRE: almacen(sala).npiezas  TAMSALA
     * Dejar (tipo, sala, almacen, nosalas)
     * POST: 		Deja una vaca en la sala indicada actualizando el almac'en y el contador de salas

     * POST: 		  almacen(i) =
     (almacen(sala) = 0  (almacen(sala) = tipo

    nosalas(tipo) =  nosalas(tipo) + 1))
      **)

    END Dejar;

    PROCEDURE Retirar (tipo : TipoVaca, sala:TipoNumSala);(**
      * PRE: almacen(sala).npiezas  0
     * Dejar (tipo, sala, almacen, nosalas)
     * POST: 		Deja una vaca en la sala indicada actualizando el almac'en y el contador de salas

     * POST:
     (almacen(sala) = 1)                         nosalas(tipo) =  nosalas(tipo) - 1)

      **)

    END Retirar;

    PROCEDURE DejarNormal (VAR sala: TipoNumSala);

    BEGIN
    (* Sincronizaci'on de entrada *)
      sala := BuscarSalaNoLlena(normal);

    IF sala = 0 THEN
      INC(nodejaresperando[normal]);

    Delay(dejaresperando[normal]);

    DEC(nodejaresperando[normal]);

    sala := saladisponible;

    END;

    *(* Actualizaci'on del almacen *)

    Dejar (normal, sala);

    (* Sincronizaci'on de salida *)

    saladisponible := sala;

    IF nodejaresperando[normal]  0 AND (almacen[sala].npiezas  TAMSALA) THEN

    Continue(dejaresperando[normal]); (* despertar en cascada *)

    ELSE

    Continue(retiraresperando[normal]);

    END;END DejarNormal;

    PROCEDURE DejarLoca (VAR sala: TipoNumSala);

    BEGIN
    (* Sincronizaci'on de entrada *)
      sala := BuscarSalaNoLlena(loca);

    IF sala = 0 THEN
      INC(nodejaresperando[loca]);

    Delay(dejaresperando[loca]);

    DEC(nodejaresperando[loca]);

    sala := saladisponible;

    END;

    (* Actualizaci'on del almacen *)

    Dejar (loca, sala);

    (* Sincronizaci'an de salida *)

    saladisponible := sala;

    IF nodejaresperando[loca]  0 AND (almacen[sala].npiezas  TAMSALA) THEN

    Continue(dejaresperando[loca]); (* despertar en cascada *)

    ELSE

    Continue(retiraresperando[loca]);

    END;

    END DejarNormal;

    PROCEDURE RetirarNormal (VAR sala: TipoNumSala);

    BEGIN
    (* Sincronizaci'on de entrada *)
      sala := BuscarSalaOcupada(normal);

    IF sala = 0 THEN
    (* No es necesario notificar el bloqueo *)

    Delay(retiraresperando[normal]);

    sala := saladisponible;

    END;

    (* Actualizaci'on del almacen *)

    Retirar (normal, sala);

    (* Sincronizaci'on de salida *)

    saladisponible := sala;

    IF nodejaresperando[loca]  0 AND (almacen[sala].npiezas = 0) AND
    (nosalas[loca]  NUMSALAS-2) THEN
      Continue(dejaresperando[loca]);

    ELSE

    Continue(dejaresperando[normal]);

    END;

    END RetirarNormal;

    PROCEDURE RetirarLoca (VAR sala: TipoNumSala);

    BEGIN
    (* Sincronizaci'on de entrada *)
      sala := BuscarSalaOcupada(loca);

    IF sala = 0 THEN
    (* No es necesario notificar el bloqueo *)

    Delay(retiraresperando[loca]);

    sala := saladisponible;

    END;

    (* Actualizaci'on del almacen *)

    Retirar (loca, sala);

    (* Sincronizaci'on de salida *)

    saladisponible := sala;

    IF nodejaresperando[normal]  0 AND (almacen[sala].npiezas = 0) AND

    (nosalas[normal] < NUMSALAS-2) THEN
      Continue(dejaresperando[normal]);

    ELSE

    Continue(dejaresperando[loca]);

    END;

    END RetirarLoca;

    BEGIN

    (* El almac'en est'a inicialmente vac'io *)

    FOR i := 1 TO NUMSALAS DO

    almacen[i].npiezas := 0

    END ;

    FOR j := normal TO loca DO

    nodejaresperando[j] := 0;  (* No hay operaciones bloqueadas *)

    nosalas[j] := 0;

    END;

    END (* MONITOR TipoGestorAlmacen *);

Next: Preguntas cortas Up: Examen de Programación Concurrente Previous: Controlador de un ascensor