mind the gap



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

18. Graphical format 18

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

20.Example of models

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?