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