Skip to content

Commit d8132da

Browse files
frank-at-adacorefrank-at-adacore
committed
Merge branch 'slides/194-245_ravenscar_tasking-into-chapters' into 'master'
Resolve "Break *245_ravenscar_tasking into chapters" Closes #194 See merge request feng/training/material!252
2 parents 9afa825 + 3cfeb09 commit d8132da

11 files changed

+785
-536
lines changed

‎courses/fundamentals_of_ada/245_ravenscar_tasking-with_tasking_overview.rst

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
*******************
2+
Ravenscar Tasking
3+
*******************
4+
5+
.. container:: PRELUDE BEGIN
6+
7+
.. container:: PRELUDE ROLES
8+
9+
.. role:: ada(code)
10+
:language: Ada
11+
12+
.. role:: C(code)
13+
:language: C
14+
15+
.. role:: cpp(code)
16+
:language: C++
17+
18+
.. container:: PRELUDE SYMBOLS
19+
20+
.. |rightarrow| replace:: :math:`\rightarrow`
21+
.. |forall| replace:: :math:`\forall`
22+
.. |exists| replace:: :math:`\exists`
23+
.. |equivalent| replace:: :math:`\iff`
24+
.. |le| replace:: :math:`\le`
25+
.. |ge| replace:: :math:`\ge`
26+
.. |lt| replace:: :math:`<`
27+
.. |gt| replace:: :math:`>`
28+
.. |checkmark| replace:: :math:`\checkmark`
29+
30+
.. container:: PRELUDE REQUIRES
31+
32+
.. container:: PRELUDE PROVIDES
33+
34+
.. container:: PRELUDE END
35+
36+
.. include:: 245_ravenscar_tasking/01-introduction.rst
37+
.. include:: 245_ravenscar_tasking/02-tasks.rst
38+
.. include:: 245_ravenscar_tasking/03-delays.rst
39+
.. include:: 245_ravenscar_tasking/04-protected_objects.rst
40+
.. include:: 245_ravenscar_tasking/05-differences_from_standard_tasking.rst
41+
.. include:: 245_ravenscar_tasking/06-tasking_behavior.rst
42+
.. include:: 245_ravenscar_tasking/07-tasking_control.rst
43+
.. include:: 245_ravenscar_tasking/99-summary.rst

‎courses/fundamentals_of_ada/245_ravenscar_tasking.rst

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
*******************
2+
Ravenscar Tasking
3+
*******************
4+
5+
.. container:: PRELUDE BEGIN
6+
7+
.. container:: PRELUDE ROLES
8+
9+
.. role:: ada(code)
10+
:language: Ada
11+
12+
.. role:: C(code)
13+
:language: C
14+
15+
.. role:: cpp(code)
16+
:language: C++
17+
18+
.. container:: PRELUDE SYMBOLS
19+
20+
.. |rightarrow| replace:: :math:`\rightarrow`
21+
.. |forall| replace:: :math:`\forall`
22+
.. |exists| replace:: :math:`\exists`
23+
.. |equivalent| replace:: :math:`\iff`
24+
.. |le| replace:: :math:`\le`
25+
.. |ge| replace:: :math:`\ge`
26+
.. |lt| replace:: :math:`<`
27+
.. |gt| replace:: :math:`>`
28+
.. |checkmark| replace:: :math:`\checkmark`
29+
30+
.. container:: PRELUDE REQUIRES
31+
32+
.. container:: PRELUDE PROVIDES
33+
34+
.. container:: PRELUDE END
35+
36+
.. include:: 245_ravenscar_tasking/01-introduction.rst
37+
.. include:: 245_ravenscar_tasking/05-differences_from_standard_tasking.rst
38+
.. include:: 245_ravenscar_tasking/06-tasking_behavior.rst
39+
.. include:: 245_ravenscar_tasking/07-tasking_control.rst
40+
.. include:: 245_ravenscar_tasking/99-summary.rst

