project Obasco

Description of Bossa events in terms of more precise state classes

The event types defined in terms of the state classes RUNNING, READY, BLOCKED, and TERMINATED are actually derived from event types defined in terms of the tuple state classes (RUNNING,RUNNING), (READY,READY), (READY,BLOCKED), (BLOCKED,READY), (BLOCKED,BLOCKED), and (TERMINATED,TERMINATED), in which the first component represents the policy's perspective on the state class of the process and the second component represents the kernel's perspective on the state class of the process. Specifically, these are defined as follows:

(RUNNING,RUNNING): Both the policy and the kernel consider the process to be running.

(READY,READY): Both the policy and the kernel consider the process to be able to run. The bossa.schedule event handler is invoked if there is any process in this state class, and must elect one such process.

(READY,BLOCKED): The policy is willing to run the process, but the process is blocked in the kernel. A running process that blocks ends up in this state class. A process that is in this state class and unblocks is returned to the (READY,READY), implying that it may be elected again.

(BLOCKED,READY): The process is not blocked waiting for anything in the kernel, but the policy is not willing to run it. This state class is used, for example, in a periodic policy when a process should not run until the beginning of its next period.

(BLOCKED,BLOCKED): Both the policy and the kernel consider the process to be unable to run. This state class may be used when a process has blocked in the kernel and receives a notification via an interrupt that its allotted elapsed time has expired within the current period. It is not possible to move directly from this state class to (READY,READY). Instead, the policy and the kernel must each indicate that the process can be run, causing the process to first pass through the (READY,BLOCKED) or (BLOCKED,READY) state class.

(TERMINATED,TERMINATED): Both the policy and the kernel consider the process to be terminated.

Roughly, processes move between the (X,READY) and (X,BLOCKED) state classes, for any X due to block.* and unblock.* events (not unblock.timer.*), while processes move between the (READY,X) and (BLOCKED,X) state classes due to the timing-related events system.clocktick and unblock.timer.*.

To avoid confusion about which tuple component is which, atomic names are used for these various state classes in a Bossa policy. The correspondences are as follows. These state classes can be used by giving the argument -pb to the Bossa compiler.

(RUNNING,RUNNING) is written as RUNNING.
(READY,READY) is written as READY.
(READY,BLOCKED) is written as POLICY_BLOCKED.
(BLOCKED,READY) is written as KERNEL_BLOCKED.
(BLOCKED,BLOCKED) is written as KERNEL_POLICY_BLOCKED.
(TERMINATED,TERMINATED) is written as TERMINATED.

The event types defined in terms of RUNNING, READY, BLOCKED, and TERMINATED are derived from the types below using the following translation:

(RUNNING,RUNNING)/RUNNING becomes RUNNING.
(READY,READY)/READY becomes READY.
(READY,BLOCKED)/POLICY_BLOCKED becomes BLOCKED.
(BLOCKED,READY)/KERNEL_BLOCKED becomes BLOCKED.
(BLOCKED,BLOCKED)/KERNEL_POLICY_BLOCKED becomes BLOCKED.
(TERMINATED,TERMINATED)/TERMINATEDbecomes TERMINATED.

The events are as follows:

process.new
process.end
block.*
unblock.preemptive
unblock.nonpreemptive
unblock.timer.*
system.clocktick
yield.system.pause.*
yield.system.immediate.*
yield.user.*
preempt
bossa.schedule

The event types defined in terms of these state classes are as follows, using the atomic names for conciseness. As compared to the event types defined in terms of RUNNING, READY, BLOCKED, and TERMINATED, the only differences are in the type rules that refer to BLOCKED. We thus explain only these cases, and refer the reader to the description of the simpler event types for further information. While these event types are more complex than those defined in terms of RUNNING, READY, BLOCKED, and TERMINATED, they can also detect more errors, in particular in policies where there are multiple reasons why a process can block, and when this blocking can occur in interrupt handlers.

An important notion in the checking of event types is the identification of those that derive from "quasi-sequences". A quasi sequence occurs when an interrupt occurs within the normal flow of execution and causes the running process to be preempted in some way. Types marked as arising from quasi-sequences (marked with -q>) are only used when an interrupt handler can create the input state.

process.new: The type rules are unchanged except that in the last case the source process is specified to be in a POLICY_BLOCKED state. Only this variant of BLOCKED is possible; the others would imply that the source process is unable to run from the point of view of the kernel, and thus is not able to create a new process.
```
[tgt in NOWHERE, src in RUNNING] ->
      { [tgt in READY], [[src, tgt] in READY] }

[[] = RUNNING, src in READY, tgt in NOWHERE] -q>
      [tgt in READY]

[[] = RUNNING, src in POLICY_BLOCKED, tgt in NOWHERE] -q>
      [tgt in READY]
```
The rule for the initial process is unchanged.
```
[tgt in NOWHERE] -> [tgt in READY, src in NOWHERE]
```

