Towards Behavioral Programming in Distributed Architectures

We propose a design pattern called BP, and an associated module called bp (whose operation is described in subsequent subsections), for iteratively creating a sequence of events, where the next event is chosen with the help of the bidding protocol described below. The bidders are Erlang processes registered as behavior threads (b-threads). In each iteration:

Requested events: events that the b-thread proposes to be considered for triggering.

Waited-for events: other events that the b-thread asks to be notified of if and when triggered.

Blocked events: events that the b-thread forbids.

In the auction step, if there are multiple requested events that are not blocked, the design pattern allows the designer to specify the event selection algorithm. Among the selection techniques we have implemented to-date are priority-based selection, random selection, probabilistic with reinforcement learning, and look-ahead subject to feedback regarding success or failure. In the remainder of the paper, we assume the priority-based selection, where b-threads are ordered subject to fixed priorities and all the requests of a given b-thread are ordered as well. The first event that is requested and not blocked is selected for triggering.

The motivation for proposing this design pattern is to provide a simple mechanism, through which systems can be constructed from software components, each of which controls and coordinates a particular aspect of desired system behavior. Such construction complements the traditional approach to software development where program modularity revolves around objects and data-structures, and simplifies the programming of required behaviors whose intuitive description involves multiple objects and is not anchored on one "classical" object. Using events as markers of system behavior, and applying the proposed bidding mechanism for choosing events, the resulting integrated system behavior is an event sequence that reflects, at each step, every b-thread's view of how the system should proceed.

The BP design pattern helps programmers maintain b-thread independence by unifying the occurrence of events requested by several b-threads into a single occurrence, and by the fact that b-threads can block events regardless of whether other b-threads request them or not. As in standard publish-subscribe protocols, b-threads do not communicate with each other directly, and they are not notified of events that they do not request or wait for.

BP is best used when the decomposition of system’s behavior into independent scenarios is natural. For example, in automated transportation, it is natural to separate navigation, speed control, and stabilization into parallel scenarios, and in a game-playing application each game rule and each player strategy can be described in a separate scenario. Since interesting system behaviors can be observed in early stages of software design and specification, with only a few b-threads, BP is valuable in experimenting with for obtaining feedbacks from stakeholders and validating the understanding of requirements.

More generally, the BP design pattern is suitable for incremental development, as it allows adding and removing system behaviors with little or no change to existing code (if that code was developed with BP).

BP is also applicable in end-user customization, where end -users can add or remove behaviors in an existing application, say, to simplify activities or avoid mistakes, by adding b-threads that handle specific sequences of events.

Clearly, the apparent ease of incremental development comes with a price. For example, after a long period of development an application may appear as a loosely coupled collection of base scenarios, exceptions and exceptions to exceptions. It is then the role of the developers to determine whether to add a new requirement as a new scenario or to modify existing scenarios, and to decide when restructuring is desired. Another concern is the security controls over incremental development and end-user customization. With idioms such as priorities and event blocking at their disposal, incremental additions can have vast effects over the behavior of the application. Developers may wish to certify sources of such updates, or to introduce explicit permission mechanisms controlling what newly added b-threads are allowed to do.

There are, of course, cases where BP may not be the first choice. One such situation is when there are hard-to-achieve performance constraints for which the general solutions offered here and elsewhere are not sufficient, and application-specific and/or optimized algorithms are needed. Another case is where the requirements scenarios are already provided as a well documented algorithm, or can be readily combined into one easy to maintain scenario. Consider for example a robot navigating a maze using the well-known left-wall rule. In [23] it is shown how the robot’s behavior can be decomposed into three scenarios (described in priority order): (1) repeatedly wait for a move forward and turn left, (2) repeatedly move forward (3) repeatedly turn right. While this decomposition is attractive in that it avoids any conditions in the scenarios, one may argue that it is excessive, and that the single scenario ‘repeatedly do the following: turn left; if the robot is facing a wall turn right; otherwise, move forward’ is preferable. In fact, there may be cases where replacing the parallel coordinated b-threads with a sequential procedure containing a few conditions may provide the necessary performance advantage. In development scenarios where incrementality is not needed, the arguments for using BP are further weakened. Nevertheless, we are interested in finding ways for optimizing performance of parallel execution of behavioral scenario bringing it as close as possible to that of more standard applications. Techniques include, among others, relaxing the synchronization requirements (as described in Sections 3 and 4), optimizing the data structures and algorithms for carrying out synchronization, designing operating systems and hardware geared explicitly to efficient execution of behavioral programs, and, synthesizing single-threaded controllers from behavioral specifications with parallel scenarios.

As for BP implementations in Erlang, it should be noted that Erlang is able to handle numerous processes [4], and indeed, in our test of thousands of Erlang b-threads randomly exchanging events at a high rate, we did not observe slowdown due to the required coordination.

In the BP design pattern a system is constructed from independent b-threads that synchronize constantly and communicate indirectly using agreed-upon events, with the help of the coordination module.

In this design pattern, the participants are:

The collaboration between the BP controller and the b-threads is as follows (also depicted in Figure 1):

Our implementation of the BP design pattern is based on a supporting module, bp. The bp module exports the following functions:

init/0 : Initialize the BP controller.

add/2 : Register a process with a given priority.

start/0 : Start the controller.

sync/1 : Send a synchronization request that includes requested, waited-for and blocked events to the controller and wait until one of the requested or waited-for events is selected. This function takes a record as an argument. The record definition is -record(rwb, {request, wait, block}), where rwb is the chosen record name and with record fields matching the respective event sets, each having an empty list as its default value. For example, the code below invokes bp:bSync, passing to it a rwb record (referenced as #rwb), where it requests the event E1, waits in addition also for E2 and E3, and blocks E4 until one of the events E1, E2, or E3 occurs:

bp:bSync(#rwb{
  request=[E1], wait=[E2,E3], block=[E4]})

remove/1 : Deregister a process from the controller.

It is the programmer's responsibility to initialize the bp process and spawn the b-threads as processes. There are no constraints on the calculations that b-threads perform before or after the calls to bp:bSync. However, when b-threads perform heavy calculations or wait for external events, they affect synchronization of all participating b-threads. Design patterns for addressing this kind of issue are presented in Section 3.

To illustrate this coding technique, consider a system for controlling the water level in a tank with hot and cold water sources (the example is borrowed from [26]). One of the b-threads in the system requests the event addHot five times. Another b-thread adds five quantities of cold water, by similarly requesting the event addCold five times. After observing a run in which the five addHot events occurred before the first addCold event, a new requirement is introduced by the developer, to the effect that water temperature should be kept relatively stable. The developer then adds a b-thread that interleaves addHot and addCold events, using the event-blocking idiom, by repeatedly performing the steps of first waiting for addHot while blocking addCold and then waiting for addCold while blocking addHot. In this example, the interleaving b-thread was added without changing existing b-threads and without specifying in the new b-thread direct interactions with the existing ones.

