dosek: A Dependability Oriented Static Embedded Kernel
← back to Overviewdosek - Extended Static Analysis
An extended static analysis of the application leverages a fully dependability-optimized system. Here, we both evaluate the application code itself, as well as the expected overall system behaviour according to the OSEK specification.
In the following, all relevant analysis steps are described based on a simple example. Further details can be found in the related publication at LCTES'15 [1].
TASK H1 {
PRIORITY = 5;
SCHEDULE = FULL;
TYPE = BASIC;
AUTOSTART = FALSE;
RESOURCE = R1;
};
TASK H2 {
PRIORITY = 4;
SCHEDULE = FULL;
TYPE = BASIC;
AUTOSTART = TRUE;
RESOURCE = R1;
};
RESOURCE {
NAME = R1;
TYPE = STANDARD;
};
Static system description: app.oil
As described in the description file (app.oil), the system consists of two Tasks (H1 and H2), and a resource (R1). Task H1 has a higher priority than Task H2 -- the higher the number, the higher the priority -- and both tasks are marked to use the resource R1. Further, both tasks are fully preemptive (SCHEDULE = FULL), and so called Basic Tasks, that is, they are not allowed to use Events. Last but not least, we see, that the low priority Task H1 is marked to be autostarted.
This is all the knowledge, we can get out of the system description. This is just enough to determine the number of kernel objects necessary to realize this application, as well as the minimal amount of operating system services needed. This system does not need any user defined interrupt handlers nor an event or alarm subsystem.
Nevertheless, the actual behaviour of the overall system cannot be determined yet. Here the analysis of the application code itself comes into play.
#include "os.h"
DeclareTask(H1);
DeclareTask(H2);
DeclareTask(H3);
DeclareResource(R1);
void os_main(void) {
StartOS(0);
}
volatile int rand_val = 42;
void test(void) {
if (rand_val) {
GetResource(R1);
// Has higher priority,
// but it is not scheduled
ActivateTask(H1);
ReleaseResource(R1);
}
}
void doSomething(void) {
rand_val++;
}
TASK(H1) {
GetResource(R1);
doSomething();
ReleaseResource(R1);
TerminateTask();
}
TASK(H2) {
test();
TerminateTask();
}
Application code: app.c
A closer look at the application code reveals the behaviour of the overall system. As described in the .oil file, Task H2 will autostart and immediately call the procedure test(). Depending on a global variable, the resource R1 is taken and the high priority Task H1 is activated. Here, the OSEK specification clearly describes the behaviour: The resource has to be realized with a priority ceiling protocol. Therefore, after getting the resource, the priority of Task H2 is increased above the priority of H1. Thus, H1 is only activated but may not run, before R1 is released. After H2 releases R1, H2 will be preempted immediately and the previously activated H1 is started and runs until completion. Finally, H1 can continue and terminate itself.
This is one possible execution. Depending on the conditional expression in test(), R1 may not be taken at all and H1 never activated. So another possible execution only consists of autostarting H2, which immediately terminates after the call of test().
It is worth to be noted, that the just mentioned possible execution patterns cannot be determined only out of the app.c file. Here, we already used a lot of information coming from the .oil description. The application code itself only shows the interaction of the different tasks and the underlying control and data flows.
In order to determine the expected system behaviour in a systematic and automated way, our extended static analysis performs various steps:
References
Dietrich, Christian ; Hoffmann, Martin ; Lohmann, Daniel: |
Drop down the various steps. Use mousewheel to zoom. Drag image to pan.
- Basic Control-Flow Graph Analysis Details
-
The first step is the examination of the control-flow graphs on function level.
- Function Call Analysis Details
-
This step evaluates the inter-function control-flow graph. Here, we simplify the graph by mergeing all basic blocks that do not contain any possible path to a relevant system call. That means, we build some kind of Atomic Basic Blocks (ABBs), as described in the RTSC project.
The call to test() is now linked to the calling ABB15 in Task H2. On the other hand, the doSomething() function called by H1 does not appear anymore, as it does not contain any relevant system calls.
The black arrows describe the inter-function control-flow graph, resulting from this analysis step, while the green arrows show the intra function control-flow.
- Function Assignment and Interrupt Lock AnalysisDetails
-
This step assigns all functions to the correspinding calling tasks, if the assigment is unambigious. Further, we evaluate all ABBs in terms of the interrupt lock state at this point in time. As an example, we see that each system call ABB blocks IRQs (block-irq: OS|All).
- Priority Spreading Pass Details
-
This pass evaluates the priority order of the system and assigns concrete priorities for each task. Here, we concentrate on the relative priorities of the tasks, and insert additional ceiling priorities, to realize the priority ceiling protocol.
The resulting static priorities can be found in the tasks' entry blocks. The analysis further determines the run time priorities of each ABB. All ABBs holding the resource R1 have an increased priority according to the ceiling priority of R1. (e.g., ABB26, ABB10).
- Symbolic System Execution Details
-
This pass determines the OS system state for each ABB along the inter-function control-flow graph, in accordance to the OSEK specification. Beginning from the StartOS() function, over the autostarted Task H2, the analysis examines all task states.
The activation of Task H1 in ABB3 is directly reflected in state of the succeeding ABB22 (H1: SPD -> H1:RDY). After releasing the resource in ABB4, H1 is activated (ABB8/kickoff). H2 is still ready, but preempted. Here, the analysis further describes the next ABB H2 is going to execute after it is dispatched again. (H2: RDY ABB5).
Finally, after all tasks terminated, the analysis ends in an endless idle loop (ABB19<->ABB23).
- System State Flow Details
-
After the symbolic system execution, we can extend the control-flow analysis to a global control-flow graph: The pink arrows represent the previously analyzed control-flow respecting the various system calls. For example, we can see the previously mentioned start of Task H1 at ABB8 after H2 released the resource in ABB4. The dynamic priority noted in ABB4 (prio: 4) is valid on entry of the ABB. That means on exit, that is after releasing the resource, the task's priority drops back to its static priority (prio: 1). Therefore, the previously activated Task H1 then has the highest priority (prio: 2) and is choosen to run next.
H2 terminates at ABB12, Task H1 continues its execution at ABB5, terminates at ABB16, and system ends up in an endless idle loop.
- Global Control Flow Graph Details
- Final Details