process.end: A process blocks itself in the kernel before terminating, and thus the target process is in either a KERNEL_BLOCKED state or a KERNEL_POLICY_BLOCKED state.
```
{ [tgt in KERNEL_BLOCKED], [tgt in KERNEL_POLICY_BLOCKED] } -> [tgt in TERMINATED]
```

block.*: This event blocks a process from the point of view of the kernel. Thus, if the target process is in either a RUNNING state or a READY state, then it is put in a KERNEL_BLOCKED, according to the first two rules. If the target process is in a POLICY_BLOCKED state, meaning that the policy does not want to run it, then it is now the case that neither the kernel nor the policy wants the process to run. Thus, the process is put in a KERNEL_POLICY_BLOCKED state.
As compared to the type rules defined in terms of RUNNING, READY, BLOCKED, and TERMINATED, in all of the type rules below, the target process must change state, due to the distinction between POLICY_BLOCKED and KERNEL_POLICY_BLOCKED.
```
[tgt in RUNNING] -> [tgt in KERNEL_BLOCKED]

[[] = RUNNING, tgt in READY] -q> [tgt in KERNEL_BLOCKED]

[[] = RUNNING, tgt in POLICY_BLOCKED] -q> [tgt in KERNEL_POLICY_BLOCKED]
```

unblock.preemptive: If the process is blocked only from the point of view of the kernel, ie in the KERNEL_BLOCKED state class, then the process is now able to run, and thus put in the READY state class. Preemption is allowed in this case, as indicated by the second rule. On the other hand, if the process is blocked both from the point of view of the kernel and from the point of view of the policy, ie in the KERNEL_POLICY_BLOCKED state class, then it must remain blocked from the point of view of the policy, and is thus put in the POLICY_BLOCKED state class. Preemption is bnot allowed in this case, because the policy is not willing to run the target process. Fibally, if the target process is not actually blocked from the kernel's point of view, then no state change is allowed, as indicated by the last type rule.
As compared to the type rules defined in terms of RUNNING, READY, BLOCKED, and TERMINATED, in all of the type rules below, the target process must change state, due to the distinction between KERNEL_POLICY_BLOCKED and POLICY_BLOCKED.
```
[tgt in KERNEL_BLOCKED] -> [tgt in READY]

[p in RUNNING, tgt in KERNEL_BLOCKED] -> [[p,tgt] in READY]

[tgt in KERNEL_POLICY_BLOCKED] -> [tgt in POLICY_BLOCKED]

{ [tgt in RUNNING], [tgt in READY], [tgt in POLICY_BLOCKED] } -> []
```

unblock.nonpreemptive: The type rules are the same as those of unblock.preemptive, except without the preemption rule.

[tgt in KERNEL_BLOCKED] -> [tgt in READY]

[tgt in KERNEL_POLICY_BLOCKED] -> [tgt in POLICY_BLOCKED]

{ [tgt in RUNNING], [tgt in READY], [tgt in POLICY_BLOCKED] } -> []

