1/* 2 * Copyright 2017, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 */ 12 13import "camkes-hardware.idl4"; 14import "gdb-delegate.camkes"; 15 16/** 17 * @file 18 * 19 * This file defines a list of connectors. A connection is an instance of a 20 * connector, allowing two components to communicate with each other. 21 * Different connectors are used for different purposes. 22 * 23 * In essence, a connector defines how exactly a component connects to another 24 * component. There are two parts, from and to. Most of the connectors are 25 * defined such that the "from" component sends data to the "to" component. So 26 * the "from" component is more like a sender and the "to" component is like a 27 * receiver. Having said that, a totally different semantic can be implemented. 28 * It's really up to the programmer to decide it. 29 * 30 * To use the connector, you define it like this: 31 * 32 * connection RPC util_fatfs_FS(from util.fs, to fatfs.fs); 33 * 34 * where the util_fatfs_FS connection is an instance of the RPC connector. It 35 * connects util.fs interface to fatfs.fs interface. 36 */ 37 38/** 39 * Asynchronous event connector 40 * 41 * Once the connection has been established, the consumer could wait for 42 * asynchronous signal sending from the emitter. The waiting process can be 43 * blocked or non-blocked. The sending process is non-blocked, that is the 44 * emitter can send data at any time and at any rate. 45 * 46 * One of the advantages of this connector is if the consumer executes much 47 * faster than the emitter. The consumer could do other stuff while waiting for 48 * the asynchronous signal from the emitter. However it's harder to synchronize 49 * the components. 50 */ 51connector seL4Notification { 52 from Event with 0 threads; 53 to Events; 54 attribute string isabelle_connector_spec = "seL4Notification"; /* builtin connector */ 55} 56connector seL4NotificationBind { 57 from Events with 0 threads; 58 to Event; 59} 60connector seL4NotificationQueue { 61 from Event with 0 threads; 62 to Events; 63} 64connector seL4NotificationNative { 65 from Events with 0 threads; 66 to Event; 67} 68 69/** 70 * Asynchronous RPC event connector 71 * 72 * This connector works exactly the same as the asynchronous event connector. 73 * The consumer and emitter shouldn't notice any difference. But the internal 74 * implementation is different. seL4Notification uses the asynchronous 75 * mechanism to send signal, whereas seL4RPCEvent uses the regular RPC 76 * to send and imitate the event signal. 77 */ 78connector seL4RPCEvent { 79 from Event; 80 to Event; 81} 82 83/** 84 * RPC connector 85 * 86 * Once the connection has been established, the user could wait for regular 87 * RPC signal sending from the provider. The sending and waiting phase are 88 * blocked. 89 */ 90connector seL4RPCCall { 91 from Procedures with 0 threads; 92 to Procedure; 93 attribute string isabelle_connector_spec = "seL4RPC"; /* builtin connector */ 94} 95 96/* Same as seL4RPCCall, except has relaxed type checking */ 97connector seL4RPCCallNoType { 98 from Procedures with 0 threads; 99 to Procedure; 100 attribute bool disable_interface_type_checking = true; 101 attribute string isabelle_connector_spec = "seL4RPC"; /* builtin connector */ 102} 103 104/** 105 * Direct Call connector 106 * 107 * Situates both components in the same protection domain, so that interface 108 * calls are backed by function calls, rather than RPCs. 109 */ 110connector seL4DirectCall { 111 from Procedure; 112 to Procedure; 113 attribute string isabelle_connector_spec = "seL4RPC"; /* builtin connector */ 114} 115 116/** 117 * Dataport connector 118 * 119 * This connector allows memory sharing between two components. 120 * 121 * The dataport size is not defined in this connector, it's up to the 122 * implementation. 123 */ 124connector seL4SharedData { 125 from Dataports with 0 threads; 126 to Dataports with 0 threads; 127 attribute string isabelle_connector_spec = "seL4SharedData"; /* builtin connector */ 128} 129 130/** 131 * Hardware MMIO dataport connector 132 * 133 * This connector has special behaviour: it designates the component on the 134 * hardware_component_data side as fictitious, and represents a hardware 135 * device. Code will therefore not be generated for that component. 136 * 137 * It also implies that the backing memory will be mapped uncached. 138 * 139 * The hardware_component_data dataport's attribute string should consist of 140 * the physical address and size of the memory window, in the following format: 141 * "0x<address>:0x<size>" 142 */ 143connector seL4HardwareMMIO { 144 from Dataports with 0 threads; 145 to hardware Dataport; 146 attribute string isabelle_connector_spec = "seL4HardwareMMIO"; /* builtin connector */ 147} 148 149/** 150 * Hardware interrupt event connector 151 * 152 * This connector has special behaviour: it designates the component on the 153 * hardware_component_interrupt side as fictitious, and represents a hardware 154 * device. Code will therefore not be generated for that component. 155 * 156 * The hardware_component_interrupt event's attribute string should consist of 157 * the interrupt number, in either decimal or (with the "0x" prefix) 158 * hexadecimal. 159 */ 160connector seL4HardwareInterrupt { 161 from hardware Event; 162 to Event; 163 attribute string isabelle_connector_spec = "seL4HardwareInterrupt"; /* builtin connector */ 164} 165connector seL4IOAPICHardwareInterrupt { 166 from hardware Event; 167 to Event; 168} 169 170/** 171 * Hardware IOPorts connector 172 * 173 * This connector has special behaviour: it designates the component on the 174 * hardware_component_data side as fictitious, and represents a hardware 175 * device. Code will therefore not be generated for that component. 176 * 177 * Note that by nature, this connector is ia32-specific. 178 * 179 * The attribute 'hardware_component_port_attributes' should be set to define the 180 * the IOPort range needed, in the following format: "0x<first_port>:0x<last_port>". 181 * The interface provided should be "IOPort". E.g. 182 * component foo { 183 * hardware; 184 * provides IOPort bar; 185 * } 186 * assembly { 187 * composition { 188 * component foo f; 189 * ... 190 * connection HardwareIOPort moo(from ..., to foo.bar); 191 * } 192 * configuration { 193 * foo.bar_attributes = "0x42:0x84"; 194 * } 195 * } 196 */ 197connector seL4HardwareIOPort { 198 from Procedure with 0 threads; 199 to hardware Procedure; 200} 201 202/** 203 * DTB hardware connector 204 * 205 * This connector allows a user to automatically generate the resources needed to 206 * interact with a device. This includes memory-mapped hardware registers and interrupts. 207 * It does so by reading from a specified DTB node. 208 209 * To use this connector, a dummy 'emits' interface needs to be created. For each 210 * pair of hardware registers and/or interrupts, you wish to initialise, a 'consumes' 211 * interface needs to be created and paired with the dummy source. E.g. 212 * 213 * consumes Dummy timer; 214 * consumes Dummy serial; 215 * emits Dummy dummy_source; 216 * ... 217 * connection seL4DTBHardware timer_conn(from dummy_source, to timer); 218 * connection seL4DTBHardware timer_conn(from dummy_source, to serial); 219 * 220 * To pass in a DTB node to the connector, the attribute 'dtb' of the 'consumes' 221 * interface must be set to the DTB path of a particular node. E.g. 222 * 223 * timer.dtb = dtb({ "path" : "/soc/serial@deadbeef" }); 224 * 225 * Interrupts will not be generated by default. To generate interrupts, set the 226 * 'generate_interrupts' attribute of the 'consumes' interface to equal to '1'. E.g. 227 * 228 * timer.generate_interrupts = 1; 229 * 230 * Warning: The connector currently assumes that the `interrupts` binding in the DTB 231 * node follow the format of the ARM GIC, i.e. cell 1 = SPI interrupt, 232 * cell 2 = interrupt number and cell 3 = interrupt flag. 233 * 234 */ 235connector seL4DTBHardware { 236 from Event with 0 threads; 237 to Events; 238 239 /* This connector by itself confers no access rights. Use other 240 * attributes to specify integrity policy for hardware. */ 241 attribute string isabelle_connector_spec = "\<lparr> 242 connector_type = NativeConnector, 243 connector_interface = EventInterface, 244 connector_access = \<lparr> 245 access_from_to = {}, 246 access_to_from = {}, 247 access_from_from = {}, 248 access_to_to = {}, 249 access_from_conn = {}, 250 access_to_conn = {} 251 \<rparr> \<rparr>"; 252} 253 254connector seL4DTBHW { 255 from hardware Event; 256 to Events; 257} 258 259connector seL4InitHardware { 260 from Event with 0 threads; 261 to Events with 0 threads; 262} 263 264/** 265 * Dataport connector 266 * 267 * This connector defines a shared DMA pool between multiple components. 268 * 269 * Supported config options: 270 * 271 * Connector instance level: 272 * paddr: Specify a physical address for the Pool to start at. Default: Any 273 * size: Specify the size of the pool. Default: 4096 274 * controller: Identify the interface instance that is allowed to make allocations. 275 * 276 * Interface instance level: 277 * %{interface_name}_cached: Cache attributes of the pool's mapping. Default: True 278 * %{interface_name}_access: Memory permissions of the pool's mapping. Default: RWXP (All) 279 * 280 */ 281connector seL4DMASharedData { 282 from Dataports with 0 threads; 283 to Dataports with 0 threads; 284 attribute string isabelle_connector_spec = "seL4SharedData"; /* builtin connector */ 285} 286