3.6 Canales de mensajes

Los canales de mensajes se usan para modelar el intercambio de datos entre procesos. Se declaran local o globalmente. En la declaración

el typename chan introduce una declaración de canal. En este caso, el canal se llama qname y se declara que es capaz de almacenar hasta dieciséis mensajes. Puede haber un número finito de campos por mensaje. En el ejemplo, se dice que cada mensaje consta de tres campos: el primero se declara de tipo short el segundo es de tipo byte y el último es de tipo bool. Cada campo debe ser un tipo definido por el usuario, como campo de la última sección, o un tipo predefinido de la Tabla 3.1. En particular, no es posible usar un array como un declarador de tipo en un campo de mensaje. Una forma indirecta de lograr este efecto es volver a insertar un array en un tipo definido por el usuario, y usar el nombre del tipo como el declarador de tipo para el campo de mensaje. Tenga en cuenta también que, dado que el tipo chan aparece en la Tabla 3.1, siempre es válido usar el propio canal como declarador de campo. Podemos hacer un buen uso de esta capacidad para pasar identificadores de canal de un proceso a otro.

Esta es una traducción del libro SPIN model checker

La declaración

envía un mensaje con los valores de las tres expresiones enumeradas en el canal que acabamos de crear. El valor de cada expresión se convierte al tipo del campo de mensaje que corresponde con su posición relativa en la lista de parámetros de mensaje. Por defecto [2] el enunciado de envío solo es ejecutable si el canal de destino aún no está lleno y de lo contrario, bloquea.

La declaración

recupera un mensaje del jefe del mismo buffer y almacena los valores de los tres campos en las variables correspondientes.

La instrucción de recepción es ejecutable solo si el canal fuente no está vacío.

Es un error enviar o recibir más o menos campos de mensaje que fueron declarados para el canal de mensaje al que se dirige.

Una notación alternativa, y equivalente, para las operaciones de envío y recepción es usar el primer campo de mensaje como una indicación de tipo de mensaje, y para encerrar los campos restantes entre paréntesis, por ejemplo de la siguiente manera:

Algunos o todos los parámetros de una operación de recepción se pueden dar como constantes (por ejemplo, constantes simbólicas mtype) en lugar de variables:

En este caso, una condición adicional sobre la ejecutabilidad de la operación de recepción es que el valor de todos los campos de mensaje especificados como constantes coinciden con el valor de los campos correspondientes en las constantes de mensaje que coinciden con el valor de los campos correspondientes en el mensaje que se va a enviar recibido. Si queremos usar el valor actual de una variable para este propósito, es decir, para restringir la operación de recepción a los mensajes que tienen un campo coincidente, podemos usar la función predefinida eval, por ejemplo, de la siguiente manera:

En este caso, la variable var1 se evalúa y su valor se utiliza como una restricción en los mensajes entrantes, al igual que una constante. La operación de recepción ahora es ejecutable solo si hay un mensaje disponible que tiene un primer campo con un valor que coincide con el valor actual de var1. Si es así, los valores de var2 y var3 se establecen en los valores de los campos correspondientes en ese mensaje, y el mensaje se elimina del canal qname. Un ejemplo simple de los mecanismos discutidos hasta ahora es el siguiente:

El modelo que se muestra aquí es una versión simplificada del protocolo de bit alternativo según lo definido por Bartlett, Scantlebury y Wilkinson [1969]. Lo ampliaremos en una versión más completa en breve, después de que hayamos cubierto un poco más del idioma.

La declaración

ntroduce a los 4 tipos de mensajes que consideraremos como constantes simbólicas.

Hemos usado una etiqueta, nombrada again en cada proctype y una declaración goto, con la semántica habitual. Hablamos con más detalle sobre construcciones de flujo de control hacia el final de este capítulo. Los primeros diez pasos de una simulación ejecutada con el modelo anterior generan la siguiente salida.

Hemos utilizado la opción SPIN -c para generar una visualización en columna de solo las operaciones de envío y recepción, que en muchos casos nos proporciona el tipo correcto de información sobre los patrones de interacción del proceso. A cada canal y cada proceso se le asigna un número de instanciación de identificación. Cada columna en la pantalla de arriba corresponde a un número de proceso como antes. Cada fila (línea) de salida también contiene el número de instanciación del canal que se dirige en el margen izquierdo.

También hemos utilizado la opción SPIN -u10 para limitar el número máximo de pasos que se ejecutarán en la simulación a diez.

