28 2 Standard and Generic Components
The hardware process is defined as:
HW = start.HW
1
HW
1
=(i
1
.saveregs + HW
1
+setregs.HW
1
+getregs.HW
1
+restoreregs.HW
1
) \ saveregs
The following pair of processes are intended to model the behaviour of
hardware when an interrupt occurs. The process Int
i
represents the ith in-
terrupt. When it receives its internal interrupt signal, i
i
, it signals that the
Interrupt Service Routine (ISR) corresponding to this interrupt should be ex-
ecuted; this is done by sending the
runisr
i
message. The interrupt process
then recurs, ready to accept another interrupt signal. The second process,
ISR

mines whether interrupts are signalled or not (it is modelled in this book by
the Lock Object-Z class).
IntMask = on.IntMask(1)
IntMask(v)=off .IntMask(0)
+on.IntMask(1)
+stat.
istat(n).IntMask(n)
The interrupt mask enables the hardware model to be extended so that inter-
rupts can be enabled and disabled under programmer control. Integration of
the interrupt mask and the process P is left as an exercise for the interested
reader.
Themodelworksasfollows.Initially,theIntMask accepts an on event to
initialise the mask. Initialisation enables interrupts and takes the state of the
mask as its parameter (the value in parentheses). After this, the mask offers
three possible actions: off to disable interrupts, on to enable them and stat to
enquire about the state of the mask. When IntMask engages in an off action, it
disables interrupts (denoted by the 0 parameter). Alternatively, it can engage
in an on action. If interrupts are currently disabled, the on action re-enables
2.4 Hardware Model 29
them; otherwise, it does nothing. Finally, some other component (say, some
software) can enquire as to the state of the interrupt mask by engaging in
the third possible action, stat (status). The IntMask process then returns the
current status (denoted by n) via an
istat (interrupt status) action; enquiry
does not affect the state of the mask. This is indicated by the recursion on
the same value as that communicated by the
istat action.
This is a single-level interrupt scheme. Some processors have a multi-level
one. At the level of detail required in this book, the differences between single-
and multi-level interrupt schemes are not significant, so a single-level scheme

being used).
The register names form the following set:
30 2 Standard and Generic Components
GENREG == {r
0
, ,r
numregs
−1
}
The contents of this set are of no further interest to us because the register
set will be manipulated as a complete entity.
The register set is defined as a function from register (index) to the value
it contains:
GENREGSET == GENREG → PSU
The status register contains a value. That value is of the following type.
It is assumed to be of the same size (in bits) as an element of PSU .
[STATUSWD]
This will be an enumeration, for example: overflow, division by zero, carry set.
The register state is defined by the following schema:
HWREGISTERS
hwregset : GENREGSET
hwstack : PSTACK
hwip : N
hwstatwd : STATUSWD
The general register set is hwregset,thestackisinhwstack, the instruction
pointer (program counter) is hwip and the status word is denoted by hwstatwd .
The following defines the zero elements for PSU and STATUSWD:
0
PSU
: PSU

1—symbolic values are used instead for easier interpretation of often complex
schemata):
INTERRUPTSTATUS ::= inton | intoff
The value inton represents the hardware state in which interrupts are enabled.
The value intoff denotes the fact that interrupts have been disabled.
The interrupt flag itself is defined as:
INTERRUPTFLAG
iflag : INTERRUPTSTATUS
When the hardware starts up, it will execute an operation similar to that
denoted by the following schema:
InitINTERRUPTFLAG
INTERRUPTFLAG

iflag

= inton
This schema is similar to the register-initialisation schema. It is assumed that
the hardware executes it before the kernel bootstrap starts executing. This
will be the only time we see this schema.
There are three operations associated with the interrupt flag. Two are
under program control: one disables and one enables interrupts. The remaining
operation raises the interrupt and performs operations such as saving the
current register state and transferring control to an ISR.
Theoperationtodisableinterruptsismodelledhereas:
DisableInterrupts
∆INTERRUPTFLAG
iflag

= intoff
The operation to enable interrupts is:

