.. index:: Ravenscar, concurrency Concurrency and Ravenscar Profile ================================= Concurrency in |SPARK| requires enabling the Ravenscar profile (see `Guide for the use of the Ada Ravenscar Profile in high integrity systems` by Alan Burns, Brian Dobbing, and Tullio Vardanega). This profile defines a subset of the Ada concurrency features suitable for hard real-time/embedded systems requiring stringent analysis, such as certification and safety analyses. In particular, it is concerned with determinism, analyzability, and memory-boundedness. In addition to the subset defined by the Ravenscar profile, concurrency in |SPARK| also requires that tasks do not start executing before the program has been completely elaborated, which is expressed by setting pragma ``Partition_Elaboration_Policy`` to the value ``Sequential``. Together with the requirement to apply the Ravenscar profile, this means that a concurrent |SPARK| program should define the following configuration pragmas, either in a configuration pragma file (see :ref:`Setting the Default SPARK_Mode` for an example of defining a configuration pragma file in your project file) or at the start of files: .. code-block:: ada pragma Profile (Ravenscar); pragma Partition_Elaboration_Policy (Sequential); GNATprove also supports the Jorvik profile, as defined in Ada 2022 RM, D.13. To use this profile simply replace ``Ravenscar`` with ``Jorvik`` in the pragma ``Profile`` in the above code. The extended profile is intended for hard real-time/embedded systems that may require schedulability analysis but not the most stringent analyses required for other domains. In particular, to increase expressive power the Jorvik profile relaxes certain restrictions defined by the standard Ravenscar profile. Notably, these relaxed constraints allow multiple protected entries per protected object, multiple queued callers per entry, and more expressive protected entry barrier expressions. The profile also allows the use of relative delay statements in addition to the absolute delay statements allowed by Ravenscar. The two forms of delay statement are processed by GNATprove based on the type of their expression, as follows (absolute and relative delays, respectively): * If the expression is of the type Ada.Real_Time.Time then for the purposes of determining global inputs and outputs the absolute delay statement is considered just like the relative delay statement, i.e., to reference the state abstraction Ada.Real_Time.Clock_Time as an input (see SPARK RM 9(17) for details). * If the expression is of the type Ada.Calendar.Time then it is considered to reference the state abstraction Ada.Calendar.Clock_Time, which is defined similarly to Ada.Real_Time.Clock_Time but represents a different time base. .. index:: tasking, data race Tasks and Data Races -------------------- [Ravenscar/Jorvik] Concurrent Ada programs are made of several `tasks`, that is, separate threads of control which share the same address space. In Ravenscar, only library-level, nonterminating tasks are allowed. Task Types and Task Objects ^^^^^^^^^^^^^^^^^^^^^^^^^^^ Like ordinary objects, tasks have a type in Ada and can be stored in composite objects such as arrays and records. The definition of a task type looks like the definition of a subprogram. It is made of two parts: a declaration, usually empty as Ravenscar does not allow tasks to have entries (for task rendezvous), and a body containing the list of statements to be executed by objects of the task type. The body of nonterminating tasks (the only ones allowed in Ravenscar) usually takes the form of an infinite loop. For task objects of a given type to be parameterized, task types can have discriminants. As an example, a task type ``Account_Management`` can be declared as follows: .. code-block:: ada package Account is Num_Accounts : Natural := 0; task type Account_Management; end Account; package body Account is task body Account_Management is begin loop Get_Next_Account_Created; Num_Accounts := Num_Accounts + 1; end loop; end Account_Management; end Account; Then, tasks of type ``Account_Management`` can be created at library level, either as complete objects or as components of other objects: .. code-block:: ada package Bank is Special_Accounts : Account_Management; type Account_Type is (Regular, Premium, Selective); type Account_Array is array (Account_Type) of Account_Management; All_Accounts : Account_Array; end Bank; If only one object of a given task type is needed, then the task object can be declared directly giving a declaration and a body. An anonymous task type is then defined implicitly for the declared type object. For example, if we only need one task ``Account_Management`` then we can write: .. code-block:: ada package Account is Num_Accounts : Natural := 0; task Account_Management; end Account; package body Account is task body Account_Management is begin loop Get_Next_Account_Created; Num_Accounts := Num_Accounts + 1; end loop; end Account_Management; end Account; .. index:: protected object; and data races Suspension_Object; and data races Constant_After_Elaboration; and data races Preventing Data Races ^^^^^^^^^^^^^^^^^^^^^ In Ravenscar, communication between tasks can only be done through shared objects (tasks cannot communicate through rendezvous as task entries are not allowed in Ravenscar). In |SPARK|, the language is further restricted to avoid the possibility of erroneous concurrent access to shared data (a.k.a. data races). More precisely, tasks can only share `synchronized` objects, that is, objects that are protected against concurrent accesses. These include atomic objects, protected objects (see :ref:`Protected Objects and Deadlocks`), and suspension objects (see :ref:`Suspension Objects`). As an example, our previous definition of the ``Account_Management`` task type was not in |SPARK|. Indeed, data races could occur when accessing the global variable ``Num_Accounts``, as detected by |GNATprove|: .. literalinclude:: /examples/ug__bank1/test.out :language: none To avoid this problem, shared variable ``Num_Account`` can be declared atomic: .. code-block:: ada package Account is Num_Accounts : Natural := 0 with Atomic; task type Account_Management; end Account; With this modification, |GNATprove| now alerts us that the increment of ``Num_Account`` is not legal, as a volatile variable (which is the case of atomic variables) cannot be read as a subexpression of a larger expression in |SPARK|: .. literalinclude:: /examples/ug__account2/test.out :language: none This can be fixed by copying the current value of ``Num_Account`` in a temporary before the increment: .. code-block:: ada declare Tmp : constant Natural := Num_Accounts; begin Num_Accounts := Tmp + 1; end; But note that even with that fix, there is no guarantee that ``Num_Accounts`` is incremented by one each time an account is created. Indeed, two tasks may read the same value of ``Num_Accounts`` and store this value in ``Tmp`` before both updating it to ``Tmp + 1``. In such a case, two accounts have been created but ``Num_Accounts`` has been increased by 1 only. There is no `data race` in this program, which is confirmed by running |GNATprove| with no error, but there is by design a `race condition` on shared data that causes the program to malfunction. The correct way to fix this in |SPARK| is to use :ref:`Protected Types and Protected Objects`. As they cannot cause data races, constants and variables that are constant after elaboration (see :ref:`Aspect Constant_After_Elaboration`) are considered as synchronized and can be accessed by multiple tasks. For example, we can declare a global constant ``Max_Accounts`` and use it inside ``Account_Management`` without risking data races: .. code-block:: ada package Account is Num_Accounts : Natural := 0 with Atomic; Max_Accounts : constant Natural := 100; task type Account_Management; end Account; package body Account is task body Account_Management is begin loop Get_Next_Account_Created; declare Tmp : constant Natural := Num_Accounts; begin if Tmp < Max_Accounts then Num_Accounts := Tmp + 1; end if; end; end loop; end Account_Management; end Account; .. index:: Part_Of; for concurrency It is possible for a task to access an unsynchronized global variable only if this variable is declared in the same package as the task and if there is a single task accessing this variable. To allow this property to be statically verified, only tasks of an anonymous task type are allowed to access unsynchronized variables and the variables accessed should be declared to belong to the task using aspect ``Part_Of``. Global variables declared to belong to a task are handled just like local variables of the task, that is, they can only be referenced from inside the task body. As an example, we can state that ``Num_Accounts`` is only accessed by the task object ``Account_Management`` in the following way: .. code-block:: ada package Account is task Account_Management; Num_Accounts : Natural := 0 with Part_Of => Account_Management; end Account; Task Contracts -------------- [SPARK] Dependency contracts can be specified on tasks. As tasks should not terminate in |SPARK|, such contracts specify the dependencies between outputs and inputs of the task `updated while the task runs`: * The `data dependencies` introduced by aspect ``Global`` specify the global data read and written by the task. * The `flow dependencies` introduced by aspect ``Depends`` specify how task outputs depend on task inputs. This is a difference between tasks and subprograms, for which such contracts describe the dependencies between outputs and inputs `when the subprogram returns`. .. index:: Global; in task contract Data Dependencies on Tasks ^^^^^^^^^^^^^^^^^^^^^^^^^^ Data dependencies on tasks follow the same syntax as the ones on subprograms (see :ref:`Data Dependencies`). For example, data dependencies can be specified for task (type or object) ``Account_Management`` as follows: .. code-block:: ada package Account is Num_Accounts : Natural := 0 with Atomic; task type Account_Management with Global => (In_Out => Num_Accounts); end Account; .. index:: Depends; in task contract Flow Dependencies on Tasks ^^^^^^^^^^^^^^^^^^^^^^^^^^ Flow dependencies on tasks follow the same syntax as the ones on subprograms (see :ref:`Flow Dependencies`). For example, flow dependencies can be specified for task (type or object) ``Account_Management`` as follows: .. code-block:: ada package Account is Num_Accounts : Natural := 0 with Atomic; task type Account_Management with Depends => (Account_Management => Account_Management, Num_Accounts => Num_Accounts); end Account; Notice that the task unit itself is both an input and an output of the task: * It is an input because task discriminants (if any) and task attributes may be read in the task body. * It is an output so that the task unit may be passed as in out parameter in a subprogram call. But note that the task object cannot be modified once created. The dependency of the task on itself can be left implicit as well, as follows: .. code-block:: ada package Account is Num_Accounts : Natural := 0 with Atomic; task type Account_Management with Depends => (Num_Accounts => Num_Accounts); end Account; .. index:: protected object; and deadlock Protected Objects and Deadlocks ------------------------------- [Ravenscar/Jorvik] In Ada, protected objects are used to encapsulate shared data and protect it against data races (low-level unprotected concurrent access to data) and race conditions (lack of proper synchronization between reads and writes of shared data). They coordinate access to the protected data guaranteeing that read-write accesses are always exclusive while allowing concurrent read-only accesses. In Ravenscar, only library-level protected objects are allowed. Protected Types and Protected Objects ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Definitions of protected types resemble package definitions. They are made of two parts, a declaration (divided into a public part and a private part) and a body. The public part of a protected type's declaration contains the declarations of the subprograms that can be used to access the data declared in its private part. The body of these subprograms are located in the protected type's body. In Ravenscar, protected objects should be declared at library level, either as complete objects or as components of other objects. As an example, here is how a protected type can be used to coordinate concurrent accesses to the global variable ``Num_Accounts``: .. code-block:: ada package Account is protected type Protected_Natural is procedure Incr; function Get return Natural; private The_Data : Natural := 0; end Protected_Natural; Num_Accounts : Protected_Natural; Max_Accounts : constant Natural := 100; task type Account_Management; end Account; package body Account is protected body Protected_Natural is procedure Incr is begin The_Data := The_Data + 1; end Incr; function Get return Natural is (The_Data); end Protected_Natural; task body Account_Management is begin loop Get_Next_Account_Created; if Num_Accounts.Get < Max_Accounts then Num_Accounts.Incr; end if; end loop; end Account_Management; end Account; Contrary to the previous version using an atomic global variable (see :ref:`Preventing Data Races`), this version prevents also any race condition when incrementing the value of ``Num_Accounts``. But note that there is still a possible race condition between the time the value of ``Num_Accounts`` is read and checked to be less than ``Max_Accounts`` and the time it is incremented. So this version does not guarantee that ``Num_Accounts`` stays below ``Max_Accounts``. The correct way to fix this in |SPARK| is to use protected entries (see :ref:`Protected Subprograms`). Note that, in |SPARK|, to avoid initialization issues on protected objects, both private variables and variables belonging to a protected object must be initialized at declaration (either explicitly or through default initialization). Just like for tasks, it is possible to directly declare a protected object if it is the only one of its type. In this case, an anonymous protected type is implicitly declared for it. For example, if ``Num_Account`` is the only ``Protected_Natural`` we need, we can directly declare: .. code-block:: ada package Account is protected Num_Accounts is procedure Incr; function Get return Natural; private The_Data : Natural := 0; end Num_Accounts; end Account; package body Account is protected body Num_Accounts is procedure Incr is begin The_Data := The_Data + 1; end Incr; function Get return Natural is (The_Data); end Num_Accounts; end Account; Protected Subprograms ^^^^^^^^^^^^^^^^^^^^^ The access mode granted by protected subprograms depends on their kind: * Protected procedures provide exclusive read-write access to the private data of a protected object. * Protected functions offer concurrent read-only access to the private data of a protected object. * Protected `entries` are conceptually procedures with a `barrier`. When an entry is called, the caller waits until the condition of the barrier is true to be able to access the protected object. So that scheduling is deterministic, Ravenscar requires that at most one entry is specified in a protected unit and at most one task is waiting on a given entry at every time. To ensure this, |GNATprove| checks that no two tasks can call the same protected object's entry. As an example, we could replace the procedure ``Incr`` of ``Protected_Natural`` to wait until ``The_Data`` is smaller than ``Max_Accounts`` before incrementing it. As only simple Boolean variables are allowed as entry barriers in Ravenscar, we add such a Boolean flag ``Not_Full`` as a component of the protected object: .. code-block:: ada package Account is protected type Protected_Natural is entry Incr; function Get return Natural; private The_Data : Natural := 0; Not_Full : Boolean := True; end Protected_Natural; Num_Accounts : Protected_Natural; Max_Accounts : constant Natural := 100; task type Account_Management; end Account; package body Account is protected body Protected_Natural is entry Incr when Not_Full is begin The_Data := The_Data + 1; if The_Data = Max_Accounts then Not_Full := False; end if; end Incr; function Get return Natural is (The_Data); end Protected_Natural; task body Account_Management is begin loop Get_Next_Account_Created; Num_Accounts.Incr; end loop; end Account_Management; end Account; This version fixes the remaining race condition on this example, thus ensuring that every new account created bumps the value of ``Num_Accounts`` by 1, and that ``Num_Accounts`` stays below ``Max_Accounts``. To avoid data races, protected subprograms should not access unsynchronized objects (see :ref:`Tasks and Data Races`). Like for tasks, it is still possible for subprograms of a protected object of an anonymous protected type to access an unsynchronized object declared in the same package as long as it is not accessed by any task or subprogram from other protected objects. In this case, the unsynchronized object should have a ``Part_Of`` aspect referring to the protected object. It is then handled as if it was a private variable of the protected object. This is typically done so that the address in memory of the variable can be specified, using either aspect ``Address`` or a corresponding representation clause. Here is how this could be done with ``Num_Account``: .. code-block:: ada package Account is protected Protected_Num_Accounts is procedure Incr; function Get return Natural; end Protected_Num_Accounts; Num_Accounts : Natural := 0 with Part_Of => Protected_Num_Accounts, Address => ... end Account; As it can prevent access to a protected object for an unbounded amount of time, a task should not be blocked or delayed while inside a protected subprogram. Actions that can block a task are said to be `potentially blocking`. For example, calling a protected entry, explicitly waiting using a ``delay_until`` statement (note that ``delay`` statements are forbidden in Ravenscar), or suspending on a suspension object (see :ref:`Suspension Objects`) are potentially blocking actions. In Ada, it is an error to do a potentially blocking action while inside a protected subprogram. Note that a call to a function or a procedure on another protected object is not considered to be potentially blocking. Indeed, such a call cannot block a task in the absence of deadlocks (which is enforced in Ravenscar using the priority ceiling protocol, see :ref:`Avoiding Deadlocks and Priority Ceiling Protocol`). |GNATprove| verifies that no potentially blocking action is performed from inside a protected subprogram in a modular way on a per subprogram basis. Thus, if a subprogram can perform a potentially blocking operation, every call to this subprogram from inside a protected subprogram will be flagged as a potential error. As an example, the procedure Incr_Num_Accounts is potentially blocking and thus should not be called, directly or indirectly, from a protected subprogram: .. code-block:: ada package Account is protected type Protected_Natural is entry Incr; private The_Data : Natural := 0; end Protected_Natural; Num_Accounts : Protected_Natural; procedure Incr_Num_Accounts; end Account; package body Account is procedure Incr_Num_Accounts is begin Num_Accounts.Incr; end Incr_Num_Accounts; end Account; Avoiding Deadlocks and Priority Ceiling Protocol ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ To ensure exclusivity of read-write accesses, when a procedure or an entry of a protected object is called, the protected object is locked so that no other task can access it, be it in a read-write or a read-only mode. In the same way, when a protected function is called, no other task can access the protected object in read-write mode. A `deadlock` happens when two or more tasks are unable to run because each of them is trying to access a protected object that is currently locked by another task. To ensure absence of deadlocks on a single core, Ravenscar requires the use of the Priority Ceiling Protocol. This protocol ensures that no task can be blocked trying to access a protected object locked by another task. It relies on task's `priorities`. The priority of a task is a number encoding its urgency. On a single core, scheduling ensures that the current running task can only be preempted by another task if it has a higher priority. Using this property, the Priority Ceiling Protocol works by increasing the priorities of tasks accessing a protected object to a priority that is at least as high as the priorities of other tasks accessing this object. This ensures that, while holding a lock, the currently running task cannot be preempted by a task which could later be blocked by this lock. To enforce this protocol, every task is associated with a `base priority`, either given at declaration using the ``Priority`` aspect or defaulted. This base priority is static and cannot be modified after the task's declaration. A task also has an `active priority` which is initially the task's base priority but will be increased when the task enters a protected action. For example, we can set the base priority of ``Account_Management`` to 5 at declaration: .. code-block:: ada package Account is task type Account_Management with Priority => 5; end Account; Likewise, each protected object is associated at declaration with a `ceiling priority` which should be equal or higher than the active priority of any task accessing it. The ceiling priority of a protected object does not need to be static, it can be set using a discriminant for example. Still, like for tasks, Ravenscar requires that it is set once and for all at the object's declaration and cannot be changed afterwards. As an example, let us attach a ceiling priority to the protected object ``Num_Accounts``. As ``Num_Accounts`` will be used by ``Account_Management``, its ceiling priority should be no lower than 5: .. code-block:: ada package Account is protected Num_Accounts with Priority => 7 is procedure Incr; function Get return Natural; private The_Data : Natural := 0; end Num_Accounts; task type Account_Management with Priority => 5; end Account; .. index:: Suspension_Object Suspension Objects ------------------ [Ravenscar/Jorvik] The language-defined package ``Ada.Synchronous_Task_Control`` provides a type for semaphores called `suspension objects`. They allow lighter synchronization mechanisms than protected objects (see :ref:`Protected Objects and Deadlocks`). More precisely, a suspension object has a Boolean state which can be set atomically to True using the ``Set_True`` procedure. When a task suspends on a suspension object calling the ``Suspend_Until_True`` procedure, it is blocked until the state of the suspension object is True. At that point, the state of the suspension object is set back to False and the task is unblocked. Note that ``Suspend_Until_True`` is potentially blocking and therefore should not be called directly or indirectly from within :ref:`Protected Subprograms`. In the following example, the suspension object ``Semaphore`` is used to make sure ``T1`` has initialized the shared data by the time ``T2`` begins processing it: .. code-block:: ada Semaphore : Suspension_Object; task T1; task T2; task body T1 is begin Initialize_Shared_Data; Set_True (Semaphore); loop ... end loop; end T1; task body T2 is begin Suspend_Until_True (Semaphore); loop ... end loop; end T2; In Ada, an exception is raised if a task tries to suspend on a suspension object on which another task is already waiting on that same suspension object. Like for verifying that no two tasks can be queued on a protected entry, this verification is done by |GNATprove| by checking that no two tasks ever suspend on the same suspension object. In the following example, the suspension objects ``Semaphore1`` and ``Semaphore2`` are used to ensure that ``T1`` and ``T2`` never call ``Enter_Protected_Region`` at the same time. |GNATprove| will successfully verify that only one task can suspend on each suspension object: .. code-block:: ada Semaphore1, Semaphore2 : Suspension_Object; task T1; task T2; task body T1 is begin loop Suspend_Until_True (Semaphore1); Enter_Protected_Region; Set_True (Semaphore2); end loop; end T1; task body T2 is begin loop Suspend_Until_True (Semaphore2); Enter_Protected_Region; Set_True (Semaphore1); end loop; end T2; .. index:: state abstraction; and concurrency External; and concurrency Synchronous_State State Abstraction and Concurrency --------------------------------- [SPARK] Protected objects, as well as suspension objects, are `effectively volatile` which means that their value as seen from a given task may change at any time due to some other task accessing the protected object or suspension object. If they are part of a state abstraction, the volatility of the abstract state must be specified by using the ``External`` aspect (see :ref:`External State Abstraction`). Note that task objects, though they can be part of a package's hidden state, are not effectively volatile and can therefore be components of normal state abstractions. For example, the package ``Synchronous_Abstractions`` defines two abstract states, one for external objects, containing the atomic variable ``V``, the suspension object ``S``, and the protected object ``P``, and one for normal objects, containing the task ``T``: .. code-block:: ada package Synchronous_Abstractions with Abstract_State => (Normal_State, (Synchronous_State with External)) is end Synchronous_Abstractions; package body Synchronous_Abstractions with Refined_State => (Synchronous_State => (P,V,S), Normal_State => T) is task T; S : Suspension_Object; V : Natural := 0 with Atomic, Async_Readers, Async_Writers; protected P is function Read return Natural; private V : Natural := 0; end P; protected body P is function Read return Natural is (V); end P; task body T is ... end Synchronous_Abstractions; To avoid data races, task bodies, as well as protected subprograms, should only access synchronized objects (see :ref:`Preventing Data Races`). State abstractions containing only synchronized objects can be specified to be synchronized using the ``Synchronous`` aspect. Only synchronized state abstractions can be accessed from task bodies and protected subprograms. For example, if we want the procedure ``Do_Something`` to be callable from the task ``Use_Synchronized_State``, then the state abstraction ``Synchronous_State`` must be annotated using the ``Synchronous`` aspect: .. code-block:: ada package Synchronous_Abstractions with Abstract_State => (Normal_State, (Synchronous_State with Synchronous, External)) is procedure Do_Something with Global => (In_Out => Synchronous_State); end Synchronous_Abstractions; task body Use_Synchronized_State is begin loop Synchronous_Abstractions.Do_Something; end loop; end Use_Synchronized_State; Project-wide Tasking Analysis ----------------------------- Tasking-related analysis, as currently implemented in |GNATprove|, is subject to two limitations: First, the analysis is always done when processing a source file with task objects or with a subprogram that can be used as a main subprogram of a partition (i.e. is at library level, has no parameters, and is either a procedure or a function returning an integer type). In effect, you might get spurious checks when: * a subprogram satisfies conditions for being used as a main subprogram of a partition but is not really used that way, i.e. it is not specified in the Main attribute of the GNAT project file you use to build executables, and * it "withs" or is "withed" (directly or indirectly) from a library-level package that declares some task object, and * both the fake "main" subprogram and the task object access the same resource in a way that violates tasking-related rules (e.g. suspends on the same suspension object). As a workaround, either wrap the fake "main" subprogram in a library-level package or give it a dummy parameter. Second, the analysis is only done in the context of all the units "withed" (directly and indirectly) by the currently analyzed source file. In effect, you might miss checks when: * building a library that declares tasks objects in unrelated source files, i.e. files that are never "withed" (directly or indirectly) from the same file, and those tasks objects access the same resource in a way that violates tasking-related rules, or * using a library that internally declares some tasks objects, they access some tasking-sensitive resource, and your main subprogram also accesses this resource. As a workaround, when building library projects add a dummy main subprogram that "withs" all the library-level packages of your project. .. index:: Attach_Handler interrupt handler Interrupt Handlers ------------------ SPARK puts no restrictions on the Ada interrupt handling and GNATprove merely checks that interrupt handlers will be safely executed. In Ada interrupts handlers are defined by annotating protected procedures, for example: .. code-block:: ada with Ada.Interrupts.Names; use Ada.Interrupts.Names; protected P is procedure Signal with Attach_Handler => SIGINT; end P; Currently GNATprove emits a check for each handler declaration saying that the corresponding interrupt might be already reserved. In particular, it might be reserved by either the system or the Ada runtime; see GNAT pragmas Interrupt_State and Unreserve_All_Interrupts for details. Once examined, those checks can be suppressed with pragma Annotate. If pragma Priority or Interrupt_Priority is explicitly specified for a protected type, then GNATprove will check that its value is in the range of the System.Any_Priority or System.Interrupt_Priority, respectively; see Ada RM D.3(6.1/3). For interrupt handlers whose bodies are annotated with SPARK_Mode => On, GNATprove will additionally check that: * the interrupt handler does not call (directly or indirectly) the Ada.Task_Identification.Current_Task routine, which might cause a Program_Error runtime exception; see Ada RM C.7.1(17/3); * all global objects read (either as an Input or a Proof_In) by the interrupt handler are initialized at elaboration; * there are no unsynchronized objects accessed both by the interrupt handler and by some task (or by some other interrupt handler); * there are no protected objects locked both by the interrupt handler and by some task (or by some other interrupt handler).