Search

In this paper, we describe DiOS , a lightweight model operating system, which can be used to execute programs that make use of POSIX APIs. Such executions are fully reproducible: running the same program with the same inputs twice will result in two exactly identical instruction traces, even if the program uses threads for parallelism. DiOS is implemented almost entirely in portable C and C++: although its primary platform is DiVM , a verification-oriented virtual machine, it can be configured to also run in KLEE, a symbolic executor. Finally, it can be compiled into machine code to serve as a user-mode kernel. Additionally, DiOS is modular and extensible. Its various components can be combined to match both the capabilities of the underlying platform and to provide services required by a particular program. Components can be added to cover additional system calls or APIs or removed to reduce overhead. The experimental evaluation has three parts. DiOS is first evaluated as a component of a program verification platform based on DiVM. In the second part, we consider its portability and modularity by combining it with the symbolic executor KLEE. Finally, we consider its use as a standalone user-mode kernel. [ABSTRACT FROM AUTHOR]

Our process scheduling algorithm was created with the help of circular linked list and skip ring data structures and algorithms. Skip ring data structure consists of circular link lists formed in layers which are linked in a canonical way. Time complexity of search, insertion and deletion equals to O (lgN) in an N-element skip ring data structure. Therefore, skip ring data structure is employed more effectively (O(lgN)) in circumstances where circular linked lists (O(N)) are used. In this paper, the applications of data structures such as red-black tree, binary search tree and skip ring were performed and the obtained results were compared. The obtained results demonstrated that skip ring data structure is superior to red-black tree and binary search tree. Process scheduling is the most important part of operating systems. Linux operating system (version 6.23) uses Completely Fair Scheduler for process scheduling by using red-black tree data structures, Whereas skip ring data structure can be used effectively instead of red-black tree data structure. A new algorithm for process scheduling which was called as Fair Priority Scheduling was proposed in this paper. [ABSTRACT FROM AUTHOR]

The paper presents a real-time operating system (RTOS) that provides a distributed shared memory (DSM) service for distributed embedded control systems. Model-based design is widely adopted in embedded control software design and the source code of software modules can be generated from a controller model. The generated software modules exchange their input and output values through shared variables. We develop a RTOS with a DSM service to provide a location-transparent environment, in which distributed software modules can exchange input and output values through the DSM. The RTOS is an extension to OSEK OS. We use a real-time network called FlexRay, which is based on a time division multiple access (TDMA) protocol. The consistency of the DSM is maintained according to the order of data transfer through FlexRay, not using inter-node synchronization. The worst case response time of the DSM is predictable if the FlexRay communication is well configured. [ABSTRACT FROM AUTHOR]

Automated verification of operating system kernels is a challenging problem, partly due to the use of shared mutable data structures. In this paper, we show how we can automatically verify memory safety and functional correctness properties of the task scheduler component of the FreeRTOS kernel using the verification system Hip/Sleek. We show how some of Hip/Sleek features such as user-defined predicates and lemmas make the specifications highly expressive and the verification process viable. To the best of our knowledge, this is the first code-level verification of memory safety and functional correctness properties of the FreeRTOS scheduler. The outcome of our experiment confirms that Hip/Sleek can indeed be used to verify code that is used in production. Moreover, since the properties that we verify are quite general, we envisage that the same approach can be adopted to verify components of other operating systems. [ABSTRACT FROM AUTHOR]