Hay muchas más operaciones en PROMELA que se pueden realizar en canales de mensajes. Revisaremos las operaciones más importantes aquí.

La función predefinida len(qname) devuelve la cantidad de mensajes almacenados actualmente en el canal qname. Algunos shorthands para los usos más comunes de esta función son: empty(qname), nempty(qname), full(qname) y nfull(qname) con las connotaciones obvias.

En algunos casos, es posible que deseemos probar si una operación de envío o recepción sería ejecutable, sin realmente ejecutar la operación. Para hacerlo, podemos transformar cada una de las operaciones del canal en una expresión libre de efectos secundarios. Por ejemplo, no es válido decir:

porque estas expresiones no se pueden evaluar sin efectos secundarios, o más al punto, porque las operaciones de envío y recepción no califican como expresiones (son declaraciones de E/S).

Para indicar una condición que debe evaluarse como verdadera cuando tanto (a¿ b) como el primer mensaje en el canal qname es del tipo msg0, podemos, sin embargo, escribir

PROMELA:

La expresión qname? [Msg0] es verdadera precisamente cuando la instrucción de recepción qname? Msg0 sería ejecutable en el mismo punto en la ejecución, pero la recepción real no se ejecuta, solo se evalúa su precondición. Cualquier instrucción de recepción puede convertirse en una expresión libre de efectos secundarios de forma similar, colocando corchetes alrededor de la lista de parámetros de mensaje. El contenido del canal no se altera por la evaluación de tales expresiones.

3.7 Operaciones de sondeo de canales

También es posible limitar el efecto de una instrucción de recepción a simplemente copiar los valores de los parámetros de los campos de mensaje, sin eliminar el mensaje del canal. Estas operaciones se llaman operaciones de sondeo de canales. Cualquier instrucción de recepción puede convertirse en una operación de sondeo al colocar corchetes angulares alrededor de su lista de parámetros. Por ejemplo, suponiendo que hemos declarado un canal q con dos campos de mensaje de tipo int, la instrucción de recepción

donde x e y son variables, es ejecutable solo si el canal q contiene al menos un mensaje y si el primer campo en ese mensaje tiene un valor que es igual al valor actual de la variable y. Cuando se ejecuta la instrucción, el valor del segundo campo en el mensaje entrante se copia en la variable x, pero el mensaje en sí no se elimina del canal.

3.8 Envío ordenado y Recepción random

Otros dos tipos de declaraciones de envío y recepción se utilizan con menos frecuencia: envío ordenado y recepción aleatoria. Una operación de envío ordenada se escribe con dos, en lugar de uno, signos de exclamación, de la siguiente manera:

Una operación de envío ordenada inserta un mensaje en el buffer del canal en orden numérico, en lugar de FIFO. Por ejemplo, si un proceso envía los números del uno al diez a un canal en orden aleatorio, pero usando la operación de envío ordenado, el canal los clasifica automáticamente y los almacena en orden numérico.

Cuando se ejecuta una operación de envío ordenada, el contenido existente del canal objetivo se escanea desde el primer mensaje hacia el último, y el nuevo mensaje se inserta inmediatamente antes del primer mensaje que lo sigue en orden numérico. Para determinar el orden numérico, todos los campos de mensaje se tienen en cuenta y se interpretan como valores enteros. La contraparte de la operación de envío ordenada es la recepción aleatoria. Está escrito con dos signos de interrogación en lugar de uno:

Una operación de recepción aleatoria es ejecutable si es ejecutable para cualquier mensaje que esté almacenado temporalmente en un canal de mensajes (en lugar de estar restringido a una coincidencia en el primer mensaje en el canal). En efecto, la operación de recepción aleatoria implementada en SPIN siempre devolverá el primer mensaje en el buffer de canal que coincida, por lo que el término ‘recepción aleatoria’ es un poco inapropiado.

Las operaciones normales de envío y recepción se pueden combinar libremente con envío ordenado y operaciones de recepción aleatoria. Como un pequeño ejemplo, si consideramos el canal con la lista ordenada de enteros del uno al diez, una operación de recepción normal solo puede recuperar el primer mensaje, que será el valor más pequeño. Una operación de recepción aleatoria en el mismo canal tendría éxito para cualquiera de los valores del uno al diez: el mensaje no necesita estar al principio de la cola. Por supuesto, una operación de recepción aleatoria solo tiene sentido si al menos uno de los parámetros es una constante y no una variable. (Tenga en cuenta que el valor de una variable no se evalúa a una constante a menos que se fuerce con una función eval).

Esta es una traducción del libro SPIN model checker