Event mechanism

The event mechanism

• is a means of synchronisation
• is only provided for extended tasks
• initiates state transitions of tasks to and from the waiting state.

Events are objects managed by the operating system. They are not independent objects, but assigned to extended tasks. Each extended task has a definite number of events. This task is called the owner of these events. An individual event is identified by its owner and its name (or mask).

#!python

module MASK
{
  signature
  {
    [ Mask ]
  }
}

#!python


module EVENT
{
  import
  {
    ex(EXTENDEDTASK)
    ex(MASK)
  }
  signature
  {
    [ Event ]
    op owner : Event -> ExtendedTask
    op mask : Event -> Mask
  }
  axioms
  {
    vars X Y : Event
    cq (X = Y) = true if (owner(X) = owner(Y)) and (mask(X) = mask(Y)) .
  }
}

When activating an extended task, these events are cleared by the operating system. Events can be used to communicate binary information to the extended task to which they are assigned.

The meaning of events is defined by the application, e.g. signalling of an expiring timer, the availability of a resource, the reception of a message, etc.

Various options are available to manipulate events, depending on whether the dedicated task is the owner of the event or another task which does not necessarily shall be an extended task. All tasks can set any events of any not suspended extended task. Only the owner is able to clear its events and to wait for the reception (= setting) of its events.

#!python

make EVENTS
(
  SET(
    EVENT { sort Elt -> Event }
  ) * {
    sort Set -> Events
  }
)

#!python

module OBSERVATION2EVENTS
{
  import
  {
    ex(OBSERVATION)
    pr(EVENTS)
  }
  signature
  {
    [ Events < Value ]
  }
}

#!python

module RAISED
{
  import
  {
    ex(OBSERVATION2EVENTS)
  }
  signature
  {
    [ Raised < Observation ]
    op __ : Raised Container -> Events
  }
}

#!python

module WAITINGFOR
{
  imports
  {
    ex(OBSERVATION2EVENTS)
    pr(EXTENDEDTASK)
  }
  signature
  {
    [ Waitingfor < Observation ]
    op subj : Waitingfor -> ExtendedTask
    op __ : Waitingfor Container -> Events
  }
}

Events are the criteria for the transition of extended tasks from the waiting state into the ready state. The operating system provides services for setting, clearing and interrogation of events and for waiting for events to occur.

Any task or ISR of category 2 can set an event for a not suspended extended task, and thus inform the extended task about any status change via this event.

The receiver of an event is an extended task in any case. Consequently, it is not possible for an interrupt service routine or a basic task to wait for an event. An event can only be cleared by the task which is the owner of the event. Extended tasks may only clear events they own, whereas basic tasks are not allowed to use the operating system service for clearing events.

An extended task in the waiting state is released to the ready state if at least one event for which the task is waiting for has occurred. If a running extended task tries to wait for an event and this event has already occurred, the task remains in the running state.

Raising and clearing events can be represented the following transitions.

#!python

module RAISE
{
  imports
  {
    ex(TRANSITION)
    pr(RAISED)
  }
  signature
  {
    [ Raise < Transition ]
    op subj : Raise -> Task
    op event : Raise -> Event
  }
  axioms
  {
    vars C : State
    vars T : Raise
    vars F : Raised
    vars E : Event
    cq (F (T C)) = ((F C), event(T))
       if pre(T,C) .
  }
}

#!python

module CLEAR
{
  imports
  {
    ex(TRANSITION)
    ex(EXTENDEDTASK)
    pr(RAISED)
  }
  signature
  {
    [ Clear < Transition ]
    op subj : Clear -> ExtendedTask
    op event : Clear -> Event
  }
  axioms
  {
    vars C : State
    vars T : Clear
    vars F : Raised
    vars E : Event
    cq (F (T C)) = ((F C)) \ event(T)
       if pre(T,C) .
  }
}