Formal Verification And Implementation Of Shared Memory IPC Mechanism

With the development of the computer’s operating system, operating systems are going to be more and more diverse, thus a lot of operating system with different structure from the traditional monolithic kernel has appeared. One of them is microkernel operating system, because of its advantages on the system security and flexibility, it gained more and more attention. The first generation of microkernel operating system was not successful. This is due to its design miscarriage. L4as the representative of the second generation microkernel operating system has conducted a re-design and greatly improved the shortcomings of the first-generation microkernel operating system. It has been widespread concerned by academia and industry.L4/Fiasco is a further development to L4by the Dresden University of Technology to provide hard real-time support. It is one of the representatives of the second-generation microkernel operating system. The IPC mechanism now using in L4/Fiasco is provided by the kernel, thus each time IPC communication requires the participation of the kernel, so IPC can easily become the performance bottleneck of L4/Fiasco.In this paper we describes the theory and technology of the microkernel operating system, focusing on the structure L4/Fiasco microkernel operating system, and analyzed its existing IPC mechanisms and its inadequate, propose a new shared memory based IPC mechanism-L4STM. L4STM provides5interface functions for threads which use IPC, and hide the details of the service threads and concurrent algorithms. L4STM used a server thread to allocation and management of shared memory region, and it also used Software Transactional Memory mechanism, then these innovations make L4STM to be an efficient IPC mechanism that achieve a low dependence on the kernel and can support data transmission between three or more processes.We introduces the concepts, principles and application of formal methods, focuses on the formal check SPIN, which is a formal verification tool for concurrent algorithms, protocols and distributed systems. And introduced SPIN into the design process of L4STM. Modeled and verified the design of parallel algorithms in L4STM, to ensure its correctness. Finally, implement L4STM code conducted a testing of it.