AdaCore Blog

On the Benefits of Families ... (Entry Families)

On the Benefits of Families ... (Entry Families)

by Pat Rogers

Ada has a concurrency construct known as “entry families” that, in some cases, is just what we need to express a concise, clear solution.

For example, let’s say we want to have a notion of “conditions” that application tasks can await, suspending until the specified condition is "signaled." At some point, other tasks will signal that these conditions are ready to be handled by the waiting tasks. Understand that conditions don't have any state of their own, they are more like "events" that have either happened or have not, and may happen more than once.

For the sake of discussion let’s generalize this idea to an enumeration type representing four possible conditions:

type Condition is (A, B, C, D);

These condition names are not very meaningful but they are just placeholders for those that applications would actually define. Perhaps a submersible's code would have conditions named Hatch_Open, Hatch_Closed, Umbilical_Detached, and so on.

Responding tasks can suspend, waiting for an arbitrary condition to be signaled, and other tasks can signal the occurrence of conditions, using a “condition manager” that the two sets of tasks call.

Here’s the declaration of the condition manager type:

type Manager is limited private;

The type is limited because it doesn’t make sense to assign one manager to another, nor to compare them via predefined equality. There’s another reason you’ll see shortly. The type is private because that’s the default for good software engineering, and there’s no reason to override that default to make the implementation visible to clients. Our API will provide everything clients require, when combined with the capabilities provided by any limited type (e.g., declaring objects, and passing them as parameters).

Tasks can wait for a single condition to be signaled, or they can wait for one of several. Similarly, tasks can signal one or more conditions at a time. Such groups of conditions are easily represented by an unconstrained array type:

type Condition_List is array (Positive range <>) of Condition;

We chose Positive as the index subtype because it allows a very large number of components, far more than is likely ever required. An aggregate value of the array type can then represent multiple conditions, for example:

Condition_List'(A, C)

Given these three types we can define a useful API:

procedure Wait
  (This         : in out Manager;
   Any_Of_These :        Condition_List;
   Enabler      :    out Condition);
--  Block until/unless any one of the conditions in Any_Of_These has been
--  Signaled. The one enabling condition chosen will be returned in the Enabler
--  parameter, and is cleared internally as Wait exits. Any other signaled
--  conditions remain signaled.

procedure Wait
  (This     : in out Manager;
   This_One : Condition);
--  Block until/unless the specified condition has been Signaled. This
--  procedure is a convenience routine that can be used instead of an
--  aggregate with only one condition component.

procedure Signal
  (This         : in out Manager;
   All_Of_These : Condition_List);
--  Indicate that all of the conditions in All_Of_These are now set. The
--  conditions remain set until cleared by Wait.

procedure Signal
  (This     : in out Manager;
   This_One : Condition);
--  Indicate that This_One condition is now set. The condition remains set
--  until cleared by Wait. This procedure is a convenience routine that can
--  be used instead of an aggregate with only one condition component.

Here’s a task that waits for either condition A or B, using a global Controller variable of the Manager type:

task body A_or_B_Processor is
   Active : Condition;
