-System software product lines such as the embedded real-time operating system eCos are a state-of-the-art solution for application scenarios with a very low hardware resource profile. Being highly configurable at compile time, eCos can be tailored to the application in terms of inclusion or exclusion of fine-grained operating system features. The mandatory manual feature selection is carried out by the developer who knows the functionality essential for the application. This process requires profound knowledge of the feature semantics, is very time-consuming, and, in particular, error-prone - most probably resulting in a resource suboptimal or even dysfunctional operating system variant. The contribution of this article is an approach to automate the eCos configuration process to a major degree, therefore reducing the outlined disadvantages significantly. A thorough examination of configurable eCos features exhibits four feature categories of varying complexity: By applying standard model checking techniques and static analysis of the application source code, we show that for at least two feature categories the configuration decisions can be taken automatically. Complementing the approach with configlets - highly eCos specific analysis code - a third category is shown to be also coverable. Index Terms-eCos, Automatic Configuration, Static Analysis, Model Checking, CTL, Software Product Lines
I. INTRODUCTION
There exist various reasons for specializing software systems
for a specific application scenario or a particular customer. In
the embedded systems domain, the primary motivation is to
minimize resource consumption: Resources such as energy,
memory or CPU cycles are scarce, and keeping the software
stack’s resource profile low directly impacts the system’s
hardware costs and therefore its competitiveness on the market.
Tailorable system software has been a focus of our research
group for several years, in particular embedded operating
systems (OS) [
This article describes a case study conducted with the
opensource, real-time embedded OS eCos1, a highly configurable
software platform, which can be tailored for the specific needs
of the application. eCos is very widespread, because of it
being freely available and its comfortable configuration process:
Guided by a GUI configuration tool, the application developer
decides from a so-called feature model [
Our contribution to the automated configuration and tailoring community is an approach to at least partially automate the process by applying standard static analysis and model checking techniques to application source code. We conducted a detailed examination of parts of the eCos 3.0 OS documentation and API in order to determine which conditions hold within an application model if it needs or does not need certain OS features. These conditions, still formulated in plain English, pose a set of requirements for static analysis and model checking. First experiments with our analysis tool prototype seem promising, but also raise new research questions.
The remainder of this paper is structured as follows: Section II gives a more detailed overview of the motivating context and our approach. Section III describes our manual examination of eCos features and examples for the resulting feature categories. Section IV outlines the steps necessary for automatic feature need derivation: application analysis, model checking, and result interpretation. Section V revisits the results from the manual feature examination, and summarizes the current state of our analysis tool prototype and preliminary results with eCos test programs. We conclude with a discussion of related work, a summary and an outlook on future work in sections VI and VII.
Infrastructure software, unlike application software, is in a unidirectional usage relationship with other software layers, and typically depicted in a hierarchy level above the infrastructure. Database software, middleware or standard C libraries, or operating systems such as eCos are typical representatives.
The categorization of eCos as a software product line (SPL)
is a bit more debatable: The SPL community defines these
not only by technical aspects like configurability and code
2eCos release 3.0; platform specific HAL and device driver features not
counted in
reuse among product line variants, but also by the engineering
process that accompanies the development [
Variability Management: Similar to the Linux
kernel [
Product Generation: The GUI tool is also capable of automatically generating the actual eCos variant from the configuration (cf. Figure 3). This process generates a new source code tree: The chosen values for the configuration
options are written as C preprocessor macro definitions in generated header files, which in turn have effects on the OS C/C++ code that is finally compiled and linked to the application.
In this so-called feature-driven product line derivation
process [
In earlier work [24] we showed that infrastructure API usage
patterns within an application allow to deduce feature need
or non-need. Ranging from the simple existence of certain
API calls to complex API call patterns and involvement
of actual parameter values, different levels of complexity
have been observed for real-world infrastructure features. In
this case study, we take a closer look at the eCos API and
its characteristics related to application analysis and feature
relevant API usage patterns. Motivated by our earlier results,
we evaluate the temporal logic CTL (computation tree logic [
For our approach, the first step towards automatic configuration comprises establishing a relationship between infrastructure features on the one hand, and properties of the application on the other hand. We conducted a thorough manual examination of the configurable features in the eCos kernel components “Kernel schedulers”, “Thread-related options” and “Synchronization primitives” in order to gain experience with real-world OS features and to study the implications for application analysis.
This manual infrastructure feature examination must not be confused with the automated analysis steps described later in this article:
This examination must be carried out only once, whereas its results can be reused in all infrastructure deployments. Therefore, an infrastructure expert (e.g., a member of its development team, outfitted with in-depth knowledge of the API semantics) can (and should) be the person conducting this analysis.
In contrast, the automated analysis steps take place later at the application developer’s site.
The aim of the manual examination of the eCos 3.0 source code and documentation was to ascertain what exact effect each configurable feature has on actual OS functionality, and especially the OS API. We show that an application, containing calls to this API, fulfills certain conditions that indicate its need for OS features. The results, including these feature conditions, were diverse and are presented in the following in terms of four feature categories, each accompanied by examples.
1) Simple API call usage: One very common case of API usage observed is the simple existence of certain API calls.
(located in the “Synchronization primitives” component) defines a preprocessor macro, which in turn adds the functions cyg_mbox_put(...) and cyg_mbox_timed_put(...) to the kernel API. Knowing this direct relationship from feature selection to the API, and being able to assure these API calls are not additionally related to other features, one can pose a simple, definitive condition on the application code: c l a s s C y g _ T h r e a d { / * . . . * / # i f d e f CYGVAR_KERNEL_THREADS_NAME p r i v a t e : / / An o p t i o n a l t h r e a d name s t r i n g , / / f o r humans t o r e a d c h a r * name ; p u b l i c : / / f u n c t i o n t o g e t t h e name s t r i n g c h a r * g e t _ n a m e ( ) ; # e n d i f / * . . . * /
Iff there exist (reachable) calls to cyg_mbox_put(...) or cyg_mbox_timed_put(...), then the feature “Message box blocking put support” is needed.
can be illustrated by the example of the feature “Support optional name for each thread”, located in the “Thread-related options” component. This option enables applications to assign a name (a C character string) to each thread, and to read that name from an arbitrary, given thread.
Once this option is enabled, the kernel’s internal thread abstraction data structure (a C++ class named Cyg_Thread) is extended by a name element (again by means of preprocessor macros, cf. Figure 4), thus saving memory (and OS code, in other parts of eCos) if this functionality is not needed.
Nevertheless, the kernel’s C API is not affected at all: Regardless of how the application developer configures eCos, the API function cyg_thread_create(...) always takes a name parameter (which is ignored if the kernel cannot store thread names), and the API function cyg_thread_get_info(...) always fills a data structure (struct cyg_thread_info) which has a name element. An application developer who does not want to give a thread a name simply passes NULL instead of a character string. If the kernel does not know a thread’s name, or is not capable of storing thread names, cyg_thread_get_info(...) returns NULL in the name element of cyg_thread_info.
This API definition allows to concentrate on an application’s usage of cyg_thread_create(...) and cyg_thread_get_info(...) for automatic configuration of this feature:
value to cyg_thread_create(...)’s name parameter, and calls cyg_thread_get_info(...) and reads the name element of its return value, the feature “Support optional name for each thread” is needed.
This condition is not completely conclusive, though: An application developer may create threads with names just for self-documenting purposes without needing the kernel to store this information. An application may even read the name element and expect it to be NULL. Nevertheless there is a strong indication that the feature is needed, so the configuration tool could give the application developer a hint to enable it.
inherent complexity, and are, due to their interrelation with concurrency and synchronization aspects, highly OS specific.
protocols” in the “Synchronization primitives” component: It
controls whether synchronization primitives should be protected
against priority inversion [
As this feature comes with quite some cost (program memory, CPU cycles at runtime), it should only be enabled if priority inversion is a problem in the application at all:
priority inversion can occur, the feature “Priority inversion protection protocols” is needed.
Unfortunately, detecting this property in an application is not trivial and can only be approached with an approximation:
levels share a common mutex, and a thread with a priority level between these two exists, the feature “Priority inversion protection protocols” is needed. There are several reasons why an application developer still may not need this feature: The application may be designed in a way that priority inversion is prevented by other means, or the occurrence of this effect may even be intended. So, again, the configuration tool should only give a hint.
4) Not derivable: For the remaining features we were unable to pose feature conditions, for different reasons. A detailed analysis of this category follows in section V.
The eCos features we examined and the resulting feature conditions imply several requirements on the application analysis:
Feature conditions that relate only to the existence of certain API calls, the least complex category identified in the previous subsection, could more or less be checked by simple text search utilities like grep. The capabilities missing (and essential for well-founded automatic configuration decisions) are a deeper understanding of C syntax and semantics – for example to differentiate between an API function mentioned in a source code comment, and real API usage – and control flow properties that indicate whether the API calls are reachable at all.
Patterns as observed in the “Support optional name for each thread” example also demand for control flow information (connecting a cyg_thread_get_info(...) call to a subsequent use of its return value) and actual parameter values, implying the need for static analysis techniques like constant folding, constant propagation, inter-procedural reaching definitions analysis [21], or interval analysis. Highly OS domain specific feature patterns concerning thread concurrency and synchronization aspects call for a very specialized program analysis technique which may not be possible to generalize further. Our first attempt to deal with these is described in subsection IV-D.
IV. STATIC APPLICATION ANALYSIS AND DETERMINATION
OF FEATURE NEED
The first step in statically deriving information from application source code is transforming it into a model suitable for the subsequent analysis steps – suitable in a way that the transformation does not lose information relevant for the problem space, leading to incorrect configuration decisions. Our examination of eCos features suggests that a C-statementlevel control flow graph (CFG) fulfills our requirements, as it maintains temporal interrelations between API calls and return value usage, and allows for reachability analysis. A CFG can also be subject to further data flow analysis and transformation steps that propagate actual values to nodes where they are passed through the OS API. Additionally, a CFG is generic enough that it still holds enough program information for the highly OS specific analyses sketched in subsection III-A3.
Motivated by our own earlier results [24] and promising
achievements in other projects applying model checking to
identify patterns in application code (such as [
We model the CFG of the application program as a Kripke
structure [
CTL formulas allow to specify temporal properties of Kripke
structures by extending classical predicate logic by temporal
connectives which establish a relationship to future states:
Every atomic proposition p 2 P is a CTL formula.
If p and q are CTL formulas, :p; p ^ q; p _
q; AX p; EX p; AG p; EG p; A[p U q] and E[p U q] are
valid formulas, too. X is the nexttime operator: AX p (resp.
EX p) means that p holds in every (in some) immediate
successor state. G is the global operator: AG p (resp.
EG p) states that p holds in all (in some) future states.
U is the until operator: A[p U q] (resp. E[p U q], cf.
Subfigure 5a) expresses that for every (for some) path starting
with the current state, there exists an initial prefix of this
path such that q holds at the last state of this prefix, and
p holds in all other states of the prefix [
The finally operators AF and EF can be seen as an abbreviated form of the until operators with p = true (a) E p U q (b) EF p (c) AF p (cf. Sub-figures 5b and 5c): They mean that on all (on some) paths the operand will hold sometime in the future (AF q , A[true U q]).
Figure 5 and the examples later in this subsection may help gaining a more intuitive understanding of CTL.
For the feature conditions identified in subsection III-A we additionally define an elementary set of atomic propositions: The trivial proposition [true] holds in every, [false] in no state. [call :somefunction(: : :)] holds in every state that contains a call to somefunction, ignoring its actual parameters. [call :somefunction(?; 4; ?)] holds if the second actual parameter is equal to 4.
Now we can formulate a subset of the feature conditions from section III-A in CTL. The condition informally introduced in subsection III-A1 can be expressed as follows:
EF ( [call :cyg_mbox_put(: : :)] _ [call :cyg_mbox_timed_put(: : :)] )
return value, . . . ” part of the condition, we can also express the condition from subsection III-A2:
:[call :cyg_thread_create(?; ?; ?; 0; ?; ?; ?; ?)]
In order to formulate this condition completely, we would need another atomic proposition for data structure access and a means to express the connection between the variable returned by cyg_thread_get_info(...) and the point where its member name is accessed. (See the discussion in subsection IV-D for a solution to this problem.)
A model checking algorithm can now check whether the
application’s Kripke structure is a model for a CTL formula –
iff this is the case, the feature condition is fulfilled. Starting
with the atomic propositions used in the CTL formula, and
recursively continuing with more and more complex
subformulas, each Kripke node is labeled with the sub-formulas
holding for this particular node. This procedure is iterated
until it can be determined whether the complete formula holds
in a starting node. For more details on the model checking
algorithm we refer to Clarke’s original publication [
Although not accounted for in section III-A, our examination of eCos features showed that often multiple feature conditions are necessary to exhaustively describe the possible API usage patterns that signify an application’s need or non-need for a certain feature. Some conditions only help deciding for or against feature need, not both: Once a single necessary (in the mathematical sense) condition is not fulfilled, the feature this condition belongs to is not needed; once a single sufficient condition is fulfilled, the feature is definitely needed. In both cases, the respective converse decision cannot be taken: The fulfillment of a necessary condition does not allow a statement on feature need.
Another orthogonal condition property is weakness: If a condition should only be used to give the user a configuration hint instead of making a fully automated configuration decision, it is called a weak condition (examples are the conditions in subsections III-A2 and III-A3), or else a definite condition.
The model checking results for all conditions of a certain feature can be combined to a resulting statement on whether the feature should be enabled or disabled. Figure 6 assembles the following propositions:
N n S s , , , all definite, necessary conditions are fulfilled (or none exists). all weak, necessary conditions are fulfilled (or none exists). some definite, sufficient condition is fulfilled.
some weak, sufficient condition is fulfilled.
One remaining case still needs to be dealt with: If a condition cannot be successfully checked (e.g., because data flow analysis fails, and therefore the possible value(s) of an actual parameter cannot be determined), we can safely proceed pretending this condition did not exist in the first place, as evidently the resulting statement is not falsified by that measure. The user should still be informed about the omission of a feature condition, as a simple code change may make the analysis possible again.
Finally, the internal dependency and restriction constraints in the eCos configuration tree need to be taken into account – a feature not directly needed by the application may still be mandatory because another feature depends on it. This S :S ^ :s :S ^ s
:N
application source code ill-formed N ^ n N ^ :n
needed
needed
not needed
decision possible
needed
not needed
needed
decision possible dependency resolution can already be conducted by the eCos
The quality of results obtained from model checking can only
be as good as the model being checked, which in the case of
control and data flow graphs (at least for real-world code input)
may not yield all necessary information (e.g., failing to trace
actual parameters to the place they are defined, or not being
able to determine the number of iterations a loop can make).
Static code analysis is well-known to be limited in theory and
practice [
Another related open question is what API the application
should be initially written against: As the API may be affected
by configuration decisions, a circular dependency exists. In
principle, a “full” API encompassing all possible configurations
(something Fröhlich [
The additional expressiveness demanded in subsection IV-B
– CTL’s lack of a means to connect several usage points of a
single variable – could be handled by a CTL extension: With
CTPL, Kinder et al. [
Unfortunately, neither CTL nor CTPL are expressive enough to cover complex feature conditions such as described in subsection III-A3. Our first attempt to deal with these highly OS domain specific conditions is to encapsulate them in small plug-ins, so-called configlets, written in C++ against an analysis API giving direct access to the underlying CFG (cf. Figure 7). A configlet can be used in place of a CTL formula, its output is processed the same way (cf. Figure 6). We are still unsure about what the interface between a configlet and the remaining analysis tool interface should look like, and are trying to find an adequate balance between a complex API with complete access to the Kripke model, and a minimal, easier to use API which still is generic enough to deal with new use cases.
The manual examination of 39 eCos features (cf. subsection III-A) resulted in a categorization into four feature categories, bearing various levels of complexity for automatic analysis. Table I lists all features, their type, their feature category, and the types of feature conditions we formulated. 7 out of 39 features were categorized into “Simple API call usage”.
rameters” category: Two of these need the CTL extension mentioned in subsection IV-D. 6 features are highly OS specific and belong to the “Domain specific patterns” category. We were able to formulate conditions for these features, but CTL (and CTPL) turned out to be insufficient. 19 features were categorized to be not derivable from an application’s source code, for different reasons:
The largest group (13) are configurable non-functional properties that have an effect on code size (e.g., explicit
Among these 19 features, 6 were additionally identified to be of interest only for the development process and/or debugging purposes. For example, “Output stack usage on thread exit” creates debugging output once a thread terminates – a feature the developer, despite being eager for automatic configuration, still would want to configure manually due to its purpose in the development process context.
The remaining two features even seem only to be there for self-documentation reasons, as they are tightly coupled with other features by dependency relationships and cannot be directly configured by the user anyways (e.g., “Idle thread must always yield” is automatically enabled once there is only a single priority level configured).
Altogether, we were able to pose feature conditions for about half of the examined features (18 out of 37 “real” features).
The prototype implementation of the described analysis and model checking steps is still very preliminary and has not yet been thoroughly tested with real-world code input. Nevertheless, our test runs with simple CTL formulas and a suite of eCos test programs (shipped with eCos 3.0), cloned and adapted for testing specific units of the prototype, are promising and will soon be extended to a full-scale evaluation.
The analysis tool prototype is based on clang, an LLVM [
The complete static analysis phase (scanning and parsing
the application’s C code, performing constant folding and
propagation) is externalized to clang. The resulting CFG is
then transformed to a Kripke structure. A C++ implementation
of Clarke’s CTL model checking algorithm [
code inlining), timing/throughput behavior, stack sizes, or Evaluating their JiM (Just-in-time middleware) paradigm,
runtime safety checks (e.g., stack canaries). Zhang et al. [
Focusing mostly on functional infrastructure properties, the aforementioned projects insufficiently deal with non-functional properties (such as code size, memory usage at runtime, timing behavior etc.). These properties have an emergent nature and therefore often cannot be directly configured, nevertheless some research work exists in this field. Pu, Massala et al. developed the research operating system Synthesis [22] which adapts to and self-optimizes for the application’s API usage patterns at runtime. Supplied by a just-in-time compiler, often used code paths are partially evaluated and tuned to high throughput.
Sincero, Hofer et al. [
This information could be used to automatically (based on a user-defined non-functional optimization goal) select one of several variants which are functionally equivalent but exhibit different non-functional properties, therefore complementing our approach.
Outside the context of infrastructure software tailoring, there
exist many other research projects that apply static analysis
and model checking to problems in their domain. For example,
Padioleau, Lawall et al. [
Our examination of a subset of eCos features showed that for about half of these we can, at least informally, define feature conditions which allow deducing feature need from an application’s source code. Aiming at automating the evaluation of these conditions, we identified control flow graphs, transformed to a Kripke structure, as an adequate model which carries enough information for subsequent analysis steps.
There exist numerous research projects engaging in
application-driven tailoring of infrastructure software. The
concept of Application-Oriented System Design was introduced
by Fröhlich [
Although the configuration automation of about 50% of
the examined features may not seem exceedingly successful,
extrapolating this to all configurable eCos features3 we could
still save the application developer about 750 configuration
decisions. For parts of the remaining half, especially the features
dealing with non-functional properties, the feedback approach
of Sincero et al. [
Our results are comparable to an earlier case study we conducted with a modified version of the Berkeley DB [24], an embedded DBMS for which we could automate an even larger portion of configuration decisions – mostly due to simpler API usage patterns and a lower quantity of features dealing with non-functional properties.
More future work includes examining additional eCos
features in order to gain more confidence on the general
soundness of our approach. We also intend to evaluate the
outlined extension to CTL, to compare it to other (potentially
more powerful) temporal logics, and to integrate the analysis
results in the eCos Configtool. In order to alleviate the
infrastructure developer’s task to describe feature conditions,
we are also going to look into simpler description languages that
can be automatically transformed into temporal logic formulas;
Kinder et al. [
Beyond these enhancements and a thorough evaluation of the outlined approach, we are looking into the research question what modifications to the infrastructure API are necessary to simplify the analysis task such that a vast majority of features can be automatically configured. Ideally, only a tiny fraction consisting of development time (debugging) and non-functional (runtime safety checks, stack sizes, runtime/code size tradeoffs) configuration decisions remains, and we believe this could be achieved by designing the API with this ambition in mind.
3(which may be, due to the small feature sample we examined, not perfectly valid)