=Paper=
{{Paper
|id=None
|storemode=property
|title=Towards eCos Autoconfiguration by Static Application Analysis
|pdfUrl=https://ceur-ws.org/Vol-688/acota2010_paper6_schirmeier.pdf
|volume=Vol-688
|dblpUrl=https://dblp.org/rec/conf/acota/SchirmeierBSS10
}}
==Towards eCos Autoconfiguration by Static Application Analysis==
https://ceur-ws.org/Vol-688/acota2010_paper6_schirmeier.pdf
ACoTA 2010 First International Workshop on Automated Tailoring and Configuration of Applications
Towards eCos Autoconfiguration by Static
Application Analysis
Horst Schirmeier, Matthias Bahne, Jochen Streicher and Olaf Spinczyk
Computer Science 12 – Embedded System Software
Technische Universität Dortmund
{horst.schirmeier,matthias.bahne,jochen.streicher,olaf.spinczyk}@tu-dortmund.de
Abstract—System software product lines such as the embedded Afterwards, an automated product generation process results
real-time operating system eCos are a state-of-the-art solution for
in an OS library the application can be linked against. This
application scenarios with a very low hardware resource profile. state-of-the-art procedure has proven to be very effective in
Being highly configurable at compile time, eCos can be tailored to
the application in terms of inclusion or exclusion of fine-grainedpractice, but also entails a non-negligible problem: In the case
operating system features. of eCos, the sheer number of more than 1.500 configurable
The mandatory manual feature selection is carried out by features2 makes the configuration process extremely complex
the developer who knows the functionality essential for the and time-consuming.
application. This process requires profound knowledge of the Our contribution to the automated configuration and tailoring
feature semantics, is very time-consuming, and, in particular,
error-prone – most probably resulting in a resource suboptimal community is an approach to at least partially automate the
or even dysfunctional operating system variant. process by applying standard static analysis and model checking
The contribution of this article is an approach to automate thetechniques to application source code. We conducted a detailed
eCos configuration process to a major degree, therefore reducing examination of parts of the eCos 3.0 OS documentation and
the outlined disadvantages significantly. A thorough examination API in order to determine which conditions hold within an
of configurable eCos features exhibits four feature categories of
varying complexity: By applying standard model checking tech- application model if it needs or does not need certain OS
niques and static analysis of the application source code, we showfeatures. These conditions, still formulated in plain English,
pose a set of requirements for static analysis and model
that for at least two feature categories the configuration decisions
can be taken automatically. Complementing the approach with checking. First experiments with our analysis tool prototype
configlets – highly eCos specific analysis code – a third categoryseem promising, but also raise new research questions.
is shown to be also coverable.
Index Terms—eCos, Automatic Configuration, Static Analysis, The remainder of this paper is structured as follows:
Model Checking, CTL, Software Product Lines Section II gives a more detailed overview of the motivating
context and our approach. Section III describes our manual
I. I NTRODUCTION examination of eCos features and examples for the resulting
There exist various reasons for specializing software systems feature categories. Section IV outlines the steps necessary for
for a specific application scenario or a particular customer. In automatic feature need derivation: application analysis, model
the embedded systems domain, the primary motivation is to checking, and result interpretation. Section V revisits the results
minimize resource consumption: Resources such as energy, from the manual feature examination, and summarizes the
memory or CPU cycles are scarce, and keeping the software current state of our analysis tool prototype and preliminary
stack’s resource profile low directly impacts the system’s results with eCos test programs. We conclude with a discussion
hardware costs and therefore its competitiveness on the market. of related work, a summary and an outlook on future work in
Tailorable system software has been a focus of our research sections VI and VII.
group for several years, in particular embedded operating
II. M OTIVATION AND A PPROACH
systems (OS) [14], [15], [18], embedded application product
lines [16], and embedded databases [23], [24]. A. eCos is an Infrastructure Software Product Line
This article describes a case study conducted with the open- Infrastructure software, unlike application software, is in a
source, real-time embedded OS eCos1 , a highly configurable unidirectional usage relationship with other software layers, and
software platform, which can be tailored for the specific needs typically depicted in a hierarchy level above the infrastructure.
of the application. eCos is very widespread, because of it Database software, middleware or standard C libraries, or
being freely available and its comfortable configuration process: operating systems such as eCos are typical representatives.
Guided by a GUI configuration tool, the application developer The categorization of eCos as a software product line (SPL)
decides from a so-called feature model [6], [9] which OS is a bit more debatable: The SPL community defines these
functionality the application mandatorily needs and therefore not only by technical aspects like configurability and code
must be included in the eCos variant deployed on the device.
2 eCos release 3.0; platform specific HAL and device driver features not
1 Embedded Configurable Operating System, http://ecos.sourceware.org/ counted in
35
ACoTA 2010 First International Workshop on Automated Tailoring and Configuration of Applications
Figure 1: eCos: Architectural overview [17]. The unidirectional
API usage relationship application–OS can be exploited for the
detection of feature need.
reuse among product line variants, but also by the engineering Figure 2: The eCos Configtool with a hierarchical display of
process that accompanies the development [5]. Nevertheless, components and different types of options.
we believe we can safely consider eCos a SPL, because it has
all properties relevant to this study:
• Variability Management: Similar to the Linux ker-
nel [25], eCos supports about a dozen different embedded
hardware architectures (with countless subarchitectures),
but clearly separates the platform specific variation points
from platform independent ones. The configuration tree,
separating problem space (configurable features relevant
for the application developer) and solution space (the Figure 3: Instantiating an eCos variant: User configuration
actual implementation behind these features), is organized drives the product generation, yielding a tailored variant
hierarchically in subsystems (Kernel, Hardware Abstrac- implementing only the desired features.
tion Layer, Standard Libraries, I/O, and other optional
subsystems) and several levels of nested components (e.g.,
Serial Device Drivers, ISO C Library String Functions), options are written as C preprocessor macro definitions
cf. Figure 2. On the configuration tree’s leaves exist three in generated header files, which in turn have effects on
different types of configuration options: binary options the OS C/C++ code that is finally compiled and linked to
(on/off), one-from-many selections (e.g., allowing the the application.
selection of one from three different scheduling algo-
In this so-called feature-driven product line derivation
rithms), and value options (e.g., a maximum number of
process [27], the application developer has to make all con-
concurrent threads, an integer number within an interval).
figuration decisions manually in order to tailor the underlying
Additionally, constraints restrict the configuration space
infrastructure product line for his application’s needs. With
to prevent impossible configurations. [28]
highly configurable, real-world product lines such as eCos,
• Product Configuration: eCos comes with a comfortable the configuration effort – although guided by a GUI tool
GUI configuration tool that allows creating a specific with automatic inter-feature dependency resolution and textual
configuration by assembling components and configuring descriptions of all configuration options – easily exceeds ac-
the contained options (cf. Figure 2). Feature constraints ceptable limits. Moreover, a vast configuration space promotes
like dependencies or mutually excluding features are chances for human mistakes, leading to a resource suboptimal
automatically enforced. (if too much functionality was configured) or insufficient
• Product Generation: The GUI tool is also capable of (essential functionality missing) infrastructure variant. Even
automatically generating the actual eCos variant from the worse, this process needs to be iterated once the application
configuration (cf. Figure 3). This process generates a new evolves. Consequently, (at least partial) automation of the
source code tree: The chosen values for the configuration process and tool support is desirable.
36
ACoTA 2010 First International Workshop on Automated Tailoring and Configuration of Applications
B. API Usage Patterns and Model Checking c l a s s Cyg_Thread {
In earlier work [24] we showed that infrastructure API usage /* . . . */
patterns within an application allow to deduce feature need # i f d e f CYGVAR_KERNEL_THREADS_NAME
or non-need. Ranging from the simple existence of certain private :
API calls to complex API call patterns and involvement / / An o p t i o n a l t h r e a d name s t r i n g ,
of actual parameter values, different levels of complexity / / f o r humans t o r e a d
have been observed for real-world infrastructure features. In char * name ;
this case study, we take a closer look at the eCos API and public :
its characteristics related to application analysis and feature / / f u n c t i o n t o g e t t h e name s t r i n g
relevant API usage patterns. Motivated by our earlier results, char * g e t _ n a m e ( ) ;
we evaluate the temporal logic CTL (computation tree logic [4]) # endif
as a language for formulating feature conditions to be checked /* . . . */
within an application model.
Figure 4: An excerpt from an eCos 3.0 internal kernel header
III. E XAMINING THE E C OS O PERATING S YSTEM file: The effect of a GUI configuration option on an internal
For our approach, the first step towards automatic con- thread abstraction data structure.
figuration comprises establishing a relationship between in-
frastructure features on the one hand, and properties of the
application on the other hand. We conducted a thorough manual Iff there exist (reachable) calls to
examination of the configurable features in the eCos kernel cyg_mbox_put(...) or cyg_mbox_timed_put(...), then
components “Kernel schedulers”, “Thread-related options” the feature “Message box blocking put support” is
and “Synchronization primitives” in order to gain experience needed.
with real-world OS features and to study the implications for 2) API call patterns and actual parameters: Another pattern
application analysis. can be illustrated by the example of the feature “Support
This manual infrastructure feature examination must not be optional name for each thread”, located in the “Thread-related
confused with the automated analysis steps described later in options” component. This option enables applications to assign
this article: a name (a C character string) to each thread, and to read that
• This examination must be carried out only once, whereas
name from an arbitrary, given thread.
its results can be reused in all infrastructure deployments. Once this option is enabled, the kernel’s internal thread
• Therefore, an infrastructure expert (e.g., a member of
abstraction data structure (a C++ class named Cyg_Thread) is
its development team, outfitted with in-depth knowledge extended by a name element (again by means of preprocessor
of the API semantics) can (and should) be the person macros, cf. Figure 4), thus saving memory (and OS code, in
conducting this analysis. other parts of eCos) if this functionality is not needed.
• In contrast, the automated analysis steps take place later
Nevertheless, the kernel’s C API is not affected at all:
at the application developer’s site. Regardless of how the application developer configures eCos,
the API function cyg_thread_create(...) always takes a name
A. Manual examination parameter (which is ignored if the kernel cannot store thread
names), and the API function cyg_thread_get_info(...) always
The aim of the manual examination of the eCos 3.0 source
fills a data structure (struct cyg_thread_info) which has a name
code and documentation was to ascertain what exact effect
element. An application developer who does not want to give a
each configurable feature has on actual OS functionality, and
thread a name simply passes NULL instead of a character string.
especially the OS API. We show that an application, containing
If the kernel does not know a thread’s name, or is not capable
calls to this API, fulfills certain conditions that indicate its need
of storing thread names, cyg_thread_get_info(...) returns NULL
for OS features. The results, including these feature conditions,
in the name element of cyg_thread_info.
were diverse and are presented in the following in terms of
four feature categories, each accompanied by examples. This API definition allows to concentrate on an application’s
usage of cyg_thread_create(...) and cyg_thread_get_info(...) for
1) Simple API call usage: One very common case of API
automatic configuration of this feature:
usage observed is the simple existence of certain API calls.
For example, enabling “Message box blocking put support” Iff the application passes a non-NULL parameter
(located in the “Synchronization primitives” component) de- value to cyg_thread_create(...)’s name parameter, and
fines a preprocessor macro, which in turn adds the functions calls cyg_thread_get_info(...) and reads the name
cyg_mbox_put(...) and cyg_mbox_timed_put(...) to the kernel element of its return value, the feature “Support
API. Knowing this direct relationship from feature selection optional name for each thread” is needed.
to the API, and being able to assure these API calls are not This condition is not completely conclusive, though: An
additionally related to other features, one can pose a simple, application developer may create threads with names just
definitive condition on the application code: for self-documenting purposes without needing the kernel to
37
ACoTA 2010 First International Workshop on Automated Tailoring and Configuration of Applications
store this information. An application may even read the name very specialized program analysis technique which may
element and expect it to be NULL. Nevertheless there is a not be possible to generalize further. Our first attempt to
strong indication that the feature is needed, so the configuration deal with these is described in subsection IV-D.
tool could give the application developer a hint to enable it.
IV. S TATIC A PPLICATION A NALYSIS AND D ETERMINATION
3) Domain specific patterns: Some options exhibit an
OF F EATURE N EED
inherent complexity, and are, due to their interrelation with
concurrency and synchronization aspects, highly OS specific. A. Static Analysis of eCos Applications
An extreme example is the option “Priority inversion protection The first step in statically deriving information from appli-
protocols” in the “Synchronization primitives” component: It cation source code is transforming it into a model suitable
controls whether synchronization primitives should be protected for the subsequent analysis steps – suitable in a way that
against priority inversion [11]. the transformation does not lose information relevant for the
As this feature comes with quite some cost (program memory, problem space, leading to incorrect configuration decisions.
CPU cycles at runtime), it should only be enabled if priority Our examination of eCos features suggests that a C-statement-
inversion is a problem in the application at all: level control flow graph (CFG) fulfills our requirements, as it
Iff the application is structured in a way that maintains temporal interrelations between API calls and return
priority inversion can occur, the feature “Priority value usage, and allows for reachability analysis. A CFG can
inversion protection protocols” is needed. also be subject to further data flow analysis and transformation
Unfortunately, detecting this property in an application is not steps that propagate actual values to nodes where they are
trivial and can only be approached with an approximation: passed through the OS API. Additionally, a CFG is generic
enough that it still holds enough program information for the
Iff at least two threads with different priority
highly OS specific analyses sketched in subsection III-A3.
levels share a common mutex, and a thread with a
priority level between these two exists, the feature B. Formalizing Feature Conditions and Model Checking
“Priority inversion protection protocols” is needed. Motivated by our own earlier results [24] and promising
There are several reasons why an application developer still achievements in other projects applying model checking to
may not need this feature: The application may be designed in identify patterns in application code (such as [10]), we decided
a way that priority inversion is prevented by other means, or to use the temporal logic CTL as a language to formalize
the occurrence of this effect may even be intended. So, again, feature conditions. CTL can express temporal relationships,
the configuration tool should only give a hint. and there exist efficient model checking algorithms [4], [10]
4) Not derivable: For the remaining features we were unable for this logic.
to pose feature conditions, for different reasons. A detailed We model the CFG of the application program as a Kripke
analysis of this category follows in section V. structure [4] M = (S, S0 , R, L) over atomic propositions P ,
where S is a (finite) set of states (representing statement-level
B. Implications for Static Analysis and Model Checking CFG nodes), S0 is a set of initial states, R ⊆ S × S is a total
The eCos features we examined and the resulting feature transition relation, and L : S → 2P is a labeling function
conditions imply several requirements on the application that associates a subset of P to each state. A proposition p
analysis: holds in a state s, if p is contained in the label of s, i.e.,
• Feature conditions that relate only to the existence of p ∈ L(s). A path π, starting at state s, is a sequence of states
certain API calls, the least complex category identified in π = s0 s1 s2 s3 . . . with s0 = s and R(si , si+1 ) for all i ≥ 0.
the previous subsection, could more or less be checked CTL formulas allow to specify temporal properties of Kripke
by simple text search utilities like grep. The capabilities structures by extending classical predicate logic by temporal
missing (and essential for well-founded automatic config- connectives which establish a relationship to future states:
uration decisions) are a deeper understanding of C syntax • Every atomic proposition p ∈ P is a CTL formula.
and semantics – for example to differentiate between an • If p and q are CTL formulas, ¬p, p ∧ q, p ∨
API function mentioned in a source code comment, and q, AX p, EX p, AG p, EG p, A[p U q] and E[p U q] are
real API usage – and control flow properties that indicate valid formulas, too. X is the nexttime operator: AX p (resp.
whether the API calls are reachable at all. EX p) means that p holds in every (in some) immediate
• Patterns as observed in the “Support optional name for successor state. G is the global operator: AG p (resp.
each thread” example also demand for control flow EG p) states that p holds in all (in some) future states.
information (connecting a cyg_thread_get_info(...) call to U is the until operator: A[p U q] (resp. E[p U q], cf. Sub-
a subsequent use of its return value) and actual parameter figure 5a) expresses that for every (for some) path starting
values, implying the need for static analysis techniques like with the current state, there exists an initial prefix of this
constant folding, constant propagation, inter-procedural path such that q holds at the last state of this prefix, and
reaching definitions analysis [21], or interval analysis. p holds in all other states of the prefix [3].
• Highly OS domain specific feature patterns concerning • The finally operators AF and EF can be seen as an
thread concurrency and synchronization aspects call for a abbreviated form of the until operators with p = true
38
ACoTA 2010 First International Workshop on Automated Tailoring and Configuration of Applications
(a) E p U q (b) EF p (c) AF p
Figure 5: Examples for simple CTL formulas and corresponding state trees.
(cf. Sub-figures 5b and 5c): They mean that on all (on C. Inferring Feature Need
some) paths the operand will hold sometime in the future Although not accounted for in section III-A, our examination
(AF q ⇔ A[true U q]). of eCos features showed that often multiple feature conditions
Figure 5 and the examples later in this subsection may help are necessary to exhaustively describe the possible API usage
gaining a more intuitive understanding of CTL. patterns that signify an application’s need or non-need for a
For the feature conditions identified in subsection III-A we certain feature. Some conditions only help deciding for or
additionally define an elementary set of atomic propositions: against feature need, not both: Once a single necessary (in
• The trivial proposition [true] holds in every, [false] in no the mathematical sense) condition is not fulfilled, the feature
state. this condition belongs to is not needed; once a single sufficient
• [call :somefunction(. . .)] holds in every state that condition is fulfilled, the feature is definitely needed. In both
contains a call to somefunction, ignoring its actual cases, the respective converse decision cannot be taken: The
parameters. [call :somefunction(?, 4, ?)] holds if the fulfillment of a necessary condition does not allow a statement
second actual parameter is equal to 4. on feature need.
Now we can formulate a subset of the feature conditions from Another orthogonal condition property is weakness: If a
section III-A in CTL. The condition informally introduced in condition should only be used to give the user a configuration
subsection III-A1 can be expressed as follows: hint instead of making a fully automated configuration decision,
it is called a weak condition (examples are the conditions in
EF ( [call :cyg_mbox_put(. . .)] ∨
subsections III-A2 and III-A3), or else a definite condition.
[call :cyg_mbox_timed_put(. . .)] ) The model checking results for all conditions of a certain
For now ignoring the “. . . and reads the name element of its feature can be combined to a resulting statement on whether
return value, . . . ” part of the condition, we can also express the feature should be enabled or disabled. Figure 6 assembles
the condition from subsection III-A2: the following propositions:
EF ( [call :cyg_thread_create(. . .)] ∧ N ⇔ all definite, necessary conditions are fulfilled
¬[call :cyg_thread_create(?, ?, ?, 0, ?, ?, ?, ?)] ∧ (or none exists).
n ⇔ all weak, necessary conditions are fulfilled
EX EF [call :cyg_thread_get_info(. . .)] )
(or none exists).
In order to formulate this condition completely, we would S ⇔ some definite, sufficient condition is fulfilled.
need another atomic proposition for data structure access and a s ⇔ some weak, sufficient condition is fulfilled.
means to express the connection between the variable returned
by cyg_thread_get_info(...) and the point where its member One remaining case still needs to be dealt with: If a condition
name is accessed. (See the discussion in subsection IV-D for cannot be successfully checked (e.g., because data flow analysis
a solution to this problem.) fails, and therefore the possible value(s) of an actual parameter
A model checking algorithm can now check whether the cannot be determined), we can safely proceed pretending
application’s Kripke structure is a model for a CTL formula – this condition did not exist in the first place, as evidently
iff this is the case, the feature condition is fulfilled. Starting the resulting statement is not falsified by that measure. The
with the atomic propositions used in the CTL formula, and user should still be informed about the omission of a feature
recursively continuing with more and more complex sub- condition, as a simple code change may make the analysis
formulas, each Kripke node is labeled with the sub-formulas possible again.
holding for this particular node. This procedure is iterated Finally, the internal dependency and restriction constraints
until it can be determined whether the complete formula holds in the eCos configuration tree need to be taken into account
in a starting node. For more details on the model checking – a feature not directly needed by the application may still
algorithm we refer to Clarke’s original publication [3]. be mandatory because another feature depends on it. This
39
ACoTA 2010 First International Workshop on Automated Tailoring and Configuration of Applications
¬N N ∧n N ∧ ¬n
Conditions or
Yes, feature definitely Yes, feature definitely
S application source
needed needed
code ill-formed
No, feature definitely Maybe, no definite Hint: No, probably not
¬S ∧ ¬s
not needed decision possible needed
No, feature definitely Hint: Yes, probably Maybe, no definite
¬S ∧ s
not needed needed decision possible
Figure 6: Combining different classes of feature conditions, yielding a configuration decision. Definite decisions, based solely
on definite conditions, have a shaded background.
dependency resolution can already be conducted by the eCos free variables (placeholders). Their modified model checking
Configtool, though. algorithm was shown to be still efficient.
Unfortunately, neither CTL nor CTPL are expressive enough
D. Discussion
to cover complex feature conditions such as described in
The quality of results obtained from model checking can only subsection III-A3. Our first attempt to deal with these highly
be as good as the model being checked, which in the case of OS domain specific conditions is to encapsulate them in small
control and data flow graphs (at least for real-world code input) plug-ins, so-called configlets, written in C++ against an analysis
may not yield all necessary information (e.g., failing to trace API giving direct access to the underlying CFG (cf. Figure 7).
actual parameters to the place they are defined, or not being A configlet can be used in place of a CTL formula, its output
able to determine the number of iterations a loop can make). is processed the same way (cf. Figure 6). We are still unsure
Static code analysis is well-known to be limited in theory and about what the interface between a configlet and the remaining
practice [10], [12], [19], [21], but nevertheless we believe that analysis tool interface should look like, and are trying to find
these limits are not pivotal for our approach: Even if some an adequate balance between a complex API with complete
configuration decisions cannot be automated because static access to the Kripke model, and a minimal, easier to use API
analysis fails, and the application developer has to configure which still is generic enough to deal with new use cases.
the respective features manually, the overall configuration effort
is still significantly reduced. Additionally, this problem could V. R ESULTS
be tackled by trying to reduce the complexity of static analysis. A. eCos examination
An interesting research question in this context would be: What
The manual examination of 39 eCos features (cf. sub-
modifications to an infrastructure’s API might be adequate to
section III-A) resulted in a categorization into four feature
facilitate static analysis and therefore improve the quality of
categories, bearing various levels of complexity for automatic
automatic configuration decisions?
analysis. Table I lists all features, their type, their feature
Another related open question is what API the application
category, and the types of feature conditions we formulated.
should be initially written against: As the API may be affected
• 7 out of 39 features were categorized into “Simple API
by configuration decisions, a circular dependency exists. In
principle, a “full” API encompassing all possible configurations call usage”.
• 5 features fall in the “API call patterns and actual pa-
(something Fröhlich [7] calls an inflated interface) needs to
be generated. This may not be possible if two API variants rameters” category: Two of these need the CTL extension
conflict (e.g., a function cannot have two different signatures mentioned in subsection IV-D.
• 6 features are highly OS specific and belong to the
in the C programming language), although this was not the
case for eCos: We were able to manually create a set of header “Domain specific patterns” category. We were able to
files valid for all possible variants. formulate conditions for these features, but CTL (and
The additional expressiveness demanded in subsection IV-B CTPL) turned out to be insufficient.
– CTL’s lack of a means to connect several usage points of a 19 features were categorized to be not derivable from an
single variable – could be handled by a CTL extension: With application’s source code, for different reasons:
CTPL, Kinder et al. [10] proposed such an extension to CTL • The largest group (13) are configurable non-functional
that allows for expressing such connections by introducing properties that have an effect on code size (e.g., explicit
40
ACoTA 2010 First International Workshop on Automated Tailoring and Configuration of Applications
Figure 7: Analysis process overview: Configlets complement CTL model checking for complex feature conditions.
Feature name Type Feature condition types found Category
Multi-level queue scheduler one-from-many sufficient 3
Bitmap scheduler one-from-many necessary 3
Number of priority levels value (1–32) 3×sufficient 3
Dequeue highest priority threads first binary – 4
Scheduler timeslicing binary 1×necessary, 1×sufficient (weak) 3
Number of ticks between timeslices value – 4
Support runtime enable of timeslice per-thread binary necessary/sufficient 1
Enable ASR support binary – 4
Make ASR function global binary – 4
Make ASR data global binary – 4
Priority inversion protection protocols binary necessary/sufficient (weak) 3
Enable priority inheritance protocols binary necessary/sufficient 2
Enable priority ceiling protocol binary necessary/sufficient 2
Default priority inversion protocol one-from-many – 4
Specify mutex priority inversion protocol at runtime binary necessary/sufficient 1
Use mboxt_plain mbox implementation binary (sufficient) 4
Message box blocking put support binary necessary/sufficient 1
Message box queue size value – 4
Condition variable timed-wait support binary necessary/sufficient 1
Condition variable explicit mutex wait support binary necessary/sufficient 2
Avoid inlines in mqueue implementation binary – 4
Allow per-thread timers binary – 4
Support optional name for each thread binary 1×necessary, 1×sufficient 2
Keep track of all threads using a linked list binary 1×sufficient 1
Keep track of the base of each thread’s stack (binary) – (4)
Check thread stacks for overflows binary – 4
Check all threads whenever possible binary – 4
Signature size in bytes, at stack top and bottom value (8–512) – 4
Measure stack usage binary necessary/sufficient 2
Output stack usage on thread exit binary – 4
Support for per-thread data binary necessary/sufficient 1
Number of words of per-thread data value (4–32) – 4
Thread destructors binary necessary/sufficient 1
Number of possible destructors value (1–65535) necessary/sufficient 3
Per-thread destructors binary – 4
Stack size for the idle thread value (512-65536) – 4
Maximal suspend count value – 4
Maximal wake count value – 4
Idle thread must always yield (binary) – (4)
Table I: The examined eCos features, listed with the feature category (cf. subsection III-A) and the condition types. The
condition types found are definite unless explicitly denoted weak. Category legend: 1) Simple API call usage, 2) API call
patterns and actual parameters, 3) Domain specific patterns, 4) Not derivable.
41
ACoTA 2010 First International Workshop on Automated Tailoring and Configuration of Applications
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. [29] tailor the middleware product line Abacus
• 4 features could not be examined in detail due to their (a CORBA middleware implementation) according to the
unclear semantics. application’s needs. In contrast to the focus of our work,
Among these 19 features, 6 were additionally identified to be they completely ignore the task of derivation of feature need
of interest only for the development process and/or debugging from the application. Source code annotations are added
purposes. For example, “Output stack usage on thread exit” to the application code to make the feature requirements
creates debugging output once a thread terminates – a feature explicit; the difference to manual infrastructure configuration
the developer, despite being eager for automatic configuration, is marginal and debatable. In their customizable embedded
still would want to configure manually due to its purpose in D REAMS OS, Böke, Chivukula et al. [1], [2] also achieve
the development process context. infrastructure tailoring by supplying an explicit requirements
The remaining two features even seem only to be there specification. The specification is on a lower abstraction level
for self-documentation reasons, as they are tightly coupled than in the Abacus case, though: The system calls and their
with other features by dependency relationships and cannot properties (precedence relation, number of calls, etc.) made
be directly configured by the user anyways (e.g., “Idle thread by each process are explicitly listed. The D REAMS tailoring
must always yield” is automatically enabled once there is only approach also benefits from the OS being explicitly designed
a single priority level configured). for automatic configuration.
Altogether, we were able to pose feature conditions for about Focusing mostly on functional infrastructure properties, the
half of the examined features (18 out of 37 “real” features). aforementioned projects insufficiently deal with non-functional
properties (such as code size, memory usage at runtime, timing
B. Implementation and preliminary evaluation behavior etc.). These properties have an emergent nature and
therefore often cannot be directly configured, nevertheless some
The prototype implementation of the described analysis and research work exists in this field. Pu, Massala et al. developed
model checking steps is still very preliminary and has not yet the research operating system Synthesis [22] which adapts to
been thoroughly tested with real-world code input. Nevertheless, and self-optimizes for the application’s API usage patterns
our test runs with simple CTL formulas and a suite of eCos at runtime. Supplied by a just-in-time compiler, often used
test programs (shipped with eCos 3.0), cloned and adapted for code paths are partially evaluated and tuned to high throughput.
testing specific units of the prototype, are promising and will Sincero, Hofer et al. [8], [26] are developing feedback approach
soon be extended to a full-scale evaluation. which systematically collects information on emerging non-
The analysis tool prototype is based on clang, an LLVM [13] functional properties in the CiAO [14] operating system to be
compiler front-end for the C, C++ and Objective-C languages. able to make educated predictions for unknown configurations.
The complete static analysis phase (scanning and parsing This information could be used to automatically (based on a
the application’s C code, performing constant folding and user-defined non-functional optimization goal) select one of
propagation) is externalized to clang. The resulting CFG is several variants which are functionally equivalent but exhibit
then transformed to a Kripke structure. A C++ implementation different non-functional properties, therefore complementing
of Clarke’s CTL model checking algorithm [4] is currently our approach.
capable of checking single CTL formulas and combining the Outside the context of infrastructure software tailoring, there
results for a configuration decision. Besides the sub-condition exist many other research projects that apply static analysis
requiring a CTL extension (cf. subsection IV-D), all feature and model checking to problems in their domain. For example,
conditions categorized in subsections III-A1 and III-A2 can Padioleau, Lawall et al. [20] utilize CTL for matching and
already be checked. A prototype configlet for the example replacing code in order to deal with collateral evolutions
condition in subsection III-A3 is under development. in the Linux kernel. The SmPL language can be used to
define so-called semantic patches which can automatically
VI. R ELATED W ORK
be transformed into CTL formulas. Another example comes
There exist numerous research projects engaging in from the systems security domain: Kinder et al. [10] formidably
application-driven tailoring of infrastructure software. The show the applicability of static analysis model checking to the
concept of Application-Oriented System Design was introduced generic detection of malicious code.
by Fröhlich [7] in the EPOS operating system. Here the set
of infrastructure symbols (i.e., a temporally unordered list of VII. C ONCLUSIONS AND F UTURE W ORK
API calls) referenced by the application determines which Our examination of a subset of eCos features showed
product line variant is needed. If multiple variants fulfill the that for about half of these we can, at least informally,
requirements, the least resource expensive one (in a fixed, define feature conditions which allow deducing feature need
manually defined cost ordering of variants) is chosen. Apart from an application’s source code. Aiming at automating
from the comparably simple static analysis the main difference the evaluation of these conditions, we identified control flow
to our approach is the lack of logical isolation between analysis graphs, transformed to a Kripke structure, as an adequate model
and configuration, established by a feature model. which carries enough information for subsequent analysis steps.
42
ACoTA 2010 First International Workshop on Automated Tailoring and Configuration of Applications
The branching-time logic CTL was attested to be expressive [4] Edmund M. Clarke, Orna Grumberg, and Doron A. Pele. Model Checking.
enough for many but not all feature conditions we found: For The MIT Press, Cambridge, Massachusetts and London, England, 3
edition, 2001.
a few cases it needs to be extended with free variables, or [5] Paul Clements and Linda Northrop. Software Product Lines: Practices
even supplemented by configlets, specialized analysis plug- and Patterns. Addison-Wesley, 2002.
ins written in a normal programming language. The first [6] Krysztof Czarnecki and Ulrich W. Eisenecker. Generative Programming.
Methods, Tools and Applications. Addison-Wesley, May 2000.
preliminary evaluation results with our analysis tool prototype [7] A. Fröhlich. Application-Oriented Operating Systems. Number 17 in
are promising, although we cannot already draw conclusions GMD Research Series. GMD - Forschungszentrum Informationstechnik,
regarding the scalability of our approach. Sankt Augustin, August 2001.
Although the configuration automation of about 50% of [8] Wanja Hofer, Julio Sincero, Daniel Lohmann, and Wolfgang Schröder-
Preikschat. Configuration of Non-Functional Properties in Embedded
the examined features may not seem exceedingly successful, Operating Systems: The CiAO Approach. Methodologies for Non-
extrapolating this to all configurable eCos features3 we could Functional Requirements in Service Oriented Architecture. IGI Global,
still save the application developer about 750 configuration Hershey, PA, USA, 2010. (To Appear).
[9] K. Kang, S. Cohen, J. Hess, W. Novak, and S. Peterson. Feature-
decisions. For parts of the remaining half, especially the features oriented domain analysis (FODA) feasibility study. Technical report,
dealing with non-functional properties, the feedback approach Carnegie Mellon University, Software Engineering Institute, Pittsburgh,
of Sincero et al. [8], [26] could offer other means of automatic PA, November 1990.
[10] Johannes Kinder, Stefan Katzenbeisser, Christian Schallhart, and Helmut
configuration. Veith. Detecting malicious code by model checking. In Klaus Julisch
Our results are comparable to an earlier case study we and Christopher Krügel, editors, GI SIG SIDAR Conference on Detection
conducted with a modified version of the Berkeley DB [24], an of Intrusions and Malware & Vulnerability Assessment (DIMVA 2005),
volume 3548 of Lecture Notes in Computer Science, pages 174–187.
embedded DBMS for which we could automate an even larger Springer-Verlag, 2005.
portion of configuration decisions – mostly due to simpler API [11] Butler W. Lampson and David D. Redell. Experience with processes and
usage patterns and a lower quantity of features dealing with monitors in mesa. Communications of the ACM, 23(2):105–117, 1980.
non-functional properties. [12] William Landi. Undecidability of static analysis. ACM Letters on
Programming Languages and Systems, 1(4):323–337, 1992.
More future work includes examining additional eCos [13] LLVM homepage. http://www.llvm.org/.
features in order to gain more confidence on the general [14] Daniel Lohmann, Wanja Hofer, Wolfgang Schröder-Preikschat, Jochen
soundness of our approach. We also intend to evaluate the Streicher, and Olaf Spinczyk. CiAO: An aspect-oriented operating-system
family for resource-constrained embedded systems. In Proceedings of the
outlined extension to CTL, to compare it to other (potentially 2009 USENIX Annual Technical Conference, pages 215–228, Berkeley,
more powerful) temporal logics, and to integrate the analysis CA, USA, June 2009. USENIX Association.
results in the eCos Configtool. In order to alleviate the [15] Daniel Lohmann, Fabian Scheler, Reinhard Tartler, Olaf Spinczyk, and
Wolfgang Schröder-Preikschat. A quantitative analysis of aspects in the
infrastructure developer’s task to describe feature conditions, eCos kernel. In Proceedings of the EuroSys 2006 Conference (EuroSys
we are also going to look into simpler description languages that ’06), pages 191–204, New York, NY, USA, April 2006. ACM Press.
can be automatically transformed into temporal logic formulas; [16] Daniel Lohmann, Olaf Spinczyk, and Wolfgang Schröder-Preikschat.
Lean and efficient system software product lines: Where aspects beat
Kinder et al. [10] suggest using macro shortcuts for the most objects. In Awais Rashid and Mehmet Aksit, editors, Transactions on
commonly used patterns, which may prove to suffice. AOSD II, number 4242 in Lecture Notes in Computer Science, pages
Beyond these enhancements and a thorough evaluation of the 227–255. Springer-Verlag, 2006.
outlined approach, we are looking into the research question [17] Anthony Massa. Embedded Software Development with eCos. Prentice
Hall Professional Technical Reference, 2002.
what modifications to the infrastructure API are necessary to [18] Matthias Meier, Michael Engel, Matthias Steinkamp, and Olaf Spinczyk.
simplify the analysis task such that a vast majority of features LavA: An open platform for rapid prototyping of MPSoCs. In
can be automatically configured. Ideally, only a tiny fraction Proceedings of the 20th International Conference on Field Programmable
Logic and Applications (FPL ’10), Milano, Italy, 2010. IEEE Computer
consisting of development time (debugging) and non-functional Society Press. to appear.
(runtime safety checks, stack sizes, runtime/code size trade- [19] Toshio Ogiso, Yusuke Sakabe, Masakazu Soshi, and Atsuko Miyaji.
offs) configuration decisions remains, and we believe this could Software tamper resistance based on the difficulty of interprocedural
analysis, August 2002.
be achieved by designing the API with this ambition in mind. [20] Yoann Padioleau, Julia Lawall, René Rydhof Hansen, and Gilles Muller.
Documenting and automating collateral evolutions in linux device drivers.
R EFERENCES In Proceedings of the EuroSys 2008 Conference (EuroSys ’08), pages
[1] Carsten Böke. Automatic Configuration of Real-Time Operating Systems 247–260, New York, NY, USA, 2008. ACM Press.
and Real Time Communication Systems for Distributed Embedded [21] H. D. Pande, W. A. Landi, and B. G. Ryder. Interprocedural def-use
Applications. Dissertation, Universität Paderborn, Heinz Nixdorf Institut, associations for c systems with single level pointers. IEEE Transactions
Entwurf Paralleler Systeme, 2004. on Software Engineering, 20(5):385–403, 1994.
[2] Ramakrishna Prasad Chivukula, Carsten Boeke, and Franz J. Rammig. [22] Calton Pu, Henry Massalin, and John Ioannidis. The Synthesis kernel.
Customizing the configuration process of an operating system using Computing Systems, 1(1):11–32, Winter 1988.
hierarchy and clustering. Proceedings of the 5th IEEE International [23] Marko Rosenmüller, Norbert Siegmund, Horst Schirmeier, Julio Sincero,
Symposium on Object-Oriented Real-Time Distributed Computing (ISORC Sven Apel, Thomas Leich, Olaf Spinczyk, and Gunter Saake. FAME-
’02), 0:0280, 2002. DBMS: Tailor-made Data Management Solutions for Embedded Systems.
[3] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification In Workshop on Software Engineering for Tailor-made Data Management,
of finite-state concurrent systems using temporal logic specifications. pages 1–6. School of Computer Science, University of Magdeburg, March
ACM Transactions on Programming Languages and Systems (TOPLAS), 2008.
2(8):244–263, 1986. [24] Horst Schirmeier and Olaf Spinczyk. Tailoring Infrastructure Software
Product Lines by Static Application Analysis. In Proceedings of the 11th
3 (which may be, due to the small feature sample we examined, not perfectly Software Product Line Conference (SPLC ’07), pages 255–260. IEEE
valid) Computer Society Press, 2007.
43
ACoTA 2010 First International Workshop on Automated Tailoring and Configuration of Applications
[25] Julio Sincero, Horst Schirmeier, Wolfgang Schröder-Preikschat, and [27] Olaf Spinczyk and Holger Papajewski. Using Feature Models for
Olaf Spinczyk. Is The Linux Kernel a Software Product Line? In Product Derivation. In Proceedings of the 11th Software Product Line
Frank van der Linden and Björn Lundell, editors, Proceedings of the Conference (SPLC ’07), pages 5–6, Kyoto, Japan, September 2007.
International Workshop on Open Source Software and Product Lines Tutorial Description.
(SPLC-OSSPL 2007), Kyoto, Japan, 2007. [28] Bart Veer and John Dallaway. The eCos Component Writer’s Guide. Free
[26] Julio Sincero, Wolfgang Schröder-Preikschat, and Olaf Spinczyk. Towards Software Foundation, Inc., 2001. http://ecos.sourceware.org/docs-3.0/.
Tool Support for the Configuration of Non-Functional Properties in SPLs. [29] Charles Zhang, Dapeng Gao, and Hans-Arno Jacobsen. Towards just-in-
In Proceedings of the 42nd Hawai’i International Conference on System time middleware architectures. In Proceedings of the 4th International
Sciences (HICSS ’09), Waikoloa, Big Island, Hawaii, January 2009. IEEE Conference on Aspect-Oriented Software Development (AOSD ’05), pages
Computer Society Press. 63–74, New York, NY, USA, 2005. ACM.
44