FAU UnivIS
Techn. Fak. Dep. Informatik
Dept. of CS > CS 4 > Research > CADOS
People, Research, Pubs
Lehre, Examensarbeiten

CADOS: Configurability Aware Development of Operating Systems

Todays operating systems (as well as other system software) offer a great deal of static configurability to tailor them with respect to a specific application or hardware platform. Linux 4.2, for instance, provides (via its Kconfig models and tools) more than fifteen thousand configurable features for this purpose. Technically, the implementation of all these features is spread over multiple levels of the software generation process, including the configuration system, build system, C preprocessor, compiler, linker, and more. This enormous variability has become unmanageable in practice; in the case of Linux it already has led to thousands of variability defects within the lifetime of Linux. With this term, we denote bugs and other quality issues related to the implementation of variable features. Variability defects manifest as configuration consistency and configuration coverage issues.

In the CADOS project, we investigate scalable methods and tools to grasp the variability on every layer within the configuration and implementation space, visualize and analyze it and, if possible, adjust it while maintaining a holistic view on variability.

Our findings have already led to more than 100 accepted patches in the Linux mainline kernel (see our EuroSys '11 and SPLC '12 papers) and an approach for the automatic tailoring of Linux server systems in order to reduce the exploitable code base (see our HotDep '12 paper). The issue of configuration coverage is addressed in our USENIX '14 paper.

CADOS is the follow-up project to VAMOS.

CADOS in the Wild

Our research students attended the LPC'14 and gave talks at the Development Tools Microconference.

Valentin Rothberg talked about his new tool undertaker-checkpatch, which analyzes patch files. The vampyr tool to configurability-aware compile test (or determine the variability of) source files was presented by Stefan Hengelein.Abstracts and slides for both talks can be found at the talk-specific sites.

The Linux Weekly News site summarizes the highlights of the Development Tools Microconference and features both CADOS talks.

Selected Publications

Please look here for the complete list of CADOS publications.

USENIX '14

Tartler, Reinhard ; Dietrich, Christian ; Sincero, Julio ; Schröder-Preikschat, Wolfgang ; Lohmann, Daniel: Static Analysis of Variability in System Software: The 90,000 #ifdefs Issue. In: USENIX Association (Ed.) : Proceedings of the 2014 USENIX Annual Technical Conference (USENIX 2014) (2014 USENIX ATC Philadelphia, PA, USA June 19-20, 2014). 2014, pp 421-432. - ISBN 978-1-931971-10-2 (BibTeX)

GPCE '14

Ziegler, Andreas ; Heinloth, Bernhard ; Lohmann, Daniel: Automatic Feature Selection in Large-Scale System-Software Product Lines. In: Flatt, Matthew (Ed.) : Proceedings of the 2014 International Conference on Generative Programming: Concepts and Experiences (13th International Conference on Generative Programming: Concepts & Experiences (GPCE '14) Västerås, Sweden Sep. 2014). New York, NY, USA : ACM Press, 2014, pp 39-48. - ISBN 978-1-4503-3161-6
[doi>10.1145/2658761.2658767] (BibTeX)

CADOS is the follow-up project to VAMOS. The following publications are forming the foundation for our CADOS research. The dissertation of Dr.-Ing. Reinhard Tartler provides a good overview over the VAMOS project.
Please look here for the complete list of VAMOS publications.

EuroSys '11

Tartler, Reinhard ; Lohmann, Daniel ; Sincero, Julio ; Schröder-Preikschat, Wolfgang: Feature Consistency in Compile-Time Configurable System Software. In: Heiser, Gernoth ; Kirsch, Christoph (Ed.) : Proceedings of the EuroSys 2011 Conference (EuroSys '11) (EuroSys 2011 Salzburg 10-13 April 2011). New York, NY, USA : ACM, 2011, pp 47-60. - ISBN 978-1-4503-0634-8
[doi>10.1145/1966445.1966451] (BibTeX)

HotDep '12

Tartler, Reinhard ; Kurmus, Anil ; Ziegler, Andreas ; Heinloth, Bernhard ; Rothberg, Valentin ; Dorneanu, Daniela ; Kapitza, Rüdiger ; Schröder-Preikschat, Wolfgang ; Lohmann, Daniel: Automatic OS Kernel TCB Reduction by Leveraging Compile-Time Configurability. In: USENIX (Ed.) : Proceedings of the 8th Workshop on Hot Topics in System Dependability (HotDep '12) (Eigth Workshop on Hot Topics in System Dependability Hollywood, CA, USA 7.10.2012). 2012, pp -. (BibTeX)

SPLC '12

Dietrich, Christian ; Tartler, Reinhard ; Schröder-Preikschat, Wolfgang ; Lohmann, Daniel: A Robust Approach for Variability Extraction from the Linux Build System. In: ACM Press (Ed.) : Proceedings of the 16th International Software Product Line Conference (16th International Software Product Line Conference Salvador - Brazil September 02 - 07, 2012). Vol. 1. New York : ACM Press, 2012, pp 21-30. - ISBN 978-1-4503-1094-9
[doi>10.1145/2362536.2362544] (BibTeX)

Dissertation, 2013

Tartler, Reinhard: Mastering Variability Challenges in Linux and Related Highly-Configurable System Software. Erlangen, Friedrich-Alexander-Universität Erlangen-Nürnberg, Ph.D. thesis, 2013. - 178 pages. (BibTeX)

People Involved in CADOS

Project Lead and Applicant

CADOS is supported by the DFG (LO 1719/3-1, 2014–).
Dr.-Ing. Daniel Lohmann

(Project Lead / Applicant)

Researchers

Tools

Various tools assist our analysis of the variability in the Linux kernel and other software projects. Our most important tool is called the undertaker, which searches and reports dead and undead conditional CPP blocks. Since its inception within VAMOS, it has matured to a toolbox of utilities for answering various research questions related to variability in general. For further details, please look into the undertaker trac.

vampyr

This tool is a wrapper for undertaker to do coverage analysis or variability-aware static analysis on source files. For the static analysis compilers such as gcc or clang are employed. Please refer to the USENIX '14 paper for detailed information.

undertaker-checkpatch

This tool reports changes to defects such as newly introduced or fixed defects. Defects can also be correlated to changes in Kconfig and the build system (Make, Kbuild) and vice versa. Additionally, undertaker-checkpatch ships the functionality to further analyze the causes of defects, displaying contradictory Kconfig items, a block's precondition or the defect causing formula. Since version 1.6, undertaker is able to minimize defect formulas (thanks to the PicoMUS-Tool which is part of PicoSAT). This functionality can be used in undertaker-checkpatch to further analyze and understand the cause of defects.

Flipper: Lightweight Kernel Tailoring

Configuring Linux is hard. With over 14,000 options to choose from, making an informed decision about every single one of them takes a very long time. While distributions for standard day-to-day use simply enable as many features (drivers, supported platforms, ...) as possible, this is not a practical solution for embedded systems, where memory is scarce and must not be wasted.
To make it easier for an engineer to derive a small starting point to configure the system, we developed Flipper. Flipper provides a lean method to trace which functionality was exerted in the kernel. Using the Tailor tool from the undertaker package, a small, use-case specific configuration for Linux can be generated from the collected data.
Flipper is part of undertaker release (v1.6) and can be downloaded here, for detailed usage instructions please read the README file provided in the tailor/flipper subdirectory.

Wundertaker

Wundertaker is a Web GUI visualizing #ifdefs and undertaker's defect reports in Linux code files. The source including installation instructions can be downloaded here. A detailed description of the tool and its implementation can also be found in the Bachelor's thesis of Patrick Plagwitz.

Theses

Please look here for the complete list of CADOS-related theses, including finished works.

Open Topics

Ongoing Theses