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

Tham khảo tài liệu 'formal models of operating system kernels phần 4', 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ả | Storage Management 153 I codeToPSUs PCODE MEM The next operation creates the sequence of bytes that will actually be copied to disk on a swap. It uses codeToPSUs as well as two A expressions that operate more as one would find in a complete model. When this schema is used that use will be a little incorrect because the extraction of start and size from data and stack segments is ignored. __CreateProcessImage__ code PCODE stkstrt datastrt ADDRESS stksz datasz N1 image MEM image codeToPSUs code A i datastrt . datasz 0 A i stkstrt . stksz 0 It is now possible to prove a few propositions about the main store and its operations. Proposition 71. RSCanAllocateStore is false iff there are no holes of positive size. Proof. By the predicate hole_size h 0 for some hole h in ran holes. Proposition 72. Each use of RSAllocateFromHole monotonically decreases available free storage. Proof. Assume there have already been allocations. Then by the invariant tiff holes hole_size holes i I yj usermem hole_size usermem j mem There are two cases. Case 1. rqsz hole size. Then the number of holes decreases by one. The sum decreases by the corresponding amount. Case 2. rqsz hole size. The hole is split into two blocks one of size rqsz and the other of size memsize h rqsz . The size of this new hole is necessarily less than memsize h . Therefore the available storage decreases. The following two propositions establish the fact that free store decreases by the action of RSAllocateFromHole when it is applicable and the action of RSFreeMainstore increases the amount of free store. Proposition 73. The action of RSAllocateFromHole k rqsz decreases the available free store by k units. 154 4 A Swapping Kernel Proof. Again without loss of generality assume there have already been allocations. Then by the invariant ho0es holesize holes i I yj usermem hole_size usermem j mem If k units are allocated from free store it follows that mem is .