low-level model can be produced in Z (later in Object-Z) in a fashion that is
relatively clear and, what is more, in a form that allows a number of properties
to be proved.
The hardware clock is associated with the interrupt number:
clockintno : INTNO
Time is modelled as a subset of the naturals:
TIMEVAL == N
Here, time is expressed in terms of uninterpreted units called “ticks” (assumed
to occur at regular intervals, say every 1/60 second).
The clock is just a register that contains the current time, expressed in
some units:
CLOCK
timenow : TIMEVAL
The hardware initialises the clock on startup. (The clock can also be reset
on some processors.)
2.4 Hardware Model 33
InitCLOCK
CLOCK

timenow

=0
The length of the clock tick often needs to be converted into some other
unit. For example, a 60Hz “tick” might be converted into seconds.
ticklength : TIMEVAL
The clock updates itself on every hardware “tick”:
UpdateCLOCKOnTick
∆CLOCK
timenow


InitTIMERRQQUEUE
TIMERRQQUEUE

telts

= ∅
The following schema defines a predicate that is true when the request
queueisempty:
EmptyTIMERRQQUEUE
ΞTIMERRQQUEUE
telts = ∅
The following three schemata define operations that add and remove re-
quests:
EnqueueTIMERRQ
∆TIMERRQQUEUE
tr?:TIMERRQ
telts

= telts ∪{tr?}
RemoveFirstTIMERRQ
∆TIMERRQQUEUE
tr!:TIMERRQ
{tr!}∪telts

= telts
This operation removes the first element of the queue. It is a non-deterministic
operation.
RemoveTIMERRQQueueElt
∆TIMERRQQUEUE
tr?:TIMERRQ

= ∅
The following condition must always hold:
Proposition 11. At any time, now:
∀ tr : TIMERRQ •
tr ∈ telts ⇒ timerrq
time(tr) > now
Proposition 12. At any time, now:
¬∃tr : TIMERRQ •
tr ∈ telts ∧ timerrq
time(tr) ≤ now
Both of these propositions are consequences of Proposition 92 (p. 173).
Their proofs are omitted.
In order to unblock those processes whose alarms have gone off, the follow-
ing schema is used. It returns a set of requests whose time component specifies
atimethatisnowinthepast:
36 2 Standard and Generic Components
TimerRequestsNowActive
∆TIMER
trqset!:F TIMERRQ
trqset!={trq : TIMERRQ | trq ∈ telts ∧ timerrq time(trq) ≤ timenow • trq}
telts

