La semántica denotacional del modelo Actor es el tema de la teoría del dominio denotacional para Actores . El desarrollo histórico de este tema se relata en [Hewitt 2008b].
Semántica de punto fijo de actor
La teoría denotacional de la semántica de sistemas computacionales se ocupa de encontrar objetos matemáticos que representen lo que hacen los sistemas. Las colecciones de tales objetos se denominan dominios . El actor utiliza el dominio de escenarios de diagramas de eventos. Es habitual asumir algunas propiedades del dominio, como la existencia de límites de cadenas (ver cpo ) y un elemento de fondo. Varias propiedades adicionales son a menudo razonables y útiles: el artículo sobre teoría de dominios tiene más detalles.
Un dominio es típicamente un orden parcial , que puede entenderse como un orden de definición. Por ejemplo, escenarios diagrama evento dado x y y , uno podría dejar " x≤y "significa eso" y extiende los cálculos x ".
La denotación matemática de un sistema. S se encuentra construyendo aproximaciones cada vez mejores a partir de una denotación vacía inicial llamada ⊥ S usando alguna función de aproximación de denotación progresión S para construir una denotación (significado) para S como sigue:
Se esperaría que La progresión S sería monótona , es decir , si x≤y entonces progresión S (x) ≤ progresión S (y) . De manera más general, esperaríamos que
- Si ∀ yo ∈ω x yo ≤ x i +1 , entonces
Esta última propiedad declarada de la progresión S se llama ω-continuidad.
Una cuestión central de la semántica denotacional es caracterizar cuándo es posible crear denotaciones (significados) de acuerdo con la ecuación para Denotar S . Un teorema fundamental de la teoría del dominio computacional es que si la progresión S es ω-continua entonces Denote S existirá.
Se sigue de la ω-continuidad de progresión S que
- progresión S ( denotar S ) = denotar S
La ecuación anterior motiva la terminología que Denote S es un punto fijo de progresión S .
Además, este punto fijo es el menor entre todos los puntos fijos de progresión S .
Composicionalidad en lenguajes de programación
Un aspecto importante de la semántica denotacional de los lenguajes de programación es la composicionalidad, mediante la cual la denotación de un programa se construye a partir de las denotaciones de sus partes. Por ejemplo, considere la expresión "
El modelo Actor proporciona una forma moderna y muy general de analizar la composicionalidad de los programas. Scott y Strachey [1971] propusieron que la semántica de los lenguajes de programación se redujera a la semántica del cálculo lambda y así heredar la semántica denotacional del cálculo lambda . Sin embargo, resultó que el cálculo concurrente no se pudo implementar en el cálculo lambda (ver Indeterminación en el cálculo concurrente ). Así surgió el problema de cómo proporcionar semántica denotacional modular para lenguajes de programación concurrentes. Una solución a este problema es utilizar el modelo de cálculo Actor. En el modelo Actor, los programas son Actores que se envían Evaluar mensajes con la dirección de un entorno (explicado a continuación) para que los programas hereden su semántica denotacional de la semántica denotacional del modelo Actor (una idea publicada en Hewitt [2006]).
Ambientes
Los entornos contienen los enlaces de los identificadores. Cuando a un entorno se le envía un Mensaje de búsqueda con la dirección de un identificador x , devuelve el último enlace (léxico) de x .
Como ejemplo de cómo funciona esto, considere la expresión lambda
λ (subárbol izquierdo, subárbol derecho) λ (mensaje) if (message == "getLeft") then leftSubTree else if (message == "getRight") then rightSubTree
Considere lo que sucede cuando una expresión de la forma "(
Sin emabargo,
Cuando C recibe el mensaje [1 2] , crea un nuevo entorno Actor F que se comporta de la siguiente manera:
- Cuando recibe un Mensaje de búsqueda para el identificador leftSubTree , responde con 1
- Cuando recibe un Mensaje de búsqueda para el identificador rightSubTree , responde con 2
- Cuando recibe un Mensaje de búsqueda para cualquier otro identificador, reenvía el Mensaje de búsqueda a E
El Actor (proceso) C luego envía un Evalúe el mensaje con el entorno F al siguiente actor (proceso):
λ (mensaje) if (mensaje == "getLeft") luego leftSubTree else if (message == "getRight") luego rightSubTree
Expresiones aritméticas
Para otro ejemplo, considere el actor de la expresión "
Otras construcciones del lenguaje de programación
La semántica de composición denotacional presentada anteriormente es muy general y puede usarse para programas funcionales , imperativos , concurrentes , lógicos , etc. (ver [Hewitt 2008a]). Por ejemplo, proporciona fácilmente semántica de denotación para constructos que son difíciles de formalizar utilizando otros enfoques como retrasos y futuros .
Modelo de Clinger
En su tesis doctoral, Will Clinger desarrolló la primera semántica de denotación para el modelo Actor.
El dominio de los cálculos del actor
Clinger [1981] explicó el dominio de los cálculos de Actor de la siguiente manera:
- Los diagramas de eventos de Actor aumentados [consulte la teoría del modelo de Actor ] forman un conjunto parcialmente ordenado < diagramas , ≤ > a partir del cual construir el dominio de potencia P [ Diagramas ] (consulte la sección sobre Denotaciones a continuación). Los diagramas aumentados son historias de cálculo parciales que representan "instantáneas" [relativas a algún marco de referencia] de un cálculo en camino a completarse. Para x , y ∈ Diagramas , x≤y significa que x es una etapa por la que podría pasar el cálculo en su camino hacia y . Los elementos completos de Los diagramas representan cálculos que han terminado y cálculos no finales que se han vuelto infinitos. Los elementos completados pueden caracterizarse abstractamente como los elementos máximos de Diagramas [véase William Wadge 1979]. Concretamente, los elementos completados son los que tienen eventos no pendientes. Intuitivamente, Los diagramas no son ω-completos porque existen secuencias crecientes de cálculos parciales finitos
- en el cual algún evento pendiente permanece pendiente para siempre mientras el número de eventos realizados crece sin límite, contrario al requerimiento del retardo finito [de llegada]. Tal secuencia no puede tener un límite, porque cualquier límite representaría un cálculo no final completo en el que un evento aún está pendiente.
- Para repetir, el dominio del diagrama de eventos del actor Los diagramas están incompletos debido al requisito de una demora de llegada finita, que permite cualquier demora finita entre un evento y un evento que activa, pero descarta una demora infinita.
Denotaciones
En su tesis doctoral, Will Clinger explicó cómo se obtienen los dominios de poder a partir de dominios incompletos de la siguiente manera:
Del artículo sobre dominios Power : P [D] es la colección de subconjuntos de dominio cerrados hacia abajo D que también están cerrados bajo los límites superiores mínimos existentes de conjuntos dirigidos en D . Tenga en cuenta que si bien el pedido en P [D] viene dado por la relación de subconjunto, los límites mínimos superiores no coinciden en general con las uniones.
- Para el dominio del diagrama de eventos del actor Diagramas , un elemento de P [ Diagramas ] representa una lista de posibles historias iniciales de un cálculo. Dado que para los elementos de x y y de Diagramas , x≤y significa que x es un segmento inicial del historial inicial y , el requisito de que los elementos de P [ Diagramas ] estar cerrado hacia abajo tiene una base clara en la intuición.
- ...
- Por lo general, se requiere que el orden parcial a partir del cual se construye el dominio de potencia sea ω-completo . Hay dos razones para esto. La primera razón es que la mayoría de los dominios de potencia son simplemente generalizaciones de dominios que se han utilizado como dominios semánticos para programas secuenciales convencionales, y dichos dominios están todos completos debido a la necesidad de calcular puntos fijos en el caso secuencial. La segunda razón es que la completitud ω permite la solución de ecuaciones de dominio recursivo que involucran el dominio de potencia como
- que define un dominio de reanudaciones [Gordon Plotkin 1976]. Sin embargo, los dominios de poder se pueden definir para cualquier dominio. Además, el dominio de potencia de un dominio es esencialmente el dominio de potencia de su ω-terminación, por lo que las ecuaciones recursivas que involucran el dominio de potencia de un dominio incompleto aún pueden resolverse, proporcionan los dominios a los que los constructores habituales (+, ×, → y *) se aplican son ω-completos. Sucede que definir la semántica de Actor como en Clinger [1981] no requiere resolver ninguna ecuación recursiva que involucre el dominio de potencia.
- En resumen, no existe ningún impedimento técnico para construir dominios de poder a partir de dominios incompletos. Pero, ¿por qué debería uno querer hacerlo?
- En semántica conductual , desarrollada por Irene Greif , el significado de programa es una especificación de los cálculos que puede realizar el programa. Los cálculos se representan formalmente mediante diagramas de eventos de Actor. Greif especificó los diagramas de eventos por medio de axiomas causales que gobiernan los comportamientos de los Actores individuales [Greif 1975].
- Henry Baker ha presentado un intérprete no determinista que genera horarios instantáneos que luego se mapean en diagramas de eventos. Sugirió que un intérprete determinista correspondiente que opere en conjuntos de programas instantáneos podría definirse utilizando la semántica del dominio de potencia [Baker 1978].
- La semántica presentada en [Clinger 1981] es una versión de la semántica del comportamiento. Un programa denota un conjunto de diagramas de eventos de Actor. El conjunto se define extensionalmente usando la semántica del dominio de poder en lugar de usar intensionalmente axiomas causales. Los comportamientos de los Actores individuales se definen funcionalmente. Sin embargo, se muestra que el conjunto resultante de diagramas de eventos de Actor consiste exactamente en aquellos diagramas que satisfacen los axiomas causales que expresan los comportamientos funcionales de los Actores. Por tanto, la semántica conductual de Greif es compatible con una semántica de dominio de poder denotacional.
- Los horarios instantáneos de Baker introdujeron la noción de eventos pendientes , que representan mensajes en el camino a sus objetivos. Cada evento pendiente debe convertirse en un evento de llegada real (realizado) tarde o temprano, un requisito denominado retraso finito . Aumentar los diagramas de eventos de Actor con conjuntos de eventos pendientes ayuda a expresar la propiedad de retardo finito, que es característica de la verdadera concurrencia [Schwartz 1979].
Los cálculos secuenciales forman un subdominio ω-completo del dominio de los cálculos de Actor
En su disertación de 1981, Clinger mostró cómo los cálculos secuenciales forman un subdominio de cálculos concurrentes:
- En lugar de comenzar con una semántica para programas secuenciales y luego intentar extenderla para la concurrencia, la semántica de Actor ve la concurrencia como primaria y obtiene la semántica de los programas secuenciales como un caso especial.
- ...
- El hecho de que existan secuencias crecientes sin límites superiores mínimos puede parecer extraño para quienes están acostumbrados a pensar en la semántica de los programas secuenciales. Puede ser útil señalar que las secuencias crecientes producidas por programas secuenciales tienen todos límites superiores mínimos. De hecho, los cálculos parciales que pueden producirse mediante el cálculo secuencial forman un subdominio ω-completo del dominio de los cálculos de Actor. Diagramas . Sigue una prueba informal.
- Desde el punto de vista del actor, los cálculos secuenciales son un caso especial de cálculos concurrentes, distinguibles por sus diagramas de eventos. El diagrama de eventos de un cálculo secuencial tiene un evento inicial y ningún evento activa más de un evento. En otras palabras, el orden de activación de un cálculo secuencial es lineal; el diagrama de eventos es esencialmente una secuencia de ejecución convencional. Esto significa que los elementos finitos de Diagramas
- correspondientes a los segmentos iniciales finitos de una secuencia de ejecución secuencial, todos tienen exactamente un evento pendiente, excepto el elemento completado más grande si el cálculo termina. Una propiedad del dominio de diagramas de eventos aumentados < diagramas , ≤ > es que si x≤y y x ≠ y , entonces algún evento pendiente de x se realiza en y . Dado que en este caso cada x i tiene como máximo un evento pendiente, cada evento pendiente en la secuencia se realiza. De ahí la secuencia
- tiene un límite superior mínimo en Diagramas acordes con la intuición.
- La prueba anterior se aplica a todos los programas secuenciales, incluso a aquellos con puntos de elección, como comandos protegidos . Por tanto, la semántica de Actor incluye los programas secuenciales como un caso especial y está de acuerdo con la semántica convencional de tales programas.
El modelo de diagramas cronometrados
Hewitt [2006b] publicó una nueva semántica denotacional para actores basada en diagramas cronometrados. El modelo de diagramas cronometrados contrasta con Clinger [1981], que construyó un dominio de poder completo from a partir de un dominio diagramático incompleto subyacente, que no incluía el tiempo. La ventaja del modelo de diagramas cronometrados de dominio es que está físicamente motivado y los cálculos resultantes tienen la propiedad deseada de ω-completitud (por lo tanto, no determinismo ilimitado) que proporciona garantía de servicio.
Dominio de cálculos de actores cronometrados
La semántica denotacional de diagramas cronometrados construye un dominio computacional ω-completo para los cálculos de Actor. En el dominio, para cada evento en un cómputo de Actor, existe un tiempo de entrega que representa el momento en el que se entrega el mensaje de tal manera que cada tiempo de entrega cumple las siguientes condiciones:
- El tiempo de entrega es un número racional positivo que no coincide con el tiempo de entrega de cualquier otro mensaje.
- El tiempo de entrega es más que un δ fijo mayor que el tiempo de su evento de activación. Más tarde resultará que el valor de δ no importa. De hecho, incluso se puede permitir que el valor de δ disminuya linealmente con el tiempo para adaptarse a la ley de Moore.
Los diagramas temporizados del evento Actor forman un conjunto parcialmente ordenado < TimedDiagrams , ≤>. Los diagramas son historias de cálculo parciales que representan "instantáneas" (relativas a algún marco de referencia) de un cálculo en camino a completarse. Para d1, d2ε TimedDiagrams , d1≤d2 significa que d1 es una etapa por la que el cálculo podría pasar en su camino hacia d2 Los elementos completados de TimedDiagrams representan los cálculos que han terminado y los no finales que se han vuelto infinitos. Los elementos completados se pueden caracterizar de forma abstracta como los elementos máximos de TimedDiagrams . Concretamente, los elementos terminados son aquellos que no tienen eventos pendientes.
Teorema: TimedDiagrams es un dominio ω-completo de cálculos de Actor, es decir,
- Si se dirige D⊆ TimedDiagrams, existe el límite superior mínimo ⊔D; además, ⊔D obedece todas las leyes de la teoría del modelo Actor .
- Los elementos finitos de TimedDiagrams son contables donde un elemento xε TimedDiagrams es finito (aislado) si y solo si D⊆ TimedDiagrams está dirigido y x≤VD, existe dεD con x≤d. En otras palabras, x es finito si uno debe pasar por x para llegar hasta o por encima de x a través del proceso de límite.
- Cada elemento de TimedDiagrams es el límite superior mínimo de una secuencia creciente contable de elementos finitos.
Dominios de poder
- Definición: El dominio
TimedDiagrams] , ⊆> es el conjunto de posibles historias iniciales M de un cálculo tal que - M está cerrado hacia abajo, es decir, si dεM, entonces ∀d'εTimedDiagrams d'≤d ⇒ d'εM
- M está cerrado por debajo de los límites superiores mínimos de los conjuntos dirigidos, es decir, si D⊆M está dirigido, entonces VDεM
- Nota: Aunque el poder [ TimedDiagrams ] es ordenado por ⊆, límites no son dadas por T . Es decir,
- (∀i∈ω M yo ≤M i + 1 ) ⇒ U yo∈ω M yo ⊆ ⊔ i∈ω M yo
- Por ejemplo, si ∀id i ε TimedDiagrams y d i ≤d i + 1 y M i = {d k | k ≤i} entonces
- {{{1}}}
- Teorema: Poder [ TimedDiagrams ] es un dominio ω-completo.
Teorema de representación de simultaneidad
El cálculo de un actor puede progresar de muchas formas. Sea d un diagrama con el próximo evento programado e y X ≡ {e '| e ─≈ → 1-mensaje e '} (ver la teoría del modelo Actor ), el flujo (d) se define como el conjunto de todos los diagramas cronometrados con dy extensiones de d por X tales que
- la llegada se ha programado todos los eventos de X donde
- los eventos de X están programados en todos los ordenamientos posibles entre los eventos futuros programados de d
- sujeto a la restricción de que cada evento en X se programe al menos δ después de e y cada evento en X se programe al menos una vez en cada intervalo δ después de eso.
(Recuerde que δ es la cantidad mínima de tiempo para entregar un mensaje).
Flujo (d) ≡ {d} si d está completo.
Sea S un sistema Actor, la progresión S es un mapeo
- Energía [ TimedDiagrams ] → Energía [ TimedDiagrams ]
- Progresión S (M) ≡ U dεM Flujo (d)
Teorema: La progresión S es ω continua.
- Es decir, si ∀i M i ⊆M i + 1 entonces Progresión S (⊔ iεω M i ) = ⊔ iεω Progresión S (M i )
Además, el punto mínimo fijo de Progresión S viene dado por el Teorema de Representación de Concurrencia de la siguiente manera:
- ⊔ iεω Progresión S i (⊥ S )
donde ⊥ S es la configuración inicial de S.
La denotación Denote S de un sistema Actor S es el conjunto de todos los cálculos de S.
Defina la abstracción de tiempo de un diagrama cronometrado para que sea el diagrama con las anotaciones de tiempo eliminadas.
Teorema de representación: la denotación S de un sistema Actor S es la abstracción temporal de
- ⊔ iεω Progresión S i (⊥ S )
El uso del dominio TimedDiagrams , que es ω-completo, es importante porque proporciona la expresión directa del teorema de representación anterior para las denotaciones de los sistemas Actor mediante la construcción directa de un punto fijo mínimo.
El criterio de continuidad para las gráficas de funciones que Scott usó para desarrollar inicialmente la semántica denotacional de funciones se puede derivar como consecuencia de las leyes de Actor para el cálculo, como se muestra en la siguiente sección.
Referencias
- Dana Scott y Christopher Strachey. Hacia una semántica matemática para lenguajes informáticos Monografía técnica del Grupo de Investigación de Programación de Oxford. PRG-6. 1971.
- Irene Greif. Semántica de la comunicación de profesiones paralelas Tesis doctoral EECS del MIT. Agosto de 1975.
- Joseph E. Stoy , Semántica denotacional: El enfoque de Scott-Strachey para la semántica del lenguaje de programación . MIT Press , Cambridge, Massachusetts, 1977. (Un libro de texto clásico aunque anticuado).
- Gordon Plotkin. Una construcción de dominio de potencia SIAM Journal on Computing, septiembre de 1976.
- Edsger Dijkstra . Una disciplina de programación Prentice Hall . 1976.
- Krzysztof R. Apt, JW de Bakker. Ejercicios de semántica denotacional MFCS 1976: 1-11
- JW de Bakker. Puntos menos fijos revisados Theor. Computación. Sci. 2 (2): 155-181 (1976)
- Carl Hewitt y Henry Baker Actores y Actas de Funcionalidad Continua de la Conferencia de Trabajo de IFIP sobre Descripción Formal de Conceptos de Programación. 1-5 de agosto de 1977.
- Henry Baker . Actor Sistemas de Computación en Tiempo Real MIT EECS Tesis Doctoral. Enero de 1978.
- Michael Smyth. Power domains Journal of Computer and System Sciences . 1978.
- COCHE Hoare . Comunicación de procesos secuenciales CACM . Agosto de 1978.
- George Milne y Robin Milner . Procesos concurrentes y su sintaxis JACM . Abril de 1979.
- Nissim Francez, CAR Hoare , Daniel Lehmann y Willem-Paul de Roever. Semántica del no determinismo, concurrencia y comunicación Journal of Computer and System Sciences. Diciembre de 1979.
- Nancy Lynch y Michael J. Fischer . Sobre describir el comportamiento de sistemas distribuidos en Semántica de Computación Concurrente. Springer-Verlag . 1979.
- Jerald Schwartz Semántica denotacional del paralelismo en Semantics of Concurrent Computation. Springer-Verlag. 1979.
- William Wadge. Un tratamiento extensivo de la semántica del interbloqueo del flujo de datos de la computación concurrente. Springer-Verlag. 1979.
- Ralph-Johan Back. Semántica del no determinismo ilimitado ICALP 1980.
- David Park. Sobre la semántica del paralelismo justo Actas de la Escuela de Invierno sobre Especificación de Software Formal. Springer-Verlag. 1980.
- Will Clinger, Fundamentos de la semántica del actor . Tesis de Doctorado en Matemáticas del MIT, junio de 1981. (Citado con permiso del autor).
- Carl Hewitt ¿Qué es el compromiso? Físico, organizacional y social Pablo Noriega et al. editores. LNAI 4386. Springer-Verlag. 2007.