The code below illustrates how to implement this system in Erlang, using the bp module. Detailed explanation of the code then follows.

requestFiveAddHotEvents() ->
  [bp:bSync(#rwb{request=[addHot]}) || _ <- seq(1,5)].

requestFiveAddColdEvents() ->
  [bp:bSync(#rwb{request=[addCold]}) || _ <- seq(1,5)].

interleave() ->
  bp:bSync(#rwb{wait=[addHot], block=[addCold]}),
  bp:bSync(#rwb{wait=[addCold], block=[addHot]}),
  interleave().

display() ->
  Event = bp:bSync(#rwb{wait=?ALL}),

io:format("Event: ~w~n", [Event]),
display().

test() ->
  bp:init(),
  bp:add(spawn(fun requestFiveAddHotEvents/0), 1),
  bp:add(spawn(fun requestFiveAddColdEvents/0), 2),
  bp:add(spawn(fun interleave/0), 3),
  bp:add(spawn(fun display/0), 4),
  bp:start().

and the resulting event log is

Event: addHot
Event: addCold
Event: addHot
Event: addCold
Event: addHot
Event: addCold
Event: addHot
Event: addCold
Event: addHot
Event: addCold

The behavior threads are implemented as four functions that are spawned to run in separate processes. The b-thread requestFiveAddHotEvents, for example, calls sync five times. The loop is implemented using Erlang list comprehensions where the expression [X || _ <- seq(1,N)] is shorthand for “perform X N times”. In each iteration of the loop the process passes addHot as the only requested event and blocks nothing. The b-thread requestFiveAddColdEvents is similar, and the b-thread interleave repeatedly waits for and blocks alternating events. The infinite loop of this b-thread is implemented by a recursive call to itself. The wait and block clauses may also use filter functions for events instead of an explicit list. For example, the macro ?ALL brings a filter for all possible events.

The display behavior thread waits for all events and for each received event it generates textual output for illustration purposes. It then invokes itself recursively. In real applications this b-thread would be replaced by an actuator that translates the events into physical outputs, such as tap opening (see more about sensors and actuators in [38] or in [5] in this journal issue).

Note also the second parameter of the bp:add function, which represents the priority of the b-thread, as discussed in Section 2.1. To appreciate the role of priority, consider, for example, the water tap application without the interleave b-thread. Because the priority of requestFiveAddHotEvents is higher than that of requestFiveAddColdEvents, we would get the five addHot events before the five addCold Events.

For completeness of the exposition of BP we include here the formal definition of behavioral programming as transition systems.

The bp module can work with main programs and b-threads, regardless of the structure of their code, as long as they use the interface methods described above. Nevertheless, as the b-thread in fact implements a transition system, it is natural to try and create a mental image of this transition system. The resulting representation of the logic can then be useful to developers and other stakeholders in maintaining the software of individual b-threads or in thinking about the collective execution of a set of b-threads. To this end we have developed a proof-of-concept tool (a module named bp_vis) that automatically produces a visual representation of a b-thread’s behavior as a transition system.

The code visualizer assumes that the code is structured as a state machine, following the method described in [2]. The code for each b-thread is contained in a separate module, and the states of the b-thread are represented as functions in the module. The function start is the first state of the b-thread. The body of each function associated with a b-thread state is written as follows:

case bp:bSync(#rwb{...}) of
  x -> state1();
  y -> state2();
  ...
end.

The function body consists of a case statement where the evaluated expression is a call to bp:bSync, and where each clause maps the returned event to another function call, which represents transitioning into the next state. The diagram is generated as a Graphviz file (see http://graphviz.org), with the following format:

For example, suppose that some device can print, scan, send a fax and stop. Consider the following single b-thread:

-module(printjob).
-compile([parse_transform, bp_vis]).
-include("bp.hrl").
-define(LIMIT, 3).

pending(N) ->
  case bp:bSync(#rbw{request=[print],
                    wait=[print, scan, fax],
                    block=[stop]}) of
    print -> working();
    _ when N < ?LIMIT -> pending(N+1);
    _ when N >= ?LIMIT -> idle()
  end.

working() ->
  case bp:bSync(#rbw{wait=[finish],
                    block=[stop]}) of
    finish -> idle()
  end.

idle() ->
  case bp:bSync(#rbw{wait=[stop]}) of
    stop -> ok
  end.

This module has the following behavior. It tries to print three times. If the printing starts, it waits for it to end. If it fails more than three times, it gives up. When waiting for printing, it prevents the machine from stopping. The output of the visualization tool for this module is depicted in Figure 2. Since this b-thread does not have a designated start function, the diagram does not include a corresponding initial state arrow.

As another example, we developed a behavioral application in Erlang for playing Tic-

Tac-Toe. Figure 3 illustrates two b-threads of this application.

In this subsection we discuss some (possibly negative) consequences and implications of the usage of BP, and ways to mitigate them.

Behavioral programming is based on consensus: It requires all participating processes to agree on the next step. It thus requires a synchronization point for all b-threads that are not waiting. To exit the blocking call to bp:bSync, each active b-thread must wait until all other active b-threads call bp:bSync. Although this is a reasonable requirement for an agreement protocol, a specialized protocol for a specific problem can be more efficient.

Reaching an agreement also requires sharing information between processes. In our implementation, we use a central process (the BP controller) to collect and handle the requests from all participating b-threads. This process is thus critical to the operation of the system. In mission critical real-world systems, special attention should be given to such potential single-point-of-failure.

Several properties of the BP architecture and its semantics can be exploited in designing the desired recovery capabilities, especially when combined with Erlang/OTP built-in recovery facilities. First, we observe that the state of the BP controller that must be saved or made redundant to enable recovery is quite minimal. It consists of the most recent declarations of all the b-threads that are presently at a synchronization point. In fact, in the absence of redundancy and state saving, a simple protocol can be established, by which a recovered BP controller inquires of all synchronized b-threads as to their most recent declarations of requested, waited for and blocked events. As to recovering a failed b-thread, all standard ways of saving a process's state during execution and using system restart and recovery capabilities, are obviously available. In addition, one way to restore the state of a restarted b-thread that is application agnostic can be as follows: During the run, make sure that the log, or trace, of triggered events is saved; start a failed b-thread at its ordinary initial state; run it in a closed "sandbox", such that it does not interfere with other b-threads; execute it in "monitoring mode", i.e., interpret all its requested events only as waited for; select at each synchronization point the event that was selected in the real run, and feed it to the recovered b-thread, until the trace is exhausted. The restarted b-thread is now in synchronization with the rest. Another recovery option is to have b-threads designed specifically for this purpose. That is, when such a b-thread starts, in an analogy to a player joining a soccer game in the middle, it explores the present configuration, and/or some limited recent history of events, and determines its own desired state.

To illustrate one of the ways in which the BP design pattern can be used, we discuss in Appendix A an example involving applications that require bulk processing of a large number of records to perform business operations, and where multiple, independent sequential processes need to be interwoven.

The event-based and state-like nature of BP makes b-threads similar to the generic finite state machine (gen_fsm) module (http://www.erlang.org/doc/man/gen_fsm.html) from the Erlang standard library. Both the gen_fsm and bp modules deal with a state-based reaction to events. However, there are several differences between the two:

One can view the bp module as an extension of gen_fsm, designed for coordinating several processes.

The synchronization and event selection driven by the bp module uses and hides the robust underlying Erlang message passing, thus creating the higher level of abstraction in the form of behavioral events. Such hiding of the underlying messaging is done also in many other Erlang generic modules.

In addition to the general capabilities and broad usage of Erlang in concurrent processing, particular attention to programming independent behaviors in Erlang can be observed in systems such as ERES rule-production [45] or eXat agent programming [44]. What distinguishes b-thread synchronization in our pattern from the classical programming of concurrent behaviors in Erlang is the ability of one process to prevent the occurrence of an event requested by another process, without any party being explicitly aware of even the existence of the other.

The collective-execution mechanism of BP calls for the synchronization of all b-threads prior to triggering an event. This, combined with event blocking, facilitates the incrementality and the ability to handle different aspects of behavior separately, as afforded by BP. However, such synchronization implies that system performance is constrained by its “weakest link”; i.e., by the time it takes, at each step, for the slowest behavior to reach the synchronization point.

Thus, In the BP design pattern there is a convention that b-threads are allowed to take only a small amount of time between synchronization points. This is a rather standard convention. It is used, e.g., for listeners in GUI frameworks and interrupt handlers, where callback routines are expected to complete quickly. Also, in the logical execution time (LET) approach proposed in [28], the design pattern relies on a “fast execution” assumption for interfacing with a physical environment in a deterministic manner.

The question of how small the processing time should be may sometimes be crucial. In way of dealing with this issue, and since smallness is relative, an application may contain behaviors that operate at different time scales. Examples include (1) handling external events whose source is not synchronized with the application; (2) interacting with (and waiting for) resources whose response time (including communications) is slower than the internal event-rate of other behaviors; and (3) a physically distributed multi-agent application, where constant, mandatory, full synchronization is counter-intuitive or impractical. Implementing solutions for these cases in the context of BP is exemplified in Sections 3.4, 3.5, and 3.6, respectively.

A related, and often-asked, question regarding BP is: “what happens if a b-thread never reaches its next synchronization point, thus stalling the entire application?”.

This is indeed a real concern. However, there are several approaches to addressing it. One kind of answer is closely related to the architecture proposed in Section 3.2 for handling external events: design the b-threads so that they do not wait for external, non-behavioral events, and do not perform heavy calculations, thus eliminating a major source of potential delay, and, of course, run the system on an infrastructure that guarantees sufficient allocation of processor resources to all b-threads. Another approach (elaborated upon in Section 3.3) is based on dividing the application into groups (nodes) of synchronized b-threads that communicate with each other only asynchronously, thus limiting the inter-b-thread dependencies. Yet another partial solution to the problem of indefinite delay in b-thread synchronization comes from the relaxed synchronization design approach described in 4. Still, we should remember that a situation where a b-thread never reaches (or is significantly delayed in reaching) its next synchronization point is often a “normal” application bug like any other. The situation may be compared to that of a standard (non-BP) application, where an infinite loop in a high priority process causes it to monopolize all system resources, stalling other processes. Tools like the model checker presented in [24] and the trace visualizer presented in [16] can help in catching such bugs.

The external environment is an essential element in the design of reactive systems. It is the source of the events that the system needs to react to, and is the target of the actions taken by the system. The actual occurrence of events in the environment, e.g., temperature rising, cannot be synchronized with the processing done by the system, and the arrival of such events, e.g., when and how a sensor reading is processed, requires special handling. In our case, for coordinating the synchronized processing of BP with an external environment, we propose a solution based on the super-step approach, as in statecharts [22] (and which is used also in, e.g., LSC execution [21]) and on the logical execution time concept used, e.g., in GIOTTO [28].

This solution is implemented by the BP infrastructure, assuming only that the application complies with simple rules, without application-specific programming. Specifically, we propose that behavioral program execution be divided into cycles, called super-steps, and external events are introduced only at the beginning of a super-step. The philosophy is that all internal events in the body of a super-step are perceived as happening in the same physical time unit but they are nevertheless ordered; i.e., there is a sequence of events (not associated with meaningful time-stamps) between the beginning and end of each super-step (c.f. hybrid time-set [37]). Thus, they are viewed as all taking place in zero time.

According to this convention, it is sufficient to consider a real-world occurrence of an external event only in relation to when super-steps begin and end; i.e., only external events have meaningful time-stamps. When sampling times need to be equidistant, as is the case when implementing algorithms for certain kinds of real time systems and in control theory, one can program the system such that all super-steps take a constant amount of time, by adding delays (under the assumption that the super-step’s internal events runs fast enough to always complete within the time frame).

One initial approach to the implementation of the above philosophy is to have a non-behavioral process handle the external event by dynamically creating a lowest-priority b-thread that will join the next synchronization point and request a corresponding behavioral event. While this approach is general and simple, it may — depending on the implementation platform and language — present performance issues related to the creation of threads and processes.

We thus propose the following design:

Actually, the first and third points above can be replaced by allowing a single b-thread to wait for an idle event, and then, wait for external events using standard (non behavioral) language constructs, such as receive in Erlang or wait in Java. This will in fact stall the process and cause the next synchronization point to be delayed until the waiting process also synchronizes, which will happen only after the next external event arrives. It does not stall the system’s operation, however, since by convention no internal events can be triggered between the idle event and the next external event. The three-point design above allows a richer variety of actions in separate b-threads, such as super-step logging, deadlock handling, blocking of external events, and additional peeking at external event queues, while replacing the first two points as suggested may be simpler and more suitable for small applications.

This approach, based on logical execution time, also explains why the BP semantics does not allow for simultaneous triggering of multiple events. On the one hand, allowing only a single event to be triggered at each synchronization point makes it possible for every b-thread to react to the triggered event and change states as needed; e.g., for subsequent requesting, waiting, or blocking events. Debugging and formal analysis of this semantics is much simpler than when simultaneous triggering is allowed. On the other hand, event sequences that do not require such strict sequencing, possibly benefiting from simultaneous event triggering, do not generally suffer from the sequencing, as all the events indeed occur within the same time slot, marked by two time ticks or two other external events. The relaxed synchronization techniques described in Section 4 also assist in enabling the desired parallel execution, when applicable. We should also note that when, for some reason, simultaneous event triggering is desired, it can be partially implemented in application-specific ways by enriching the event objects to represent sets of more primitive events. Finally, if desired, an implementation of BP can easily allow for simultaneous event triggering, for example by triggering all (or some) of the events that were requested and not blocked, notifying all b-threads that requested or waited for any of them, and returning to each of the notified b-threads either the entire set of triggered events or just those relevant to it.

Many applications that include behaviors of different time-scales can be decomposed as follows. The application is divided into groups of behaviors, with all behaviors in a group being on the same time-scale. If desired, such groups can be further broken down into sub-groups; e.g., by physical components or specific relevant events. Note that the behaviors in each such sub-group are, by definition, of the same time-scale. In the context of BP we call such a group of behaviors a behavior node, or b-node, for short. The work shown here is a continuation and generalization of the InterPlay tool that was designed to allow coordinated execution of multiple LSC and statechart specifications [6].

All the b-threads in each b-node run in a synchronized manner, as described in Section 2. In actuality, the b-threads in a b-node may run on multiple cores or, when the time scale allows, on multiple computers, where the execution environment (e.g., native operating system, JVM, Erlang, etc.) facilitates the constant inter-b-thread synchronization implemented in the BP collective-execution mechanism. Here we focus on inter-b-node coordination and not on intra-b-node parallelism.

Each event generated by the environment is processed by a designated b-node, as described in Section 3.2. Communication between b-nodes is carried out only through external events, which can be sent and received by all behavioral programs in a consistent and standard way, as follows:

Note that the result of an incoming external event could be that some of the b-node’s b-threads decide to block certain events internal to the node, until some specific other external event arrives. This allows one b-node to cause the blocking of events in other b-nodes. Since blocking is central to the incrementality afforded by BP, the ability to propagate event-blocking is an important feature of the proposed decentralized architecture.

This design for communication between behavioral programs reflects several choices that we believe are common and natural in development situations. First, consider a b-node busily working autonomously. When an external event arrives, which is expected to change the behavior of the node, it is acceptable that one or more events of the b-thread’s autonomous behavior be triggered before the new course of action is taken. This form of inertia is commonly observable not only in the physical world and in typical human handling of interrupts (“please just let me finish sending this email, and I’ll be right with you”), but also in the delays tolerated when sensing events or handling interrupts in computer systems.

The second choice is that even a node that wishes to be extremely attentive to external events should not be synchronized with the source of those events, the way, e.g., that b-threads are synchronized within a b-node. Consider a corporation, and a manager-employee analogy for the relationship between two b-nodes. Employees who follow their managers everywhere in order to be ready to respond quickly to new requests may be inefficient and disruptive. Put differently, excessive synchronization between b-nodes can greatly increase the computational overhead in the system. We believe that the proposed design nicely balances the use of autonomous behavioral components with efficiency. In particular, we expect that the delay in reacting to messages will be tolerable in a computer application that is properly decomposed according to behaviors (similarly to the case of a corporation).

We believe that this combination of (1) synchrony within a b-node, (2) asynchronous communication between b-nodes, and (3) translation of asynchronous messages and events back into behavioral events in each receiving b-node, allows one to retain the natural and incremental application development offered by BP, while overcoming some of the performance constraints associated with synchronizing many b-threads.

To demonstrate how a behavioral program handles external events, we describe the architecture and implementation of a modest computer game. Specifically, we decompose the game into separate, independently programmed behaviors (all in a single b-node), and show how external events are introduced at the end of super-steps.

In this game, the goal is to land a rocket which descends vertically from the top of the screen back on its landing pad which is located on the ground, and moves left or right at random. The player can nudge the descending rocket left or right (but not upwards), and can fire a short exhaust burst to delay the fall. The player wins if the rocket ends up on the landing pad, and loses if it hits the ground. Figure 4 shows the player interface of the game.

In this section we demonstrate how an application can be composed of behavioral components, namely b-nodes, that operate on different time scales and communicate via events. The example is part of the control software for a quadrotor, a flying vehicle powered by four rotors (see schematic drawing in Figure 6). The behaviorally-programmed piece is responsible for stabilizing the aircraft. It was experimentally tested by plugging behavioral modules written in Java into the comprehensive quadrotor-control simulation model developed by Bouabdallah et al. [9, 10]. This model is based on MATLAB/Simulink and simulates full control of the quadrotor flight including physical aspects. A high-level description of this use-case appeared also in [27].

The model of Bouabdallah et al. is modified, as illustrated in Figure 7. The b-node High-Level Control translates measured differences between actual and desired flight parameters (e.g., orientation, altitude) into four forces (thrust, roll, pitch and yaw — see Figure 6). It consists of four b-threads: one for each of the yaw, pitch and roll axis and one for thrust. Each of these b-threads computes the respective force by applying a standard Proportional Integral

Derivative control based on the differences between measurements and desired value, as obtained, e.g, from the remote control or as dictated by a higher level navigation algorithm.

The b-node ‘Forces to RPMs’ operates at a higher frequency than the ‘High-Level Control’. This component receives the four desired forces as external input events and translates them into rotor RPMs, via a fast coordinated sequence of events, where different b-threads balance the competing needs. For illustration, the reader may compare the action of our b-thread with the way sound-mixing is where a sound engineer deals with competing goals, such as balancing the guitar and the piano, and controlling overall volume by small adjustments of the available controls (without attempting to solve complex mathematical equations).

In the ‘Forces to RPMs’ b-node, each of the four forces is independently interpreted by a dedicated b-thread as a target, and is translated to desired changes to RPM of the various rotors. The b-threads attempt to attain their targets by requesting events that represent (small) increases or decreases of individual rotor RPM towards the target and, blocking events that work away from it, as shown in Figure 8. The composite behavioral execution mechanism interlaces the execution of all b-threads, transforming their possibly-conflicting requests into integrated control.

For example, to increase the pitch (raise the front), the system requests the events of increasing the front rotor’s RPM and decreasing the back rotor’s RPM, while blocking the opposite (complementary) events. Note that desired flight results depend only on the total numbers of events that increase or decrease the controlled value, and the difference between their numbers, while the actual mix of events may vary. Specifically in this example (see Figure 8), in order to allow finer control, the b-threads translate the input force into a sequence of events that affect the rotor speed by smaller increments. Furthermore, to accommodate behaviors that require concurrent actions on multiple rotors, all behaviors entertain a “slack”, in which they allow a small number of undesired events to occur before blocking them completely. In this manner, the ThrustBT can increase the RPM of all rotors equally, one at a time, without interference from b-threads that try to create a difference between certain rotor RPMs.

In our simulation, the super-step is orchestrated as follows. A lowest-priority b-thread repeatedly waits for RPM-change events, as described above, and keeps track of all desired rotor RPMs by changing in-memory values by fixed amounts. This b-thread repeatedly requests an output event that contains those values, but due to its low priority, output is triggered only when there are no other events to trigger (i.e., the four force-control b-threads have attained their targets). The output event marks the completion of a super-step. Four inputs (target forces) are then presented again (by a high priority b-thread that polls an external queue), marking the beginning of the next super-step. Throughout, an actuator b-thread waits for output events and transmits the required signals to the rotors. The detailed simulations we carried out show that his behavioral solution indeed stabilizes the quadrotor, as can be seen in Figure 9.

Subsequently, we have begun to implement a behavioral programming environment written in C that can run directly on a quadrotor, and have shown that the design and the b-threads shown above indeed can stabilize a UAV. In fact, initial versions of this are already flying in our lab.

When proceeding on the actual implementation in a flying quadrotor, additional considerations of course emerge in order to meet the real-time constraints. The first and foremost consideration for BP in this regard is having efficient processing at the underlying BP infrastructure, controlling the synchronization of b-threads, collection of their declarations, event selection, and b-thread resumption. One such approach is to turn events into bits and event sets into easily managed bit vectors. Then come the additional real-time considerations of ensuring that the infrastructure and application allow the non-behavioral sensor and actuator processes to interact with the real world at the desired frequency, and that the b-threads of system behavior are efficient and predictable in completing their reactive scenarios before arrival of the next environment-driven event. For example, towards predictability, in our experimentation on the real quadrotor, we initiate the output event at a fixed time frequency, regardless of whether the b-threads have completed their negotiations over the right changes to all RPM values or not. Both the BP infrastructure optimization and more comprehensive design guidelines regarding real time behavioral applications are the subject of future research and are outside of the scope of the present paper.

Summary. In creating composite behavior, the quadrotor application uses very local behaviors, such as controlling roll and pitch, to achieve higher level goals such as maintaining stability. Longer term behaviors, such as traveling between stations in a multi-stop trip, or keeping maintenance and refueling schedules, can be constructed from similar elements. While all these facets can be programmed as compositions of b-threads, gluing them together is easier with an infrastructure that can support multiple time scales. Clearly, a b-thread that controls a multi-stop navigation itinerary can suffice with occasional changing of the required speed and direction, and does not require the constant synchronization and attentiveness of the stabilization modules described above.

The quadrotor application also shows how behavioral programming can be used in developing hybrid control, i.e., a combination of discrete logic and actuation with the sensing of continuous system variables [36]. In [26] we discuss the application of BP to hybrid control, by using fuzzy logic to translate continuous information into discrete categories that can be refereed to in naturally-programmed scenarios.

In this section we demonstrate how multiple behavioral programs coordinated only by external events can retain much of the incrementality of a single fully synchronized behavioral system, i.e., that functionality can be enhanced by adding b-threads and b-nodes.

We present the development of a multi-agent application, where agents include vehicles traveling in open terrain and advisors affecting the vehicles. First, we list the behaviors that are responsible for the movement of a vehicle. To each vehicle we then add behaviors that allow it to interact with external systems. Finally, again incrementally, we program the vehicle agents to react to an advisor agent responsible for directing particular aspects of the vehicles' travel. The communication between the vehicles and the advisor uses the architecture for external events described in Section 3.2. This small example can be readily extended to make it easily possible to add agents (vehicles, advisors), as well as new kinds of interactions among existing agents (inter-vehicle or inter-advisor).

As discussed in Section 3.1, a behavioral program’s execution speed is constrained by its slower threads, because the behavioral execution mechanism needs to receive the declarations of requested and blocked events of all threads before triggering an event. However, in some cases these constraints may be relaxed, as we now demonstrate.

Let $P$ denote a set of threads that constitute a behavioral program, and assume that at some point during $P$’s execution a subset $P\_\{\backslash text\{sync\}\}\; \backslash subset\; P$ of the threads has reached a synchronization point, while the rest are still executing. Further, assume that the execution mechanism has additional information about the events that the threads in $P\; \backslash setminus\; P\_\{\backslash text\{sync\}\}$ will request and block when they synchronize. If, combining the information from threads in $P\_\{\backslash text\{sync\}\}$ with the information about threads in $P\; \backslash setminus\; P\_\{\backslash text\{sync\}\}$, the execution mechanism can find an event $e$ that will be enabled at the highest priority when all threads have synchronized, then $e$ can immediately be chosen for triggering.

The execution mechanism may then pass $e$ on to the threads in $P\_\{\backslash text\{sync\}\}$ to let them continue their execution, without waiting for the remaining threads to synchronize. Once any of these other threads reaches its synchronization point, the execution mechanism immediately passes it event $e$, since $e$ was the event selected for that particular synchronization point. This is accomplished by having a designated queue for each of the b-threads, of events that are waiting to be passed, and putting $e$ in the queues corresponding to the as-of-yet not synchronized threads. The execution mechanism described is eager, in the sense that it uses predetermined information to choose the next event as early as possible.

When a thread $BT$ reaches a synchronization point, if the corresponding queue is nonempty, the execution mechanism dequeues the next pending event $e\text{'}$. If $BT$ requests or waits for $e\text{'}$, it is passed to the thread, which then continues to execute. Otherwise, $e\text{'}$ is ignored, and the execution mechanism continues with the next event pending in the queue. In order to reflect the semantics of BP, from the execution mechanism's global perspective $BT$ is not considered synchronized as long as it has events pending in the queue. Specifically, the events that are requested or blocked by $BT$ at this point are irrelevant for the selection of the next event; they have already been considered when the event $e\text{'}$, which is now at the head of the thread's queue, was triggered by the execution mechanism, ensuring that $e\text{'}$ was a valid choice. Observe that the eager execution mechanism strictly adheres to the semantics of BP, as described in Section 2.9: at every synchronization point, the triggered event is indeed the enabled event of highest priority². The key point, however, is that the eager mechanism makes its decisions more quickly, and can thus produce more efficient runs.

Note that, under certain conditions, event queues for slow threads can grow to any arbitrary length. Consequently, we propose to cap the length of these queues, based on available system resources. When the cap is reached, the system must wait for the slower threads to catch up. Hopefully, the slow threads will not have requested or waited-for many of the events in their queues, allowing them to catch up quickly.

It remains to show how the execution mechanism knows which events could be requested and blocked by threads that are yet to synchronize. We propose two approaches: one based on static information and the other on dynamic information, discussed and demonstrated in Sections 4.2 and 4.3, respectively. For a rigorous formulation of the eager execution mechanism, we refer the reader to Appendix B.

In this approach, the execution mechanism is given in advance a static over-approximation of the events that a thread might block when synchronizing. More specifically, if a thread has states $s\_1,\; \backslash dots,\; s\_n$, this over-approximation is $\backslash bigcup\_\{1\; \backslash leq\; i\; \backslash leq\; n\}\; B(s\_i)$, where $B(s\_i)$ is the set of events blocked in state $s\_i$. This information is static, in the sense that the over-approximation does not change throughout the run. Also, since it does not depend on the threads' specific states, this approach is unaffected (complexity-wise) by the number of events stored in the threads' queues.

When a thread synchronizes, the execution mechanism attempts to resolve the synchronization point, based on the information gathered so far. It finds the highest-priority event that is requested and not blocked by threads in $P\_\{\backslash text\{sync\}\}$. This event may immediately be triggered, if two conditions hold: (1) it is guaranteed to remain enabled when more threads

synchronize, ascertained by checking that it does not appear in the over-approximations of blocked events of any of the unsynchronized threads, and (2) it is guaranteed to be the highest-priority enabled event at the synchronization point, ascertained by requiring that all threads that have higher priorities than the thread requesting the selected event have already synchronized.

If such an event exists, it can be triggered immediately. Otherwise, the execution mechanism waits for more b-threads to synchronize. This generally results in more events becoming eligible for selection, since the actual set of events that are blocked by a thread in a given state is always a subset of the over-approximation, which includes all the events that are ever blocked by the b-thread, and since additional requested events are revealed as additional b-threads synchronize. As soon as enough information is gathered to deduce that an event is the highest-priority enabled event at the synchronization point in question, it is immediately triggered and passed to all synchronized threads.

This mechanism can be improved further. In particular, it is sometimes possible to deduce that an enabled event $e$ is the highest-priority enabled event even when a higher priority thread has not yet synchronized. This can be accomplished by keeping over-approximations of the requested events of threads, and checking that all events that may be requested by this higher-priority thread are already blocked by synchronized threads.

Observe that we only discuss over-approximating requested and blocked events, but not their under-approximations, although these can be used analogously. The reason is that typically there are no events that are requested/blocked in each and every state of the thread, and so the under-approximations are typically empty.

In this approach, the execution mechanism is given complete state graphs of threads, which are generated before the program is executed. The labeled vertices of a state graph correspond to the thread's synchronization points and the events that it requests/blocks at these points, and the edges, labeled with non-blocked program events, describe the thread's transitions from one synchronization point to another. The graph thus provides a complete description of the thread from the execution mechanism's point of view — that is, a complete description of the events requested and blocked by the thread, but without any calculations or input/output actions performed by the thread when not synchronized. For more details on these state graphs, see [25].

During runtime, the execution mechanism keeps track of the threads' positions in the graphs, allowing it to approximate the events they will request and block at the next synchronization point — even before they actually synchronize. This method is dynamic, in the sense that the approximations for a given thread can change during the run, as different states are visited. As is the case with static information, the complexity of this approach is unaffected by the number of events stored in the threads' queues. In order to make triggering decisions, it is enough for the event selection mechanism to remember the “current” state for each thread (that is — the state it would reach after processing all events in its queue), and this state can be updated every time an event is added to the queue.

We stress the fundamental difference between running a thread and simulating its run using its state graph. In the former, transitions can be considered immediate, whereas in the latter, additional non-trivial computation may be performed, and the transitions can take longer. For instance, in a recent behavioral application implementing a web-server, we used threads to calculate checksums over TCP segments and to read web pages from the disk. Both actions were time consuming, and hence the threads performing them did not immediately arrive at the next synchronization point. In such cases, simulating threads using their state graphs is faster than actually running them.

Recall that our definition of a thread dictates that its transitions be deterministic. Therefore, simulating a thread through its state graph yields precise predictions of its requested and blocked events at each synchronization point. In the nondeterministic model, where threads may depend on coin tosses or inputs from the environment, it may be impossible for the execution mechanism to determine a thread’s exact state until it synchronizes. However, the execution mechanism can approximate the thread’s requested and blocked events by considering all the states to which the nondeterministic transitions might send it. If, due to a previous transition, the thread is known to be in one of states $s\_1,\; \backslash dots,\; s\_n$, then the blocked events may be over-approximated by $\backslash bigcup\_\{1\; \backslash leq\; i\; \backslash leq\; n\}\; B(s\_i)$ — similarly to what is done when using static approximations. Analogously, the requested events may be under-approximated by $\backslash bigcap\_\{1\; \backslash leq\; i\; \backslash leq\; n\}\; R(s\_i)$. For more details see Appendix C. As before, if these approximations leave no enabled events that are eligible for triggering, the execution mechanism waits for more threads to synchronize.

The other details are as they were in the static approximation scheme. Once an event is triggered, it is immediately sent to all synchronized threads, and is placed in the queues of the threads that are yet to synchronize.

sketch. 1: By induction on $k$. For $k\; =\; 0$ the claim follows from the fact that $\backslash bar\{q\}\_0\; =\; q\_0\; \backslash in\; Q$; the induction step follows from Lemma 1.

2: By an inductive construction of the execution, which similarly follows from Lemma 1. $\backslash square$

Proof. 1: As $q$ is terminal, by the definition of $\backslash widehat\{\backslash delta\}$ it holds that all the queues in $q$ are empty (otherwise, $\backslash widehat\{\backslash delta\}(q,\; \backslash varepsilon)\; \backslash neq\; \backslash emptyset$); i.e., $q\; =\; \backslash langle\; q^i,\; \backslash varepsilon\; \backslash rangle\_\{i=1\}^n$. Let $a\; \backslash in\; \backslash Sigma$. Because $q$ is terminal, $a\; \backslash notin\; \backslash mathcal\{E\}(q)$. Thus, by (C.3), $a\; \backslash notin\; E(\backslash bar\{q\})$, and therefore by the definition of $\backslash delta$, $\backslash delta(\backslash bar\{q\},\; a)\; =\; \backslash emptyset$.

2: For each state $q\; =\; \backslash langle\; q^i,\; u^i\; \backslash rangle\_\{i=1\}^n\; \backslash in\; \backslash widehat\{Q\}$, consider the total size of the queues, denoted by $\backslash varphi(q)\; :=\; \backslash sum\_\{i=1\}^n\; |u^i|\; \backslash in\; \backslash mathbb\{N\}$. Given such an infinite sequence of states, $\backslash varphi$ is strictly decreasing (by the definition of $\backslash widehat\{\backslash delta\}$), which contradicts the well-foundedness of the natural numbers. $\backslash square$

Corollary 2. Let $r\_0\; \backslash xrightarrow\{\backslash sigma\_1\}\; r\_1\; \backslash xrightarrow\{\backslash sigma\_2\}\; \backslash dots$ be a complete (finite or infinite) execution of $\backslash widehat\{\backslash text\{LTS\}\}(P)$. There exists a complete (finite or infinite, respectively) execution $s\_0\; \backslash xrightarrow\{a\_1\}\; s\_1\; \backslash xrightarrow\{a\_2\}\; \backslash dots$ of $\backslash text\{LTS\}(P)$ such that $\backslash sigma\_1\; \backslash sigma\_2\; \backslash dots\; =\; a\_1\; a\_2\; \backslash dots$.

The corollary follows from Corollary 1 and Lemma 2. It is equivalent to $\backslash mathfrak\{L\}(\backslash widehat\{\backslash text\{LTS\}\}(P))\; \backslash subseteq\; \backslash mathfrak\{L\}(\backslash text\{LTS\}(P))$, as needed.

As we briefly mentioned in the paper, eager execution can be adapted to programs with nondeterministic threads. We now discuss this adaptation more thoroughly.

In this section we extend the formal definitions of eager execution in the natural way, to include proper handling of nondeterministic threads. While many of the particulars remain the same as in the deterministic case, we repeat them here for completeness. For simplicity, we assume all the threads in the program have equal priorities.

Let $P\; =\; \backslash \{BT^1,\; \backslash dots,\; BT^n\backslash \}$ be a behavioral program, where $n\; \backslash in\; \backslash mathbb\{N\}$ and each $BT^i$ is a distinct, possibly nondeterministic b-thread. In order to define the eager execution mechanism, we construct a labeled transition system (LTS) denoted by $\backslash widehat\{\backslash text\{LTS\}\}(P)\; =\; \backslash langle\; \backslash widehat\{Q\},\; \backslash widehat\{q\}\_0,\; \backslash widehat\{\backslash delta\}\; \backslash rangle$, which is defined as follows.

Moreover, we require that in case a thread is synchronized, the two approximations are precise. More formally, if $u^i\; =\; \backslash varepsilon$ for some $i\; \backslash in\; [n]$ (consequently, $\backslash delta^i(q^i,\; u^i)\; =\; \backslash \{q^i\backslash \}$), then

From these, we obtain that the approximated enabled events, defined in the following, are contained in the enabled events at any of the states in $\backslash text\{ind\}(q)$; i.e., $\backslash forall\; \backslash bar\{q\}\; \backslash in\; \backslash text\{ind\}(q)$

In case all threads are synchronized, i.e., $u^i\; =\; \backslash varepsilon$ for all $i\; \backslash in\; [n]$, we obtain that $\backslash text\{ind\}(q)\; =\; \backslash \{\backslash langle\; q^1,\; \backslash dots,\; q^n\; \backslash rangle\backslash \}$ and

The definitions above capture the case of nondeterministic threads. They can be used to prove the result of the matching section in the paper for the nondeterministic case: that in the nondeterministic case it also holds that each complete run of $\backslash widehat\{\backslash text\{LTS\}\}(P)$ is a complete run of $\backslash text\{LTS\}(P)$; i.e., $\backslash mathfrak\{L\}(\backslash widehat\{\backslash text\{LTS\}\}(P))\; \backslash subseteq\; \backslash mathfrak\{L\}(\backslash text\{LTS\}(P))$. The actual proof is similar to that of the deterministic case.

In this section we provide a rigorous definition of the model, and prove that the runs that it produces abide by the semantics of BP.

Let $P\; =\; \backslash \{BT^1,\; \backslash dots,\; BT^m\backslash \}$ be a (possibly nondeterministic) behavioral program, where $n\; \backslash in\; \backslash mathbb\{N\}$ and each $BT^i$ is a distinct b-thread, and let $f\; :\; 2^\backslash Sigma\; \backslash setminus\; \backslash \{\backslash emptyset\backslash \}\; \backslash rightarrow\; \backslash Sigma$ be a deterministic event selection function. Suppose that the threads run on different machines $M\_1,\; \backslash dots,\; M\_k$. Each machine is defined as the set of thread that it runs, i.e. $\backslash bigcup\_\{i=1\}^k\; M\_i\; =\; P$.

Each machine $M\_i$ has a coordinator agent, $C\_i$; this agent acts as the coordinator for the threads of $M\_i$, and answers their synchronization requests. Each coordinator agent is supplied with the state graphs of all threads in the system, and uses these graphs to locate nondeterministic transitions of the threads throughout the run.

The pseudocode for coordinator agent $C\_i$ in charge of managing threads $M\_i$ is given below. The agent uses variables $s\_1,\; \backslash dots,\; s\_n$ to keep track of the states of all threads in the system.

Coordinator Agent $C\_i$:

1: $\backslash forall\; i,\; s\_i\; \backslash leftarrow\; q\_0^i$
2: $\backslash text\{LastEvent\}\; \backslash leftarrow\; \backslash phi$
3: while true do
4:   $\backslash text\{Sync\}\; \backslash leftarrow\; \backslash phi$
5:   while  do
6:     Receive synchronization request from thread $BT^j$
7:     Mark the new state of $BT^j$ as $s\text{'}\_j$
8:     if $\backslash text\{LastEvent\}\; \backslash neq\; \backslash phi$ and $|\backslash delta^j(s\_j,\; \backslash text\{LastEvent\})|\; >\; 1$ then
9:       Broadcast $s\text{'}\_j$
10:    $s\_j\; \backslash leftarrow\; s\text{'}\_j$
11:    $\backslash text\{Sync\}\; \backslash leftarrow\; \backslash text\{Sync\}\; \backslash cup\; BT^j$
12:  for $BT^\backslash ell\; \backslash notin\; M\_i$ do
13:    if $\backslash text\{LastEvent\}\; \backslash neq\; \backslash phi$ then
14:      if $|\backslash delta^\backslash ell(s\_\backslash ell,\; \backslash text\{LastEvent\})|\; >\; 1$ then
15:        Update $s\_\backslash ell$ according to broadcasts from other agents
16:      else
17:        $s\_\backslash ell\; \backslash leftarrow\; \backslash delta^\backslash ell(s\_\backslash ell,\; \backslash text\{LastEvent\})$
18:    $E\; \backslash leftarrow\; \backslash bigcup\_\{j=1\}^n\; (R^j(s\_j))\; -\; \backslash bigcup\_\{j=1\}^n\; (B^j(s\_j))$
19:    $\backslash text\{LastEvent\}\; \backslash leftarrow\; f(E)$
20:    Inform threads in $M\_i$ that LastEvent was triggered

Note the slight abuse of notation of line 17 — where $\backslash delta^\backslash ell(s\_\backslash ell,\; \backslash text\{LastEvent\})$ is not the state of the thread, but rather a set containing that state. Also, we implicitly assume that all broadcasts between the coordinator agents contain the index of the synchronization point that they refer to, to prevent cases where information about synchronization point $t\_1$ could be mistakenly used in synchronization point $t\_2$.

Intuitively, the coordinator agent waits for the threads that it manages (loop on line 5), same as in the centralized case. Whenever a thread synchronizes, the agent checks if the thread's last transition was nondeterministic (line 8). If so, the new state is broadcasted to the other agents — as they have no other way of finding out which transition was taken.

Once all the agent's threads have synchronized, it turns to consider threads that run on other machines. The key fact is that if a non-local thread is at a nondeterministic transition (line 14), the agent has to wait to receive a broadcast message (line 15) in order to determine the new state of that thread. Otherwise, it can go ahead and determine the thread's state locally (line 17).

After the synchronization requests of all threads have been determined, the next event to be triggered is selected (line 19), and then broadcasted to the agent's threads. This part is the reason for stipulating that $f$ be a deterministic function — in order to maintain cohesiveness, all agents much trigger the same event on line 19.

Observe that each coordinator agent uses information regarding the transition functions (lines 8 and 14) and synchronization requests (line 18) of all the threads in the system — both threads that run locally on that agent, and threads that run on other agents. This information is given prior to the run, in the form of the state graphs of all the threads in the system.

Having formally defined the operation of each agent, we can now prove the following proposition, which is a technical formulation of Lemma 3:

Proposition 3. Let $P\; =\; \backslash \{BT^1,\; \backslash dots,\; BT^n\backslash \}$ be a behavioral program, divided into machines $M\_1,\; \backslash dots,\; M\_k$ with coordinator agents $C\_1,\; \backslash dots,\; C\_k$. Let $f\; :\; 2^\backslash Sigma\; \backslash setminus\; \backslash \{\backslash emptyset\backslash \}\; \backslash rightarrow\; \backslash Sigma$ be a deterministic event selection function. Then agents $C\_1,\; \backslash dots,\; C\_k$ produce a cohesive run; that is, there exists a unique run $e\_1\; e\_2\; \backslash dots$ such that at synchronization point $i$, every coordinator $C\_\backslash ell$ triggers $e\_i$. Further, the sequence $e\_1\; e\_2\; \backslash dots$ is a valid run (under BP's semantics).

For simplicity, we prove the lemma for the case of two machines, i.e. $n\; =\; 2$; the proof can easily be extended to any $n\; \backslash in\; \backslash mathbb\{N\}$. The proof follows directly from the next proposition, which is in turn proven by induction over the index of the synchronization points of the run.

Proposition 4. For $i\; \backslash in\; \backslash mathbb\{N\}$ and $m\; \backslash in\; \backslash \{1,\; 2\backslash \}$, let $s\_m^i(BT^\backslash ell)$ denote the state of thread $BT^\backslash ell$ at synchronization point $i$, from the point of view of coordinator agent $m$. Let $S\_m^i$ denote the system-wide state at synchronization point $i$ from the point of view of coordinator agent $m$; that is, $S\_m^i\; =\; (s\_m^i(BT^1),\; \backslash dots,\; s\_m^i(BT^n))$. Then for all $i\; \backslash in\; \backslash mathbb\{N\}$, it holds that $S\_1^i\; =\; S\_2^i$.

Proof. Let $i\; =\; 1$, which is the first synchronization point in the program. At this point, by the initialization in line 1 in the coordinator agent's code, $s\_1^1(BT^\backslash ell)\; =\; q\_0^\backslash ell$ and $s\_2^1(BT^\backslash ell)\; =\; q\_0^\backslash ell$ for all $\backslash ell$. Consequently, $S\_1^1\; =\; S\_2^1$.

Now, suppose that $S\_1^i\; =\; S\_2^i$ for some $i$. At synchronization point $i$, both coordinator agents triggered the same event $e\_i$. This is so because the event selection function is deterministic, and thus both agents triggered event $e\_i\; =\; f(E(S\_1^i))\; =\; f(E(S\_2^i))$. This event was passed to all threads of the system by their respective coordinator agents.

Observe synchronization point $i\; +\; 1$ from the point of view of $C\_1$. As soon as all threads in $M\_1$ have synchronized, $C\_1$ knows their states. In order to determine the states of the remaining threads (those running on machine $M\_2$), $C\_1$ uses their pre-supplied state graphs. For any $BT^\backslash ell\; \backslash in\; M\_2$, agent $C\_1$ checks whether $|\backslash delta^\backslash ell(s\_1^i(BT^\backslash ell))|\; =\; 1$, and if so it deduces that $s\_1^\{i+1\}(BT^\backslash ell)\; =\; \backslash delta^\backslash ell(s\_1^i(BT^\backslash ell))$. In this case, $C\_2$ will learn the state of $BT^\backslash ell$ when that thread synchronizes, and it will hold that $s\_2^\{i+1\}(BT^\backslash ell)\; =\; s\_1^\{i+1\}(BT^\backslash ell)$.

The other option is that thread $BT^\backslash ell$ is performing a nondeterministic transition, i.e. $|\backslash delta^\backslash ell(s\_1^i(BT^\backslash ell))|\; >\; 1$. In this case, $C\_1$ has to wait for thread $BT^\backslash ell$ to synchronize and reveal its state to $C\_2$, after which $C\_2$ will broadcast this state to $C\_1$. In this case, it will also hold that $s\_1^\{i+1\}(BT^\backslash ell)\; =\; s\_2^\{i+1\}(BT^\backslash ell)$.

Further, upon receiving the synchronization request from a local thread $BT^t$, agent $C\_1$ uses its stored state graphs to check whether $|\backslash delta^t(s\_1^i(BT^t))|\; >\; 1$. If so, $C\_1$ transmits the thread's new state as learned from the synchronization request, $s\_1^\{i+1\}(BT^t)$, to $C\_2$ — to inform $C\_2$ of how that nondeterministic transition was resolved.

As agent $C\_2$ behaves symmetrically, we conclude that for all $t$ it holds that $s\_1^\{i+1\}(BT^t)\; =\; s\_2^\{i+1\}(BT^t)$, and consequently that $S\_1^\{i+1\}\; =\; S\_2^\{i+1\}$. $\backslash square$ $\backslash square$

Proposition 3 immediately follows from Proposition 4, and from the fact that $f$ is a deterministic function. Indeed, $S\_1^\{i+1\}\; =\; S\_2^\{i+1\}$ implies identical calculation of the set $E$ (line 18 in both agents, and thus the same output for $f(E)$). Finally, the fact that the resulting run is a legal BP follows from the definition of the set $E$ to be the set of enabled events at the synchronization point.

The distributed execution mechanism described above utilizes eager execution in the sense that each machine may be able to continue its execution without waiting for slower machines — except in nondeterministic transitions. We point out that further relaxation can be achieved by using static or dynamic thread information within the scope of each coordinator agent. As in the non-distributed case, this would allow faster threads within the same machine to continue their execution without waiting for their slower counterparts.

Another possible enhancement for the distributed model above is to use approximations for nondeterministic threads on other machines that slow down execution. Suppose that controller agent $C\_1$ of machine $M\_1$ is waiting for thread $BT\; \backslash in\; M\_2$ to finish its nondeterministic transition in order to trigger an event. As was the case in the centralized version, if $C\_1$ can deduce, using the state graph of $BT$, that its next state will be either $s\_1$ or $s\_2$, it can approximate its requested and blocked events with $\backslash mathcal\{R\}\; =\; R(s\_1)\; \backslash cap\; R(s\_2)$ and $\backslash mathcal\{B\}\; =\; B(s\_1)\; \backslash cup\; B(s\_2)$. This further reduces the dependency between the different machines, hopefully achieving better optimization.