3.9 Comunicación Rendezvous

Hasta ahora hemos hablado de la comunicación asíncrona entre procesos a través de canales de mensajes que se declaran, por ejemplo, como

donde N es una constante positiva que define la cantidad máxima de mensajes que se pueden almacenar en el canal. Una extensión lógica es permitir la declaración

Esta es una traducción del libro SPIN model checker

para definir un puerto de encuentro(rendezvous port). La capacidad del canal ahora es cero, es decir, el puerto del canal puede pasar, pero no puede almacenar mensajes. Las interacciones de mensajes a través de tales puertos de encuentro(rendezvous port) son por definición, sincrónicas. Considere el siguiente ejemplo:

El nombre del canal es un puerto de encuentro(rendesvous port). Los dos procesos ejecutan de forma sincrónica su primer enunciado: un protocolo de enlace en el msgtype y una transferencia del valor 124 del proceso A al estado de variable local en el proceso B. El segundo enunciado del proceso A no es ejecutable (bloquea) porque no hay correspondencia recibir la operación para ello en el proceso B.

Si el nombre del canal está definido con una capacidad de memoria intermedia distinta de cero, el comportamiento es diferente. Si el tamaño del buffer es al menos dos, el proceso del tipo A puede completar su ejecución, incluso antes de que su par comience. Si el tamaño del buffer es uno, la secuencia de eventos es la siguiente. El proceso de tipo A puede completar su primera acción de envío, pero se bloquea en el segundo, porque el canal ahora está lleno a su capacidad. El proceso de tipo B puede recuperar el primer mensaje y terminar. En este punto A se vuelve a ejecutar y también termina, dejando su segundo mensaje como un residuo en el canal.

La comunicación de Rendezvous es binaria: solo dos procesos, un emisor y un receptor, pueden encontrarse en un apretón de manos(handshake) de la reunión.

Los parámetros de mensaje siempre pasan por valor en PROMELA. Esto aún deja abierta la posibilidad de pasar el valor de un canal de mensaje declarado localmente e instanciado de un proceso a otro. El valor almacenado en una variable de tipo chan no es más que la identidad del canal que se necesita para direccionar el canal en las operaciones de envío y recepción. Aunque no podemos enviar el nombre de las operaciones de recepción. Aunque no podemos enviar el nombre de la variable en la que está almacenada la identidad de un canal, podemos enviar la propia identidad como un valor y, de ese modo hacer que incluso un canal local sea accesible para otros procesos. Sin embargo, cuando el proceso que declara e instancia un canal muere, el objeto del canal correspondiente desaparece, y cualquier intento de acceder a él desde otro proceso falla (causando un error que se puede atrapar en el modo de verificación). Como ejemplo, considere el siguiente modelo:

Hay dos canales en este modelo, declarados e instanciados en dos niveles diferentes de alcance(scope). El canal llamado glob es inicialmente visible para ambos procesos. El canal llamado loc inicialmente solo es visible para el proceso que contiene su declaración. El proceso A envía el valor de su variable de canal local al proceso B a través del canal global y, por lo tanto, lo pone a disposición de ese proceso para futuras comunicaciones. El proceso B ahora transmite un mensaje del tipo apropiado a través de un apretón de manos rendezvous en ese canal y ambos procesos pueden terminar. Cuando el proceso A muere, el canal loc es destruido y cualquier intento adicional de utilizarla ocasionará un error.

3.10 Reglas para la ejecutabilidad

La definición de PROMELA se centra en su semántica de ejecutabilidad, que proporciona los medios básicos en el lenguaje para modelar sincronizaciones de procesos.

Dependiendo del estado del sistema, cualquier instrucción en un modelo SPIN es ejecutable o bloqueada.

Ya se han visto cuatro tipos básicos de declaraciones en PROMELA: imprimir declaraciones, asignaciones, declaraciones de entrada/salida y declaraciones de expresión. Una curiosidad en PROMELA es que las expresiones se pueden usar como si fuesen declaraciones en cualquier contexto. Son ”ejecutables” (es decir, transitables) si y solo si evalúan el valor booleano verdadero, o equivalentemente a un valor entero distinto de cero. Las reglas de semántica de PROMELA establecen además que las instrucciones de impresión y las asignaciones siempre son incondicionalmente ejecutables. Si un proceso llega a un punto en su código donde no tiene sentencias ejecutables pendientes de ejecutar, simplemente se bloquea.