unblock.timer.*: The following type rules apply to unblock.timer.* and to unblock.timer.name, where name is the name of a timer declared in the process/scheduler structure of the current scheduler. In the first rule, processes can change state within a state class, regardless of the state class of the target process. Such state changes are allowed by all of the other rules as well. The second rule additionally specifies that if the target process is initially running, then it can move to a state in the READY or POLICY_BLOCKED state class. It cannot move to a state of the KERNEL_BLOCKED or the KERNEL_POLICY_BLOCKED state class, because the exipiration of a timer created by the policy does not do anything to make the process unable to run from the kernel's point of view. The next two rules allow the target process to move between the READY and POLICY_BLOCKED state classes. Again runnability of the process does not change from the point of view of the kernel, and so the process cannot move to the KERNEL_BLOCKED state class or the KERNEL_POLICY_BLOCKED state class. In the next two rules, the target process can move between the KERNEL_BLOCKED and the KERNEL_POLICY_BLOCKED state classes. Here, the process remains unable to run from the kernel's point of view, but the policy can change its mind about whether it would like to allow the process to run when it becomes able to do so. In the final rule, if the target process ends up in a READY state, then the running process can additionally be preempted.
```
{ [tgt in RUNNING], [tgt in READY], [tgt in POLICY_BLOCKED], [tgt in KERNEL_BLOCKED], [tgt in KERNEL_POLICY_BLOCKED] } ->
  [READY!, POLICY_BLOCKED!, KERNEL_BLOCKED!, KERNEL_POLICY_BLOCKED!]

[tgt in RUNNING] ->
  { [tgt in READY!, POLICY_BLOCKED!, KERNEL_BLOCKED!, KERNEL_POLICY_BLOCKED!],
    [READY!, tgt in POLICY_BLOCKED!, KERNEL_BLOCKED!, KERNEL_POLICY_BLOCKED!] }

[tgt in READY] ->
  [READY!, tgt in POLICY_BLOCKED!, KERNEL_BLOCKED!, KERNEL_POLICY_BLOCKED!]

[tgt in POLICY_BLOCKED] ->
  [tgt in READY!, POLICY_BLOCKED!, KERNEL_BLOCKED!, KERNEL_POLICY_BLOCKED!]

[tgt in KERNEL_BLOCKED] ->
  [READY!, POLICY_BLOCKED!, KERNEL_BLOCKED!, tgt in KERNEL_POLICY_BLOCKED!]

[tgt in KERNEL_POLICY_BLOCKED] ->
  [READY!, POLICY_BLOCKED!, tgt in KERNEL_BLOCKED!, KERNEL_POLICY_BLOCKED!]

{ [p in RUNNING, tgt in READY], [p in RUNNING, tgt in POLICY_BLOCKED] } ->
    [[p,tgt] in READY!, POLICY_BLOCKED!, KERNEL_BLOCKED!, KERNEL_POLICY_BLOCKED!]
```
The following type rules apply to unblock.timer.name, where name is the name of a timer declared as a global variable in the current scheduler. The first rule states that if there is any process in any of the state class, then transitions are allowed within all of the state classes. The next five rules allow transitions between state classes analogous to the transitions of the target process in the rules above. Note that transitions are only allowed from a single state class to another single state class; other processes must remain within their current state classes. This can be seen as a limitation. The last rule allows preemption of the running process when processes move from the POLICY_BLOCKED state class to the READY state class. In contrast to the case where the timer is associated with a specific procss, there is no case for preemption when processes move within the READY state class. This case is subsumed by the second rule, which allows the running process to move to a READY state and arbitrary transitions within the READY state class.
```
{ [p in RUNNING], [p in READY], [p in POLICY_BLOCKED], [p in KERNEL_BLOCKED], [p in KERNEL_POLICY_BLOCKED] } ->
  [READY!, POLICY_BLOCKED!, KERNEL_BLOCKED!, KERNEL_POLICY_BLOCKED!]

[p in RUNNING] ->
  { [p in READY!, POLICY_BLOCKED!, KERNEL_BLOCKED!, KERNEL_POLICY_BLOCKED!],
    [READY!, p in POLICY_BLOCKED!, KERNEL_BLOCKED!, KERNEL_POLICY_BLOCKED!] }

[p in READY] ->
  [READY!, p in POLICY_BLOCKED!, KERNEL_BLOCKED!, KERNEL_POLICY_BLOCKED!]

[p in POLICY_BLOCKED] ->
  [p in READY!, POLICY_BLOCKED!, KERNEL_BLOCKED!, KERNEL_POLICY_BLOCKED!]

[p in KERNEL_BLOCKED] ->
  [READY!, POLICY_BLOCKED!, KERNEL_BLOCKED!, p in KERNEL_POLICY_BLOCKED!]

[p in KERNEL_POLICY_BLOCKED] ->
  [READY!, POLICY_BLOCKED!, p in KERNEL_BLOCKED!, KERNEL_POLICY_BLOCKED!]

[p in RUNNING, p1 in POLICY_BLOCKED] ->
    [[p,p1] in READY!, POLICY_BLOCKED!, KERNEL_BLOCKED!, KERNEL_POLICY_BLOCKED!]
```

system.clocktick: A clocktick can preempt the running process either by putting it in a READY state, implying that the process can be elected if there is no other eligible process, or by putting it in a POLICY_BLOCKED state, implying that the process cannot be elected until it is moved to a READY state by some subsequent event. KERNEL_BLOCKED and KERNEL_POLICY_BLOCKED are not options, because running out of time does not make a process unable to run from the kernel's point of view (eg, the process is not waiting for any resource).
```
[tgt in RUNNING] -> { [], [tgt in READY], [tgt in POLICY_BLOCKED] }
```

yield.*: All of the yield events have the same type. The target process can be in POLICY_BLOCKED when a handler for an event occurring in an interupt has decided to block the process just as it was planning to yield. The compiler only takes this type into account if there is such an interrupt handler.
```
[tgt in RUNNING] -> [tgt in READY]

[[] = RUNNING, tgt in READY] -q> [tgt in READY]

[[] = RUNNING, tgt in POLICY_BLOCKED] -q> []
```

preempt: No change.
```
[tgt in RUNNING] -> [tgt in READY]
```

bossa.schedule: No change.

[[] = RUNNING, p in READY] -> [p in RUNNING, READY!]

Last modified: November 1, 2004 - Julia.Lawall@inria.fr