1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(NICTA_GPL)
9 *)
10
11chapter {* \label{sec:types}Types *}
12
13(*<*)
14theory Types_CAMKES
15imports Main
16begin
17(*>*)
18
19text {*
20  This section describes the types of entities that appear in the CAmkES
21  Interface Definition Language (IDL) and Architecture Description Language
22  (ADL). The model assumes that all syntactic elements are available in a single
23  environment; that is, all @{term import} inclusion statements have already
24  been processed and all references are to be resolved within this context.
25*}
26
27subsection {* \label{subsec:symbols}Symbols *}
28text {*
29  CAmkES has two types of symbols that exist in separate namespaces. Symbols of
30  the first type are used in IDL descriptions to identify method names and
31  parameters. These symbols are used during code generation and therefore need
32  to be distinct within a specific interface.
33*}
34type_synonym idl_symbol = string
35
36text {*
37  The second type of symbols are used in ADL descriptions to identify components,
38  connectors and other architecture-level entities. These symbols are also used
39  during code generation, but are lexically scoped. E.g. Instantiated interfaces
40  within separate components can have an identical name.
41*}
42type_synonym adl_symbol = string
43
44text {*
45  Although both symbols map to the same underlying type, these have different
46  constraints (e.g. IDL symbols become direct substrings of code-level symbols
47  and hence need to respect symbol naming restrictions for the target
48  language(s)).
49*}
50
51subsection {* \label{subsec:methods}Methods *}
52text {*
53  Methods are the elements that make up a CAmkES procedure (described below).
54  Each method within a CAmkES procedure has a list of parameters defined by a
55  type, direction and symbol name. Each method also has an optional return
56  value type. The valid types for method parameters and return values include
57  a set of high level types designed to abstract the types available in a
58  general programming language. By using only these types in a procedure
59  description, the interface can be implemented in any valid target language.
60
61  When fixed width types are required for an interface there are a set of types
62  available that are C-specific. Using these types in a procedure description
63  precludes implementing or using the procedure in a component not written in C.
64  In general the high-level types should be used in preference to the C-specific
65  types.
66
67  In high-level languages, arrays may have attached size information, while in
68  C this information is passed as an extra parameter to their containing
69  method. Arrays are parameterised with the underlying type of
70  their elements. Similar to primitive types, using a high-level type for the
71  elementary type of an array allows it to be implemented or used in any
72  component, while using a C-specific type prevents implementing or using it in
73  a component not written in C. Arrays of arrays and multidimensional arrays are
74  not supported.
75*}
76
77datatype number =
78    \<comment> \<open>High level types\<close>
79    UnsignedInteger
80  | Integer
81  | Real
82  | Boolean
83    \<comment> \<open>C-specific types\<close>
84  | uint8_t
85  | uint16_t
86  | uint32_t
87  | uint64_t
88  | int8_t
89  | int16_t
90  | int32_t
91  | int64_t
92  | double
93  | float
94  | uintptr_t
95
96datatype textual =
97    \<comment> \<open>High level types\<close>
98    Character
99  | String
100    \<comment> \<open>C-specific types\<close>
101  | char
102
103datatype primitive =
104    Numerical number
105  | Textual textual
106
107datatype array =
108    SizedArray primitive
109  | TerminatedArray primitive
110
111datatype param_type =
112    Primitive primitive
113  | Array array
114
115text {*
116  Rather than having a single return value per procedure method, each
117  method parameter can be an input parameter, an output parameter, or both.
118*}
119datatype param_direction =
120    InParameter (* also covers 'refin' *)
121  | OutParameter
122  | InOutParameter
123
124text {*
125  Each procedure comprises a collection of methods that each have an
126  optional return type,
127  identifier and a list of parameters. Each parameter has a type and an
128  identifier.
129*}
130record parameter =
131  p_type        :: param_type
132  p_direction   :: param_direction
133  p_name        :: idl_symbol
134
135record "method" =
136  m_return_type :: "param_type option"
137  m_name        :: idl_symbol
138  m_parameters  :: "parameter list"
139text {*
140  The translation from procedure methods in IDL to their representation in
141  Isabelle is straightforward. The CAmkES method
142
143\begin{verbatim}
144  int foo(in string s);
145\end{verbatim}
146
147  is translated to the Isabelle representation
148*}
149(*<*)value(*>*)
150  "\<lparr>m_return_type = Some (Primitive (Numerical Integer)),
151    m_name = ''foo'',
152    m_parameters = [
153      \<lparr>p_type = Primitive (Textual String),
154       p_direction = InParameter,
155       p_name = ''s''\<rparr>
156    ]\<rparr>"
157text {*
158  More examples are given in \autoref{sec:examples}.
159*}
160
161subsection {* \label{subsec:interfaces}Interfaces *}
162text {*
163  Connections between two components are made from one interface to another.
164  CAmkES distinguishes between
165  interfaces that consist of a list of function calls and interfaces
166  that have other patterns of interaction.
167
168  There are three basic types of supported interfaces. The first, @{text procedure},
169  is used for modelling traditional caller-callee semantics of interaction. The
170  second, @{text event}, is used for asynchronous notifications such as interrupts.
171  Finally, @{text dataport}, is used to model shared memory communication.
172*}
173type_synonym procedure = "method list"
174type_synonym event     = nat \<comment> \<open>ID\<close>
175type_synonym dataport  = "string option" \<comment> \<open>type\<close>
176datatype interface =
177    Procedure procedure
178  | Event event
179  | Dataport dataport
180
181subsection {* \label{subsec:connectors}Connectors *}
182text {*
183  Two components are connected via a connector. The type of a connector is an
184  abstraction of the underlying communication mechanism. Connectors come in three
185  distinct types, native connectors, hardware connectors and export connectors.
186
187  Native connectors map directly to implementation mechanisms. These are the
188  types of connectors that are found in almost all component platform models. The
189  event-style connector, @{text AsynchronousEvent}, is
190  used to model communication consisting of an identifier with no associated message
191  data.
192*}
193datatype native_connector_type =
194    AsynchronousEvent \<comment> \<open>an asynchronous notification\<close>
195  | RPC \<comment> \<open>a synchronous channel\<close>
196  | SharedData \<comment> \<open>a shared memory region\<close>
197
198text {*
199  Recalling that hardware devices are modelled as components in CAmkES, hardware
200  connectors are used to connect the interface of a device to the interface of a
201  software component. Devices must be connected using the connector type that
202  corresponds to the mode of interaction with the device.
203*}
204datatype hardware_connector_type =
205    HardwareMMIO \<comment> \<open>memory mapped IO\<close>
206  | HardwareInterrupt \<comment> \<open>device interrupts\<close>
207  | HardwareIOPort \<comment> \<open>IA32 IO ports\<close>
208
209text {*
210  Export connectors are used when
211  specifying a compound component. A compound component has a set of interfaces
212  that are a subset of the unconnected interfaces of its constituent components.
213  The exposed interfaces of the compound component are defined by using export
214  connectors to map these to the interfaces of the internal components.
215
216  Export connectors are purely an architectural-level entity and do not exist at
217  runtime. During code generation connections through exported interfaces are
218  flattened. That is, a connection from interface A to exported interface B that
219  exports interface C is instantiated as a connection from interface A to interface
220  C would be. They can be thought of as a design-level convenience.
221
222  \begin{figure}[h]
223  \begin{center}
224  \caption{\label{fig:export}An export connector}
225  \includegraphics{imgs/composite-passthrough}
226  \end{center}
227  \end{figure}
228*}
229datatype export_connector_type =
230    ExportAsynchronous
231  | ExportRPC
232  | ExportData
233
234datatype connector_type =
235    Native native_connector_type
236  | Hardware hardware_connector_type
237  | Export export_connector_type
238
239text {*
240  Connectors are distinguished by the mode of interaction they enable. The
241  reason for this will become clearer in \autoref{subsec:wconnectors}.
242*}
243datatype connector =
244    SyncConnector connector_type
245  | AsyncConnector connector_type
246  | MemoryConnector connector_type
247
248subsection {* \label{subsec:components}Components *}
249text {*
250  Functional entities in a CAmkES system are represented as components. These
251  are re-usable collections of source code with explicit descriptions of the
252  exposed methods of interaction (@{term interfaces} described above).
253
254  Components have three distinct modes of communication:
255  \begin{enumerate}
256    \item Synchronous communication over procedures. This communication is
257      analogous to a function call and happens over a channel established from
258      a @{text requires} interface to a @{text provides} interface.
259    \item Asynchronous communication using events. This is suitable for things
260      like interrupts and happens over a channel from an @{text emits} interface to
261      a @{text consumes} interface.
262    \item Bidirectional communication via shared memory. This is suitable for
263      passing large data between components. It happens over a channel between
264      two @{text dataports}.
265  \end{enumerate}
266*}
267record component =
268  control     :: bool
269  requires    :: "(adl_symbol \<times> procedure) list"
270  provides    :: "(adl_symbol \<times> procedure) list"
271  dataports   :: "(adl_symbol \<times> dataport) list"
272  emits       :: "(adl_symbol \<times> event) list"
273  consumes    :: "(adl_symbol \<times> event) list"
274  attributes  :: "(adl_symbol \<times> param_type) list"
275
276subsection {* \label{subsec:assembling}Assembling a System *}
277text {*
278  A complete system is formed by instantiating component types that have been
279  defined, interconnecting these instances and specifying a system
280  configuration. Connections are specified by the two interfaces they connect
281  and the communication mechanism in use.
282*}
283record connection =
284  conn_type   :: connector
285  conn_from   :: "(adl_symbol \<times> adl_symbol) list"
286  conn_to     :: "(adl_symbol \<times> adl_symbol) list"
287
288text {*
289  A composition block is used to contain all components of the system and the
290  connections that define their communication with each other.
291*}
292record composition =
293  components  :: "(adl_symbol \<times> component) list"
294  connections :: "(adl_symbol \<times> connection) list"
295
296text {*
297  Configurations are used as a way of adding extra information to a component
298  or specialising the component in a particular context. The attributes
299  available to set are specified in the definition of the component, as
300  indicated above. These attributes are accessible to the component at the
301  code level at runtime.
302*}
303type_synonym configuration =
304  "(adl_symbol \<times> adl_symbol \<times> string) list"
305
306text {*
307  Finally the system specification is expressed at the top level as an
308  assembly. This extra level of abstraction allows more flexible re-use of
309  compositions and configurations.
310*}
311record assembly =
312  composition   :: "composition"
313  configuration :: "configuration option"
314
315subsection {* \label{subsec:future}Future Work *}
316subsubsection {* \label{subsubsec:composites}Component Hierarchy *}
317text {*
318  Some component platforms support the notion of explicit composite components.
319  This allows a composition of components to be re-used as a component itself.
320  In the context of the model presented above, this would allow a
321  @{term composition} element to appear anywhere a @{term component} element
322  is expected. Flexibility like this is desirable to avoid repeatedly
323  constructing common design patterns involving fine grained components. There
324  are plans to extend CAmkES to add this functionality.
325*}
326
327subsubsection {* \label{subsubsec:iarrays}Interface Arrays *}
328text {*
329  When specifying a more complicated dynamic component, it can be desirable to
330  define an array of interfaces. For example, a component that
331  provides an arbitrary number of copies of a specified procedure. This would
332  be implemented by the size of the array (the number of such copies) being
333  made available to the component at runtime and an index being provided with
334  each procedure method invocation. An example of how this could be useful is
335  discussed in \autoref{subsec:terminal}.
336
337  Extending this further, allowing the specification of interface arrays that
338  can be resized at runtime, by adding or removing connections, enables even
339  greater flexibility. Supporting this kind of dynamism in a system requires
340  meta functions (for modifying the interface array) and introduces further
341  complexity in handling failures of these.
342*}
343
344(*<*)end(*>*)
345