Por ejemplo, en lugar de escribir un bucle de espera ocupado

logramos el mismo efecto en PROMELA con la declaración única

El mismo efecto podría obtenerse en PROMELA con una construcción como

pero esto siempre es menos eficiente.

Vimos anteriormente que las expresiones en PROMELA deben ser sin efectos secundarios. La razón será clara: una declaración de expresión de bloqueo puede tener que evaluarse varias veces antes de que sea ejecutable, y si cada evaluación pudiera tener un efecto secundario, se produciría un caos. Existe una excepción a la regla. Una expresión que contiene el operador térmico que discutimos anteriormente puede tener un efecto secundario y, por lo tanto, está sujeta a algunas restricciones sintácticas. La principal restricción es que solo puede haber un operador de ejecución en una expresión y, si aparece, no se puede combinar con ningún otro operador. Esto, por supuesto, todavía nos permite usar un enunciado de ejecución como una expresión potencialmente bloqueante. Podemos indicar este efecto más explícita mente si en vez de escribir

escribimos:

—

Debido al límite en el número de procesos que pueden ejecutarse simultáneamente, el intento 255 de instanciar un nuevo proceso fallará. El error hace que la expresión de ejecución evalúe a toZero y, por lo tanto, bloquea permanentemente el proceso. El proceso bloqueado ahora no puede alcanzar el final de su código y, por lo tanto, no puede terminar o morir. Como resultado, ninguno de sus predecesores puede morir tampoco.

El sistema de 255 procesos se detiene con 254 procesos finalizados pero bloqueados en su intento de morir, y un proceso bloqueado en su intento de iniciar un nuevo proceso. Si la evaluación de la expresión de ejecución devuelve cero, bloques de ejecución, pero no se han producido efectos secundarios, por lo que tampoco hay peligro de efectos secundarios repetidos en pruebas consecutivas de ejecutabilidad.

Si la evaluación devuelve un valor distinto de cero, hay un efecto secundario a medida que se completa la ejecución de la declaración, pero la declaración en su conjunto no puede bloquearse. Definitivamente sería dudoso si las condiciones compuestas pudieran construirse con los operadores de ejecución. Por ejemplo,

bloquearía si no se pudieran crear instancias de ambos procesos, pero no revelaría si se creó un proceso o ninguno. Similar,

se bloquearía si fallaran ambos intentos de crear instancias de un proceso, pero si tuviera éxito no revelaría cuál de los dos procesos se creó.

3.11 Asignaciones y Expresiones

Como en C, las asignaciones

pueden ser abreviadas a:

pero, a diferencia de C,

no es una tarea válida en PROMELA, porque el operando del lado derecho no es una expresión libre de efectos secundarios. No hay equivalente a los shorthands

en PROMELA, porque las declaraciones de asignación como

cuando se toman como una unidad no son equivalentes a expresiones en PROMELA. Con estas restricciones, una instrucción como –c es siempre indistinguible de c–, que es compatible.

En tareas tales como

Los valores de todos los operandos utilizados en la expresión del lado derecho del operador de asignación se transfieren primero a enteros con signo, antes de aplicar cualquiera de los operandos. Los precedentes del operador de C determinan el orden de evaluación.

Después de completar la evaluación de la expresión del lado derecho, y antes de que se lleve a cabo la asignación, el valor producido se convierte al tipo de la variable objetivo. Si el lado derecho produce un valor fuera del rango del tipo de objetivo, puede producirse el truncamiento del valor asignado. En el modo de simulación, SPIN emite una advertencia cuando esto ocurre; en modo de verificación, sin embargo, este tipo de truncamiento no se intercepta.

También es posible usar expresiones condicionales estilo C en cualquier contexto donde las expresiones estén permitidas. La sintaxis, sin embargo, es un contexto donde las expresiones están permitidas. La sintaxis, sin embargo, es ligeramente diferente de la utilizada en C. Donde en C uno escribiría

uno escribe en PROMELA

El símbolo de flecha se usa aquí para evitar una posible confusión con la marca de pregunta de las operaciones de recepción de PROMELA. El valor de la expresión condicional es igual al valor de expr2 si y solo si expr1 se evalúa como verdadero y de lo contrario es igual al valor de expr3. En PROMELA las expresiones condicionales deben estar rodeadas por pares (paréntesis) para evitar interpretaciones erróneas de la flecha como un separador de enunciados.

Esta es una traducción del libro SPIN model checker