Separating Concerns:
Actors, Coordination Constraints,
and Implementation Protocols in a
Reflective Architecture
Gul Agha
University of Illinois at UrbanaChampaign
http://osl.cs.uiuc.edu
Collaborators
•
•
•
•
•
•
•
Mark Astley
Svend Frolund
YoungMin Kwon
Ian Mason
Jose Meseguer
Shangping Ren
Koushik Sen
Nov 7, 2006
•
•
•
•
•
Scott Smith
Dan Sturman
Carolyn Talcott
Prasanna Thati
Nalini
Venkatasubramanian
• Reza Ziaei
2
The Actor Model
A Model of Distributed Object Computation
Interface
State
Thread
Interface
Procedure
State
Thread
Messages
Procedure
Interface
State
Thread
Procedure
Nov 7, 2006
3
The Actor Model
• Actor system - collection of independent agents
interacting via message passing
• Features
– Acquaintances - initial, created, acquired
– History Sensitive
– Asynchronous fair communication
• An actor can:
– create a new actor and initialize its behavior
– send a message to an existing actor that is an
acquaintance
– change its local state or behavior
Nov 7, 2006
4
Ticker Actor Specification
• States: T(n) -- n a number
• Messages: tick, [email protected] -- c an actor id
• Reaction Rules:
( t | T(n) ) t  tick
==>
( t | T(n+1) ) t  tick
( t | T(n) ) t  [email protected]
==>
( t | T(n) ) c  reply(n)
Nov 7, 2006
5
Ticker Actor Specification
States: T(n) -- n a number
 Messages:
tick, [email protected] -- c an actor id
 Reaction Rules:
( t | T(n) ) t  tick
==>
( t | T(n+1) ) t  tick

( t | T(n) ) t  [email protected]
==>
( t | T(n) ) c  reply(n)
Ticker Actor Scenario
(t|T(2))
ttick
...
...
(c|..t..)
dlv(ttick)
... c ...
(t|T(3))
ttick
...
t[email protected]
(c|..t..)
dlv(t[email protected])
(t|T(n))
ttick
creply(3)
...
(c|..t..)
Nov 7, 2006
7
The Actor Model
send
ready
create
Nov 7, 2006
8
Operational Semantics
Notion of equivalence
Nov 7, 2006
9
May versus Must Testing
Nov 7, 2006
10
Join Continuation
a2
a1
v1
v2
f (v1,v2)
Nov 7, 2006
11
Local Synchronization Constraints
• Recipient Actor may not be ready to
accept a message in current state
Nov 7, 2006
12
Separate Synchronization
Constraints
• Abstract Data Types separate the interface
(what ) from the representation (how)
• Synchronization constraints express when
in terms of what
constrain get ( ) when empty?(buffer)
constrain put ( ) when full?(buffer)
Conditions are functions over the state.
Nov 7, 2006
13
Actor Languages
Primitives extended by
• join continuations
• local synchronization constraints
• Synchronous communication
Translated to primitive (kernel) actor
language
(see Mason & Talcott U2K)
Translation preserves actor semantics
Nov 7, 2006
14
How to Specify Actor Systems
• SpecDiagrams (Smith & Talcott): graphical
notation for specifying message passing
behavior of open distributed object systems
• Draws upon concepts from various formalisms
– Dynamic name generation and name passing as in
the pi-calculus
– Asynchronous communication and locality discipline
on names as in concurrent object models such as
Actors
– Imperative notions such as variables, environments,
and assignments
– Logical features such as assertions and constraints,
which are appropriate for specification languages.
Nov 7, 2006
15
SpecDiagrams
Nov 7, 2006
16
SpecDiagrams Syntax
D := 0 | ae | a(x):D | D1 // D2 | (ν a) D | recX:D | X
(asynch π)
| D1;D2 | D1 + D2 | fork(D) (control)
| { γ : D } | x := e
| pick(x) := e (imperative)
| pick(x) : D | wait(∅) (logical)
Let rcp(D) be the set of all free names in D that
occur as an input subject.
Uniqueness of names: If D1 ; D2 are two top-level
diagrams, then rcp(D1) ∩ rcp(D2) = ∅
Nov 7, 2006
17
Example: Memory Cell
Specification
Nov 7, 2006
18
Example:
Specification of Two Tickers
Nov 7, 2006
19
A UML Specification and Its
SpecDiagram
Nov 7, 2006
20
Refining Specifications
Nov 7, 2006
21
Reasoning about SpecDiagrams
• Trace-based equivalence relation for maytesting
• Executable Semantics in Term Rewriting
(Thati, Agha & Talcott 2004)
Nov 7, 2006
22
Policies as
Coordination Constraints
• Local synchronization constraints express
constraints over the history of single actor
• Synchronization between actors
–
–
–
–
precedence of actions
“atomic” actions
real-time constraints
Example: two robots with a shared task
• Express coordination constraints modularly
• Real-time constraints
Nov 7, 2006
23
Coordinating Robot Arms
Synchronizer SimulRobot (actor leftHand, rightHand) {
Constrain
lhand.release ( ) : rhand.grasp ( )
}
Nov 7, 2006
24
Transforming Constraints
• Dynamically customize schedulers
S. Frolund,
Coordinating Distributed
Objects, MIT Press
Nov 7, 2006
25
Abstracting Interaction
• Interaction may involve more than
synchronization constraints
• Separate interaction policy from protocols used
to implement policy
Nov 7, 2006
26
What is a Protocol?
• A protocol defines a role for each participating
actor relative to the protocol
• Primary Backup
•NovPeriodic
7, 2006 Checkpoint
27
Specifying Protocols
Protocol Auragen-backup {
parameter declarations
requirements
protocol methods and initialization
role definitions
}
Nov 7, 2006
28
Protocol Instances
• Protocol instances are runtime
instantiatons of protocols:
– A participant actor has a role in a protocol
– An actor may participate in multiple protocols
– Protocol methods may be invoked on
instances
Nov 7, 2006
29
Transparent Implementation
of Protocols
Reflection enables protocol implementations to be independent of
application implementations
• A meta-level actor describes functionality of actor.
• To change the application’s behavior, modify the relevant metaactor.
Nov 7, 2006
30
Dynamic Environment
• Unpredictable requirements
• Heterogeneity, e.g. Mobile Agents or Devices
Nov 7, 2006
31
The Two Level Actor Model

