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

Tham khảo tài liệu 'formal models of operating system kernels phần 10', 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ả | Using Virtual Storage 301 system from user space is achieved by a mode switch . The mode switch activates additional instructions for example those manipulating interrupts and the translation lookaside buffer. How the mode switch is performed is outside the scope of this book for reasons already given. Mode switches are though very common on hardware that supports virtual store. In some systems there are parts of the kernel space that are shared between all processes in the system. These pages are pre-allocated and added to the process image when it is created. Because they are pre-allocated the allocation of user pages in that process must be allocated at some page whose logical page number is greater than zero. The constant pgallocstart denotes this offset. Usually the offset is used in the data segment only. For simplicity the offset is here set to 0. Moreover it is uniformly applied to all segments since it is 0 this does not hurt . The one hard constraint on virtual store is that some physical pages must never be allocated to user space. These are the pages that hold the device registers and other special addresses just mentioned. Virtual-store pages are frequently marked as execute only which implies read-only read-only read-write. Sometimes pages are marked write-only. This is unusual for user pages but could be common if device buffers are mapped to virtual store pages. The operations required to mark pages alter the attributes defined at the start of this chapter. The operations are relatively simple to define and are also intuitively clear. They are operations belonging to the class defined below in Section in the meanwhile they are presented without comment. MarkPageAsReadOnly MakePageReadable A IsPageWritable A MakePageNotWritable V IsPageExecutable A MakePageNotExecutable MarkPageAsReadWrite Ma kePa geRea d able 0 MakePageWritable A IsPageExecutable A MakePageNotExecutable MarkPageAsCode MakePageExecutable 0 MakePageReadable A .