1
------------------------------------------------------------------------------
2
--                                                                          --
3
--                           OCARINA COMPONENTS                             --
4
--                                                                          --
5
--     O C A R I N A . B A C K E N D S . C H E D D A R . M A P P I N G      --
6
--                                                                          --
7
--                                 S p e c                                  --
8
--                                                                          --
9
--                       Copyright (C) 2020 OpenAADL                        --
10
--                                                                          --
11
-- Ocarina  is free software; you can redistribute it and/or modify under   --
12
-- terms of the  GNU General Public License as published  by the Free Soft- --
13
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
14
-- sion. Ocarina is distributed in the hope that it will be useful, but     --
15
-- WITHOUT ANY WARRANTY; without even the implied warranty of               --
16
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                     --
17
--                                                                          --
18
-- As a special exception under Section 7 of GPL version 3, you are granted --
19
-- additional permissions described in the GCC Runtime Library Exception,   --
20
-- version 3.1, as published by the Free Software Foundation.               --
21
--                                                                          --
22
-- You should have received a copy of the GNU General Public License and    --
23
-- a copy of the GCC Runtime Library Exception along with this program;     --
24
-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
25
-- <http://www.gnu.org/licenses/>.                                          --
26
--                                                                          --
27
--                    Ocarina is maintained by OpenAADL team                --
28
--                              (info@openaadl.org)                         --
29
--                                                                          --
30
------------------------------------------------------------------------------
31

32
------------------------------------------------------------------------------
33
--                                                                          --
34
--                           OCARINA COMPONENTS                             --
35
--                                                                          --
36
--     O C A R I N A . B A C K E N D S . C H E D D A R . M A P P I N G      --
37
--                                                                          --
38
--                                 S p e c                                  --
39
--                                                                          --
40
--                   Copyright (C) 2010-2018 ESA & ISAE.                    --
41
--                                                                          --
42
-- Ocarina  is free software; you can redistribute it and/or modify under   --
43
-- terms of the  GNU General Public License as published  by the Free Soft- --
44
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
45
-- sion. Ocarina is distributed in the hope that it will be useful, but     --
46
-- WITHOUT ANY WARRANTY; without even the implied warranty of               --
47
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                     --
48
--                                                                          --
49
-- As a special exception under Section 7 of GPL version 3, you are granted --
50
-- additional permissions described in the GCC Runtime Library Exception,   --
51
-- version 3.1, as published by the Free Software Foundation.               --
52
--                                                                          --
53
-- You should have received a copy of the GNU General Public License and    --
54
-- a copy of the GCC Runtime Library Exception along with this program;     --
55
-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
56
-- <http://www.gnu.org/licenses/>.                                          --
57
--                                                                          --
58
--                 Ocarina is maintained by the TASTE project               --
59
--                      (taste-users@lists.tuxfamily.org)                   --
60
--                                                                          --
61
------------------------------------------------------------------------------
62

63
with Ocarina.ME_AADL;
64
with Ocarina.ME_AADL.AADL_Instances.Nutils;
65
with Ocarina.ME_AADL.AADL_Instances.Nodes;
66
with Ocarina.Backends.Properties;
67
with Ocarina.Backends.Helper;
68
with Ocarina.Backends.Utils;
69

70
package Ocarina.Backends.Cheddar.Mapping is
71

72
   use Ocarina.ME_AADL;
73
   use Ocarina.ME_AADL.AADL_Instances.Nodes;
74
   use Ocarina.Backends.Properties;
75
   use Ocarina.Backends.Helper;
76
   use Ocarina.Backends.Utils;
77

78
   package AIN renames Ocarina.ME_AADL.AADL_Instances.Nodes;
79
   package AINU renames Ocarina.ME_AADL.AADL_Instances.Nutils;
80

81
   function Map_HI_Node (E : Node_Id) return Node_Id;
82
   function Map_HI_Unit (E : Node_Id) return Node_Id;
83

84
   function Map_Processor (E : Node_Id) return Node_Id with
