Formal Models of Operating System Kernels phần 2

Tham khảo tài liệu formal models of operating system kernels phần 2, công nghệ thông tin, hệ điều hành phục vụ nhu cầu học tập, nghiên cứu và làm việc hiệu quả
Nội dung trích xuất từ tài liệu:
Formal Models of Operating System Kernels phần 228 2 Standard and Generic Components The hardware process is defined as:HW = start .HW1HW1 = (i1 .saveregs + HW1 +setregs .HW1 +getregs .HW1 +restoreregs .HW1 ) saveregs The following pair of processes are intended to model the behaviour ofhardware when an interrupt occurs. The process Inti represents the i th in-terrupt. When it receives its internal interrupt signal, ii , it signals that theInterrupt Service Routine (ISR) corresponding to this interrupt should be ex-ecuted; this is done by sending the runisr i message. The interrupt processthen recurs, ready to accept another interrupt signal. The second process,ISRi , is intended roughly to model the actions of the ISR corresponding tointerrupt i . When the ISR receives the signal to execute (runisri ), it performsthe service action and then instructs the hardware to restore the register setto the way it was before the interrupt occurred. The ISR process then recurs,so that it can accept another interrupt.Inti = i 1 .runisr 1 .IntiISRi = runisr .service .restoreregs .ISRi The hardware and interrupt subsystem can be thought of as the following(parallel) composition of processes:H = HW | Πi ∈I (Inti | ISRi ) The next process models the interrupt mask. The interrupt mask deter-mines whether interrupts are signalled or not (it is modelled in this book bythe 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 ofthe interrupt mask and the process P is left as an exercise for the interestedreader. The model works as follows. Initially, the IntMask accepts an on event toinitialise the mask. Initialisation enables interrupts and takes the state of themask as its parameter (the value in parentheses). After this, the mask offersthree possible actions: off to disable interrupts, on to enable them and stat toenquire about the state of the mask. When IntMask engages in an off action, itdisables interrupts (denoted by the 0 parameter). Alternatively, it can engagein an on action. If interrupts are currently disabled, the on action re-enables 2.4 Hardware Model 29them; otherwise, it does nothing. Finally, some other component (say, somesoftware) can enquire as to the state of the interrupt mask by engaging inthe third possible action, stat (status). The IntMask process then returns thecurrent status (denoted by n ) via an istat (i nterrupt stat us) action; enquirydoes not affect the state of the mask. This is indicated by the recursion onthe same value as that communicated by the istat action. This is a single-level interrupt scheme. Some processors have a multi-levelone. 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 schemeis assumed for simplicity. Purely for interest, a multi-level interrupt mask, MLIMask , can be definedas follows. First, the mask is initialised by participating in an allon (all on)action:MLIMask = allon .MLIMask (S )Here, the parameter S denotes the set of all interrupt levels. The mask nowbehaves as follows:MLIMask (S ) = off (i ).MLIMask (S {i }) +on (i ).MLIMask (S ∪ {i }) +ison (i ).istat (i ∈ S ).MLIMask (S ) +offm (I ).MLIMask (S I ) +onm (I ).MLIMask (S ∪ I )where I denotes a set of interrupt levels and i is an individual level.2.4.2 RegistersThe processor contains a set of general-purpose registersas well as a set ofmore specialised ones: stack register, instruction pointer and status register(sometimes called the “status word”). It is assumed that each register is onePSU wide. The model of the registers is rather minimal. There is not a lot that canbe proved about it. It is assumed that the hardware is not a stack machine (i.e., a single-address machine, that is). If a stack machine were the target, the registerswould not strictly be required. Actually, many stack machines do have theodd off-stack register just as an optimisation. The number of general-purpose registers is given by: numregs : N1Note that no value is given. This is a partial specification (it is, in any case,impossible to assign a value to numregs without knowing which processor isbeing used). The register names form the following set:30 2 Standard and Generic ComponentsGENREG == {r0 , . . . , rnumregs−1 }The contents of this set are of no further interest to us because the registerset will be manipulated as a complete entity. The register set is defined as a ...