Slides/194 245 ravenscar tasking into chapters

courses/fundamentals_of_ada/245_ravenscar_tasking-with_tasking_overview.rst

@@ -0,0 +1,43 @@
+*******************
+Ravenscar Tasking
+*******************
+
+.. container:: PRELUDE BEGIN
+
+.. container:: PRELUDE ROLES
+
+.. role:: ada(code)
+    :language: Ada
+
+.. role:: C(code)
+    :language: C
+
+.. role:: cpp(code)
+    :language: C++
+
+.. container:: PRELUDE SYMBOLS
+
+.. |rightarrow| replace:: :math:`\rightarrow`
+.. |forall| replace:: :math:`\forall`
+.. |exists| replace:: :math:`\exists`
+.. |equivalent| replace:: :math:`\iff`
+.. |le| replace:: :math:`\le`
+.. |ge| replace:: :math:`\ge`
+.. |lt| replace:: :math:`<`
+.. |gt| replace:: :math:`>`
+.. |checkmark| replace:: :math:`\checkmark`
+
+.. container:: PRELUDE REQUIRES
+
+.. container:: PRELUDE PROVIDES
+
+.. container:: PRELUDE END
+
+.. include:: 245_ravenscar_tasking/01-introduction.rst
+.. include:: 245_ravenscar_tasking/02-tasks.rst
+.. include:: 245_ravenscar_tasking/03-delays.rst
+.. include:: 245_ravenscar_tasking/04-protected_objects.rst
+.. include:: 245_ravenscar_tasking/05-differences_from_standard_tasking.rst
+.. include:: 245_ravenscar_tasking/06-tasking_behavior.rst
+.. include:: 245_ravenscar_tasking/07-tasking_control.rst
+.. include:: 245_ravenscar_tasking/99-summary.rst

courses/fundamentals_of_ada/245_ravenscar_tasking.rst

@@ -0,0 +1,40 @@
+*******************
+Ravenscar Tasking
+*******************
+
+.. container:: PRELUDE BEGIN
+
+.. container:: PRELUDE ROLES
+
+.. role:: ada(code)
+    :language: Ada
+
+.. role:: C(code)
+    :language: C
+
+.. role:: cpp(code)
+    :language: C++
+
+.. container:: PRELUDE SYMBOLS
+
+.. |rightarrow| replace:: :math:`\rightarrow`
+.. |forall| replace:: :math:`\forall`
+.. |exists| replace:: :math:`\exists`
+.. |equivalent| replace:: :math:`\iff`
+.. |le| replace:: :math:`\le`
+.. |ge| replace:: :math:`\ge`
+.. |lt| replace:: :math:`<`
+.. |gt| replace:: :math:`>`
+.. |checkmark| replace:: :math:`\checkmark`
+
+.. container:: PRELUDE REQUIRES
+
+.. container:: PRELUDE PROVIDES
+
+.. container:: PRELUDE END
+
+.. include:: 245_ravenscar_tasking/01-introduction.rst
+.. include:: 245_ravenscar_tasking/05-differences_from_standard_tasking.rst
+.. include:: 245_ravenscar_tasking/06-tasking_behavior.rst
+.. include:: 245_ravenscar_tasking/07-tasking_control.rst
+.. include:: 245_ravenscar_tasking/99-summary.rst

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

@@ -0,0 +1,78 @@
+==============
+Introduction
+==============
+
+--------------------------------
+What Is the Ravenscar Profile?
+--------------------------------
+
+* A **subset** of the Ada tasking model
+
+  + Defined in the RM D.13
+
+* Use concurrency in embedded real-time systems
+
+   - Verifiable
+   - Simple (Implemented reliably and efficiently)
+
+* Scheduling theory for accurate analysis of real-time behavior
+* Defined to help meet **safety-critical real-time** requirements
+
+   - Determinism
+   - Schedulability analysis
+   - Memory-boundedness
+   - Execution efficiency and small footprint
+   - Certification
+
+* :ada:`pragma Profile (Ravenscar)`
+
+-----------------------------
+What Is the Jorvik profile?
+-----------------------------
+
+* A **non-backwards compatible profile** based on Ravenscar
+
+  + Defined in the RM D.13 (Ada 2022)
+
+* Remove some constraints
+
+  - Scheduling analysis may be harder to perform
+
+* Subset of Ravenscars' requirements
+* This class is about the more widespread Ravenscar
+
+  + But some of Jorvik's differences are indicated
+
+* :ada:`pragma Profile (Jorvik)`
+
+-------------------------
+What Are GNAT Runtimes?
+-------------------------
+
+* The :dfn:`runtime` is an embedded library
+
+  - Executing at run-time
+  - In charge of standard's library support...
+  - ...including tasking
+
+* Standard runtime
+
+  - Full runtime support
+  - "Full-fledged" OS target (Linux, WxWorks...)
+  - Large memory footprint
+  - Full tasking (not shown in this class)
+
+* Embedded runtime
+
+  - Baremetal and RTOS targets
+  - Reduced memory footprint
+  - Most of runtime, except I/O and networking
+  - Ravenscar/Jorvik tasking
+
+* Light runtime
+
+  - Baremetal targets
+  - Very small memory footprint
+  - Selected, very limited, runtime
+  - Optional Ravenscar tasking (*Light-tasking* runtime)
+

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

