------------------------------------------------------------------------------ ------------------------------------------------------------------------------ -- Cheddar is a GNU GPL real-time scheduling analysis tool. -- This program provides services to automatically check schedulability and -- other performance criteria of real-time architecture models. -- -- Copyright (C) 2002-2020, Frank Singhoff, Alain Plantec, Jerome Legrand, -- Hai Nam Tran, Stephane Rubini -- -- The Cheddar project was started in 2002 by -- Frank Singhoff, Lab-STICC UMR CNRS 6285, Universite de Bretagne Occidentale -- -- Cheddar has been published in the "Agence de Protection des Programmes/France" in 2008. -- Since 2008, Ellidiss technologies also contributes to the development of -- Cheddar and provides industrial support. -- -- The full list of contributors and sponsors can be found in AUTHORS.txt and SPONSORS.txt -- -- This program is free software; you can redistribute it and/or modify -- it under the terms of the GNU General Public License as published by -- the Free Software Foundation; either version 2 of the License, or -- (at your option) any later version. -- -- This program is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -- GNU General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with this program; if not, write to the Free Software -- Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA -- -- -- Contact : cheddar@listes.univ-brest.fr -- ------------------------------------------------------------------------------ -- Last update : -- $Rev$ -- $Date$ -- $Author: singhoff $ ------------------------------------------------------------------------------ ------------------------------------------------------------------------------ with systems; use systems; with processors; use processors; with processor_set; use processor_set; with processor_interface; use processor_interface; with scheduler_interface; use scheduler_interface; with scheduler.user_defined.interpreted; use scheduler.user_defined.interpreted; with scheduler_interface; use scheduler_interface; with core_units; use core_units; use core_units.core_units_table_package; with tasks; use tasks; with task_set; use task_set; use task_set.generic_task_set; with Text_IO; use Text_IO; with dependencies; use dependencies; with task_dependencies; use task_dependencies; with framework_config; use framework_config; use task_dependencies.half_dep_set; with ada.exceptions; use ada.exceptions; with Ada.Real_Time; use Ada.Real_Time; with Ada.Calendar; with Ada.Calendar.Formatting; with Ada.Text_IO; use Ada.Text_IO; with Ada.Integer_Text_IO; use Ada.Integer_Text_IO; package body scheduling_anomalies_services is --------------------------------------------------------------------------------- function get_scheduler(a_core : core_unit_ptr) return schedulers_type is a_sched : schedulers_type := no_scheduling_protocol; ok : boolean:=true; begin if (a_core.scheduling.scheduler_type=pipeline_user_defined_protocol) then to_schedulers_type(To_Unbounded_String("toto"), a_sched, ok); if not ok then Raise_Exception (processor_set.invalid_parameter'identity, " invalid value for user_defined_scheduler_protocol_name"); end if; return a_sched; else return a_core.scheduling.scheduler_type; end if; end get_scheduler; -- Store the architecture model before simulation -- initial_model : system; -- Store if the initial mode is compliant with static constraints for each anomaly -- static_processor_speed_increase : boolean :=false; static_precedence_constraint_change : boolean :=false; static_task_execution_time_decrease : boolean :=true; static_processor_add : boolean :=false; static_task_period_increase : boolean :=false; static_task_late_execution : boolean :=false; static_task_priority_change : boolean :=false; procedure initialize(model : in system) is begin initial_model:=model; -- Check static constraint on the architecture model static_task_execution_time_decrease := check_static_task_execution_time_decrease(initial_model); static_processor_speed_increase:= check_static_processor_speed_increase(initial_model); static_processor_add:=check_static_processor_add(initial_model); static_task_period_increase :=check_static_task_period_increase(initial_model); static_task_late_execution :=check_static_task_late_execution(initial_model); static_task_priority_change :=check_static_task_priority_change(initial_model); static_precedence_constraint_change :=check_static_precedence_constraint_change(initial_model); end initialize; procedure dynamically_check_anomaly (inp : in handler_input_parameter; current_scheduler : in generic_scheduler'class; outp : out handler_output_parameter) is begin case inp.event.type_of_event is -- report the end of task capacity when end_of_task_capacity => Put_Line("begin of end_of_task_capacity "); check_dynamic_task_execution_time_decrease(inp,outp); Put_Line("end of end_of_task_capacity "); -- report the start of the task execution when start_of_task_capacity => Put_Line("begin of start_of_task_capacity "); check_dynamic_task_execution_time_decrease(inp,outp); check_dynamic_task_period_increase(inp,outp); check_dynamic_task_priority_change(inp,outp); check_dynamic_precedence_constraint_change(inp,outp); check_dynamic_processor_add(inp,outp); check_dynamic_task_late_execution(inp,outp); Put_Line("end of start_of_task_capacity "); -- report the activation of a task when task_activation => Put_Line("begin of task_activation "); check_dynamic_task_execution_time_decrease(inp,outp); check_dynamic_task_period_increase(inp,outp); check_dynamic_task_priority_change(inp,outp); check_dynamic_precedence_constraint_change(inp,outp); check_dynamic_processor_add(inp,outp); check_dynamic_processor_speed_increase(inp,current_scheduler,outp); Put_Line("end of task_activation "); -- report the execution of a task during a time unit when running_task => Put_Line("begin of running_task "); check_dynamic_task_execution_time_decrease(inp,outp); check_dynamic_task_period_increase(inp,outp); check_dynamic_task_priority_change(inp,outp); check_dynamic_precedence_constraint_change(inp,outp); check_dynamic_processor_speed_increase(inp,current_scheduler,outp); Put_Line("begin of running_task "); when others => null; end case; end dynamically_check_anomaly; --------------------------------------------------------------------------------- -- verify if an anomaly occur when a task is activate procedure check_dynamic_processor_speed_increase (inp : in handler_input_parameter; current_scheduler : in generic_scheduler'class ; outp : out handler_output_parameter) is a_core_unit : Core_Unit_Ptr; my_core_iterator : core_units_iterator; my_processor_iterator: processors_iterator; my_processor:Generic_Processor_Ptr; result : Boolean := False; begin -- check if the static constraint is verify before loooking for the anomaly if (static_processor_speed_increase) then reset_iterator (initial_model.processors, my_processor_iterator); reset_iterator (initial_model.core_units, my_core_iterator); loop current_element (initial_model.processors, my_processor, my_processor_iterator); current_element (initial_model.core_units, a_core_unit, my_core_iterator); -- check if the system is a monoprocessor or not if (my_processor.processor_type = monocore_type) then result := True; -- check if the speed of the core have been increase if (a_core_unit.speed < current_scheduler.corresponding_core_unit.speed) then outp.detected_anomaly := processor_speed_increase; end if; else if (a_core_unit.name = current_scheduler.corresponding_core_unit.name) and (a_core_unit.speed < current_scheduler.corresponding_core_unit.speed) then outp.detected_anomaly := processor_speed_increase; exit; end if; end if; exit when ((is_last_element (initial_model.processors, my_processor_iterator)) or (is_last_element (initial_model.core_units, my_core_iterator)) or (result = True)); next_element (initial_model.processors, my_processor_iterator); next_element (initial_model.core_units, my_core_iterator); end loop; else outp.detected_anomaly:=no_potential_anomaly; end if; end check_dynamic_processor_speed_increase; procedure check_dynamic_processor_add (inp : in handler_input_parameter; outp : out handler_output_parameter) is -- position: tasks_range; begin if (static_processor_add) then outp.detected_anomaly := processor_add; else outp.detected_anomaly := no_potential_anomaly; end if; -- null; end check_dynamic_processor_add; procedure check_dynamic_task_execution_time_decrease (inp : in handler_input_parameter; outp : out handler_output_parameter) is position: tasks_range; iterator1: tasks_iterator; my_task: Generic_Task_Ptr; begin -- null; if (static_task_execution_time_decrease) then case inp.event.type_of_event is -- save the current task at the end of its execution when end_of_task_capacity => for i in 0 .. inp.runtime_data.number_of_tasks - 1 loop if (inp.event.end_task.name = inp.runtime_data.tcbs(i).tsk.name) then position := i; end if; end loop; -- save the current task at the start of its execution when start_of_task_capacity => for i in 0 .. inp.runtime_data.number_of_tasks - 1 loop if (inp.event.start_task.name = inp.runtime_data.tcbs(i).tsk.name) then position := i; end if; end loop; -- save the current task at its activation when task_activation => for i in 0 .. inp.runtime_data.number_of_tasks - 1 loop if (inp.event.activation_task.name = inp.runtime_data.tcbs(i).tsk.name) then position := i; end if; end loop; -- save the current task during its execution when running_task => for i in 0 .. inp.runtime_data.number_of_tasks - 1 loop if (inp.event.running_task.name = inp.runtime_data.tcbs(i).tsk.name) then position := i; end if; end loop; when others => null; end case; -- recover the initial system reset_iterator(initial_model.tasks, iterator1); -- find the active task of the system loop current_element (initial_model.tasks, my_task, iterator1); if (my_task.name = inp.runtime_data.tcbs(position).tsk.name) then exit; end if; exit when is_last_element (initial_model.tasks, iterator1); next_element (initial_model.tasks, iterator1); end loop; -- check if its capacity have been reduce -- put_line("capacity of the initial system of the task: "& To_String(my_task.name)&" is : " & my_task.capacity'img); -- put_line("task capacity of runtime task : "& To_String(inp.runtime_data.tcbs(position).tsk.name)&" is : "& inp.runtime_data.tcbs(position).tsk.capacity'img); -- put_line("rest_of_capacity : "& To_String(inp.runtime_data.tcbs(position).tsk.name)&" is : "& inp.runtime_data.tcbs(position).rest_of_capacity'img); -- put_line("used_capacity of runtime task : "& To_String(inp.runtime_data.tcbs(position).tsk.name)&" is : "& inp.runtime_data.tcbs(position).used_capacity'img); -- Put_Line("the position of the task is :"& position'img); if ( my_task.capacity > inp.runtime_data.tcbs(position).tsk.capacity) then outp.detected_anomaly:=task_execution_time_decrease; put_line("THE CAPACITY OF TASK " & To_String(inp.runtime_data.tcbs(position).tsk.name) & " HAVE BEEN REDUCE AND CAN MAKE THE SYSTEM NOT SCHEDULABLE"); -- else -- put_line("dans le sinon du test de la reduction de capacité"); end if; else outp.detected_anomaly := no_potential_anomaly; end if; end check_dynamic_task_execution_time_decrease; procedure check_dynamic_task_period_increase (inp : in handler_input_parameter; outp : out handler_output_parameter) is position: tasks_range; iterator1: tasks_iterator; my_task: Generic_Task_Ptr; begin -- null; if (static_task_period_increase ) then case inp.event.type_of_event is -- save the current task at the end of its execution when end_of_task_capacity => for i in 0 .. inp.runtime_data.number_of_tasks - 1 loop if (inp.event.end_task.name = inp.runtime_data.tcbs(i).tsk.name) then position := i; end if; end loop; -- save the current task at the start of its execution when start_of_task_capacity => for i in 0 .. inp.runtime_data.number_of_tasks - 1 loop if (inp.event.start_task.name = inp.runtime_data.tcbs(i).tsk.name) then position := i; end if; end loop; -- save the current task at its activation when task_activation => for i in 0 .. inp.runtime_data.number_of_tasks - 1 loop if (inp.event.activation_task.name = inp.runtime_data.tcbs(i).tsk.name) then position := i; end if; end loop; -- save the current task during its execution when running_task => for i in 0 .. inp.runtime_data.number_of_tasks - 1 loop if (inp.event.running_task.name = inp.runtime_data.tcbs(i).tsk.name) then position := i; end if; end loop; when others => null; end case; -- recover the initial system reset_iterator(initial_model.tasks, iterator1); -- find the active task of the system loop current_element (initial_model.tasks, my_task, iterator1); if (my_task.name = inp.runtime_data.tcbs(position).tsk.name) then exit; end if; exit when is_last_element (initial_model.tasks, iterator1); next_element (initial_model.tasks, iterator1); end loop; -- check if the task period has been increased if(Periodic_Task_ptr(my_task).period < Periodic_task_ptr(inp.runtime_data.tcbs(position).tsk).period) then outp.detected_anomaly:=task_period_increase; end if; else outp.detected_anomaly := no_potential_anomaly; end if; end check_dynamic_task_period_increase; procedure check_dynamic_task_late_execution (inp : in handler_input_parameter; outp : out handler_output_parameter) is begin null; end check_dynamic_task_late_execution; procedure check_dynamic_task_priority_change (inp : in handler_input_parameter; outp : out handler_output_parameter) is position: tasks_range; iterator1: tasks_iterator; my_task: Generic_Task_Ptr; begin --null; if(static_task_priority_change) then case inp.event.type_of_event is -- save the current task at the end of its execution when end_of_task_capacity => for i in 0 .. inp.runtime_data.number_of_tasks - 1 loop if (inp.event.end_task.name = inp.runtime_data.tcbs(i).tsk.name) then position := i; end if; end loop; -- save the current task at the start of its execution when start_of_task_capacity => for i in 0 .. inp.runtime_data.number_of_tasks - 1 loop if (inp.event.start_task.name = inp.runtime_data.tcbs(i).tsk.name) then position := i; end if; end loop; -- save the current task at its activation when task_activation => for i in 0 .. inp.runtime_data.number_of_tasks - 1 loop if (inp.event.activation_task.name = inp.runtime_data.tcbs(i).tsk.name) then position := i; end if; end loop; -- save the current task during its execution when running_task => for i in 0 .. inp.runtime_data.number_of_tasks - 1 loop if (inp.event.running_task.name = inp.runtime_data.tcbs(i).tsk.name) then position := i; end if; end loop; when others => null; end case; -- recover the initial system reset_iterator(initial_model.tasks, iterator1); -- find the active task of the system loop current_element (initial_model.tasks, my_task, iterator1); if (my_task.name = inp.runtime_data.tcbs(position).tsk.name) then exit; end if; exit when is_last_element (initial_model.tasks, iterator1); next_element (initial_model.tasks, iterator1); end loop; -- check if the priority of the task have been changed if(my_task.priority /= inp.runtime_data.tcbs(position).tsk.priority) then outp.detected_anomaly:=task_priority_change; end if; else outp.detected_anomaly := no_potential_anomaly; end if; end check_dynamic_task_priority_change; procedure check_dynamic_precedence_constraint_change (inp : in handler_input_parameter; outp : out handler_output_parameter) is my_dependencies, my_dependencies_initial : tasks_dependencies_ptr; my_iterator_initial, my_iterator : tasks_dependencies_iterator; a_half_dep, a_half_dep_initial : dependency_ptr; begin -- null; -- check if some precedence constraint have been delete if (static_precedence_constraint_change) then my_dependencies_initial := initial_model.dependencies; my_dependencies:=inp.runtime_data.dependencies; if is_Empty(my_dependencies_initial.depends) then Put_Line("no precedence constraint in the initial system"); outp.detected_anomaly:=no_potential_anomaly; else Put_Line("there is an precedence constraint in the inital system"); if is_empty(my_dependencies.depends) then Put_Line("the precedence constraint have been delete and that can make the systeme not schedulable"); outp.detected_anomaly:=precedence_constraint_change; else reset_iterator (my_dependencies_initial.depends, my_iterator_initial); reset_iterator (my_dependencies.depends, my_iterator); loop current_element(my_dependencies_initial.depends,a_half_dep_initial, my_iterator_initial); current_element(my_dependencies.depends,a_half_dep,my_iterator); if (a_half_dep_initial.type_of_dependency /= a_half_dep.type_of_dependency) then outp.detected_anomaly:=precedence_constraint_change; end if; exit when (is_last_element (my_dependencies.depends, my_iterator)) or (is_last_element(my_dependencies_initial.depends, my_iterator_initial)); next_element (my_dependencies.depends, my_iterator); next_element(my_dependencies_initial.depends, my_iterator_initial); end loop; end if; end if; else outp.detected_anomaly := no_potential_anomaly; end if; end check_dynamic_precedence_constraint_change; ----------------------------------------------------------------------------------- function check_c1_mono_processor_system (a_system : in system) return Boolean is iterator1 : processors_iterator; processor1 : generic_processor_ptr; --Monoprocessor1 : Mono_Core_Processor_Ptr; result : Boolean := True; begin reset_iterator (a_system.processors, iterator1); loop current_element (a_system.processors, processor1, iterator1); if (processor1.processor_type /= monocore_type) then result := False; end if; exit when ((is_last_element (a_system.processors, iterator1)) or (result = False)); next_element (a_system.processors, iterator1); end loop; return result; end check_c1_mono_processor_system; ----------------------------------------------------------------------------------------------- function check_c2_multiprocessor_system (a_system : in system) return Boolean is begin return not check_c1_mono_processor_system (a_system); end check_c2_multiprocessor_system; ------------------------------------------------------------------- function check_c3_partitionned_scheduling (a_system : in system) return Boolean is iterator1 : processors_iterator; processor1 : generic_processor_ptr; result : Boolean := True; begin reset_iterator (a_system.processors, iterator1); loop current_element (a_system.processors, processor1, iterator1); if (processor1.migration_type /= no_migration_type) then result := False; end if; exit when is_last_element (a_system.processors, iterator1); next_element (a_system.processors, iterator1); end loop; return result; end check_c3_partitionned_scheduling; -------------------------------------------------------------------- function check_c4_global_scheduling (a_system : in system) return Boolean is iterator1 : processors_iterator; processor1 : generic_processor_ptr; result : Boolean := True; begin reset_iterator (a_system.processors, iterator1); loop current_element (a_system.processors, processor1, iterator1); if (not check_c2_multiprocessor_system (a_system)) then result := False; end if; exit when is_last_element (a_system.processors, iterator1); next_element (a_system.processors, iterator1); end loop; return result; end check_c4_global_scheduling; -------------------------------------------------------------------- function check_c5_fixed_priority (a_system : in system) return Boolean is iterator1 : processors_iterator; processor1 : generic_processor_ptr; monoprocessor1 : mono_core_processor_ptr; multiprocessor1 : multi_cores_processor_ptr; result : Boolean := True; begin reset_iterator (a_system.processors, iterator1); loop current_element (a_system.processors, processor1, iterator1); if (check_c1_mono_processor_system (a_system)) then monoprocessor1 := mono_core_processor_ptr (processor1); if (get_scheduler(monoprocessor1.core)/= rate_monotonic_protocol) and (get_scheduler(monoprocessor1.core)/= posix_1003_highest_priority_first_protocol) and (get_scheduler(monoprocessor1.core)/= deadline_monotonic_protocol) then result := False; end if; else multiprocessor1 := multi_cores_processor_ptr (processor1); for i in 0 .. multiprocessor1.cores.nb_entries - 1 loop if (get_scheduler(multiprocessor1.cores.entries (i)) /= rate_monotonic_protocol) and (get_scheduler(multiprocessor1.cores.entries (i)) /= posix_1003_highest_priority_first_protocol) and (get_scheduler(multiprocessor1.cores.entries (i)) /= deadline_monotonic_protocol) then result := False; end if; end loop; end if; exit when is_last_element (a_system.processors, iterator1); next_element (a_system.processors, iterator1); end loop; return result; end check_c5_fixed_priority; -------------------------------------------------------------------- function check_c6_edf_algorithm (a_system : in system) return Boolean is iterator1 : processors_iterator; processor1 : generic_processor_ptr; monoprocessor1 : mono_core_processor_ptr; multiprocessor1 : multi_cores_processor_ptr; result : Boolean := True; begin reset_iterator (a_system.processors, iterator1); loop current_element (a_system.processors, processor1, iterator1); if (check_c1_mono_processor_system (a_system)) then monoprocessor1 := mono_core_processor_ptr (processor1); if (get_scheduler(monoprocessor1.core) /= earliest_deadline_first_protocol) then result := False; end if; else multiprocessor1 := multi_cores_processor_ptr (processor1); for i in 0 .. multiprocessor1.cores.nb_entries - 1 loop if (get_scheduler(multiprocessor1.cores.entries (i)) /= earliest_deadline_first_protocol) then result := False; end if; end loop; end if; exit when is_last_element (a_system.processors, iterator1); next_element (a_system.processors, iterator1); end loop; return result; end check_c6_edf_algorithm; -------------------------------------------------------------------- function check_c7_dm_algorithm (a_system : in system) return Boolean is iterator1 : processors_iterator; processor1 : generic_processor_ptr; monoprocessor1 : mono_core_processor_ptr; multiprocessor1 : multi_cores_processor_ptr; result : Boolean := True; begin reset_iterator (a_system.processors, iterator1); loop current_element (a_system.processors, processor1, iterator1); if (check_c1_mono_processor_system (a_system)) then monoprocessor1 := mono_core_processor_ptr (processor1); if (get_scheduler(monoprocessor1.core) /= deadline_monotonic_protocol) then result := False; end if; else multiprocessor1 := multi_cores_processor_ptr (processor1); for i in 0 .. multiprocessor1.cores.nb_entries - 1 loop if (get_scheduler(multiprocessor1.cores.entries (i)) /= deadline_monotonic_protocol) then result := False; end if; end loop; end if; exit when is_last_element (a_system.processors, iterator1); next_element (a_system.processors, iterator1); end loop; return result; end check_c7_dm_algorithm; -------------------------------------------------------------------- function check_c8_preemptive_processor (a_system : in system) return Boolean is iterator1 : processors_iterator; processor1 : generic_processor_ptr; monoprocessor1 : mono_core_processor_ptr; multiprocessor1 : multi_cores_processor_ptr; result : Boolean := True; begin reset_iterator (a_system.processors, iterator1); loop current_element (a_system.processors, processor1, iterator1); if (check_c1_mono_processor_system (a_system)) then monoprocessor1 := mono_core_processor_ptr (processor1); if (monoprocessor1.core.scheduling.preemptive_type /= preemptive) then result := False; end if; else multiprocessor1 := multi_cores_processor_ptr (processor1); for i in 0 .. multiprocessor1.cores.nb_entries - 1 loop if (multiprocessor1.cores.entries (i).scheduling .preemptive_type /= preemptive) then result := False; end if; end loop; end if; exit when is_last_element (a_system.processors, iterator1); next_element (a_system.processors, iterator1); end loop; return result; end check_c8_preemptive_processor; -------------------------------------------------------------------- function check_c9_non_preemptive_processor (a_system : in system) return Boolean is begin return not check_c8_preemptive_processor (a_system); end check_c9_non_preemptive_processor; -------------------------------------------------------------------- function check_c10_synchronous_departure (a_system : in system) return Boolean is iterator1 : tasks_iterator; task1, task0 : generic_task_ptr; result : Boolean := True; begin reset_iterator (a_system.tasks, iterator1); current_element (a_system.tasks, task0, iterator1); loop current_element (a_system.tasks, task1, iterator1); if (task1.start_time /= task0.start_time) then result := False; end if; exit when is_last_element (a_system.tasks, iterator1); next_element (a_system.tasks, iterator1); end loop; return result; end check_c10_synchronous_departure; -------------------------------------------------------------------- function check_c11_asynchronous_departure (a_system : in system) return Boolean is begin return not check_c10_synchronous_departure (a_system); end check_c11_asynchronous_departure; -------------------------------------------------------------------- function check_c12_tasks_are_periodic (a_system : in system) return Boolean is iterator1 : tasks_iterator; task1 : generic_task_ptr; result : Boolean := True; begin reset_iterator (a_system.tasks, iterator1); loop current_element (a_system.tasks, task1, iterator1); if (task1.task_type /= periodic_type) then result := False; end if; exit when is_last_element (a_system.tasks, iterator1); next_element (a_system.tasks, iterator1); end loop; return result; end check_c12_tasks_are_periodic; -------------------------------------------------------------------- function check_c13_tasks_are_independent (a_system : in system) return Boolean is my_dependencies : tasks_dependencies_ptr; result : Boolean := True; begin my_dependencies := a_system.dependencies; if not is_empty (my_dependencies.depends) then result := False; end if; return result; end check_c13_tasks_are_independent; -------------------------------------------------------------------- function check_c14_tasks_are_suspended (a_system : in system) return Boolean is result : Boolean := False; begin null; return result; end check_c14_tasks_are_suspended; -------------------------------------------------------------------- function check_c15_tasks_have_precedence_constraint (a_system : in system) return Boolean is my_dependencies : tasks_dependencies_ptr; my_iterator1 : tasks_dependencies_iterator; a_half_dep : dependency_ptr; result : Boolean := True; begin my_dependencies := a_system.dependencies; if not is_empty (my_dependencies.depends) then reset_iterator (my_dependencies.depends, my_iterator1); loop current_element (my_dependencies.depends, a_half_dep, my_iterator1); if (a_half_dep.type_of_dependency /= precedence_dependency) then result := False; end if; exit when is_last_element (my_dependencies.depends, my_iterator1); next_element (my_dependencies.depends, my_iterator1); end loop; else result := False; end if; return result; end check_c15_tasks_have_precedence_constraint; -------------------------------------------------------------------- function check_c16_tasks_have_shared_resouces (a_system : in system) return Boolean is my_dependencies : tasks_dependencies_ptr; my_iterator1 : tasks_dependencies_iterator; a_half_dep : dependency_ptr; result : Boolean := True; begin my_dependencies := a_system.dependencies; if not is_empty (my_dependencies.depends) then reset_iterator (my_dependencies.depends, my_iterator1); loop current_element (my_dependencies.depends, a_half_dep, my_iterator1); if (a_half_dep.type_of_dependency /= resource_dependency) then result := False; end if; exit when is_last_element (my_dependencies.depends, my_iterator1); next_element (my_dependencies.depends, my_iterator1); end loop; else result := False; end if; return result; end check_c16_tasks_have_shared_resouces; -------------------------------------------------------------------- function check_c17_tasks_are_aperiodic (a_system : in system) return Boolean is iterator1 : tasks_iterator; task1 : generic_task_ptr; result : Boolean := True; begin reset_iterator (a_system.tasks, iterator1); loop current_element (a_system.tasks, task1, iterator1); if (task1.task_type /= aperiodic_type) then result := False; end if; exit when is_last_element (a_system.tasks, iterator1); next_element (a_system.tasks, iterator1); end loop; return result; end check_c17_tasks_are_aperiodic; -------------------------------------------------------------------------------- function check_static_processor_speed_increase (a_system : in system) return Boolean is --C1, C3, C5, C8, C11, C12, C16 --C1, C3, C5, C9, C11, C12, C13 begin return (check_c1_mono_processor_system (a_system) and check_c3_partitionned_scheduling (a_system) and check_c5_fixed_priority (a_system) and check_c8_preemptive_processor (a_system) and check_c11_asynchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c16_tasks_have_shared_resouces (a_system)) or (check_c1_mono_processor_system (a_system) and check_c3_partitionned_scheduling (a_system) and check_c5_fixed_priority (a_system) and check_c9_non_preemptive_processor (a_system) and check_c11_asynchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c13_tasks_are_independent (a_system)); end check_static_processor_speed_increase; -------------------------------------------------------------------------- function check_static_task_execution_time_decrease (a_system : in system) return Boolean is --C1, C3, C5, C10, C12, C15 --C1, C3, C5, C9, C10, C12, C13 --C1, C3, C7, C8, C10, C12, C16 --C1, C3, C6, C8, C11, C12,C13, C14 --C2, C4,C5, C8, C11, C12, C13, C17 --C2, C3, C5, C9, C10, C12, C16 --C2, C4, C5, C9, C10, C12, C15 begin return (check_c1_mono_processor_system (a_system) and check_c3_partitionned_scheduling (a_system) and check_c5_fixed_priority (a_system) and check_c10_synchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c15_tasks_have_precedence_constraint (a_system)) or (check_c1_mono_processor_system (a_system) and check_c3_partitionned_scheduling (a_system) and check_c5_fixed_priority (a_system) and check_c9_non_preemptive_processor (a_system) and check_c10_synchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c13_tasks_are_independent (a_system)) or (check_c1_mono_processor_system (a_system) and check_c3_partitionned_scheduling (a_system) and check_c7_dm_algorithm (a_system) and check_c8_preemptive_processor (a_system) and check_c10_synchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c16_tasks_have_shared_resouces (a_system)) or (check_c1_mono_processor_system (a_system) and check_c3_partitionned_scheduling (a_system) and check_c6_edf_algorithm (a_system) and check_c8_preemptive_processor (a_system) and check_c11_asynchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c13_tasks_are_independent (a_system) and check_c14_tasks_are_suspended (a_system)) or (check_c2_multiprocessor_system (a_system) and check_c4_global_scheduling (a_system) and check_c5_fixed_priority (a_system) and check_c8_preemptive_processor (a_system) and check_c11_asynchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c13_tasks_are_independent (a_system) and check_c17_tasks_are_aperiodic (a_system)) or (check_c2_multiprocessor_system (a_system) and check_c3_partitionned_scheduling (a_system) and check_c5_fixed_priority (a_system) and check_c9_non_preemptive_processor (a_system) and check_c10_synchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c16_tasks_have_shared_resouces (a_system)) or (check_c2_multiprocessor_system (a_system) and check_c4_global_scheduling (a_system) and check_c5_fixed_priority (a_system) and check_c9_non_preemptive_processor (a_system) and check_c10_synchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c15_tasks_have_precedence_constraint (a_system)); end check_static_task_execution_time_decrease; --------------------------------------------------------------------------- function check_static_processor_add (a_system : in system) return Boolean is --C2, C4, C5, C9, C10, C12, C15 begin return (check_c2_multiprocessor_system (a_system) and check_c4_global_scheduling (a_system) and check_c5_fixed_priority (a_system) and check_c9_non_preemptive_processor (a_system) and check_c10_synchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c15_tasks_have_precedence_constraint (a_system)); end check_static_processor_add; function check_static_task_period_increase (a_system : in system) return Boolean is --C2, C4, C7, C10, C12, C13 --C2, C4, C5, C8, C10, C12, C13 --C2, C4, C6, C8, C10, C12, C13 --C2, C3, C5, C8, C10, C12, C13 begin return (check_c2_multiprocessor_system (a_system) and check_c4_global_scheduling (a_system) and check_c7_dm_algorithm (a_system) and check_c10_synchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c13_tasks_are_independent (a_system)) or (check_c2_multiprocessor_system (a_system) and check_c4_global_scheduling (a_system) and check_c5_fixed_priority (a_system) and check_c8_preemptive_processor (a_system) and check_c10_synchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c13_tasks_are_independent (a_system)) or (check_c2_multiprocessor_system (a_system) and check_c4_global_scheduling (a_system) and check_c6_edf_algorithm (a_system) and check_c8_preemptive_processor (a_system) and check_c10_synchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c13_tasks_are_independent (a_system)) or (check_c2_multiprocessor_system (a_system) and check_c3_partitionned_scheduling (a_system) and check_c5_fixed_priority (a_system) and check_c8_preemptive_processor (a_system) and check_c10_synchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c13_tasks_are_independent (a_system)); end check_static_task_period_increase; function check_static_task_late_execution (a_system : in system) return Boolean is -- C1, C3, C5, C8, C10, C12, c16 begin return (check_c1_mono_processor_system (a_system) and check_c3_partitionned_scheduling (a_system) and check_c5_fixed_priority (a_system) and check_c8_preemptive_processor (a_system) and check_c10_synchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c16_tasks_have_shared_resouces (a_system)); end check_static_task_late_execution; function check_static_task_priority_change (a_system : in system) return Boolean is --C2, C4, C5, C9, C10, C12, C15 begin return (check_c2_multiprocessor_system (a_system) and check_c4_global_scheduling (a_system) and check_c5_fixed_priority (a_system) and check_c9_non_preemptive_processor (a_system) and check_c10_synchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c15_tasks_have_precedence_constraint (a_system)); end check_static_task_priority_change; function check_static_precedence_constraint_change (a_system : in system) return Boolean is --C1, C3, C5, C10, C12, C15 --C2, C4, C5, C9, C10, C12, C15 begin return (check_c1_mono_processor_system (a_system) and check_c3_partitionned_scheduling (a_system) and check_c5_fixed_priority (a_system) and check_c10_synchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c15_tasks_have_precedence_constraint (a_system)) or (check_c2_multiprocessor_system (a_system) and check_c4_global_scheduling (a_system) and check_c5_fixed_priority (a_system) and check_c9_non_preemptive_processor (a_system) and check_c10_synchronous_departure (a_system) and check_c12_tasks_are_periodic (a_system) and check_c15_tasks_have_precedence_constraint (a_system)); end check_static_precedence_constraint_change; ----------------------------------------------------------------------- function print_duration_time_exec return String is the_clock : constant Ada.Real_Time.Time := Ada.Real_Time.Clock; -- Convert to Time_Span as_time_span : Ada.Real_Time .Time_Span; --:= The_Clock - Time_Of(0, Time_Span_Zero); -- Epoch ? -- Epoch : constant Ada.Calendar.Time := Ada.Calendar.Time_Of(1970, 01, 01); -- Dur ? dur : Duration; begin as_time_span := Ada.Real_Time.Clock - the_clock; dur := Ada.Real_Time.To_Duration (as_time_span); return Duration'image (dur); end print_duration_time_exec; --------------------------------------------------------------------- procedure check_static_constraint (a_system : in system; to_check : in potential_anomaly_type; result : out Boolean) is begin null; end check_static_constraint; procedure check_dynamic_constraint (a_system : in system; to_check : in potential_anomaly_type) is begin null; end check_dynamic_constraint; procedure scheduling_anomalies_analyzer (a_system : in system; msg : out Unbounded_String) is result : Boolean; the_clock : constant Ada.Real_Time.Time := Ada.Real_Time.Clock; -- Convert to Time_Span as_time_span : Ada.Real_Time .Time_Span; --:= The_Clock - Time_Of(0, Time_Span_Zero); dur, dur1 : Duration; msg1 : Unbounded_String; begin -- msg1:=To_Unbounded_String(print_duration_time_exec); --Put_Line(To_String(msg1)); as_time_span := Ada.Real_Time.Clock - the_clock; dur := Ada.Real_Time.To_Duration (as_time_span); msg1 := To_Unbounded_String ("begin of the procedure scheduling_anomalies:" & Duration'image (dur)); Put_Line (To_String (msg1)); result := check_c1_mono_processor_system (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C1_uniprocessor =" & result'img); result := check_c2_multiprocessor_system (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C2_MultiProcessor =" & result'img); result := check_c3_partitionned_scheduling (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C3:Partitionned Scheduling =" & result'img); result := check_c4_global_scheduling (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C4:Multiprocessor with global scheduling =" & result'img); result := check_c5_fixed_priority (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C5:fixed priority =" & result'img); result := check_c6_edf_algorithm (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C6:Algorithm EDF =" & result'img); result := check_c7_dm_algorithm (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C7:Algorithm DM =" & result'img); result := check_c8_preemptive_processor (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C8:Preemptive system =" & result'img); result := check_c9_non_preemptive_processor (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C9:Non preemptive system =" & result'img); result := check_c10_synchronous_departure (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C10:synchronous departure = " & result'img); result := check_c11_asynchronous_departure (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C11:asynchronous departure = " & result'img); result := check_c12_tasks_are_periodic (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C12:Periodic Tasks = " & result'img); result := check_c13_tasks_are_independent (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C13:tasks are independent = " & result'img); result := check_c14_tasks_are_suspended (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C14:tasks are suspended = " & result'img); result := check_c15_tasks_have_precedence_constraint (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C15:tasks have precedence constraint = " & result'img); result := check_c16_tasks_have_shared_resouces (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C16:Shared resources = " & result'img); result := check_c17_tasks_are_aperiodic (a_system); msg := msg & ASCII.LF & To_Unbounded_String ("Condition C17:tasks are aperiodics = " & result'img); as_time_span := Ada.Real_Time.Clock - the_clock; dur1 := Ada.Real_Time.To_Duration (as_time_span); dur := dur1 - dur; msg1 := To_Unbounded_String ("end of the procedure scheduling_anomalies:" & Duration'image (dur1)); Put_Line (To_String (msg1)); msg1 := To_Unbounded_String ("execution time of the procedure scheduling_anomalies:" & Duration'image (dur)); Put_Line (To_String (msg1)); end scheduling_anomalies_analyzer; end scheduling_anomalies_services;