= telts \ trqset!
This is the basis of a CLOCK process:
OnTimerInterrupt =
(UpdateCLOCKOnTick
o
9
((TimerRequestsNowActive[trqset/trqset!] ∧
(∀ trq : TIMERRQ | trq ∈ trqset ∧ timerrq

each hardware clock “tick”, the time quantum is decremented. When the
quantum reaches some threshold value, the process is suspended. When that
same process is executed the next time, it is assigned a new quantum.
To begin, the type of time
quantum is defined:
time quantum : TIMEVAL
2.4 Hardware Model 37
For the purpose of this book, every user process uses the same values for
initialisation and threshold.
The following schema retrieves the value of a process’ time quantum from
the process table.
ProcessQuantum
ΞPROCESSES
pid?:PREF
timeq!:TIMEVAL
timeq!=pquants(pid?)
The next schema defines an operation that sets the initial value for its
time quantum:
SetInitialProcessQuantum
∆PROCESSES
pid?:PREF
time quant?:TIMEVAL
pquants

= pquants ∪{pid? → time quant?}
When a process’ time quantum is to be reset, the following operation does
the work:
ResetProcessTimeQuantum =
(∃ q : TIMEVAL | q = time
quantum •

time quantum has expired:
CurrentProcessQuantumHasExpired
ΞCURRENTPROCESSpq
tq ≤ 0
The current process quantum is read from the storage location by the next
schema:
CurrentProcessQuantum
ΞCURRENTPROCESSpq
tquant!:TIMEVAL
tquant!=tq
On each hardware clock tick, the current process’ time quantum is updated
by the following operation:
UpdateCurrentQuantumOnTimerClick =
(TimeNow[now/now !] ∧
UpdateCurrentProcessQuantum[now/now?])
\ {now}
This operation is already represented in the last line of OnTimerInterrupt.
When a process is blocked, the following are required:
SaveCurrentProcessQuantum =
(CurrentProcessQuantum[tquant/tquant!] ∧
UpdateProcessQuantum[tquant/timeq?])
\ {tquant}
This expands into:
ΞCURRENTPROCESSpq
∆PROCESSES
(∃ tquant : TIMEVAL •
tquant = tq ∧
pquants

= pquants ⊕{pid? → tquant?})

Each process is represented by an entry in the process table; the entry is a
process descriptor. The process descriptor contains a large amount of infor-
mation about the state of the process it represents; the actual contents of the
process descriptor depend upon the kernel, its design and its purpose (e.g.,
a real-time kernel might contain more information about priorities and time
than one for an interactive system as well as the hardware).
The purpose of this section is not to define the canonical process descriptor
and process table for the kernels in this book (which, in any case, differ among
themselves), nor to define the canonical structure for the process table (the one
here is somewhat different from those that follow). Instead, it is intended as a
general definition of these structures and as a place where general properties
can be identified and proved.
As will become clear from the kernel models that follow, the process table
in this section differs somewhat from the others in this book. In particular, the
process table here is modelled as a collection of mappings, while the others
are more obviously “tables”. The reasons for this difference are many. The
most important, for present purposes, are:
40 2 Standard and Generic Components
• The current model is at a higher level than the others.
• The current model separates the different attributes of the process descrip-
tor into individual mappings.
Some kernels (e.g., some versions of Unix) use the representation used here.
The representation of this section has a slight advantage over the standard
table representation: for fast real time, it is possible to access components of
the process descriptor simultaneously—this might also be of utility in a kernel
running on a multi-processor system.
The section begins with a set of definitions required to support the defini-
tion of the process descriptor and the process table.
In particular, there is a limit to the number of processes that can be
present in the system. There is one process descriptor for each process, so this

pstrunning
| pstready
| pstwaiting
|
pstswappedout
| pstzombie
| pstterm
Processes come in three kinds:
PROCESSKIND ::= ptsysproc
| ptuserproc
| ptdevproc
These kinds are system, user and device processes.
The code and data areas of a process’ main-store image need to be repre-
sented:
[PCODE, PDATA]
For the time being, we can ignore PCODE and PDATA. Their elements are
structured in a way that will only be relevant during refinement; similarly, the
PSTACK type also has elements whose structures can, for the most part, be
ignored. (The structure of elements of type PSTACK is only really of relevance
to interrupt service routines and the mechanisms that invoke them—typically
they push a subset of the current register set onto the stack.)
The process descriptor (sometimes called the process record) is defined
by the following schema; together all process descriptors in the system form
the process table. It is the primary data structure for recording important
information about processes. The information includes a representation of
the process’ state, which is retained while the process is not executing. On
a context switch, the state (primarily, hardware registers, IP and stack) is
copied into the process descriptor for storage until the process is next ex-
ecuted. When next selected to run, the state is copied back into registers.
The process descriptor does hold other information about the process: data

NullProcRef ∈ known procs
known procs = dom pstatus
dom pstatus = dom pkinds
dom pkinds = dom pprios
dom pprios = dom pregs
dom pregs = dom pstacks
dom pstacks = dom pstackwds
dom pstackwds = dom pcode
dom pcode = dom pdata
dom pdata = dom pips
known uids = ran pips
The conjunct, NullProcRef , is added to the predicate because it is required
that NullProcRef actually refer to the null process. It should never be the
case that the null process appears in the process table.
It is possible to exclude IdleProcRef from the process table in a manner
identical to NullProcRef . In the case of IdleProcRef , matters are less clear.
The idle process is a real process: it has code but probably no data or stack
areas. It is quite possible to have an idle process without representing it in
the process table. The idle process is only executed whenever the ready queue
is empty, so a small piece of code can do all the necessary work. To some,
this will appear an ad hoc solution; to others, it will appear totally natural.
2.5 Processes and the Process Table 43
At the moment, the idle process will be represented in the process table, even
though it requires an additional slot (this is, after all, a specification, not an
implementation).
When refinement is performed, the inclusion of IdleProcRef and the ex-
clusion of NullProcRef are of some importance. They determine the range of
possible values for the domains of the components of process descriptors. In
other words, their inclusion and exclusion determine what a “real process”
can be; this is reflected in the type to which PREF refines: REALPROCS

Furthermore, the domains are all identical to known procs since dom pstatus =
known
procs.SinceNullProcRef ∈ known procs, it follows that NullProcRef ∈
dom pregs (for example). By Definition 1, the null process is not a “real” pro-
cess. ✷
44 2 Standard and Generic Components
The process table is initialised by the following operation:
InitPROCESSES
PROCESSES

known procs

= ∅
A process is removed from the process table by the operation modelled by
the following schema:
DelProcess
∆PROCESSES
pid?:PREF
pstatus

= {pid?}
−
 pstatus
pkinds

= {pid?}
−
 pkinds
pprios


Taking domains and using the identity dom pregs = known
procs:
dom pregs

= known
procs

= dom({p}
−
 pregs)
= dom(pregs \{p})
Therefore, p ∈ known
procs

.
The same reasoning can be applied to all similar functions in PROCESSES. ✷
A process is added to the process table by the AddProcess operation:
AddProcess
∆PROCESSES
pid?:PREF
knd?:PROCESSKIND
status?:PROCSTATUS
stat?:STATUSWD
regs ?:GENREGSET
2.5 Processes and the Process Table 45
stk?:PSTACK
prio?:PRIO
ip?:N
pstatus


: PREF  → PSTACK •
pstacks

= pstacks ∪{p? → stk}∧
pstacks

= {p?}
−
 pstacks

which simplifies to:
pstacks

= {p?}
−
 (pstacks ∪{p? → stk})
So:
dom({p?}
−
 (pstacks ∪{p? → stk}))
= (dom pstacks ∪ dom{p? → stk}) \{p?}
= ((dom pstacks) ∪{p?}) \{p?}
Therefore:
dom pstacks

= dom(pstacks ∪{p?}) \{p?}
= dom pstacks
✷
The priority of a process is returned by the following operation:
ProcessPriority

pstat?:PROCSTATUS
pstatus

= pstatus ⊕{pid? → pstat}
The following operations set the process status to designated values as and
when required:
SetProcessStatusToNew =
([pstat : PROCSTATUS | pstat = pstnew] ∧
UpdateProcessStatus[pstat/pstat?])
\ {pstat}
This operation is called when a process has been created but not added to
the ready queue.
When a process enters the ready queue, the following operation changes
its status to reflect the fact:
2.5 Processes and the Process Table 47
SetProcessStatusToReady
=
([pstat : PROCSTATUS | pstat = pstready] ∧
UpdateProcessStatus[pstat/pstat?])
\ {pstat}
The SetProcessStatusToRunning operation should be called when a pro-
cess begins execution:
SetProcessStatusToRunning =
([pstat : PROCSTATUS | pstat = pstrunning] ∧
UpdateProcessStatus[pstat/pstat?])
\ {pstat}
When a process is suspended for whatever reason, the following operation
is called to set its status to pstwaiting:
SetProcessStatusToWaiting =
([pstat : PROCSTATUS | pstat = pstwaiting] ∧

NextPREF
PROCESSES
pid!:PREF
(∃ p : PREF | p ∈ (PREF \ known procs) •
p = NullProcRef ∧ p = IdleProcRef ∧
pid!=p)
or:
pid! ∈{p : PREF • p ∈ known procs}
The way names are allocated to new processes is as follows. There is a set
of all possible process references, PREF . If a process’ identifier is not in
known
procs, the set of known processes (i.e., the names of all processes
that are currently in the system—the domain of all attribute mappings), it
can be allocated. Allocation is, here, the addition of a process reference to
known
procs.
If all processes have been allocated, the following schema’s predicate is
satisfied.
ProcessesFullyAllocated
PROCESSES
known procs = PREF \{NullProcRef , IdleProcRef }
Note that neither IdleProcRef,norNullProcRef represent real processes that
can be allocated and deallocated in the usual way. Indeed, IdleProcRef denotes
the idle process that runs whenever there is nothing else to do; it is already
defined within the kernel. The constant NullProcRef denotes the null process
and is only used for initialisation or in cases of error.
The following is just a useful synonym:
CannotAllocateProcess = ProcessesFullyAllocated
Proposition 16. For any process, p, such that p ∈ known
procs:

concluded that the predicate of ¬ ProcessesFullyAllocated

does not hold. ✷
It might be useful to know whether there are any processes in the system.
The following schema provides that ability:
NoProcessesInSystem
ΞPROCESSES
known procs = ∅
Proposition 17. AddProcess ⇒ pid ∈ known procs

.
Proof. For AddProcess, consider the case pstacks

= pstacks ∪{p? → stk}.
Since dom pstacks = known
procs and dom pstacks

= known procs

, it fol-
lows that: dom pstacks = known
procs and:
dom pstacs = dom(pstacks ∪{p? → stk})
= (dom pstacks) ∪ (dom{p? → stk})
= dom pstacks ∪{p?}
= known
procs

✷
Proposition 18.

=(PREF \{NullProcRef , IdleProcRef }) \ known procs

=(PREF \{NullProcRef , IdleProcRef }) \ (known procs ∪{p})
where p is the newly allocated identifier.
Consequently, for (NextPREF [p
m
] ∧ AddProcess[p
m
/pid?, ])
m
and for some
m, 0 < m < maxprocs − 1
A

=(PREF \{NullProcRef , IdleProcRef }) \ known procs

=(PREF \{NullProcRef , IdleProcRef }) \ (known
procs ∪{p
1
, ,p
m−1
})
Therefore, for m = maxprocs,
A

=(PREF \{NullProcRef , IdleProcRef }) \ known procs

=(PREF \{NullProcRef , IdleProcRef }) \ known
procs ∪{p
1

be allocated to the processor. They are also required for the specification of
semaphores.
There are two main operations involved in context switching: one to copy
state data from the process descriptor to the hardware and one to copy data
in the opposite direction. The schemata defined in this section are included as
an illustration. They will be redefined with slight variations when required.
The SaveAllHWRegisters operation copies the contents of the registers
used by a process into its process descriptor. The operation is complemented
by RestoreAllHWRegisters, which reads the process descriptor and copies
items from it to the hardware’s general-purpose registers. In the represen-
tation below, the instruction pointer is the last register to be set from the
process descriptor.
SaveAllHWRegisters
∆PROCESSES
HWREGISTERS
pid?:PREF
(∀ r : GENREG •
pregs

(pid?)(r)=hwregset(r))
pstacks

(pid?) = hwstack
pstatwds

(pid?) = hwstatwd
pips

(pid?) = hwip
SwitchContextOut = SaveAllHWRegisters

pid?:PREF
(∀ r : GENREG •
pregs

(pid?)(r)=hwregset(r))
SavePartialContext 
= SaveHWGeneralRegisters
RestoreHWGeneralRegisters
∆PROCESSES
ΞHWREGISTERS
pid?:PREF
∀ r : GENREG •
hwregset(r)=pregs

(pid?)(r)
RestorePartialContext 
= RestoreHWGeneralRegisters
2.7 Current Process and Ready Queue
This section presents a simple model of the operation of the kernel’s scheduler.
It uses a simple FIFO queue to hold the processes that are ready to execute;
this is readyq. The identifier of the process currently executing is stored in
currentp.
CURRENTPROCESS
currentp : PREF
readyq : ProcQueue
Here, ProcQueue can either be regarded as an instantiation of the generic
QUEUE type or of a new type.