‎courses/fundamentals_of_ada/245_ravenscar_tasking/01-introduction.rst

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
==============
2+
Introduction
3+
==============
4+
5+
--------------------------------
6+
What Is the Ravenscar Profile?
7+
--------------------------------
8+
9+
* A **subset** of the Ada tasking model
10+
11+
+ Defined in the RM D.13
12+
13+
* Use concurrency in embedded real-time systems
14+
15+
- Verifiable
16+
- Simple (Implemented reliably and efficiently)
17+
18+
* Scheduling theory for accurate analysis of real-time behavior
19+
* Defined to help meet **safety-critical real-time** requirements
20+
21+
- Determinism
22+
- Schedulability analysis
23+
- Memory-boundedness
24+
- Execution efficiency and small footprint
25+
- Certification
26+
27+
* :ada:`pragma Profile (Ravenscar)`
28+
29+
-----------------------------
30+
What Is the Jorvik profile?
31+
-----------------------------
32+
33+
* A **non-backwards compatible profile** based on Ravenscar
34+
35+
+ Defined in the RM D.13 (Ada 2022)
36+
37+
* Remove some constraints
38+
39+
- Scheduling analysis may be harder to perform
40+
41+
* Subset of Ravenscars' requirements
42+
* This class is about the more widespread Ravenscar
43+
44+
+ But some of Jorvik's differences are indicated
45+
46+
* :ada:`pragma Profile (Jorvik)`
47+
48+
-------------------------
49+
What Are GNAT Runtimes?
50+
-------------------------
51+
52+
* The :dfn:`runtime` is an embedded library
53+
54+
- Executing at run-time
55+
- In charge of standard's library support...
56+
- ...including tasking
57+
58+
* Standard runtime
59+
60+
- Full runtime support
61+
- "Full-fledged" OS target (Linux, WxWorks...)
62+
- Large memory footprint
63+
- Full tasking (not shown in this class)
64+
65+
* Embedded runtime
66+
67+
- Baremetal and RTOS targets
68+
- Reduced memory footprint
69+
- Most of runtime, except I/O and networking
70+
- Ravenscar/Jorvik tasking
71+
72+
* Light runtime
73+
74+
- Baremetal targets
75+
- Very small memory footprint
76+
- Selected, very limited, runtime
77+
- Optional Ravenscar tasking (*Light-tasking* runtime)
78+

‎courses/fundamentals_of_ada/245_ravenscar_tasking/02-tasks.rst

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
=======
2+
Tasks
3+
=======
4+
5+
------------------
6+
Task Declaration
7+
------------------
8+
9+
* Each instance of a task type is executing **concurrently**
10+
* The **whole** tasking setup must be **static**
11+
12+
- Compiler "compiles-in" the scheduling
13+
14+
* Task instances must be declared at the **library level**
15+
16+
- Reminder: :ada:`main` declarative part is **not** at library level
17+
18+
* Body of a task must **never stop**
19+
* Tasks should probably **yield**
20+
21+
- For example with :ada:`delay until`
22+
- Or also a **protected entry guard** (see later)
23+
- Because of **Ravenscar scheduling** (see later)
24+
25+
-------------------------------------
26+
Ravenscar Tasks Declaration Example
27+
-------------------------------------
28+
29+
:filename:`my_tasks.ads`
30+
31+
.. code:: Ada
32+
33+
package My_Tasks is
34+
task type Printer;
35+
36+
P1 : Printer;
37+
P2 : Printer;
38+
end My_Tasks;
39+
40+
:filename:`my_tasks.adb`
41+
42+
.. code:: Ada
43+
44+
with Ada.Text_IO; use Ada.Text_IO;
45+
with Ada.Real_Time; use Ada.Real_Time;
46+
47+
package body My_Tasks is
48+
P3 : Printer; -- correct
49+
50+
task body Printer is
51+
Period : Time_Span := Milliseconds (100);
52+
Next : Time := Clock + Period;
53+
-- P : Printer -- /!\ Would be incorrect: not at library level
54+
begin
55+
loop
56+
Put_Line ("loops");
57+
58+
-- Yielding
59+
delay until Next;
60+
Next := Next + Period;
61+
end loop;
62+
end Printer;
63+
end My_Tasks;
64+

