stringtranslate.com

Teoría del modelo actoral

En informática teórica , la teoría del modelo de actor se ocupa de cuestiones teóricas relacionadas con el modelo de actor .

Los actores son los elementos primitivos que forman la base del modelo de 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 ordenamientos

De la definición de Actor se desprende que tienen lugar 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 únicamente 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 Contabilidad : Hay como máximo un número contable de eventos.

Orden de activación

El orden de activación ( -≈→) es un ordenamiento fundamental que modela un evento que activa otro (debe haber un flujo de energía en el mensaje que pasa de un evento a un evento que activa).

Pedidos de llegada

El orden de llegada de un Actor x( -x→ ) modela el orden (total) de eventos en los que un mensaje llega a x. El orden de llegada se determina mediante arbitraje en el procesamiento de mensajes (que a menudo hace uso de un circuito digital llamado árbitro ). Los eventos de llegada de un Actor están en su línea de mundo . El orden de llegada significa que el modelo de Actor tiene indeterminación inherente (consulte Indeterminación en computación concurrente ).

Pedido combinado

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 obviamente transitivo por definición.

En [Baker y Hewitt 197?], se conjeturó que las leyes anteriores podrían implicar la siguiente ley:

Ley de cadenas finitas entre eventos en el ordenamiento combinado : No hay cadenas infinitas ( es decir , conjuntos ordenados linealmente) de eventos entre dos eventos en el ordenamiento 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 Ordenamiento Combinado es independiente de las leyes anteriores, es decir ,

Teorema. La Ley de Cadenas Finitas Entre Eventos en el Ordenamiento Combinado no se sigue de las leyes enunciadas anteriormente.

Prueba. Es suficiente demostrar que existe un cómputo de Actor que satisface las leyes enunciadas anteriormente pero viola la Ley de Cadenas Finitas Entre Eventos en el Ordenamiento Combinado.

Considere un cálculo que comienza cuando se le envía un mensaje a un actor InitialStart que hace que realice las siguientes acciones
  1. Crea un nuevo actor Greeter 1 al que se le envía el mensaje SayHelloTocon la dirección de Greeter 1
  2. Enviar Inicial el mensaje Againcon la dirección del Recepcionista 1
A partir de entonces el comportamiento de Initial es el siguiente al recibir un Againmensaje con dirección Greeter i (al que llamaremos evento ):Againi
  1. Crea un nuevo actor Greeter i+1 al que se le envía el mensaje SayHelloTocon la dirección Greeter i
  2. Enviar Inicial el mensaje Againcon la dirección del Greeter i+1
Obviamente el cálculo del envío inicialAgain de mensajes nunca termina.
El comportamiento de cada Actor Greeter i es el siguiente:
  • Cuando recibe un mensaje SayHelloTocon la dirección Greeter i-1 (al que llamaremos evento ), envía un mensaje a Greeter i-1SayHelloToiHello
  • Cuando recibe un Hellomensaje (al que llamaremos evento ), no hace nada.Helloi
Ahora bien, es posible que cada vez y por tanto .Helloi -Greeteri→ SayHelloToiHelloi→SayHelloToi
También cada vez y por lo tanto .Againi -≈→ Againi+1Againi → 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:Again1SayHelloTo1
Again1→...→Againi→......→Helloi→SayHelloToi→...→Hello1→SayHelloTo1

Sin embargo, sabemos por la física que no se puede gastar energía infinita a lo largo de una trayectoria finita. Por lo tanto, dado que el modelo del actor se basa en la física, la Ley de cadenas finitas entre eventos en el ordenamiento combinado se tomó como un axioma del modelo del actor.

Ley de discreción

La Ley de Cadenas Finitas Entre Eventos en el Ordenamiento Combinado está estrechamente relacionada con la siguiente ley:

Ley de discreción : Para todos los eventos y , el conjunto es finito.e1e2{e|e1→e→e2}

De hecho, se ha demostrado que las dos leyes anteriores son equivalentes:

Teorema [Clinger 1981]. La Ley de Discreción es equivalente a la Ley de Cadenas Finitas entre Eventos en el Ordenamiento Combinado (sin utilizar el axioma de elección).

La ley de discreta descarta las máquinas de Zenón y está relacionada con los resultados en redes de Petri [Best et al. 1984, 1987].

La ley de discreción implica la propiedad de no determinismo ilimitado . El ordenamiento combinado es utilizado por [Clinger 1981] en la construcción de un modelo denotacional de actores (véase semántica denotacional ).

Semántica denotacional

Clinger [1981] utilizó el modelo de eventos de Actor descrito anteriormente para construir un modelo denotacional para Actores utilizando dominios de potencia . Posteriormente, Hewitt [2006] amplió los diagramas con tiempos de llegada para construir un modelo denotacional técnicamente más simple y más fácil de entender.

Véase también

Referencias