begin
   loop
      Wait (Controller, Any_Of_These => Condition_List'(A, B), Enabler => Active);
      Put_Line ("A_or_B_Processor responding to condition " & Active'Image);
   end loop;
end A_or_B_Processor;

When the call to Wait returns, at least one of either A or B was signaled. One of those signaled conditions is then selected and returned in the Enabler parameter. That selected condition is no longer signaled when the call returns, and will stay that way until another call to procedure Signal changes it. The other condition is not affected, whether or not it was also signaled.

A signaling task could use the API to signal one condition:

Signal (Controller, This_One => B);

or to signal multiple conditions:

Signal (Controller, All_Of_These => Condition_List'(A, C, D));

Now let’s consider the Manager implementation. As this is a concurrent program, we need it to be thread-safe. We’ve declared the Manager type as limited, so either a task type or a protected type would be allowed as the type’s completion. (That’s the other reason the type is limited.) There’s no need for this manager to do anything active, it just suspends some tasks and resumes others when called. Therefore, a protected type will suffice, rather than an active thread of control.

Clearly, tasks that await conditions must suspend until a requested condition has been signaled, assuming it was not already signaled when the call occurred, so a protected procedure won’t suffice. Protected procedures only provide mutual exclusion. Hence we'll use a protected entry for the waiters to call. As you will see later, there is another reason to use protected entries here.

Inside the Manager protected type we need a way to represent whether conditions have been signaled. We can use an array of Boolean components for this purpose, with the conditions as the indexes. For any given condition, if the corresponding array component is True the condition has been signaled, otherwise it has not.

type Condition_States is array (Condition) of Boolean;

Signaled : Condition_States := (others => False);

Thus, for example, if Signaled (B) is True, a task that calls Wait for B will be able to return at once. Otherwise, that task will be blocked and cannot return from the call. Later another task will set Signaled (B) to True, and then the waiting task can be unblocked.

Since an aggregate can also contain only one component if desired, we can use a single set of protected routines for waiting and signaling in the Manager protected type. We don't need one set of routines for waiting and signaling a single condition, and another set of routines for waiting and signaling multiple conditions. Here then is the visible part:

protected type Manager is
   entry Wait
     (Any_Of_These : Condition_List;
      Enabler      : out Condition);
   procedure Signal (All_Of_These : Condition_List);
private
   …
end Manager;

Both the entry and the procedure take an argument of the array type, indicating one or more conditions. The entry, called by waiting tasks, also has an output argument, Enabler, indicating which specific entry enabled the task to resume, i.e., which condition was found signaled and was selected to unblock the task. We need that parameter because the task may have specified that any one of several conditions would suffice, and more than one could have been signaled.

The bodies of our API routines are then just calls into the protected Manager argument. For example, here are two of the four:

procedure Wait
  (This         : in out Manager;
   Any_Of_These :        Condition_List;
   Enabler      :    out Condition)
is
begin
   This.Wait (Any_Of_These, Enabler);
end Wait;

procedure Signal
  (This     : in out Manager;
   This_One : Condition)
is
begin
   This.Signal (Condition_List'(1 => This_One));
end Signal;

Now let’s examine the implementation of the protected type. It gets slightly complicated, but only a little.

Our entry Wait allows a task to request suspension until one of the indicated conditions is signaled, as specified by the entry argument. Normally we’d expect to use the entry barrier to express this so-called “condition synchronization” by querying the conditions’ state array. If one of the requested conditions is True the barrier would allow the call to execute and complete. However, barriers do not have compile-time visibility to the entry parameters, so they cannot be referenced in the barriers. That's also true for the Boolean guards controlling task entry accept statements within select statements.

Why not? Ada synchronization constructs are based on “avoidance synchronization,” meaning that 1) the user-written controls that enable/disable the execution of task entry accept statements and protected entry bodies are intended to enable them only when they can actually provide the requested service, and 2) that runtime determination is based on information known prior to the execution of the accept statement or entry body. For example, at runtime, if a bounded buffer is full, that fact can be determined from the buffer's state: is the count of contained items equal to the capacity of the backing array? If so, the controls disallow the operation to insert another value. Likewise, if the buffer is empty, the removal operation is disallowed. When we write the buffer implementation we know beforehand what the operations will try to do, so we can write the controls to disallow them at runtime until they can succeed. Most of the time that’s sufficient, but not always. When we can't know precisely what the operations will do when we write the code, avoidance synchronization doesn't fit the bill. That's the case with the condition manager: we don’t know beforehand which conditions the Wait caller will specify, and we can't refer to the parameters in the barrier, therefore we cannot use the barrier to enable or disable execution of the Wait entry body.

To handle cases in which avoidance synchronization is insufficient Ada defines the “requeue” statement. Calling an entry that uses a requeue statement is much like calling a large company on the telephone. Calling the main number connects you to a receptionist (if you're lucky and don't get an annoying menu). If the receptionist can answer your question, they do so and then you both hang up. Otherwise, the receptionist forwards ("requeues") the call to the person you need to speak with. After doing so, the receptionist hangs up, because from their point of view the call is complete. The call is not complete from your point of view, though, until you finish your conversation with the new receiver. And of course you may have to wait to speak to that person.

In this metaphor, a task calling entry Wait is the person calling the large corporation. Like the receptionist, Wait must take (execute) the call without knowing the requested conditions, because the entry barrier cannot reference the entry arguments. The specified conditions and their states are only known once the entry body executes. Therefore, Wait may or may not be able to allow the caller to return from the call immediately. If not, it requeues the call and finishes, leaving the call still pending on the requeue target. Because Wait always takes a call, the entry barrier is just hard-coded to True. (That’s always a strong indication that requeue is involved.) Even though this barrier always allows a call, much like a protected procedure, we must use an entry because only protected entries can requeue callers.

Inside the entry body the specified conditions’ states are checked, looking for one that is True. If one is found, the entry body completes and the caller returns to continue further, responding to the found condition. If no requested condition is True, though, we cannot let the caller continue. We block it by requeueing the caller on to another entry. Eventually that other entry will allow the caller to return, when an awaited condition finally becomes True via Signal.

Here then is the full declaration for the protected type Manager:

type Condition_States is array (Condition) of Boolean;

protected type Manager is
   entry Wait
     (Any_Of_These : Condition_List;
      Enabler      : out Condition);
   procedure Signal (All_Of_These : Condition_List);
private
   Signaled          : Condition_States := (others => False);
   Prior_Retry_Calls : Natural := 0;
   entry Retry
     (Any_Of_These : Condition_List;
      Enabler      : out Condition);
end Manager;

The private part contains the condition states, a management variable, and the other entry, Retry, onto which we will requeue when necessary. Note that this other entry is only meant to be called by a requeue from the visible entry Wait, so we declare it in the private part to ensure there are no other calls to it.

Here’s the body of the entry Wait:

entry Wait 
  (Any_Of_These : Condition_List;  
   Enabler      : out Condition) 
when 
   True 
is
   Found_Awaited_Condition : Boolean;
begin
   Check_Conditions (Any_Of_These, Enabler, Found_Awaited_Condition);
   if not Found_Awaited_Condition then
      requeue Retry;
   end if;
end Wait;

The hard-coded entry barrier ("when True") always allows a caller to execute, subject to the mutual exclusion requirement. In the body, we call an internal procedure to check the state of the requested condition(s). If we don’t find one of the specified conditions True, we requeue the caller to the Retry entry. The entry parameters are the same in this case so they go to the Retry entry as usual. On the other hand, if we did find a specified condition True, we just exit the call, Enabler having been set already.

Eventually, presumably, an awaited False condition will become True. That happens when Signal is called:

procedure Signal (All_Of_These : Condition_List) is
begin
   for C of All_Of_These loop
      Signaled (C) := True;
   end loop;
   Prior_Retry_Calls := Retry'Count;
end Signal;

After setting the specified conditions' states to True, Signal captures the number of queued callers waiting on Retry. (The variable Prior_Retry_Calls is an internal component declared in the protected type. The value is never presented to callers, but is, instead, used only to manage callers.)

At long last, here’s the body of Retry:

entry Retry 
  (Any_Of_These : Condition_List;  
   Enabler      : out Condition) 
when 
   Prior_Retry_Calls > 0
is
   Found_Enabling_Condition : Boolean;
begin
   Prior_Retry_Calls := Prior_Retry_Calls - 1;
   Check_Conditions (Any_Of_These, Enabler, Found_Enabling_Condition);
   if not Found_Enabling_Condition then
      requeue Retry;
   end if;
end Retry;

Recall that when a protected procedure or entry exits a protected object, the run-time system re-evaluates all the object’s entry barriers, looking for an open (True) barrier with a caller queued, waiting. If one is found, that entry body is allowed to execute on behalf of that caller. On exit, the evaluation/execution process repeats. This process is known as a “protected action” and is one reason protected objects are so expressive and powerful. The protected action continues iterating, executing enabled entry bodies on behalf of queued callers, until either no barriers are open or no open barriers have callers waiting.

Therefore, when procedure Signal sets Prior_Retry_Calls to a value greater than zero and then exits, the resulting protected action allows Retry to execute. Furthermore, Retry continues to execute, attempting to service all the prior callers in the protected action, because its barrier is False only when all those prior callers have been serviced.

For each caller, Retry attempts the same thing Wait did: if a requested condition is True the caller is allowed to return from the call. Otherwise, the caller is requeued onto Retry. So yes, Retry requeues the caller onto itself! Doing so is not necessarily a problem, but in this case a caller would continue to be requeued indefinitely when the requested condition is False, unless something prevents that from happening. That’s the purpose of the count of prior callers. Only that number of callers are executed by the body of Retry in the protected action. After that the barrier is closed by Prior_Retry_Calls becoming zero, the protected action ceases when the entry body exits, and any unsatisfied callers remain queued.

All well and good, this works, but have you noticed the underlying assumption? The code assumes that unsatisfied callers are placed onto the entry queue at the end of the queue, i.e., in FIFO order. Consequently, they are not included in the value of the Prior_Retry_Calls count and so do not get executed again until Signal is called again. But suppose we have requested that entry queues (among other things) are ordered by caller priority? We’d want that for a real-time system. But then a requeued caller would not go to the back of the entry queue and would, instead, execute all over again, repeatedly. The prior caller count wouldn’t solve that problem.

If priority queuing might be used, we must change the internal implementation so that the queuing policy is irrelevant. We’ll still have Wait do a requeue when necessary, but no requeue will ever go to the same entry executing the requeue statement. Therefore, the entry queuing order won't make a difference. The entry family facilitates that change, and rather elegantly, too.

An entry family is much like an array of entries, each one identical to the others. To work with any one of the entries we specify an index, as with an array. For example, here’s a requeue to Retry as a member of an entry family, with Active_Retry as the index:

requeue Retry (Active_Retry)

In the above, the caller uses the value of Active_Retry as an index to select a specific entry in the array/family.

The resulting changes to the Manager type are as follows:

type Retry_Entry_Id is mod 2;
type Retry_Barriers is array (Retry_Entry_Id) of Boolean;

protected type Manager is
   … as before
private
   Signaled      : Condition_States := (others => False);
   Retry_Enabled : Retry_Barriers := (others => False);
   Active_Retry  : Retry_Entry_Id := Retry_Entry_Id'First;
   entry Retry (Retry_Entry_Id)
     (Any_Of_These : Condition_List;
      Enabler      : out Condition);
end Manager;

Our entry family index type is Retry_Entry_Id. We happen to need two entries in this implementation, so a modular type with two values will suffice. Modular arithmetic will also express the logic nicely, as you’ll see. The variable Active_Retry is of this type, initialized to zero.

The entry Retry is now a family, as indicated by the entry declaration syntax specifying the index type Retry_Entry_Id within parentheses. Each entry has the same parameters as any others in the family, in this case the same parameters as in the previous implementation.

We thus have two Retry entries so that, at any given time, one of the entries can requeue onto the other one, instead of onto itself. An entry family makes that simple to express.

At runtime, one of the Retry entries will field requeue calls from Wait, and will also be the entry enabled by Signal. That entry is designated the “active” retry target, via the index held in the local variable Active_Retry.

Here’s the updated body of Wait accordingly:

entry Wait 
  (Any_Of_These : Condition_List;  
   Enabler      : out Condition) 
when 
   True 
is
   Found_Enabling_Condition : Boolean;
begin
   Check_Conditions (Any_Of_These, Enabler, Found_Enabling_Condition);
   if not Found_Enabling_Condition then
      requeue Retry (Active_Retry) with abort;
   end if;
end Wait;

The body is as before, except that the requeue target depends on the value of Active_Retry. (We'll discuss "with abort" shortly.)

When Signal executes, it now enables the “active retry” entry barrier:

procedure Signal (All_Of_These : Condition_List) is
begin
   for C of All_Of_These loop
      Signaled (C) := True;
   end loop;
   Retry_Enabled (Active_Retry) := True;
end Signal;

The barrier variable Retry_Enabled is now an array, using the same index type as the entry family.

The really interesting part of the implementation is the body of Retry, showing the expressive power of the language. The entry family member enabled by Signal goes through all its pending callers, attempting to satisfy them and requeuing those that it cannot. But instead of requeuing onto itself, it requeues them onto the other entry in the family. As a result, the order of the queues is immaterial. Again, the entry family makes this easy to express:

entry Retry (for K in Retry_Entry_Id)
  (Any_Of_These : Condition_List;
   Enabler      : out Condition)
when 
   Retry_Enabled (K)
is
   Found_Enabling_Condition : Boolean;
begin
   Check_Conditions (Any_Of_These, Enabler, Found_Enabling_Condition);
   if Found_Enabling_Condition then
      return;
   end if;
   --  otherwise...
   if Retry (K)'Count = 0 then -- current caller is the last one present
      Retry_Enabled (K) := False;
      Active_Retry := Active_Retry + 1;
   end if;
   requeue Retry (K + 1) with abort;
end Retry;

Note the first line:

entry Retry (for K in Retry_Entry_Id)

as well as the entry barrier (before the reserved word “is”):

when Retry_Enabled (K)

“K” is the entry family index, in this case iterating over all the values of Retry_Entry_Id (i.e., 0 .. 1).

We don’t have to write a loop checking each family member’s barrier; that happens automatically, via K. When a barrier at index K is found to be True, that corresponding entry can execute a prior caller. Slick, isn’t it? Ada is a very powerful language.

Note the last statement, the one performing the requeue:

requeue Retry (K + 1) with abort;

Like the Active_Retry variable, the index K is of the modular type with two possible values, so K + 1 is always the “other” entry of the two. The addition wraps around, conveniently. As a result, the requeue is always onto the other entry, never itself, so the entry queue ordering makes no difference.

The “with abort” is important but is not a controlling design factor. In a nutshell, it means that task abort is enabled for the requeued task. The significance is that an aborted task that is suspended on an entry queue is removed from that queue. That’s allowable in this case because we are not using the count of prior callers to control the number of iterations in the protected action, unlike the FIFO implementation. In that other implementation we could not allow requeued tasks to be aborted because the count of prior callers would no longer match the number of queued callers actually present. The protected action would await a caller that would never execute. In this implementation that cannot happen so it is safe to allow aborted tasks to be removed from the queue.

Note that we do still check the count of pending queued callers, we just don't capture it and use it to control the number of iterations in the protected action. If we’ve processed the last caller for member K, we close member K’s barrier immediately, and then set the active retry index to the other entry member so that Wait will requeue to the new “active retry” entry and Signal will, eventually, enable it.

Because we did not make the implementation visible to the package’s clients, our internal changes will not require users to change any of their code.

Note that both the Ravenscar and Jorvik profiles allow entry families, but Ravenscar only allows one member per family because only one entry is allowed per protected object. Such an entry family wouldn't be much use. Jorvik allows multiple entry family members because it allows multiple entries per protected object. However, neither profile allows requeue statements, for the sake of simplifying the underlying run-time library implementation.

For more on tasking and topics like this, see the book by Burns and Wellings, Concurrent and Real-Time Programming In Ada, Cambridge University Press, 2007. Yes, 2007, but it is still excellent and directly applicable today. Indeed, this solution to the condition manager is based on their Resource_Controller example and was supplied to a customer this year.

Thanks to Andrei Gritsenko (Андрей Гриценко@disqus_VErl9jPNvR) for suggesting a nice simplification of the FIFO version of the facility. This blog entry has been updated accordingly.

The full code for the entry-family approach follows. Note that we have used a generic package so that we can factor out the specific kind of conditions involved, via the generic formal type. As long as the generic actual type is a discrete type the compiler will be happy. That’s essential because we use the condition type as an index for an array type.

--  This package provides a means for blocking a calling task until/unless any
--  one of an arbitrary set of "conditions" is signaled.

--  NOTE: this implementation allows either priority-ordered or FIFO-ordered
--  queuing.

generic
   type Condition is (<>);
package Condition_Management is

   type Manager is limited private;

   type Condition_List is array (Positive range <>) of Condition;

   procedure Wait
     (This         : in out Manager;
      Any_Of_These :        Condition_List;
      Enabler      :    out Condition);
   --  Block until/unless any one of the conditions in Any_Of_These has been
   --  Signaled. The one enabling condition will be returned in the Enabler
   --  parameter, and is cleared internally as Wait exits. Any other signaled
   --  conditions remain signaled.

   procedure Wait
     (This     : in out Manager;
      This_One : Condition);
   --  Block until/unless the specified condition has been Signaled. This
   --  procedure is a convenience routine that can be used instead of an
   --  aggregate with only one condition component.

   procedure Signal
     (This         : in out Manager;
      All_Of_These : Condition_List);
   --  Indicate that all of the conditions in All_Of_These are now set. The
   --  conditions remain set until cleared by Wait.

   procedure Signal
     (This     : in out Manager;
      This_One : Condition);
   --  Indicate that This_One condition is now set. The condition remains set
   --  until cleared by Wait. This procedure is a convenience routine that can
   --  be used instead of an aggregate with only one condition component.

private

   type Condition_States is array (Condition) of Boolean;

   type Retry_Entry_Id is mod 2;

   type Retry_Barriers is array (Retry_Entry_Id) of Boolean;

   protected type Manager is
      entry Wait
        (Any_Of_These : Condition_List;
         Enabler      : out Condition);
      procedure Signal (All_Of_These : Condition_List);
   private
      Signaled      : Condition_States := (others => False);
      Retry_Enabled : Retry_Barriers := (others => False);
      Active_Retry  : Retry_Entry_Id := Retry_Entry_Id'First;
      entry Retry (Retry_Entry_Id)
        (Any_Of_These : Condition_List;
         Enabler      : out Condition);
   end Manager;

end Condition_Management;



package body Condition_Management is

   ----------
   -- Wait --
   ----------

   procedure Wait
     (This         : in out Manager;
      Any_Of_These :        Condition_List;
      Enabler      :    out Condition)
   is
   begin
      This.Wait (Any_Of_These, Enabler);
   end Wait;

   ----------
   -- Wait --
   ----------

   procedure Wait
     (This     : in out Manager;
      This_One : Condition)
   is
      Unused : Condition;
   begin
      This.Wait (Condition_List'(1 => This_One), Unused);
   end Wait;

   ------------
   -- Signal --
   ------------

   procedure Signal
     (This         : in out Manager;
      All_Of_These : Condition_List)
   is
   begin
      This.Signal (All_Of_These);
   end Signal;

   ------------
   -- Signal --
   ------------

   procedure Signal
     (This     : in out Manager;
      This_One : Condition)
   is
   begin
      This.Signal (Condition_List'(1 => This_One));
   end Signal;

   -----------
   -- Event --
   -----------

   protected body Manager is

      procedure Check_Conditions
        (These   : Condition_List;
         Enabler : out Condition;
         Found   : out Boolean);

      ----------
      -- Wait --
      ----------

      entry Wait 
        (Any_Of_These : Condition_List;  
         Enabler      : out Condition) 
      when 
         True 
      is
         Found_Enabling_Condition : Boolean;
      begin
         Check_Conditions (Any_Of_These, Enabler, Found_Enabling_Condition);
         if not Found_Enabling_Condition then
            requeue Retry (Active_Retry) with abort;
         end if;
      end Wait;

      ------------
      -- Signal --
      ------------

      procedure Signal (All_Of_These : Condition_List) is
      begin
         for C of All_Of_These loop
            Signaled (C) := True;
         end loop;
         Retry_Enabled (Active_Retry) := True;
      end Signal;

      -----------
      -- Retry --
      -----------

      entry Retry (for K in Retry_Entry_Id)
        (Any_Of_These : Condition_List;
         Enabler      : out Condition)
      when 
         Retry_Enabled (K)
      is
         Found_Enabling_Condition : Boolean;
      begin
         Check_Conditions (Any_Of_These, Enabler, Found_Enabling_Condition);
         if Found_Enabling_Condition then
            return;
         end if;
         --  otherwise...
         if Retry (K)'Count = 0 then -- current caller is the last one present
            Retry_Enabled (K) := False;
            Active_Retry := Active_Retry + 1;
         end if;
         requeue Retry (K + 1) with abort;
      end Retry;

      ----------------------
      -- Check_Conditions --
      ----------------------

      procedure Check_Conditions
        (These   : Condition_List;
         Enabler : out Condition;
         Found   : out Boolean)
      is
      begin
         for C of These loop
            if Signaled (C) then
               Signaled (C) := False;
               Enabler := C;
               Found := True;
               return;
            end if;
         end loop;
         Found := False;
      end Check_Conditions;

   end Manager;

end Condition_Management;

Posted in #Ada    #Concurrency    #Entry Families   

About Pat Rogers

Pat Rogers

Dr. Patrick Rogers has been a computing professional since 1975, primarily working on embedded real-time applications including high-fidelity flight simulators and Supervisory Control and Data Acquisition (SCADA) systems controlling hazardous materials. He was director of the Ada9X Laboratory for the U.S. Air Force’s Joint Advanced Strike Technology Program, Principal Investigator in distributed systems and fault tolerance research projects using Ada for the U.S. Air Force and Army, and Associate Director for Research at the NASA Software Engineering Research Center. As a member of the Senior Technical Staff at AdaCore, he specializes in supporting real-time/embedded application developers, develops bare-board products and demonstrations for AdaCore, and creates training courses and presentations. He serves as Convenor of ISO/IEC JTC 1/SC 22/WG 9, the group responsible for the Ada standard.