Adaptive Programming.
An adaptive program is one that changes its behavior base on the current state of its environment. This notion of adaptivity is formalized, and a logic for reasoning about adaptive programs is presented. The logic includes several composition operators that can be used to define an adaptive program in terms of given constituent programs; programs resulting from these compositions retain the adaptive properties of their constituent programs. The authors begin by discussing adaptive sequential programs, then extend the discussion to adaptive distributed programs. The relationship between adaptivity and self-stabilization is discussed. A case study for constructing an adaptive distributed program where a token is circulated in a ring of processes is presented.
Introduction
An adaptive program is one that changes its behavior according to its environment. Often,
the motivation for changing the program behavior is to satisfy some performance criteria: the
performance of one behavior is superior to that of other behaviors in some environment. In
this case, adaptivity is a technique for performance optimization in a dynamic environment.
Another reason for changing the program behavior has to do with logical correctness: only
one behavior is correct in a certain environment. In this case, adaptivity is a matter of the
program functioning properly in a changing environment.
This paper is an investigation of a particular class of adaptive programs. The following
examples motivate the investigation.
ffl Consider a system of distributed processes that communicate via a shared bus. At
each instance, the processes use either one of two protocols to control their access to
the bus - an Ethernet-like protocol [11] and a token-ring protocol [9]. The Ethernet-like
protocol performs well during periods of low contention (when a small number
of processes need to use the bus), but performs poorly during periods of high con-
tention. On the other hand, the token-ring protocol works well during periods of high
contention, but is less efficient than the Ethernet-like protocol during periods of low
contention. The system should dynamically switch between the Ethernet-like protocol
and the token-ring protocol based on the activity of the bus. Ideally, any switch from
one protocol to another should occur instantaneously at all processes; however, because
the system is distributed, there may be a short period in which some processes
have switched protocols while other processes have not.
ffl A resource allocation program is required to minimize the amortized cost of resource
allocation. Two strategies are employed for resource allocation: a pessimistic strategy
and an optimistic one. Comparing the amortized cost of the two strategies, it happens
that the pessimistic strategy has a lower cost when worst-case resource requests are a
significant proportion of all resource requests; otherwise the optimistic strategy has a
lower cost. The program monitors resource requests and, from time to time, switches
from one strategy to another as is appropriate.
ffl In a distributed system for traffic control, traffic routes are changed to optimize traffic
flow. It is given that traffic patterns depend on the time of day; but time is measured
by local clocks that may drift apart. The system executes an adaptive program that
optimally controls traffic in spite of discrepancies in the local clocks. For instance,
the transition from morning to afternoon may not be instantaneous, but eventually
all clocks agree that it is afternoon - then the system should route traffic to optimize
for afternoon patterns.
These three examples illustrate the main characteristics of the class of adaptive programs
that we are interested in:
1. Changes in the environment do not necessarily occur instantly, but may occur gradually
over a short period of time. (In the above traffic control example, some clocks
may indicate a change in the environment, while others may not. This continues for
a few seconds due to the drift between the clocks; then all clocks indicate the same
change in the environment.)
2. Periods of change in the environment are relatively short and are usually followed
by long periods of stability. (In the traffic control example, a 24-hour day is divided
into say three periods: morning, afternoon, and night. The environment remains
unchanged during each period; it changes only at the end of the period. Thus, each
change in the environment is followed by a long period of stability during which the
environment remains unchanged for a few hours.)
3. During periods of change in the environment, the adaptive program behaves arbi-
trarily; in other words, nothing can be asserted about the program's behavior during
those periods. On the other hand, during periods of stability where the environment
remains unchanged, the adaptive program secures a behavior that is consistent with
the current environment. (In the traffic control example, the controller program behaves
arbitrarily for a short period, e.g. a few seconds, during which the environment
switches from morning to afternoon. When the environment settles in the afternoon
period, the controller secures a behavior that optimizes the afternoon traffic patterns.)
In this paper, the environment of a program is defined by a set of "input" variables that
can be read, but not written, by the program. We assume that program computation and
environmental change are asynchronous. That is, at any time during program execution,
the values of input variables can change arbitrarily. As a consequence, it is difficult to say
in all cases what correct adaptivity should be. For instance, in response to an environmental
change, the adaptive program may compensate by computing a choice for a new
but by the time the choice is effected, the environment may have changed input
variables again. So long as this scenario is repeated, the adaptive program cannot behave
appropriately for the current values of its input variables.
The notion of an adaptive program is somewhat similar to the notion of a self-stabilizing
program [2, 3, 6, 10]. A self-stabilizing program has the property that its computation leads
to and maintains a "legitimate" state from any, arbitrarily chosen, initial state. Because it
is an arbitrary state, the initial state of a self-stabilizing program has no special attributes.
Consequently, self-stabilizing programs are interesting because they prevail over transient
faults: the program state following a transient fault is, in effect, a new initial state. In
the same way, we view environmental change as a transient phenomenon, after which an
adaptive program will converge to appropriate behavior.
In this paper, we formalize the definition of program adaptivity, and present some logical
properties of the definition; we also present some operators for combining adaptive programs
while retaining all their adaptive properties. We begin by discussing adaptive sequential
programs in Sections 2 and 3, then extend the discussion to adaptive distributed programs
in Sections 4 and 5. In Section 6, we investigate the relationship between adaptivity and self-
stabilization. In Section 7, we outline a case study for constructing an adaptive distributed
program where a token is circulated in a ring of processes. Section 8 contains a discussion
of the applicability of the proposed methods. Concluding remarks are in Section 9.
2 Adaptivity of Sequential Programs
In this section, the concepts of programs and program computations are defined. The
characteristic property of adaptive programs, called secures, is also defined. Although
these definitions are restricted to sequential programs, they are extended to distributed
programs in Section 4.
Let S be a sequential program defined by is a set of variables and A is
a set of actions. Every variable in V has a prescribed domain and is either an input variable
or an internal variable. Each action in A is a guarded assignment of the form P ! C;
where P is a predicate over the variables in V; and C is an assignment statement that
assigns values to internal variables only.
The state-space of S is the cartesian product of the domains of all variables in V: A state
of S is an element of the state-space; it thus denotes a value for each variable in V: A state
predicate is a boolean function of the state-space. If the value of a state predicate P is true
at some state then we say P holds at r:
A state predicate P is an input predicate in program S; denoted input P in S (or simply
input P when S is understood) iff P is a predicate whose definition makes no reference
to any internal variable of S:
A transition of S is an ordered pair of states (r; s) so that S has an action P ! C; where P
holds at and s is obtained from r by replacing the values of internal variables as indicated
by the assignment statement C: If (r; s) is a transition and P holds at then we say
is enabled at r: Note that our definition of transition introduces nondeterminism:
more than one transition may originate from a state r if more than one action is enabled at
r:
A computation is a sequence of states so that every consecutive pair is a transition. Empty
and single-state sequences are therefore computations and any prefix or suffix of a computation
is a computation. We restrict the scope of prefix and suffix as follows. Any prefix of
a computation is a finite sequence; any suffix of a computation is a suffix with respect to a
(finite) prefix; any suffix of a non-empty computation is a non-empty computation.
A computation is maximal iff it is not a proper prefix of any computation. That is, a
maximal computation is either infinite or there exists no transition originating at the last
state of the computation.
A sequential program is adaptive iff all its properties of interest can be stated in terms of
the following secures relation:
secures Q in S (adaptivity)
iff P is an input predicate in S; and for each maximal computation of S: if P holds at each
state in the computation then there exists a suffix of the computation such that Q holds at
each state in the suffix.
For convenience, we write P secures Q when the program S is understood.
Operationally, we interpret P secures Q in S as follows. If P is an input predicate (other
than false), then it is possible for the environment to set the values of the input variables
of program S so that P is satisfied. After P is satisfied, program S will converge on its own
accord to a situation in which Q holds and continues to hold indefinitely. After Q is satisfied,
if the environment should again change, subsequent program transitions in effect constitute
a new computation, and the definition of adaptivity applies to this new computation.
Example 1. Consider the following program that has three input variables b; c; and d;
one internal variable z; and two actions.
input variable b; c; d :
internal variable z
actions
For this program we prove (b = There are two proof obligations
from the definition of secures. First, (b = 0) is an input predicate because b is
an input variable. Second, consider any maximal computation where (b = 0) holds at each
state. Only the first action is enabled at each state of this computation. Thus, the first transition
in the computation establishes (b subsequent transitions
leave the state unchanged. This completes our proof of (b =
Similarly it can be shown that (b = 1) secures
The secures properties of a program can be proved by appealing to the definition of secures
or can be deduced from the following inference rules. (Correctness of these rules can be
established from the definition of secures; the proofs are given in the Appendix.)
input P
secures true
secures Q
secures Q; input R, R )
R secures Q
secures Q; Q
P secures R
(weakening)
secures Q; R secures T
(junction)
Other properties of secures can be derived by various combinations of these rules. For
instance,
input P
secures P (stability)
can be derived from the truth and sharpening rules. Similarly,
false secures R (falsehood)
can be derived from the stability and weakening rules.
3 Composition of Sequential Programs
Adaptive programs can be composed by combining "smaller" adaptive programs: the composed
programs retain all the secures properties of their constituent programs. This section
describes two types of composition: level and hierarchical. Level composition combines two
programs so that they have equal roles in the resulting composite program. Hierarchical
composition combines two programs so that one of the programs is subordinate to the other.
These compositions can be applied repeatedly to combine any finite number of programs
into a single program.
3.1 Level Composition
Level composition is our principle tool for constructing an adaptive program. Prerequisite for
level composition of two programs is their compatibility and their having secures properties.
Compatibility is a syntactic restriction on the variables of the programs.
Given two sequential programs S and T; S compatible T holds iff each variable with the
same name in both S and T has the same type in both programs. Note that the type of a
variable determines whether the variable is an input or internal variable; it also determines
the domain of values for the variable. Note also that compatibility of two programs is not
difficult to achieve: by renaming variables in one program so that no name is common to
both programs, compatibility is assured.
Let S and T be two compatible sequential programs, and let e be an input boolean variable
that does not occur in S or T: Let S / e . T denote the program (W; B) where
W is the union of feg; the variables of T; and the variables of S;
B is the union of two sets of actions: the first set contains, for each action
of program S; the action the second set contains, for each action
the action (:e - P
Based on this definition, the following rule can be proved.
secures Q in S;
P secures R in T;
compatible T
secures Q in S / e . T;
secures R in S / e . T
(level composition)
Example 2. It is required to design a traffic control program. In the "morning" the
program directs traffic either right or across, and in the "evening" it directs traffic either
left or across. Consequently we propose a program that has an internal variable traffic that
can take any of the values: left, right, or across. Inspired by our level composition rule, we
start with two adaptive programs, a morning program S and an evening program T: Each
of these two programs contains assignments to the internal variable traffic. By combining
the two programs using an input variable named morning, we construct the required traffic
control program as S / morning . T:
The morning program S is defined as follows.
input variable waiting: boolean;
internal variable traffic: (left, right, across);
actions waiting ! traffic := across, :waiting ! traffic := right.
It can be shown that
waiting secures
:waiting secures
This result can be reduced by the junction and sharpening rules to
true secures ((waiting -
(:waiting
The evening program T is defined as:
input variable waiting: boolean;
internal variable traffic: (left, right, across);
actions waiting ! traffic := across, :waiting ! traffic := left
By symmetry with S the adaptivity property of T is
true secures ((waiting -
(:waiting
The required traffic control program S / morning . T is:
input variable waiting, morning: boolean;
internal variable traffic: (left, right, across);
actions (morning - waiting) ! traffic := across;
(morning
(:morning
(:morning
The following adaptivity property of program S / morning . T is obtained from the level
composition rule. After simplification the result is
true secures (waiting -
(:waiting - morning -
(:waiting - :morning -
For an operational view of this simple example, consider the effect of a change in the
program's environment. After an environmental change, it is enough that the environment
be static long enough for execution of one action of S / morning . T to assure that the
program correctly adapts to its current environment by assigning traffic to the appropriate
value. If the environment changes during execution of an action, the assignment to traffic
may be inappropriate; however secures does not specify behavior when the environment
changes during computation. As soon as the environment stabilizes long enough for the
complete execution of an action, the program correctly adapts.
3.2 Hierarchical Composition
The notation for a hierarchical composition of programs T and S is T ; which informally
means that the execution of program S is suspended until program T terminates; variables
declared as input variables in S may be internal variables in T so that T can play the role
of environment for S:
A prerequisite for hierarchical composition of two programs is the controllability of one of
them by the other. For sequential programs S and T; the relation T controls S holds iff
each variable with the same name in both S and T has the same domain in both programs,
and no internal variable of S is a variable in T: There is no restriction on the input variables
in S: an input variable in S may be an internal or input variable in T:
The following two definitions introduce notation to state the hierarchical composition rule.
Let idle:T; for a sequential program T; denote the conjunction of the negated guards of all
actions of T; i.e.,
Thus, idle.T holds at any state where no action of T is enabled.
Let S and T be two sequential programs where T controls S: Let S; T denote the
program (W; B) where
W is the union of the variables of T and the variables of S that are not variables of
T: (Thus, any variable that is internal to program T and also input to program S is
internal to program W:)
B is the union of the actions of two sets of actions: the first set consists of the actions of
program T ; the second set contains, for each action P ! C of program S; the action
Based on this definition, the following rule can be proved.
secures
Q secures R in
T controls S
P secures R in T ; S
(hierarchical composition)
An operational interpretation of this rule is as follows. Suppose that the execution of
the program T ; S starts at a state satisfying P and not Q. At this state, the actions
of T are enabled and can be executed to secure Q while the other actions, of the form
disabled. The execution of the T actions continues until Q
is established ensuring idle:T: At this state, the actions of S become enabled and can be
executed to secure R: Note that this notion of hierarchical composition is more or less
similar to the notion of superposition of Chandy and Misra in [4].
Example 3. Let program Y be defined as follows.
input variable clock:
internal variable morning: boolean;
actions
clock morning := true;
morning := false
It is straightforward to show that program Y is suitable for hierarchical composition with
the composite program S / morning . T of Example 2. The proof consists of four steps.
First, it can be shown that
secures morning in Y
Second, it can be shown that
The third condition follows by the level composition rule:
morning secures ((waiting -
(:waiting - traffic = right)) in S / morning . T
Fourth, the internal variable traffic of S / morning . T does not appear in Y; therefore Y
controls S / morning . T .
Thus, the hierarchical composition rule can be applied to combine the two programs Y and
S / morning . T into one program Y ; (S / morning . T ) with the result
((waiting -
(:waiting
4 Adaptivity of Distributed Programs
A distributed program is defined as a sequential program that meets some additional constraints
imposed by partitioning its variable set and its action set. Thereby, the definitions
of adaptivity, compatibility and composition in Sections 2 and 3 have straightforward extensions
for distributed programs.
A distributed program is a pair (S; ff); where is a sequential program and ff is a
partition of variables V and actions A subject to the following constraint: ff partitions V
into a collection of sets partitions the actions of A into sets A i ;
such that for every
the assignment statement C assigns
values to variables of V i
only. Note that some of the sets in fV i
and fA i
g may be empty.
In this definition, a distributed program (S; ff) may be interpreted as a collection of sequential
programs called processes.
Each process S i is defined by
are corresponding sets of variables and actions defined by the partition ff;
and W i is the set of all variables appearing in A i but not in V i .
Observe that for a given sequential program S there may be many choices of ff to satisfy
the definition of a distributed program. The partition possible for any S;
in which case (S; ff) is the single process S: Also notice that, whereas ff partitions V into
disjoint sets, processes may share variables - provided that no two processes assign to the
same variable. Thus, ff locates each variable at exactly one process such that a process may
read from, but not write to, variables located at other processes. Input variables are exempt
from these considerations: since no process writes to an input variable, the location of an
input variable is arbitrary (for example, ff could place all input variables in some V k and let
A k be empty). In practice, the location of input variables is a significant consideration for
distributed systems, and we develop a special rule in Section 5 to deal with this concern.
The computations of the distributed program (S; ff) are exactly the computations of the
sequential program S: That is, we model concurrency by interleaving: each
computation of (S; ff) is an interleaving of the computations of its processes. The definition
of secures for a distributed program is as follows.
secures Q in (S; ff) iff
(S; ff) is a distributed program and P secures Q in S (concurrency)
From this definition, the rules for reasoning about the secures properties of sequential
programs extend in a straightforward way for reasoning about the secures properties of
distributed programs.
5 Composition of Distributed Programs
Two distributed programs are combined by combining their corresponding processes. To
this end we extend the notions of level and hierarchical composition to distributed programs.
5.1 Distributed Level Composition
We start by extending the notion of compatible to distributed programs.
compatible T; and for every
variable x named in both S and
x is assigned in S i
assigned in T k
This definition of compatible is intended to preserve the structure of ff (and fi) in the
composite program consisting of (S; ff) and T; fi); that is, the partition of variables in
the composite program has the same rank as that of ff (and fi). For example, the definition
assures that no two processes in the composite program write to a common variable.
Note that the requirement that is made for simplicity; for instance, if
then we can define some ff 0 by "padding" the partition of variables given
by ff with empty sets to satisfy rank(ff 0
Let e be a vector of input boolean variables, that is,
the two predicates all:e and no:e as follows.
Given two compatible distributed programs (S; ff) and (T; fi); let e be a vector of boolean
input variables that occurs neither in S nor T: The distributed level composition of compatible
distributed programs is written (S; ff)/e.(T; fi); which denotes the distributed program
whose processes are fS i
secures Q in (S; ff);
P secures R in (T; fi);
secures Q in (S; ff) / e . (T; fi);
secures R in (S; ff) / e . (T; fi)
(distributed level composition)
The proof for this rule is similar to the proof for the level composition rule given in the


Appendix

.
5.2 Distributed Hierarchical Composition
Let (S; ff) and (T; fi) be two distributed programs. (T; fi) controls (S; ff) iff
rank(fi) and T controls S.
Suppose (S; ff) controls (T; fi); the distributed hierarchical composition of (S; ff) and
(T; fi) is written (T; fi); (S; ff); which denotes the distributed program whose processes are
In order that this distributed hierarchical composition have the
desired adaptivity properties, we define the following property of a distributed program's
computation.
Let (S; ff) be a distributed program. (S; ff) fair-under P holds iff for every computation
of (S; ff) where such that P holds at all states, every suffix of the computation contains a
transition of S i ; for every i in the range 0
secures Q in (T; fi);
Q secures R in (S; ff);
P secures R in (T; fi); (S; ff)
(distributed hierarchical composition)
The proof of this rule is similar to the proof of the hierarchical rule in the Appendix.
Note that it may not be possible to partition a computation of (T; fi); (S; ff) so that all the
transitions corresponding to (T; fi) precede all the transitions corresponding to (S; ff): For
instance, it is possible that some action from S j
executes, and later some action from T k
executes (k 6= j). This is possible because in the composite (T; fi); (S; ff) the guard corresponding
to the S j
action depends on idle:T j ; but does not depend on idle:T k : However,
within each process T i
, the actions of T i
have "priority" over the actions of S i
so long
as some action of T k , for some k is enabled, it will eventually be executed thanks to (S; ff)
fair-under P , which assures that continued execution of (S; ff) depends on some action
from S k - and T k actions have priority over S k actions. Thus, (S; ff) cannot prevent the
eventual progress of (T; fi) in the composite program.
6 Adaptivity and Self-Stabilization
In this section, we discuss the relationship between adaptivity and self-stabilization. In
many cases, adaptivity appears to be a generalization of self-stabilization. We start by
defining the notion of self-stabilization in terms of our model of computation.
For a sequential program S and predicate Q; S self-stabilizes to Q iff each maximal
computation of S can be partitioned into a prefix and a suffix where each state in the prefix
satisfies :Q and each state in the suffix satisfies Q:
In the definition of self-stabilization, the predicate Q is "stable" (or closed) with respect to
computation: once a state satisfying Q is reached, all subsequent states also satisfy Q: In the
literature of self-stabilization [3, 2, 6], the predicate Q is typically a predicate over internal
variables of the program. However, the definition above also permits Q to refer to input
variables. If Q refers to input variables, then the meaning of "legitimate" state depends on
the environment; such a self-stabilizing program also "adapts" to its environment. Thus we
view self-stabilization as a particular type of adaptivity.
The relationship between self-stabilization and adaptivity is stated by the rule
S self-stabilizes to Q
true secures Q in S
which can be easily proven from the definitions of secures and self-stabilization.
The converse of the above rule does not hold in general. That is, true secures Q in a
program does not imply that the program self-stabilizes to Q: There are programs for which
true secures Q holds, but the predicate Q is not stable because there exist transitions of
the form (r; s) where r satisfies Q; but s does not satisfy Q (Section 7 contains an example
of this).
Usually, if true secures Q holds, then there exists some predicate R such that R ) Q
and the program self-stabilizes to R; in such cases, there is a kind of converse relationship
between adaptivity and self-stabilization. However, the following example demonstrates
that not all instances of true secures Q imply underlying self-stabilization. The example is
of theoretical interest because it exploits the nondeterminism in our model of computation.
Let Z be the program
internal variable x : domain (0,1,2)
actions
It is straightforward to show that true secures (x 6= 2) in Z : every maximal computation
whose initial state is has a suffix where at every state; also every
maximal computation whose initial state is x = 1 has a suffix where either at every
state or x = 0 at every state.
We now refute the possibility of some R satisfying Z self-stabilizes to R and R )
Expansion of R ) four possibilities for R: false,
In each of these four cases we exhibit a maximal computation that cannot be partitioned
to satisfy Z self-stabilizes to R: First, Z does not self-stabilize to false because maximal
computations of Z are non-empty. Second, Z does not self-stabilize to
is a maximal computation consisting of its states. Third, Z does not self-
stabilize to there is a maximal computation consisting of its
states. Fourth, Z does not self-stabilize to (x 6= 2) due to following maximal computation:
a non-empty sequence of followed by a state, followed by an infinite
sequence of states. (end of refutation).
7 Case Study: The Adaptive Token
In this section, we apply the two distributed composition rules (level and hierarchical) to
construct an adaptive distributed program where a token is circulated in a ring of processes.
The construction proceeds in three steps. First, two distributed programs are presented:
in each program, a token is circulated in a ring of processes, but the two programs differ
in their policies for token circulation. Second, these two programs are combined, using the
distributed level composition rule, to form an adaptive program whose behavior can be
switched between the behaviors of its two constituent programs. Third, this adaptive program
is combined with a controller program, using the distributed hierarchical composition
rule. The controller program selects, based on the current environment, which of the two
constituent programs is to be executed.
The two constituent programs have different policies for circulating the token. One program
circulates a token continuously (busy token); the other program circulates the token only
when some process, other than the current holder, requests the token (lazy token). A busy
token behavior is more reasonable in an environment where the token is requested frequently
by different processes. A lazy token behavior is more reasonable in an environment where the
token is infrequently needed. The adaptive program switches between these two behaviors
according to the observed frequency of token requests.
7.1 Busy Token
The busy token program, henceforth called Busy, continuously circulates one token among
a set of n processes: Busy j fS i
each process S i
is defined as
follows.
internal variable x i
actions x i
In the above program and for the remainder of the case study, we adopt the convention that
all subscripts of the are modulo n where n is the number of processes in
the system.
We say that process S i holds a token when x i mod the predicate homebusy be
true iff the state of Busy satisfies: there is exactly one process S i satisfying
Informally, homebusy describes a state where exactly one process either has a token or will
have a token immediately after its next transition.
It can be shown that
true secures homebusy in Busy :
The proof consists of showing that Busy self-stabilizes to L where L is a predicate satisfying
predicate L has a complicated formulation, and the proof of
self-stabilization has little in common with the methods of this paper, we did not include
the proof in the paper. (The reader can find the proof in [8]. It is not the case that Busy
self-stabilizes to homebusy - there exist transitions from a state with exactly one token
to a state with two tokens.)
7.2 Lazy Token
The lazy token program, henceforth called Lazy, circulates one token among a set of n processes
when and only when one or more of the processes needs a token: Lazy j fT
each process T i is defined as follows.
internal variable x i
internal variable y
input variable z
actions
Each process T i has an integer variable x i and two boolean variables y i and z i . Variable z i
is an input variable indicating the need for a token by its process T i . We say that process
holds a token when x i mod The following predicate is used in the guard of one
action:
The predicate m i
holds when T i
has a token, or T i+1
has a token, or when there is a token
and T i+1
The adaptivity property for this program is
true secures homelazy in Lazy
where the homelazy predicate holds at any state where there is exactly one process T i
satisfying
7.3 Adaptive Token
The busy and lazy token programs are compatible; hence they can be composed using the
distributed level composition rule. The resulting composite program Busy /e.Lazy satisfies
all:e secures homebusy, and
no:e secures homelazy
The program Busy / e . Lazy is applicable in an environment where all:e or no:e holds.
Presumably, all:e should hold in an environment where processes frequently require use of
the token, that is, where the Busy program behavior is more appropriate.
To illustrate hierarchical composition, we present a fully distributed program to obtain the
consensus all:e from input variables that may have arbitrary values. Let b be an array of
boolean input variables that represent frequency of token requirement, that is, the variable
b i is true iff process i of Busy / e . Lazy "frequently" requires the token. We define the
program Concur j fZ i j
each process Z i is defined as follows.
internal variable a
internal variable e
input variable b
actions
a ii
a ii
:= a (i\Gamma1)k ]
The function f outputs a boolean value from an input n-element boolean array (majority
vote is a plausible definition for f). The last line of the program denotes the actions
that copy, for each k; where the boolean variables a (i\Gamma1)k into a ik . It
can be shown that all computations of Concur are finite, and that Concur satisfies
By the junction rule, it follows that true secures (a i
holds for all i. Thus, each process
holds an image of b in the vector a i
. Consequently, it is straightforward to show
secures all:e - :f(b) secures no:e
By inspection, Concur controls Busy / e . Lazy can be verified. In [8] it is shown that
Concur ; (Busy / e .Lazy ) fair-under true holds. Therefore distributed hierarchical composition
is applicable with the result
secures homebusy in Concur ; (Busy / e . Lazy) and
secures homelazy in Concur ; Busy / e . Lazy)
8 Applicability
This section addresses some of the concerns related to application of the definitions and
composition rules given in this paper. We discuss limitations of our methodology: level
composition is a tool for constructing a particular class of adaptive programs, so its domain
of applicability is limited. Our definition of secures limits our ability to describe certain
aspects of program behavior.
Our view of adaptivity as "different programs for different environments" is not the traditional
meaning for an adaptive program. Typically, the behavior of an adaptive program is
seen as one program parametrized by environmental inputs. For instance, if P secures Q in
S and Q specifies constraints on input variables, then we have one behavior - the behavior
of S - and S adapts to its environment. This kind of adaptive behavior we call "incremental
adaptivity." Instances of adaptive behavior that are better modeled as different programs
for different behaviors we call "threshold adaptivity." The distinction between incremental
and threshold adaptivity is largely methodological; there are adaptive programs where it is
difficult to say which view is better suited. The methodology for constructing incremental
adaptive programs is outside the scope of this paper. Our methodological contribution is
limited to those adaptive programs for which threshold adaptivity is appropriate.
A significant application of threshold adaptivity appears in [1], which presents an adaptive
routing protocol. The problem of adaptive routing in a network is well-known [12]. An
optimal route of a message to its destination is a minimum cost path between the message's
source and destination. As the network changes, costs change and optimal routes have
to be recomputed. Two distributed protocols, each self-stabilizing, are given in [1] for
calculating minimum cost paths in a network. Since both protocols are self-stabilizing, they
are (incrementally) adaptive, responding to changes in network costs. One of the protocols
is a "lazy" program: it reaches a fixed point and performs no computations so long as the
network costs do not change. The other protocol is a "busy" program that repetitively
computes minimum cost paths even if the network costs are static. It turns out that the
lazy protocol is preferable if the network changes infrequently whereas the busy protocol is
better for a rapidly changing network. The two protocols are combined by distributed level
composition to obtain a (threshold) adaptive protocol. If a message is to be routed during
the time of a switch from one protocol to the other, the computation of minimum cost paths
may be incomplete; such a message could be misrouted, delayed or lost. We expect that
message retransmission, after a timeout, can be used to tolerate such transient errors.
Some limitations of secures are related to issues of program behavior during periods of
environmental change or immediately following a change in the environment. To show 'P
secures Q' it is enough to prove that a program converges to Q and maintains Q. But
during convergence to Q; the program may exhibit undesirable behavior. For example, if an
adaptive program is part of a distributed data base service, a transaction might be lost during
convergence to appropriate behavior. Conceivably, such a situation could be addressed
by proving that desired properties hold during convergence (e.g., proving that program
behavior during convergence satisfies safety properties). However, proving properties about
convergence is difficult in the context of our work because the definition of secures does not
permit specification of the initial values of a program's internal variables. Instead of proving
desired properties hold during convergence, we recommend that applications of the methods
in this paper be limited to situations in which unpredictable behavior can be tolerated. For
a data base service, if a transaction is lost, the client of the service could resubmit the
transaction.
A question frequently asked about (adaptive) distributed systems is: How does a user of
the system know when the system is behaving properly? For a distributed system, it is not
possible to answer this question. At any instant, a user of the distributed system has only
a local view; because asynchronous environmental change is possible, information accumulated
by messages from other locations could be inaccurate by the time the information is
assembled to form a global view. The same question is posed of self-stabilizing systems, e.g.,
when does a user know that the system has stabilized? Instead of attempting to answer this
question directly, researchers typically answer the question: How long can it take to stabi-
lize? For an adaptive program in terms of our model, the corresponding question is: what is
the maximum number of transitions required to correctly adapt to the current environment?
This question can be answered for most adaptive programs by the same techniques used
to calculate the costs of self-stabilization (e.g. see [5, 7]). Although we have not done so
for the examples in this paper, it is feasible to analyze worst-case scenarios and bound the
number of transitions required for convergence. After calculating an upper bound for the
number of transitions needed for convergence, if an estimate is given for "real time" taken
by a program transition, then it is possible to specify how long a period of environmental
stability must be to guarantee correct adaptation to a program's current environment.
An exception is the theoretical example given in Section 6, where the nondeterminism in
a maximal computation defies any upper bound on the number of transitions needed for
convergence.
Although we have claimed that it is not possible to correctly adapt to an asynchronously
changing environment during the instant of its change, in practice some changes in the
environmental conditions are acceptable. Often it is enough to have "approximate" adap-
tivity. In order to formalize the notion of approximate adaptivity, stronger assumptions
about the environment are needed: some synchrony between the environment and program
could be given, and the domain of input variables may be specialized. In the framework
of this paper, we do not address approximate adaptivity; however, our tool for variable
abstraction, hierarchical composition, could be useful for approximate adaptivity. Consider,
for instance, a scenario in which the environment changes so frequently that there is never
an adequately long period of stability to assure proper adaptation. By judicious use of
hierarchical composition, it may be possible to "buffer" change in the environment, thereby
allowing the subordinate adaptive program to function for a while in some behavior, rather
than spending all effort switching from one behavior to another.
9 Conclusions
We have studied the problem of adaptivity in a distributed system. One object of our
study is to reason about program behavior with respect to its environment by using few assumptions
about the environment and program computation: we assume that computation
and environmental change are asynchronous; that environmental change is unpredictable;
our model of computation is simple and does not depend on fair computation or control
structures (thereby our results may appeal to implementations driven by interrupts). We
have shown how, even under these restricted assumptions, a logic for reasoning about adaptive
behavior is possible. By restricting our assumptions, we hope that our results have
broad applicability; for example, our results apply to situations of fair computation and a
predictable environment.
A second object of our study is methodological, to develop techniques for constructing adaptive
programs. We do not claim that the techniques proposed in this paper constitute the
only possible solution to adaptive programming, even for the case of "threshold" adaptivity.
An alternative method might resemble the following scenario: periodically, the environment
is sampled; if the sample indicates that a change in behavior should be effected, then a
"broadcast quiesce" operation is initiated; then, after all processes acknowledge that the
active behavior has quiesced, a "broadcast start" operation is initiated for a new behavior.
Such a method relies on distributed synchronization to start and stop behavior (even so, the
signal to start a behavior cannot be instantaneous in a distributed system). Consequently,
programs of individual processes have to deal with problems of distributed control. Note
that if a behavior is explicitly started by some signal, its internal variables can be initialized
at the time a start signal is detected; by contrast, our definition of secures assures that
programs eventually behave properly without any initialization of internal variables. Our
desire to separate concerns of adaptivity from concerns of distributed control led us to the
definition of secures, which does not depend on variable initialization.
Some questions related to our study merit further investigation. If program computation and
environmental change are synchronous, then more specific types of adaptivity can be con-
sidered. For example, if change in the environment has a sinusoidal pattern, with a certain
frequency, can a program adapt to a change in the frequency? Another question is related
to the composition operators we have proposed. Roughly speaking, our hierarchical composition
rule corresponds to sequential composition (;) in a sequential programming language.
Our level composition rule corresponds to the alternative construct (if . then . else . )
in a sequential programming language. Is there also some composition rule corresponding
to an iterative construct (while . do . ) of a sequential programming language?

Appendix


10.1 Proofs of Inference Rules
Each of the proofs in this section is based on the definition of adaptivity, that is P secures Q
for some form of P and Q: From the definition of secures there are two proof obligations.
The first obligation is to establish that P is an input predicate; this is a trivial task of
verification that we omit. The second obligation is to show that every maximal computation
has an appropriate suffix where Q holds at each state - this is the part of the proof we
present in each case below. To further streamline the presentation, we observe that there are
two cases for a maximal computation, either it is empty or non-empty. In case it is empty the
definition of secures reduces to universal quantification over an empty range and secures
holds trivially. Therefore maximal computations are assumed to be non-empty in the proofs.
Consider any maximal computation such that P holds at each state. Observe that
true is a tautology, so true holds at all states.
Sharpening: From the antecedent, in each maximal computation where P holds at each
state there exists a suffix in which Q holds at each state; therefore (P - Q) holds at each
state in the suffix.
Strengthening: Consider a maximal computation - in which R holds at each state. From
also holds at each state in -: The antecedent P secures Q implies
that Q holds at each state in some suffix of -:
Junction (conjunction): Consider a maximal computation - in which (P - R) holds at
each state. Observe that (P - R) ) P and (P - R) ) R; so both antecedents are
applicable; - has a suffix where Q holds at each state and - has a suffix where T holds at
each state, therefore - has a suffix where (Q - T ) holds at each state.
Junction (disjunction): Consider a maximal computation - in which (P - R) holds at
each state. Let (r; s) be some transition in -: There are three cases for
holds at holds at or (iii) (P - R) holds at r: The predicates P and
R are input predicates, so the case (i)-(iii) for state s is the same as the case for r - input
variable values do not change due to transitions. Moreover, one case (i)-(iii) holds for all
states in -: For case (i); P holds at each state in -; and the antecedent asserts there is a suffix
where Q holds at each state, hence Q - T holds at each state of the suffix. The treatment
of case (ii) follows by symmetry. Case (iii) follows from conjunction, shown above, and the
fact
10.2 Proofs of Composition Rules
For proofs of the composition rules we define state projections. A projection maps a state
of a composite program to a state of one of its constituent programs. For instance, let S ffi T
be some composition of the two programs S and T ; let h be the projection from a state of
to a state of S : h excludes variables that appear in S ffi T but not in S: We extend
projections to operate on sequences of states by element-wise application. Observe that if
ae is a sequence of states of S ffi T and P is a predicate over the variables of S; then P holds
at each state in ae iff P holds at each state in h(ae):
Level Composition: The two parts of the rule's conclusion are symmetric, so we demonstrate
one part only. Let f be the projection from a state of S /e.T to a state of S: Observe
that if - is a maximal computation of S / e . T where e is true at all states, then f(- ) is
a maximal computation of S: To complete the proof, let ! be a maximal computation of
S /e.T such that (P - e) holds at each state. By the antecedent (P secures Q in S), the
maximal computation f(!) therefore has a suffix where Q holds at each state. Therefore !
has a suffix where Q holds at each state.
Hierarchical Composition: Let - be an arbitrary maximal computation of T ; S: The
proof obligation is to show that if P holds at each state in -; then - has a suffix in which
R holds at each state. We show this in two steps. First, - can be partitioned into a prefix
and suffix so that Q holds at each state in the suffix. Second, this suffix is a maximal
computation which has, in turn, a suffix in which R holds at each state. For the remainder
of the proof we assume P holds at each state in -: Let f be a projection from a state of T
to a state of S and let g be a projection from a state of T ; S to a state of T:
First step (to show existence of suffix wherein Q holds). Let is the maximal
prefix of - such that some action of T is enabled in each state of g(ffi): We consider three
cases for -:
Case of T is changed in, or missing from the composite T ; S: Each
action of T ; S that is derived from an action of S is not enabled if :idle:T holds.
Therefore the computation g(ffi) is a maximal computation of T: By the antecedent
secures Q in T ), there is a suffix of g(ffi) such that Q holds at each state in the
suffix, hence Q holds at each state in a suffix of -:
of T is enabled in g(- ). Therefore any transition of - is due to
an action derived from program S and f(- ) is a maximal computation of S: Observe
that the first state of g(- ) constitutes a maximal computation of T ; by the antecedent
secures Q in T , it follows that Q holds at the first state of g(- Consequently Q
holds at the first state of - and also at the first state of f(- ) By the definition of Q
secures R in S; the predicate Q satisfies input Q in S; so Q holds at each state of
f(- ), hence at each state of -:
Case 2 Both ffi and ! are non-empty. Since P holds at each state in - and no action of T
is enabled at the first state of g(!), from the antecedent P secures Q in T it follows
that Q holds at the first state of g(!); hence Q holds at the first state of !: Since Q is
an input predicate to program S; no transition derived from an action of S can falsify
Q: Therefore idle:T and Q hold at each state in !:
Second step (to show existence of suffix wherein R holds). Let ae be a suffix of - such that
Q holds at each state in ae: We have assumed that P holds at each state in ae and by the
antecedent no action of T is enabled in g(ae). Observe that ae is a
maximal computation of T holds at all states, and therefore f(ae) is a
maximal computation of S: By the antecedent (Q secures R in S), f(ae) has a suffix so
that R holds at each state in the suffix, hence ae has a suffix in which R holds at each state.



--R

"Composite Routing Protocols,"
"Token Systems that Self-Stabilize,"
"Uniform Self-Stabilizing Rings,"
Parallel Program Design: a Foundation
"On the Costs of Self-Stabilization,"
"Self-stabilizing Systems in Spite of Distributed Control,"
"Convergence/Response Tradeoffs in Concurrent Sys- tems,"
Department of Computer Sciences
IEEE 802.5 Token Ring Access Method
"Self-Stabilizing Extensions for Message-Passing Systems,"
"Ethernet: Distributed Packet Switching for Local Computer Networks,"
Computer Networks
--TR
On the costs of self-stabilization
Parallel program design: a foundation
Uniform self-stabilizing rings
Token Systems That Self-Stabilize
Self-stabilizing extensions for message-passing systems
Ethernet
Self-stabilizing systems in spite of distributed control

--CTR
Mohamed G. Gouda, Multiphase stabilization, IEEE Transactions on Software Engineering, v.28 n.2, p.200-208, February 2002
M. G. Gouda, Multiphase Stabilization, IEEE Transactions on Software Engineering, v.28 n.2, p.201-208, February 2002
Frdric Duclos , Jacky Estublier , Philippe Morat, Describing and using non functional aspects in component based applications, Proceedings of the 1st international conference on Aspect-oriented software development, April 22-26, 2002, Enschede, The Netherlands
J. Beauquier , B. Brard , L. Fribourg , F. Magniette, Proving convergence of self-stabilizing systems using first-order rewriting and regular languages, Distributed Computing, v.14 n.2, p.83-95, April 2001
I. S. W. B. Prasetya , S. D. Swierstra, Formal design of self-stabilizing programs, Journal of High Speed Networks, v.14 n.1, p.59-83, January 2005
Marco Schneider, Self-stabilization, ACM Computing Surveys (CSUR), v.25 n.1, p.45-67, March 1993
adaptivity;token ring networks;adaptive distributed programs;formal logic;adaptive systems;composition operators;self-stabilization;programming theory;parallel programming;adaptive sequential programs;constituent programs