Resource management

The resource management is used to co-ordinate concurrent accesses of several tasks with different priorities to shared resources, e.g. management entities (scheduler), program sequences, memory or hardware areas.

We prepare the modules for resources.

#!python

module RESOURCE
{
  signature
  {
    [ Resource ]
  }
}

#!python

module EXTERNAL-RESOURCE
{
  imports
  {
    ex(RESOURCE)
  }
  signature
  {
    [ ExternalResource < Resource ]
  }
}

We also prepare the modules for sets of resources

#!python

make RESOURCES
(
  SET(
    RESOURCE {sort Elt -> Resource }
  ) * {
    sort Set -> Resources
  }
)

#!python

make EXTERNAL-RESOURCES
(
  SET(
    EXTERNAL-RESOURCE {sort Elt -> ExternaResource }
  ) * {
    sort Set -> ExternaResources
  }
)

To describe state transitions on resources, we have to prepare an observation which returns a set of resources.

#!python

module OBSERVATION2RESOURCES
{
  imports
  {
    ex(OBSERVATION)
    pr(RESOURCES)
  }
  signature
  {
    [ Resources < Value ]
  }
}

#!python

module OBSERVATION2EXTERNAL-RESOURCES
{
  imports
  {
    ex(OBSERVATION)
    pr(EXTERNAL-RESOURCES)
  }
  signature
  {
    [ ExternalResources < Value ]
  }
}

For each entity, resources which it will access are statically defined.

#!python

module ACCESS
{
  imports
  {
    pr(RESOURCE)
    pr(ENTITY)
  }
  signature
  {
    op access : Entity Resource -> Bool
  }
}

The resource management is mandatory for all conformance classes. The resource management can optionally be extended to co-ordinate concurrent accesses of tasks and interrupt service routines.

Resource management ensures that

• two tasks cannot occupy the same resource at the same time.
• priority inversion can not occur.
• deadlocks do not occur by use of these resources.
• access to resources never results in a waiting state. If the resource management is extended to the interrupt level it assures in addition that
• two tasks or interrupt routines cannot occupy the same resource at the same time.

The functionality of resource management is useful in the following cases:

• preemptable tasks
• non preemptable tasks, if the user intends to have the application code executed under other scheduling policies, too
• resource sharing between tasks and interrupt service routines
• resource sharing between interrupt service routines

If the user requires protection against interruptions not only caused by tasks, but also caused by interrupts, he/she can also use the operating system services to enable/disable interrupts which do not cause rescheduling.

Behaviour during access to occupied resources

OSEK OS prescribes the OSEK priority ceiling protocol.Consequently, no situation occurs in which a task or an interrupt tries to access an occupied resource. If the resource concept is used for co-ordination of tasks and interrupts the OSEK operating system ensures also that an interrupt service routine is only processed if all resources which might be occupied by that interrupt service routine during its execution have been released.