Stratify actors into
– Base-level actors (application)
– Meta-level actors (OS, communication,
middleware)

Meta-level actors
– can examine/modify runtime state and annotations
of base-level objects.
– notified when base-level events of interest to them
occur.
– distributed groups of meta-actors cooperate to
provide local and system wide services.
(Venkatasubramanian & Talcott)
TLAM structure/syntax

TLAM = < Net, TLAS, loc >
– Net - distributed computer network with
– processor nodes
– communication link between nodes
– TLAS - a two level actor system with
–
–
–
–
base- and meta-level actor states
base- and meta-level messages
annotations on base-level actors and messages
reaction rules for messages and events
– loc - distribution function mapping actors to nodes
TLAM semantics

Labeled transition system
– Trans  C  Lab  C

A configuration C = < lc, nq, ac>
– a (hypothetical) global snapshot
– lc - link configuration -- messages in transit
– nq - node buffer configuration -- messages queued
– ac - actor configuration -- base- and meta-level actor states

Two kinds of transitions:
– communication -- moving messages
– execution -- computation step followed by event handling
Ticker Monitor Rules
(tm | M(t,mc,tx,rx))
={dlv(ttick)/ }=>
(tm | M(t,mc,tx+1,rx))
(tm | M(t,mc,tx,rx))
={dlv(t[email protected])/ }=>
(tm | M(t,mc,tx,rx+1)) mc  log(t,tx,rx+1,c)
(tm | M(t,mc,tx,rx)) tm  reset
={ /t:=T(0)}=>
(tm | M(t,mc,0,0)) mc  reset-ack
Monitored Ticker Scenario
(tm|M(t,mc,2,0))
(t|T(2))
ttick
...
...
dlv(ttick) ... c ...
(c|..t..)
(tm|M(t,mc,3,0))
(t|T(3))
...
ttick
t[email protected]
(c|..t..)
mclog(t,3,0)
(tm|M(t,mc,3,1))
dlv(t[email protected])
(t|T(n))
creply(3)
(c|..t..)
ttick
...
TLAM modeling
• System
– set of configurations closed under TLAM transitions
• System properties specified in terms of
properties of
– configurations
– transitions
– admissible computations
• Restriction to base level measures meta-level
effect on functionality
Nov 7, 2006
37
Log Service Example
• Logging Service
– logs messages delivered to a given set of
base actors and when requested reports the
messages logged since the previous request.
• To provide the service, we specify a set of
meta-actor behaviors and configure a
service based on these behaviors.
Nov 7, 2006
38
Logging Service Specification
A system S provides logging service w.r.t.
– loggable actors A
– request GetLog : ActorId  Message and
– reply LogReply : ActorId  Message*  Message
if every request
GetLog(client)
gets a unique reply,
LogReply(client, log), s.t.
– log is a subset of the messages delivered to loggable actors,
– no messages in log have previously been reported.
– every message delivered to a loggable actor will eventually be
reported.
Nov 7, 2006
39
Logging Behavior
A system S with logging behavior has
• a logger on each node, that does the recording
for the loggable actors on its node,
• a reporter on each node, that does the reporting
for the loggable actors on its node, and
• a log server ls (one for the system) that
– receives log requests: GetLog(c) = ls  [email protected],
– collects reports from each node in the system, and
– sends the log reply: LogReply(c,L) = c 
getLogReply(L)@ls.
Nov 7, 2006
40
Logger Rule
(la : logger(A))
=={deliver(av)/
seta(a,Log,
geta(a,Log)+{av})}==>
(la : logger(A))
if a in A
Nov 7, 2006
41
Reporter Rule
(ra : reporter(A)) (ra  [email protected])
==
{ /seta(a,Log,{}) for a in A}==>
(ra : reporter(A))
(c  report(L)@ra)
where L = Union(a in A, get(a,Log))
Nov 7, 2006
42
Log Server Rules
(ls : logServerI(R)) ( ls  [email protected] )
==>
(ls : logServerW(R,c,{},R))
{r  [email protected] | r in R }
(ls : logServerW(R,c,L,R'+r)) ( ls  report(L')@r )
==>
(ls : logServerW(R,c,L+L',R')) if r not in R’
(ls : logServerW(R,c,L,{}))
==>
(ls : logServerI(R)) ( c  getLogReply(L)@ls )
Nov 7, 2006
43
Logging Non-interference
Requirement
A system S satisfies the logging noninterference requirement if:
– non-logging meta actors do not set Log
attributes
– the only messages sent to logging meta
actors by non-logging meta actors are log
request messages addressed to the log
server
Nov 7, 2006
44
Logging Theorems
• Theorem 1 (Base-meta noninterference)
– If system S has Logging Behavior, then Log
meta-actors of S preserve base-level
behavior.
• Theorem 2 (Behavior implies service)
– If system S has Logging Behavior and
satisfies the logging initial conditions and noninterference requirements, then S provides
logging service.
Nov 7, 2006
45
Theorem 2 Proof -- LogOk
LogOk holds for all system configurations:
• If the log server is idle, then there are no
undelivered internal logger system messages.
• If the log server is waiting for reports from R',
then there are no undelivered messages to or
from the other reporters, and for each reporter ra
in R' there is a single undelivered message,
either
– (ra  [email protected])
or
– (ls  report(L)@ra)
Nov 7, 2006
46
Theorem 2 Proof Responsiveness
Every request receives a unique reply
• by fairness messages will be delivered
(once)
• by LogOk a waiting log server will get the
expected replies and respond to the
request it is handling
Nov 7, 2006
47
QoS Broker Case Study
• Multimedia (MM) Server Design & Management
– Multimedia Load Management
• Adaptive scheduling of incoming MM requests
• Reconfigure data to optimize servicing of requests
– Cost-based QoS metrics
• QoS Broker
– coordinates activities in a distributed MM system
• interactions between multiple QoS sessions
• interactions across multiple system services
– manages requests -- admission control
– manages data placement activities
(Venkatasubramanian, Talcott & Agha, TOSEM 2004 )
Nov 7, 2006
48
Light-weight Verification Methods
• Concolic Testing
– Combine symbolic and concrete testing
• Runtime Verification
– Monitoring specifications
• Probabilistic Models
– Statistical Model Checking
As opposed to
• Theorem Proving
• Model Checking all states
Nov 7, 2006
49
Decentralized Runtime Monitoring
• Distribute property
– Properties expressed with respect to a process
– Local properties at every process
• Decentralize Monitoring
–
–
–
–
Maintain knowledge of global state at each process
Update knowledge with incoming messages
Attach knowledge with outgoing messages
At each process check safety property against local
knowledge
Nov 7, 2006
50
Decentralized Monitoring
Example
“If a receives a value from b then b calculated the
value after receiving request from a”
valRcv → @b((valComputed  @a(valReq)))
valComputed  @a(valReq)
@a(valReq)
(valComputed  @a(valReq))
b
valComputed
a
valReq
Nov 7, 2006
valRcv
valReq
valRcv → @b((valComputed  @a(valReq)))
51
Past time Distributed Temporal Logic (ptDTL)
• Based on epistemic logic
– [Aumann76][Meenakshi et. al. 00]
• Properties with respect to a process, say p
• Interpreted over a sequence of global states that
the process p is aware of
– Each process monitors the properties local to it
– No need for extra messages to create a relevant
portion of global state
– KnowledgeVector keeps track of relevant global state
that can effect a property.
Nov 7, 2006
52
Remote Expressions in pt-DTL
• Remote expressions – arbitrary expressions
related to the state of a remote process
• Propositions constructed from remote and local
expressions
“If my alarm is set then eventually in past
difference between my temperature and
temperature at process b exceeded the allowed
value”
alarm → ((myTemp - @btemp) > allowed)
Nov 7, 2006
53
Safety in Airplane Landing
“ If my airplane is landing then the runway
that the airport has allocated matches the
one that I am planning to use”
landing → (runway = @airportallocRunway)
Nov 7, 2006
54
Leader Election Example
“If a leader is elected then if the current
process is a leader then, at its knowledge,
none of the other processes is a leader”
elected → (state=leader → /\i≠j(@j(state ≠ leader)))
Nov 7, 2006
55
pt-DTL syntax and semantics
• Fi ::= true | false | P(Ei) | : Fi | Fi Æ Fi
| ¯ Fi | ¡ Fi | Fi | Fi S Fi
| @jFj
• Ei ::= c | vi 2 Vi | f(Ei)
| @jEj
propositional
temporal
epistemic
functional
epistemic
• ¯ Fi : previously Fi
• c : constant
• ¡ Fi : always in past Fi
• vi : variable at process I
• Fi : eventually in past Fi
•P(Ei) : predicate on Ei
• Fi S F’i : Fi since F’i
• f(Ei) : function f applied to Ei
• @jFj: Fj at process j
• @jEj : expression Ej at process j
Nov 7, 2006
56
Interpretation of @jEj at process i
s31
p3
m1
p2
s32
s33
m4
s22
m2
s21
s23
m3
p1
s11
s12
Since, at s23 p2 is aware of s12 of p1
value of @1E in s23 at p2 = value of E in s12 at p1
Nov 7, 2006
57
Monitoring Algorithm
• Requirements
– Should be fast so that online monitoring is
possible
– Little memory overhead
– Additional messages sent should be minimal;
ideally zero
• KnowledgeVector
– Motivated by Vector Clocks
– Unlike Vector Clocks size independent of
number of processes
Nov 7, 2006
58
KnowledgeVector
• KV is a vector
– one entry for each process appearing in
formula
– KV[j] denotes entry for process j
– KV[j].seq is the sequence number of last
event seen at process j
– KV[j].values stores values of j-expressions
and j-formulae
Nov 7, 2006
59
KnowledgeVector Algorithm
• [internal event]: (at process i)
store eval(Ei,si) and eval(Fi,si) for each @iEi and @iFi in
KVi[i].values
• [send m]:
KVi[i].seq à KVi[i].seq + 1. Send KVi with m as KVm
• [receive m]:
for all j, if KVm[j].seq > KVi[j].seq then
– KVi[j].seq à KVm[j].seq
– KVi[j].values à KVm[j].value
– store eval(Ei,si) and eval(Fi,si) for each @iEi and @iFi
in KVi[i].values
Nov 7, 2006
60
Example
0
2
2
5
6
6
p3
0
2
2
2
5
6
6
6
p2
Y=7
Y=3
violation
0
0
1
1
2
5
9
9
6
6
p1
X=5
X=9
X=6
¡(Y ¸ @1X) at p2
Nov 7, 2006
KV[1].seq
KV[1].values
61
DIANA Architecture
pt-DTL
Monitor
Nov 7, 2006
62
Modeling Large Scale
Distributed Systems
• Each node is modeled by a finite state
machine
• Cannot represent the state of all nodes
as a product of individual states
– 1000 nodes of 5 state machines  51000
states
Nov 7, 2006
63
Models of Time
• Global synchronous wall clock
– Synchronization is too tight
– Too detailed an execution model
t
Future causality
R
• Asynchronous, distributed time
– Vector clocks are too expensive
– Application behavior is complicated
Need a more expressive model of
time:
• Notion of distance and
distribution.
• Space-Time cone of causal
influence.
Nov 7, 2006
Q
P
Not
Causally
related
x
S
Past causally
connected
y
Light Cones
64
WSN modeling
• Statistically abstract the state of a WSN
– Represent a state as a probability mass
function (pmf)
– e.g.: 90% of the nodes are in ‘READY’ state.
• Model a WSN as Discrete Time Markov
Chain (DTMC)
• Periodic sampling of a real WSN  DTMC
estimation
Nov 7, 2006
65
Features
1.0
A
B
1.0
• With PCTL like logics, ‘P[X=A] > .3 is always true’ is
always false regardless of initial pmfs
• However if 50 out of 100 nodes are in A state and the
others are in B state =>
50% of the nodes are always in A state.
• iLTL can specify this situation because it works on pmf
Nov transitions
7, 2006
66
iLTL Formula
• Syntax
Nov 7, 2006
67
iLTL Formula
:atomic propositions
• At least 10% more nodes are in READY
state than in IDLE state
– P[X=READY] > P[X=IDLE] + 0.1
– P[X=READY] - P[X=IDLE] > 0.1
• Expected Queue length is less than 2
– 1*P[Q=S1] + 2*P[Q=S2] + 3*P[Q=S3] < 2
• Availability of a system X is 10% larger than
that of a system Y
– P[X=READY] > P[Y=READY] + 0.1
Nov 7, 2006
68
Main Theorem
• If
– Markov matrix M is diagonalizable
– Absolute value of second largest eigenvalue of M is
strictly less than 1
– For all inequalities of an iLTL formula Ψ, the steady
state expected value of LHS is not equal to its RHS
• Then
– There is a bound N after which all inequalities of Ψ
become constants
Nov 7, 2006
69
Model Checking Algorithm
Nov 7, 2006
70
iLTLChecker
• http://osl.cs.uiuc.edu/~ykwon4
Nov 7, 2006
71
Example Markov Reward Model
• Example:
– send/ack
– S={s, ra, rX, XX, d}
– Expected energy consumption
Nov 7, 2006
72
Model Checking
an Agilla Application
• Agilla is an agent middleware for sensor
networks
• Markov Chain Agilla=(S,M),
– S = {Halt, Wait, Arrive, Leave }
– M is 4x4 matrix that is estimated
• Energy consumption for each state
– r = [0,1,3,10] pA for each state from 3V source
– Expected energy consumption
– E[energy] = r*x, where xi = P [X=si]
Nov 7, 2006
73
Model Estimation
•
Nov 7, 2006
Sampling from 20 motes -> Markov model estimation
74
Model Checking
Model:
Markov chain Agilla
has states :
{ H, W, A, L},
transits by :
[
0.5405,
0.4039,
0.0567,
0.3765,
0.2973,
0.0381,
0.1055,
0.1815,
0.0175,
0.3444,
0.5593,
0.0788,
0.7020;
0.1044;
0.0000;
0.1936
]
Specification:
a : 1*P{Agilla=W}+ 3*P{Agilla=A}+ 10*P{Agilla=L} > 2.25,
b : 1*P{Agilla=W}+ 3*P{Agilla=A} +10*P{Agilla=L} < 2.3
<>[] ~ (a /\ b)
Is the expected energy between 2.25 to
2.3pW?
Nov 7, 2006
75
Conclusions
• Programming Abstractions
• Richer models of time, state, and
transitions
– Probabilistic models and properties
• Lightweight Formal Methods
Nov 7, 2006
76
Descargar

Separating Concerns: Actors, Coordination Constraints, …