Lenguaje de coordinación reo

Reo ^{[1] [2]} es un lenguaje específico de dominio para programar y analizar protocolos de coordinación que componen procesos individuales en sistemas completos , en sentido amplio. Entre los ejemplos de clases de sistemas que se pueden componer con Reo se incluyen sistemas basados ​​en componentes , sistemas orientados a servicios , sistemas multihilo , sistemas biológicos y protocolos criptográficos. Reo tiene una sintaxis gráfica en la que cada programa Reo, llamado conector o circuito , es un hipergrafo dirigido etiquetado . Dicho grafo representa el flujo de datos entre los procesos del sistema. Reo tiene una semántica formal , que se encuentra en la base de sus diversas técnicas de verificación formal y herramientas de compilación.

En Reo, un sistema concurrente consta de un conjunto de componentes que están unidos por un circuito que permite el flujo de datos entre los componentes. Los componentes pueden realizar operaciones de E/S en los nodos límite del circuito al que están conectados. Hay dos tipos de operaciones de E/S: las solicitudes put envían elementos de datos a un nodo y las solicitudes get obtienen elementos de datos de un nodo. Todas las operaciones de E/S son bloqueantes, lo que significa que un componente puede continuar solo después de que su operación de E/S pendiente se haya procesado correctamente.

La figura de la parte superior derecha muestra un ejemplo de un sistema productor-consumidor con tres componentes: dos productores a la izquierda y un consumidor a la derecha. El circuito del medio define el protocolo, que establece que los productores deben enviar datos de manera sincrónica, mientras que el consumidor los recibe en orden alterno.

Formalmente, la estructura de un circuito se define de la siguiente manera:

Definición 1. Un circuito es un triplete donde: ${\displaystyle R=(N,B,C,t)}$

1. N es un conjunto de nodos ;
2. ${\displaystyle B\subseteq N}$es un conjunto de nodos límite ;
3. ${\displaystyle C\subseteq 2^{N}\times 2^{N}}$es un conjunto de canales ;
4. ${\displaystyle t:C\rightarrow T}$Asigna un tipo a cada canal.

tal que , para todo . Si es un canal, entonces I se denomina el conjunto de nodos de entrada de c y O se denomina el conjunto de nodos de salida de c . ${\displaystyle |I\cup O|=2}$${\displaystyle (I,O)\en C}$${\displaystyle c=(I,O)\en C}$

La dinámica de un circuito se asemeja al flujo de señales a través de un circuito electrónico .

Los nodos tienen un comportamiento fijo de replicador-fusión: los datos de uno de los canales entrantes se propagan a todos los canales salientes, sin almacenar ni alterar los datos (es decir, comportamiento de replicador). Si varios canales entrantes pueden proporcionar datos, el nodo realiza una elección no determinista entre ellos (es decir, comportamiento de fusión). Los nodos con solo canales entrantes o salientes se denominan nodos receptores o nodos fuente , respectivamente; los nodos con canales entrantes y salientes se denominan nodos mixtos .

A diferencia de los nodos, los canales tienen un comportamiento definido por el usuario representado por su tipo. Esto significa que los canales pueden almacenar o modificar los elementos de datos que fluyen a través de ellos. Aunque cada canal conecta exactamente dos nodos, estos nodos no necesitan ser de entrada y salida. Por ejemplo, el canal vertical de la figura de la parte superior derecha tiene dos entradas y ninguna salida. El tipo de canal define el comportamiento del canal con respecto a los datos. A continuación, se incluye una lista de tipos comunes:

• Sincronizar : obtiene datos de forma atómica desde su nodo de entrada y los propaga a su nodo de salida.
• LossySync : igual que Sync, pero puede perder datos si su nodo de salida no está listo para tomar datos.
• Fifo ⟨ n ⟩ : obtiene datos de su nodo de entrada, los almacena temporalmente en un buffer interno de tamaño n y los propaga a su nodo de salida (siempre que este nodo de salida esté listo para tomar datos).
• SyncDrain : obtiene de forma atómica datos de ambos nodos de entrada y los pierde.
• Filtro ⟨ c ⟩ : obtiene atómicamente los datos de su nodo de entrada y los propaga a su nodo de salida sise cumple la condición de filtro c ; pierde los datos en caso contrario.

Una forma de clasificar los lenguajes de coordinación es en términos de su locus : el locus de coordinación se refiere a dónde tiene lugar la actividad de coordinación, clasificando los modelos y lenguajes de coordinación como endógenos o exógenos . ^[3] Los modelos y lenguajes endógenos, como Linda , proporcionan primitivos que deben incorporarse dentro de un cálculo para su coordinación. En aplicaciones que utilizan tales modelos, los primitivos que afectan la coordinación de cada módulo están dentro del módulo mismo. Por el contrario, Reo es un lenguaje exógeno que proporciona primitivos que admiten la coordinación de entidades desde fuera. En aplicaciones que utilizan modelos exógenos, los primitivos que afectan la coordinación de cada módulo están fuera del módulo mismo.