@@ -0,0 +1,64 @@
+=======
+Tasks
+=======
+
+------------------
+Task Declaration
+------------------
+
+* Each instance of a task type is executing **concurrently**
+* The **whole** tasking setup must be **static**
+
+    - Compiler "compiles-in" the scheduling
+
+* Task instances must be declared at the **library level**
+
+    - Reminder: :ada:`main` declarative part is **not** at library level
+
+* Body of a task must **never stop**
+* Tasks should probably **yield**
+
+    - For example with :ada:`delay until`
+    - Or also a **protected entry guard** (see later)
+    - Because of **Ravenscar scheduling** (see later)
+
+-------------------------------------
+Ravenscar Tasks Declaration Example
+-------------------------------------
+
+:filename:`my_tasks.ads`
+
+.. code:: Ada
+
+    package My_Tasks is
+        task type Printer;
+
+        P1 : Printer;
+        P2 : Printer;
+    end My_Tasks;
+
+:filename:`my_tasks.adb`
+
+.. code:: Ada
+
+    with Ada.Text_IO; use Ada.Text_IO;
+    with Ada.Real_Time; use Ada.Real_Time;
+
+    package body My_Tasks is
+        P3 : Printer; --  correct
+
+        task body Printer is
+            Period : Time_Span := Milliseconds (100);
+            Next : Time := Clock + Period;
+            -- P : Printer -- /!\ Would be incorrect: not at library level
+        begin
+            loop
+                Put_Line ("loops");
+
+                --  Yielding
+                delay until Next;
+                Next := Next + Period;
+            end loop;
+        end Printer;
+    end My_Tasks;
+

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

@@ -0,0 +1,26 @@
+======
+Delays
+======
+
+-------------
+Delay Keyword
+-------------
+
+- :ada:`delay` keyword part of tasking
+- Blocks for a time
+- Absolute: Blocks until a given :ada:`Ada.Real_Time.Time`
+- Relative: exists, but forbidden in Ravenscar
+
+.. code:: Ada
+
+    with Ada.Real_Time; use Ada.Real_Time;
+
+    procedure Main is
+        Next : Time := Clock;
+    begin
+        loop
+            Next := Next + Milliseconds (10);
+            delay until Next;
+        end loop;
+    end Main;
+

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

@@ -0,0 +1,111 @@
+===================
+Protected Objects
+===================
+
+-------------------
+Protected Objects
+-------------------
+
+* **Multitask-safe** accessors to get and set state
+* **No** direct state manipulation
+* **No** concurrent modifications
+* :ada:`limited` types (No copies allowed)
+
+.. container:: columns
+
+ .. container:: column
+
+  .. code:: Ada
+
+   protected type
+     Protected_Value is
+      procedure Set (V : Integer);
+      function Get return Integer;
+   private
+      Value : Integer;
+   end Protected_Value;
+
+ .. container:: column
+
+  .. code:: Ada
+
+   protected body Protected_Value is
+      procedure Set (V : Integer) is
+      begin
+         Value := V;
+      end Set;
+
+      function Get return Integer is
+      begin
+         return Value;
+      end Get;
+   end Protected_Value;
+
+.
+
+--------------------------
+Misc: Single Declaration
+--------------------------
+
+ * Instantiate an **anonymous** task (or protected) type
+ * Declares an object of that type
+
+    - Body declaration is then using the **object** name
+
+ .. code:: Ada
+
+   task Printer;
+
+.. code:: Ada
+
+   task body Printer is
+   begin
+      loop
+        Put_Line ("loops");
+      end loop;
+   end Printer;
+
+-------------------------------------
+Protected: Functions and Procedures
+-------------------------------------
+
+* A :ada:`function` can **get** the state
+
+   - Protected data is **read-only**
+   - Concurrent call to :ada:`function` is **allowed**
+   - **No** concurrent call to :ada:`procedure`
+
+* A :ada:`procedure` can **set** the state
+
+   - **No** concurrent call to either :ada:`procedure` or :ada:`function`
+
+* In case of concurrency, other callers get **blocked**
+
+    - Until call finishes
+
+-------------------
+Protected Entries
+-------------------
+
+* A :ada:`entry` is equivalent to a procedure but
+
+   - It can have a **guard condition**
+
+       + Must be a **Boolean variable**
+       + Declared as :ada:`private` member of the type
+
+   - Calling task **blocks** on the guard until it is lifted
+
+       + At most one task blocked (in Ravenscar)
+
+   - At most one entry per protected type (in Ravenscar)
+
+.. code:: Ada
+
+    protected Blocker is
+        entry Wait when Ready;
+        procedure Mark_Ready; --  sets Ready to True
+    private
+        Ready : Boolean := False;
+    end protected;
+