Operating Systems

HelenOS and GSoC

Projects

Publications

Research Goals

Our goals in the area of operating systems research are formal reasoning about correctness and safety properties of both embedded and general-purpose operating systems. To achieve this we make use of methods of formal description of operating system architecture and behavior, implementing parts of the operating system as fine-grained software components and also building on the state-of-the-art software engineering principles.

HelenOS and Google Summer of Code

GSoC 2012 logo
GSoC 2011 logo

Our department has been selected as Google Summer of Code mentoring organization for HelenOS in the year 2011 and again in the year 2012. We consider this as a great honour and a recognition of outstanding qualities and potential of the HelenOS project by Google.

HelenOS is a state-of-the-art operating system based on microkernel multiserver design principles. HelenOS decomposes key operating system functionality (including device drivers and file systems) into many isolated but intensively communicating server processes that reside entirely in user space. HelenOS thus provides a computing environment that has several virtues, such as flexibility, increased robustness, well-defined explicit interfaces between isolated software components and reduced complexity as compared to other operating system architectures.

HelenOS does not aim to be another clone of Unix or some other legacy operating system and is not POSIX-compliant (even though it may seem POSIX-similar at times). Instead, we try to design it according to our taste and sense for what is the most elegant and right thing to do. What makes HelenOS unique among the other multiserver operating systems is its multiplatform and multiprocessor microkernel and understandable source code. HelenOS runs on 7 different processor architectures, ranging from a 32-bit uniprocessor little-endian ARMv4 and a commodity PC with x86 and x86-64 processors to a 64-bit multicore big-endian UltraSPARC T1.

The people around HelenOS do not forget the student roots of the project and appreciate the continuous cooperation with students. HelenOS has been a subject of 13 successfully defended bachelor and master theses (spreading two universities), 3 student team projects and 3 GSoC 2011 projects. 7 more master theses and 1 bachelor thesis based on HelenOS are currently in progress. The learning curve of HelenOS is gradual as we put a lot of stress on source code readability and clean structure.

Consider reading about our GSoC 2011 experience on the Google Open Source blog and have a look at our ideas list from GSoC 2011 and GSoC 2012.

Projects

  • HelenOS – Research development operating system based on microkernel multiserver paradigm, built from fine-grained software components and with partial formal description of architecture and behavior
  • MSIM – Light-weight MIPS R4000 computer simulator
  • LFS – Log-structured file system for Linux
  • zlomekFS – Networked file system
  • vmtune – Tuning Virtual Memory for Performance
  • OBJIX – A class hierarchy framework-based operating system
  • RCU – Research related to the Read-Copy-Update synchronization scheme

Publications

2012 (1)

Refereed (journals/proceedings)

PDF, Link Podzimek A., Děcký M., Bulej L., Tůma P.: A Non-Intrusive Read-Copy-Update for UTS,
Published in the Proceedings of the 18th IEEE International Conference on Parallel and Distributed Systems (ICPADS 2012), IEEE Computer Society, ISBN 978-1-4673-4565-1, December 2012

2010 (1)

Refereed (journals/proceedings)

PDF Děcký M.: A Road to a Formally Verified General-Purpose Operating System,
In the Proceedings of the 1st International Symposium on Architecting Critical Systems (federate event of CompArch 2010), pp. 72 - 88, LNCS 6150, Springer-Verlag, ISBN 978-3-642-13555-2, June 2010

2009 (1)

Refereed (journals/proceedings)

PDF Hocko M., Kalibera T.: Reducing Performance Non-determinism via Cache-aware Page Allocation Strategies,
Accepted at First Joint WOSP/SIPEW International Conference on Performance Engineering, September 2009

2008 (1)

Refereed (journals/proceedings)

Link Babka V., Bulej L., Děcký M., Holub V., Tůma P.: Teaching Operating Systems: Student Assignments and the Software Engineering Perspective,
In the Proceedings of the 2008 International Workshop on Software Engineering in East and South Europe (SEESE), Leipzig, Germany, Copyright (C) ACM, New York, NY, USA, ISBN 978-1-60558-076-0, pp. 71-77, May 2008

2007 (3)

Refereed (journals/proceedings)

PDF, PostScript Jambor M., Hrubý T., Tauš J., Krchák K., Holub V.: Implementation of a Linux Log-Structured File System with a Garbage Collector,
in Operating Systems Review special issue 41(1), ACM Press, ISSN 0163-5980, January 2007

Master Theses

PDF Hocko M.: Tuning Virtual Memory for Performance,
Master Thesis, advisor: Tomas Kalibera, July 2007

Nonrefereed

PDF Děcký M.: Component-based General-purpose Operating System,
In the Proceedings of WDS'07, Edited by J. Safrankova, June 2007

1995 (1)

Refereed (journals/proceedings)

Smolík T.: An Object-Oriented File System - an Example of Using the Class Hierarchy Framework Concept,
ACM SIGOPS Operating Systems Review,, April 1995

1994 (1)

Refereed (journals/proceedings)

Plášil F., Grof M.: Using both Virtual 8086 and Protected Modes to Implement Objix Mikrokernel,
In Journal of Microcomputer Applications 17, pg. 381-396., 1994

1993 (2)

Refereed (journals/proceedings)

Plášil F.: Employing Multiple Inheritance in the Objix Microkernel,
In Proceedings of Third IWOOOS '93, IEEE CS Press, Asheville, North Carolina, December 1993
Fanta R.: From Processes to Threads,
In Proceedings of Third IWOOOS '93, IEEE CS Press, Asheville, North Carolina, December 1993
Modified on 2012-03-29