85
     Pre => (True and then
86
               --  1/ Typing
87
               AINU.Is_Processor (E) and then
88

89
               --  2/ Property requirements
90
               --  a) Scheduling_Protocol policy is specified
91
               (Get_Scheduling_Protocol (E) /= Unknown_Scheduler)
92
            );
93

94
   function Map_Process (E : Node_Id) return Node_Id with
95
     Pre => (
96
             --  1/ Typing
97
             AINU.Is_Process (E)
98
            );
99

100
   function Map_Thread (E : Node_Id) return Node_Id with
101
     Pre => (True and then
102
               --  1/ Typing
103
               AINU.Is_Thread (E) and then
104

105
               --  2/ Property requirements
106
               --  The thread a) has dispatch protocol specified, b)
107
               --  has compute_execution_time specified, if it is
108
               --  either periodic or sporadic, then it has a period
109

110
               (Get_Thread_Dispatch_Protocol (E) /= Thread_None) and then
111
               (Get_Execution_Time (E) /= Empty_Time_Array) and then
112
               (if Get_Thread_Dispatch_Protocol (E) = Thread_Periodic or else
113 1
                  Get_Thread_Dispatch_Protocol (E) = Thread_Sporadic then
114
                    Get_Thread_Period (E) /= Null_Time) and then
115

116
              --  3/ Architecture requirements
117
              --  a) There is a linked processor P for E
118
              (for some P of Processors (Get_Root_Component (E)) =>
119 1
                AINU.Is_Processor (P) and then
120 1
                P = Get_Bound_Processor
121 1
                (Corresponding_Instance
122 1
                   (Get_Container_Process (Parent_Subcomponent (E)))))
123
            );
124

125
   function Map_Data (E : Node_Id) return Node_Id with
126
     Pre => (True and then
127
               --  1/ Typing
128
               AINU.Is_Data (E) and then
129

130
               --  2/ Architecture requirements
131
               --  a) There is a linked processor P for E
132
               (for some P of Processors (Get_Root_Component (E)) =>
133 1
                  AINU.Is_Processor (P) and then
134 1
                  P = Get_Bound_Processor
135 1
                  (Corresponding_Instance
136 1
                     (Get_Container_Process (Parent_Subcomponent (E)))))
137
               and then
138

139
               --  b) There is at least one thread accessing the data
140

141
               (for some T of Threads (Get_Root_Component (E)) =>
142
                  (for some C of Connections_Of
143
                     (Corresponding_Instance
144
                        (Get_Container_Process
145
                           (Parent_Subcomponent (E))))
146 1
                     => T = Corresponding_Instance
147 1
                     (Item (AIN.First_Node
148 1
                              (Path (Destination (C)))))))
149

150
            );
151

152
   function Map_Buffer (E : Node_Id; P : Node_Id) return Node_Id with
153
     Pre => (True and then
154
               --  1/ Typing
155

156
               --  a) E is a thread
157
               AINU.Is_Thread (E) and then
158

159
               --  b) P is an in event (data) port of E
160
               AINU.Is_Port (P) and then
161
               Is_Event (P) and then
162
               Is_In (P) and then
163
               (for some F of Features_Of (E) => P = F) and then
164

165
               --  2/ Architecture requirements
166

167
               --  a) There is a linked processor P for E
168
               (for some CPU of Processors (Get_Root_Component (E)) =>
169 1
                  AINU.Is_Processor (CPU) and then
170 1
                  CPU = Get_Bound_Processor
171 1
                  (Corresponding_Instance
172 1
                     (Get_Container_Process (Parent_Subcomponent (E)))))
173
               and then
174

175
               --  b) P is connected to some threads
176
               not AINU.Is_Empty (Get_Source_Ports (P))
177
            );
178

179
   function Map_Dependency (E : Node_Id; P : Node_Id) return Node_Id;
180

181
end Ocarina.Backends.Cheddar.Mapping;

Read our documentation on viewing source code .

Loading