tailieunhanh - Formal Models of Operating System Kernels phần 6

Tham khảo tài liệu 'formal models of operating system kernels phần 6', 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ả | 68 3 A Simple Kernel by elements of IPREF and whose elements are objects of type ProcessDescr. The class also has state variable known_procs to record the elements in the domain of procs it is a record of the identifiers of those processes currently in the system. The variable freeids is a set of actual process identifiers that represent those process references not currently referring to processes in the system. The idea is that the identifier of a process is its index in the process table. The kernel only allocates actual processes that is processes other than the null and idle processes. For this reason freeids is a set of type APREF. The procs mapping table is of type IPREF the reason for this being that the idle process is represented by a process descriptor that is allocated in the process table when the kernel is initialised. Apart from its initialisation operation again INIT the process table exports operations to create the idle process CreateIdleProcess and to add and delete process descriptors AddProcess and DelProcess respectively as well as an operation to return the descriptor of a process DescrOfProcess . The operation to create the idle process could be defined in a higher layer of the model. Since the idle process owns no resources and executes a piece of code that will be supplied with the kernel and whose address can therefore be made available at kernel initialisation time it seems reasonable to make idle process creation a process table operation. __ProcessTable I INIT CreateldleProcess AddProcess DelProcess DescrOfProcess procs IPREF ProcessDescr known_procs FIPREF freeids F APREF INIT known_procs IdleProcRef freeids 1 . maxprocs 1 3 ipd ProcessDescr createIdleProcess __CreateIdleProcess__ 3pr PRIO stat PROCSTATUS stwd STATUSWD emptymem MEMDESC stkdesc MEMDESC memsz N ipd ProcessDescr stat pstready A prio pr A stwd 0S A .