展开查看详情
1 . Mind the gap:
between real-time Linux and real-time theory
Part I
Daniel Bristot de Oliveira
2 . In the beginning
In the begin a program was only a logical sequence,
Then gosh said: we can’t wait forever, we need to put time on this,
Since then we have two problems:
The logical correctness, and the timing correctness.
2
3 . In theory...
The systems defined as a set of tasks τ
Each task is a set of variables that defines its timing behavior, e.g.,
τ i {P , C , D , B , J }
=
Then, they try to define/develop a scheduler in such way that,
for each task i in τ :
the response time of τ i < Di
3
4 . For task level fixed priority scheduler:
∀ task i∈ τ :
W i +J j
W i =C i +B i + ∑ j∈hp(i)
Ri =W i +J i
⌈ Pj ⌉ Cj
is schedulable ⇔ ∀ task i∈ τ∣R i < D i
4
5 . For Early Deadline First
∀ task i∈ τ :
Ci
U i=
Pi
is schedulable ⇔ ∀ task i∈ τ∣∑ U i <1
5
6 .The development of a new scheduler is
done with mathematical reasoning.
7 . But generally, they relax in the task model
- The system is fully preemptive;
- Tasks are completely independent;
- Operations are atomic;
- There is no overhead.
7
8 .We can’t say that these assumptions are
not realistic...
9 .But, what is our reality?
10 . Our reality
- The system is not fully preemptive;
- Tasks are not completely independent;
- Operations are not atomic;
- There is overhead.
10
11 .Math side: But talk is cheap…
12 .Dev side: Read the code, it is there, boy!
13 .Math side: Talk is cheap...
Show me the math!
14 . Towards a Linux task model
● Inside our mind, we have an implicit task model:
○ We know preemption causes latency
○ We know the difference in the behavior of a mutex and the spin lock
○ We know we have interrupts
● But, how do we explain these things without missing details?
○ Natural language is ambiguous…
○ e.g., preemption disabled is bad for latency, right?
14
15 . Towards a Linux task model
● We need an explicit task model
○ Using a formal language/method
○ Abstracting the code
○ Without losing contact with the terms that we use in practice.
15
16 . Toward a Linux task model
● Linux developers use tracing features to analyze the system:
○ They see tracing events that cause states change of the system.
● Discrete Event Systems (DES) methods also use these concepts:
○ events, trace and states...
● DES is can be used in the formalization of system.
● So, why not try to describe Linux using a DES method?
16
17 . Background
● Automata is a method to model Discrete Event Systems (DES)
● Formally, an automaton is defined as:
○ G = {X , E, f , x0 , Xm }, where:
■ X = finite set of states;
■ E = finite set of events;
■ F is the transition function = (X x E) → X;
■ x0 = Initial state;
■ Xm = set of final states.
● The language - or traces - generated/recognized by G is the L(G).
17
19 . Modeling of complex systems
● Rather than modeling the system as a single automaton, the modular
approach uses generators and specifications.
○ Generators:
■ Independent subsystems models
■ Generates all chain of events (without control)
○ Specification:
■ Control/synchronization rules of two or more subsystems
■ Blocks some events
● The parallel composition operation synchronizes them.
○ The result is an automaton with all chain of events possible in a
controlled system.
19
21 . Generators of events
21
22 . Generators of events
22
23 . Eita, boia,
This is boring…
24 .Specifications: Sufficiency conditions
25 .Specifications: Sufficiency conditions
26 .Specifications: Sufficiency conditions
27 .Specifications: Necessary condition
28 . Synchronizing the modules, we have the model
The complete model has:
- 12 generators + 33 specifications
- 34 different events
- > 10000 states!
The benefit of this:
- Validating the model against the kernel, and vice-versa, is O(1)
- One kernel event generates one automata transition
28
29 .Nice! But what do we do with this
information?
热门城市
