EMN, INRIA 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: 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.

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

The events are as follows:

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.


Last modified: November 1, 2004 - julia@diku.dk