‎courses/fundamentals_of_ada/245_ravenscar_tasking/03-delays.rst

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
======
2+
Delays
3+
======
4+
5+
-------------
6+
Delay Keyword
7+
-------------
8+
9+
- :ada:`delay` keyword part of tasking
10+
- Blocks for a time
11+
- Absolute: Blocks until a given :ada:`Ada.Real_Time.Time`
12+
- Relative: exists, but forbidden in Ravenscar
13+
14+
.. code:: Ada
15+
16+
with Ada.Real_Time; use Ada.Real_Time;
17+
18+
procedure Main is
19+
Next : Time := Clock;
20+
begin
21+
loop
22+
Next := Next + Milliseconds (10);
23+
delay until Next;
24+
end loop;
25+
end Main;
26+

‎courses/fundamentals_of_ada/245_ravenscar_tasking/04-protected_objects.rst

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
===================
2+
Protected Objects
3+
===================
4+
5+
-------------------
6+
Protected Objects
7+
-------------------
8+
9+
* **Multitask-safe** accessors to get and set state
10+
* **No** direct state manipulation
11+
* **No** concurrent modifications
12+
* :ada:`limited` types (No copies allowed)
13+
14+
.. container:: columns
15+
16+
.. container:: column
17+
18+
.. code:: Ada
19+
20+
protected type
21+
Protected_Value is
22+
procedure Set (V : Integer);
23+
function Get return Integer;
24+
private
25+
Value : Integer;
26+
end Protected_Value;
27+
28+
.. container:: column
29+
30+
.. code:: Ada
31+
32+
protected body Protected_Value is
33+
procedure Set (V : Integer) is
34+
begin
35+
Value := V;
36+
end Set;
37+
38+
function Get return Integer is
39+
begin
40+
return Value;
41+
end Get;
42+
end Protected_Value;
43+
44+
.
45+
46+
--------------------------
47+
Misc: Single Declaration
48+
--------------------------
49+
50+
* Instantiate an **anonymous** task (or protected) type
51+
* Declares an object of that type
52+
53+
- Body declaration is then using the **object** name
54+
55+
.. code:: Ada
56+
57+
task Printer;
58+
59+
.. code:: Ada
60+
61+
task body Printer is
62+
begin
63+
loop
64+
Put_Line ("loops");
65+
end loop;
66+
end Printer;
67+
68+
-------------------------------------
69+
Protected: Functions and Procedures
70+
-------------------------------------
71+
72+
* A :ada:`function` can **get** the state
73+
74+
- Protected data is **read-only**
75+
- Concurrent call to :ada:`function` is **allowed**
76+
- **No** concurrent call to :ada:`procedure`
77+
78+
* A :ada:`procedure` can **set** the state
79+
80+
- **No** concurrent call to either :ada:`procedure` or :ada:`function`
81+
82+
* In case of concurrency, other callers get **blocked**
83+
84+
- Until call finishes
85+
86+
-------------------
87+
Protected Entries
88+
-------------------
89+
90+
* A :ada:`entry` is equivalent to a procedure but
91+
92+
- It can have a **guard condition**
93+
94+
+ Must be a **Boolean variable**
95+
+ Declared as :ada:`private` member of the type
96+
97+
- Calling task **blocks** on the guard until it is lifted
98+
99+
+ At most one task blocked (in Ravenscar)
100+
101+
- At most one entry per protected type (in Ravenscar)
102+
103+
.. code:: Ada
104+
105+
protected Blocker is
106+
entry Wait when Ready;
107+
procedure Mark_Ready; -- sets Ready to True
108+
private
109+
Ready : Boolean := False;
110+
end protected;
111+

0 commit comments

Comments
 (0)