Los modelos endógenos son a veces más naturales para una aplicación dada. Sin embargo, generalmente conducen a una mezcla de primitivas de coordinación con código de cálculo, lo que enreda la semántica del cálculo con los protocolos de coordinación. Esta mezcla tiende a dispersar las primitivas de comunicación/coordinación en todo el código fuente, lo que hace que el modelo de cooperación y el protocolo de coordinación de una aplicación sean nebulosos e implícitos: generalmente, no hay ningún fragmento de código fuente identificable como el modelo de cooperación o el protocolo de coordinación de una aplicación, que pueda diseñarse, desarrollarse, depurarse, mantenerse y reutilizarse de forma aislada del resto del código de la aplicación. Por otro lado, los modelos exógenos fomentan el desarrollo de módulos de coordinación por separado e independientemente de los módulos de cálculo que se supone que deben coordinar. En consecuencia, el resultado del esfuerzo sustancial invertido en el diseño y desarrollo del componente de coordinación de una aplicación puede manifestarse como "módulos coordinadores puros" tangibles que son más fáciles de entender y también pueden reutilizarse en otras aplicaciones.

Los circuitos Reo son compositivos. Esto significa que se pueden construir circuitos complejos reutilizando circuitos más simples. Para ser más explícitos, dos circuitos se pueden pegar juntos en sus nodos límite para formar un nuevo circuito conjunto. A diferencia de muchos otros modelos de concurrencia (por ejemplo, el cálculo pi ), la sincronía se conserva bajo la composición. Esto significa que si componemos un circuito con flujo sincrónico entre los nodos A y B con otro circuito con flujo sincrónico entre los nodos B y C, el circuito conjunto tiene flujo sincrónico entre los nodos A y C. En otras palabras, la composición de dos circuitos sincrónicos produce un circuito sincrónico.

La semántica de un circuito Reo es una descripción formal de su comportamiento. Existen varias semánticas para Reo. ^[4]

Históricamente, la primera semántica de Reo se basó en la noción coalgebraica de flujos (es decir, secuencias infinitas). ^[5] Esta semántica se basa en el concepto de un flujo de datos cronometrado , que es un par que consiste en un flujo de elementos de datos y un flujo de marcas de tiempo monótonamente crecientes (números reales). Al asociar cada nodo con dicho flujo de datos cronometrado, el comportamiento de un canal se puede modelar como una relación en los flujos de los nodos conectados.

Más tarde, se desarrolló una semántica basada en autómatas , llamada autómatas de restricción . ^[6] Un autómata de restricción es un sistema de transición etiquetado, donde las etiquetas de transición consisten en una restricción de sincronización y una restricción de datos . Una restricción de sincronización especifica qué nodos se sincronizan en el paso de ejecución modelado por la transición, y una restricción de datos especifica qué elementos de datos fluyen en estos nodos.

Una limitación de los autómatas de restricción (y de los flujos de datos temporizados) es que no pueden modelar directamente el comportamiento sensible al contexto , donde el comportamiento de un canal depende de la (no) disponibilidad de una operación de E/S pendiente. Por ejemplo, utilizando autómatas de restricción, es imposible modelar directamente el comportamiento de un LossySync, que debería perder datos solo si su nodo de salida no tiene ninguna solicitud de obtención pendiente. Para resolver este problema, se ha desarrollado otra semántica de Reo, llamada coloración de conectores . ^[7]

Otras semánticas de Reo permiten modelar el comportamiento cronometrado ^[8] o probabilístico ^[9] .

Las herramientas de coordinación extensible (ECT) son un conjunto de complementos para Eclipse que constituyen un entorno de desarrollo integrado (IDE) para Reo. ECT consta de un editor gráfico para dibujar circuitos y un motor de animación para animar el flujo de datos a través de circuitos. Para la generación de código, ECT contiene un compilador de Reo a Java, que genera código para circuitos en función de la semántica de su autómata de restricción. En particular, en la entrada de un circuito Reo, produce una clase Java, que simula el autómata de restricción que modela el circuito. Para la verificación, ECT contiene una herramienta que traduce circuitos Reo a definiciones de proceso en mCRL2 . Los usuarios pueden utilizar posteriormente mCRL2 para la comprobación de modelos con respecto a las especificaciones de propiedades de cálculo mu . (Alternativamente, el verificador de modelos Vereofy también admite la verificación de circuitos Reo).

Otra implementación de Reo se desarrolla en el lenguaje de programación Scala y ejecuta circuitos de manera distribuida. ^[10]

• Sitio web de Reo