OSEK strictly forbids nested access to the same resource. In the rare cases when nested access is needed, it is recommended to use a second resource with the same behaviour as the first resource. The OIL language supports the definition of resources with identical behaviour (so-called ‘linked resources').

The following module declares an observation which returns a set of resources occupied by the designated task.

#!python

module OCCUPYING
{
  imports
  {
    ex(OBSERVATION2RESOURCES)
    ex(ENTITY)
  }
  signature
  {
    [ Occupying < Observation ]
    op subj : Occupying -> Entity
  }
  axioms
  {
    vars X : Entity
    eq occupying(X)(init) = nil .
  }
}

The following module declares an observation which returns an entity which occupies the designated resource.

#!python

module OCCUPIED
{
  imports
  {
    ex(OBSERVATION2ENTITIES)
    ex(RESOURCE)
  }
  signature
  {
    [ Occupied < Observation ]
    op subj : Occupied -> Resource
  }
}

A state transition when an entity occupy a resource is described in the following module.

#!python

module OCCUPY
{
  imports
  {
    ex(TRANSITION)
    pr(OCCUPYING)
    pr(OCCUPIED)
    pr(ACCESS)
  }
  signature
  {
    [ Occupy < Transition ]
    op sub : Occupy -> Entity
    op res : Occupy -> Resource
  }
  axioms
  {
    vars C : State
    vars T : Occupy
    cq access(sub(T),res(T)) = true
       if pre(T,C) .
    cq occupied(res(T))(C) = nil
       if pre(T,C) .
    cq occupying(sub(T))(T(C)) = (occupying(sub(T))(C)),res(T)
       if pre(T,C) .
    cq occupied(res(T))(T(C)) = (occupied(res(T))(C)),sub(T)
       if pre(T,C) .
    eq rev(T,occupying(sub(T))) = true .  
    eq rev(T,occupied(res(T))) = true .  
  }
}

A state transition when an entity release a resource is described in the following module.

#!python

module FREE
{
  imports
  {
    ex(TRANSITION)
    pr(OCCUPYING)
    pr(OCCUPIED)
  }
  signature
  {
    [ Free < Transition ]
    op sub : Free -> Entity
    op res : Free -> Resource
  }
  axioms
  {
    vars C : State
    vars T : Free
    cq sub(T) @ occupied(res(T))(C) = true
       if pre(T,C) .
    cq occupying(sub(T))(T(C)) = (occupying(sub(T))(C)) \ res(T)
       if pre(T,C) .
    cq occupied(res(T))(T(C)) = (occupied(res(T))(C)) \ sub(T)
       if pre(T,C) .
    eq rev(T,occupying(sub(T))) = true .  
    eq rev(T,occupied(res(T))) = true .  
  }
}

Restrictions when using resources

TerminateTask, ChainTask, Schedule, WaitEvent shall not be called while a resource is occupied. Interrupt service routine shall not be completed with a resource occupied. In case of multiple resource occupation within one task, the user has to request and release resources following the LIFO principle (stack like).

Scheduler as a resource

If a task shall protect itself against preemptions by other tasks, it can lock the scheduler. The scheduler is treated like a resource which is accessible to all tasks. Therefore a resource with a predefined name RES_SCHEDULER is automatically generated.

#!python

module SCHEDULER
{
  imports
  {
    ex(MODERATOR)
    ex(RESOURCE)
  }
  signature
  {
    [ Scheduler < Moderator Resource ]
    op RES-SCHEDULER : -> Scheduler
  }
}

#!python

module OCCUPATION-on-DISABLE
{
  imports
  {
    pr(DISABLE)
    pr(OCCUPYING)
    pr(EXTERNAL-RESOURCE)
  }
  axioms
  {
    vars C : State
    vars T : Disable
    vars R : ExternalResource
    cq R @ occupying(sub(T))(C) = false
       if pre(T,C) .
  }
}

Internal Resources

Internal resources are resources which are not visible to the user and therefor can not be addressed by the system functions GetResource and ReleaseResource. Instead, they are managed strictly internally within a clearly defined set of system functions. Besides that, the behaviour of internal resources is exactly the same as standard resources (priority ceiling protocol etc.).

#!python

module INTERNAL-RESOURCE
{
  imports
  {
    ex(RESOURCE)
  }
  signature
  {
    [ InternalResource < Resource ]
  }
}

#!python

make INTERNAL-RESOURCES
(
  SET(
    RESOURCE {sort Elt -> InternalResource }
  ) * {
    sort Set -> InternalResources
  }
)

#!python

module OBSERVATION2INTERNAL-RESOURCES
{
  imports
  {
    ex(OBSERVATION)
    pr(INTERNAL-RESOURCES)
  }
  signature
  {
    [ InternalResources < Value ]
  }
}

Internal resources are restricted to tasks. At most one internal resource can be assigned to a task during system generation. If an internal resource is assigned to a task, the internal resource is managed as follows:

• The resource is automatically taken when the task enters the running state9, except when it has already taken the resource. As a result, the priority of the task is automatically changed to the ceiling priority of the resource.

• At the points of rescheduling, the resource is automatically released.10 The implementation may optimise, e.g. only free/take the resource within the system service Schedule if there is a need for rescheduling.

#!python

module ASSOCIATE
{
  imports
  {
    pr(TASK)
    pr(INTERNAL-RESOURCES)
    pr(ACCESS)
  }
  signature
  {
    op associate : Task -> InternalResources
  }
  axioms
  {
    vars X : Task
    vars R : InternalResource
    eq #(associate(X)) <= 1 = true .
    cq access(X,R) = true
       if R @ associate(X) .
  }
}

#!python

module EXECUTED
{
  imports
  {
    ex(OBSERVATION2BOOL)
    pr(TASK)
  }
  signature
  {
    op executed : Task -> Observation2Bool
  }
}