En informática teórica , la teoría del modelo Actor se ocupa de cuestiones teóricas para el modelo Actor .
Los actores son las primitivas que forman la base del modelo Actor de computación digital concurrente. En respuesta a un mensaje que recibe, un actor puede tomar decisiones locales, crear más actores, enviar más mensajes y designar cómo responder al siguiente mensaje recibido. La teoría del modelo de actor incorpora teorías de los eventos y estructuras de los cálculos de actor, su teoría de prueba y modelos denotacionales .
Eventos y sus pedidos
A partir de la definición de Actor, se puede ver que ocurren numerosos eventos: decisiones locales, creación de Actores, envío de mensajes, recepción de mensajes y designación de cómo responder al siguiente mensaje recibido.
Sin embargo, este artículo se centra solo en aquellos eventos que son la llegada de un mensaje enviado a un actor.
Este artículo informa sobre los resultados publicados en Hewitt [2006].
- Ley de la contabilización : hay, como mucho, innumerables eventos.
Pedido de activación
El orden de activación ( -≈→
) es un orden fundamental que modela un evento activando otro (debe haber un flujo de energía en el mensaje que pasa de un evento a un evento que activa).
- Debido a la transmisión de energía, el orden de activación es relativista invariante ; es decir, para todos los eventos . , si , entonces el tiempo de precede al tiempo de en los marcos de referencia relativistas de todos los observadores.
e1
e2
e1 -≈→ e2
e1
e2
- Ley de causalidad estricta para el ordenamiento de la activación : porque ningún evento lo hace
e -≈→ e
. - Ley de Predecesión Finita en el Orden de Activación : Para todos los eventos, el conjunto es finito.
e1
{e|e -≈→ e1}
Pedidos de llegada
El orden de llegada de un Actor x
( -x→
) modela el orden (total) de los eventos a los que llega un mensaje x
. El orden de llegada se determina mediante arbitraje en el procesamiento de mensajes (a menudo haciendo uso de un circuito digital llamado árbitro ). Los eventos de llegada de un actor están en su línea mundial . El orden de llegada significa que el modelo Actor tiene inherentemente indeterminación (ver Indeterminación en cálculo concurrente ).
- Debido a que todos los eventos del orden de llegada de un actor
x
ocurren en la línea mundial dex
, el orden de llegada de un actor es relativistamente invariante . Es decir , para todos los actoresx
y eventos . , si , entonces el tiempo de precede al tiempo de en los marcos de referencia relativistas de todos los observadores.e1
e2
e1 -x→ e2
e1
e2
- Ley de la predecesión finita en los pedidos de llegada : para todos los eventos y actores, el conjunto es finito.
e1
x
{e|e -x→ e1}
Pedidos combinados
El ordenamiento combinado (denotado por →
) se define como el cierre transitivo del ordenamiento de activación y los ordenamientos de llegada de todos los Actores.
- El ordenamiento combinado es relativista invariante porque es el cierre transitivo de ordenamientos relativista invariante. Es decir , para todos los eventos . , si . entonces el tiempo de precede al tiempo de en los marcos de referencia relativistas de todos los observadores.
e1
e2
e1→e2
e1
e2
- Ley de causalidad estricta para el ordenamiento combinado : porque ningún evento lo hace
e→e
.
El ordenamiento combinado es obviamente transitivo por definición.
En [Baker y Hewitt 197?], Se conjeturaba que las leyes anteriores podrían implicar la siguiente ley:
- Ley de cadenas finitas entre eventos en el orden combinado : No hay cadenas infinitas ( es decir , conjuntos ordenados linealmente) de eventos entre dos eventos en el orden combinado →.
Independencia de la ley de cadenas finitas entre eventos en el ordenamiento combinado
Sin embargo, [Clinger 1981] demostró sorprendentemente que la Ley de Cadenas Finitas entre Eventos en el Orden Combinado es independiente de las leyes anteriores, es decir ,
Teorema. La Ley de Cadenas Finitas entre Eventos en el Orden Combinado no se sigue de las leyes establecidas anteriormente.
Prueba. Es suficiente mostrar que hay un cómputo de Actor que satisface las leyes establecidas anteriormente pero viola la Ley de Cadenas Finitas entre Eventos en el Orden Combinado.
- Considere un cálculo que comienza cuando a un actor Inicial se le envía un
Start
mensaje, lo que hace que tome las siguientes acciones- Crea un nuevo actor Greeter 1 al que se le envía el mensaje
SayHelloTo
con la dirección de Greeter 1 - Envíe Inicial el mensaje
Again
con la dirección de Greeter 1
- Crea un nuevo actor Greeter 1 al que se le envía el mensaje
- A partir de entonces, el comportamiento de Initial es el siguiente al recibir un
Again
mensaje con la dirección Greeter i (que llamaremos el evento ):Againi
- Cree un nuevo actor Greeter i + 1 al que se le envíe el mensaje
SayHelloTo
con la dirección Greeter i - Enviar Inicial el mensaje
Again
con la dirección de Greeter i + 1
- Cree un nuevo actor Greeter i + 1 al que se le envíe el mensaje
- Obviamente, el cálculo del envío inicial de mensajes en sí mismo
Again
nunca termina.
- El comportamiento de cada Actor Greeter i es el siguiente:
- Cuando recibe un mensaje
SayHelloTo
con la dirección Greeter i-1 (que llamaremos el evento ), envía un mensaje a Greeter i-1SayHelloToi
Hello
- Cuando recibe un
Hello
mensaje (que llamaremos evento ), no hace nada.Helloi
- Cuando recibe un mensaje
- Ahora es posible que siempre y por tanto .
Helloi -Greeteri→ SayHelloToi
Helloi→SayHelloToi
- También cada vez y por lo tanto .
Againi -≈→ Againi+1
Againi → Againi+1
- Además, se cumplen todas las leyes establecidas antes de la Ley de causalidad estricta para el ordenamiento combinado.
- Sin embargo, puede haber un número infinito de eventos en el orden combinado entre y como sigue:
Again1
SayHelloTo1
Again1→...→Againi→......→Helloi→SayHelloToi→...→Hello1→SayHelloTo1
Sin embargo, sabemos por la física que la energía infinita no se puede gastar a lo largo de una trayectoria finita. Por tanto, dado que el modelo Actor se basa en la física, se tomó como axioma del modelo Actor la Ley de Cadenas Finitas entre Eventos en el Orden Combinado.
Ley de la discreción
La ley de cadenas finitas entre eventos en el orden combinado está estrechamente relacionada con la siguiente ley:
- Ley de la discreción : para todos los eventos y , el conjunto es finito.
e1
e2
{e|e1→e→e2}
De hecho, se ha demostrado que las dos leyes anteriores son equivalentes:
- Teorema [Clinger 1981]. La ley de la discreción es equivalente a la ley de las cadenas finitas entre eventos en el orden combinado (sin usar el axioma de elección).
La ley de la discreción descarta las máquinas Zeno y está relacionada con los resultados en las redes de Petri [Best et al. 1984, 1987].
La ley de la discreción implica la propiedad del no determinismo ilimitado . El ordenamiento combinado es usado por [Clinger 1981] en la construcción de un modelo denotacional de Actores (ver semántica denotacional ).
Semántica denotacional
Clinger [1981] utilizó el modelo de eventos de Actor descrito anteriormente para construir un modelo denotacional para Actores que utilizan dominios de poder . Posteriormente, Hewitt [2006] aumentó los diagramas con tiempos de llegada para construir un modelo denotacional técnicamente más simple y más fácil de entender.
Ver también
Referencias
- Carl Hewitt y col. Acta de la conferencia de inducción y metaevaluación de actores del simposio de ACM sobre principios de lenguajes de programación, enero de 1974.
- Irene Greif. Semántica de la comunicación de procesos paralelos Tesis doctoral EECS del MIT. Agosto de 1975.
- Edsger Dijkstra. Una disciplina de programación Prentice Hall. 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 y Carl Hewitt The Incremental Garbage Collection of Processes Proceedings of the Symposium on Artificial Intelligence Programming Languages. Avisos SIGPLAN 12, agosto de 1977.
- Carl Hewitt y Henry Baker Leyes para la comunicación de procesos paralelos IFIP-77, agosto de 1977.
- Aki Yonezawa Especificaciones y técnicas de verificación para programas paralelos basadas en la semántica de aprobación de mensajes MIT EECS Tesis doctoral. Diciembre de 1977.
- Peter Bishop Espacio de direcciones muy grande Sistemas informáticos extensibles modularmente MIT EECS Disertación de doctorado. Junio de 1977.
- Carl Hewitt. Visualización de las estructuras de control como patrones de transmisión de mensajes Journal of Artificial Intelligence. Junio de 1977.
- Henry Baker. Actor Sistemas de Computación en Tiempo Real MIT EECS Tesis Doctoral. Enero de 1978.
- Carl Hewitt y Russ Atkinson. Técnicas de especificación y prueba para serializadores IEEE Journal on Software Engineering. Enero de 1979.
- Carl Hewitt, Beppe Attardi y Henry Lieberman. Delegación en las actas de aprobación de mensajes de la Primera Conferencia Internacional sobre Sistemas Distribuidos Huntsville, AL. Octubre de 1979.
- Russ Atkinson. Verificación Automática de Serializadores Tesis Doctoral del MIT. Junio de 1980.
- Bill Kornfeld y Carl Hewitt. La metáfora de la comunidad científica Transacciones IEEE sobre sistemas, hombre y cibernética. Enero de 1981.
- Gerry Barber. Razonamiento sobre el cambio en los sistemas de oficina bien informados Tesis doctoral del MIT EECS. Agosto de 1981.
- Bill Kornfeld. Paralelismo en la resolución de problemas MIT EECS Tesis doctoral. Agosto de 1981.
- Will Clinger. Fundamentos de la semántica del actor MIT Matemáticas Tesis doctoral. Junio de 1981.
- Eike Best . Comportamiento concurrente: secuencias, procesos y axiomas Lecture Notes in Computer Science Vol.197 1984.
- Gul Agha. Actores: un modelo de computación concurrente en sistemas distribuidos Tesis doctoral. 1986.
- Eike Best y R. Devillers. Comportamiento secuencial y concurrente en la teoría de la red de Petri. Informática teórica Vol.55 / 1. 1987.
- Gul Agha, Ian Mason, Scott Smith y Carolyn Talcott. A Foundation for Actor Computation Journal of Functional Programming, enero de 1993.
- Satoshi Matsuoka y Akinori Yonezawa . Análisis de anomalías de herencia en lenguajes de programación concurrente orientados a objetos en Direcciones de investigación en programación orientada a objetos concurrentes. 1993.
- Jayadev Misra. Una lógica para la programación concurrente: Safety Journal of Computer Software Engineering. 1995.
- Luca de Alfaro, Zohar Manna, Henry Sipma y Tomás Uribe. Verificación Visual de Sistemas Reactivos TACAS 1997.
- Thati, Prasanna, Carolyn Talcott y Gul Agha. Técnicas de ejecución y razonamiento sobre diagramas de especificación Conferencia internacional sobre metodología algebraica y tecnología de software (AMAST), 2004.
- Giuseppe Milicia y Vladimiro Sassone. La anomalía de la herencia: diez años después de las actas del Simposio ACM sobre Computación Aplicada (SAC) de 2004, Nicosia, Chipre, del 14 al 17 de marzo de 2004.
- Petrus Potgieter. Máquinas Zeno e hipercomputación 2005
- Carl Hewitt ¿Qué es el compromiso? Físico, organizacional y social COINS @ AAMAS. 2006.