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/** 13 * @file 14 * 15 * This file defines a list of connectors. A connection is an instance of a 16 * connector, allowing two components to communicate with each other. 17 * Different connectors are used for different purposes. 18 * 19 * In essence, a connector defines how exactly a component connects to another 20 * component. There are two parts, from and to. Most of the connectors are 21 * defined such that the "from" component sends data to the "to" component. So 22 * the "from" component is more like a sender and the "to" component is like a 23 * receiver. Having said that, a totally different semantic can be implemented. 24 * It's really up to the programmer to decide it. 25 * 26 * To use the connector, you define it like this: 27 * 28 * connection RPC util_fatfs_FS(from util.fs, to fatfs.fs); 29 * 30 * where the util_fatfs_FS connection is an instance of the RPC connector. It 31 * connects util.fs interface to fatfs.fs interface. 32 */ 33 34/** 35 * RPCCallSignal connector 36 * 37 * This connector is like the regular RPCCall connector, except that 38 * there is a Notification endpoint allocated and associated with the 39 * connector. The Notification endpoint is a 1-to-n relationship in that 40 * a component connected to many other components on the same interface 41 * with this connector is able to signal the connected components individually. 42 * 43 * It requires an attribute to define a badge for it to use and to couple 44 * the RPC connector and the associated dataport. The badge can be any 45 * unique number. 46 * <from_component>.<from_interface>_attributes = "<badge>"; 47 * 48 * The 'from' side of the connector can access the associated Notification 49 * endpoint via this exposed function: 50 * seL4_CPtr <interface name>_notification(void); 51 * 52 * The 'to' side of the connector can signal the desired connected component 53 * by passing the component's badge into the following function: 54 * void <interface_name>_emit(unsigned int badge); 55 * There is also a function to query the largest badge of all the connected 56 * components: 57 * int <interface_name>_largest_badge(void); 58 */ 59connector seL4RPCCallSignal { 60 from Procedures; 61 to Procedure; 62 attribute bool from_global_endpoint = True; 63} 64 65/** 66 * RPCDataport connect 67 * 68 * This connect provides a regular RPCCall connector, except that 69 * it allocates an additional shared dataport between each sender 70 * and receiver. The intention being that each client can place 71 * data directory into a buffer, and then use RPC as the control 72 * interface. 73 * 74 * It requires an attribute to define a badge for it to use and to couple 75 * the RPC connector and the associated dataport. The badge can be any 76 * unique number. 77 * <from_component>.<from_interface>_attributes = "<badge>"; 78 * 79 * The 'from' side of the connector can access its dataport by 80 * using a symbol named '<from_interface>_buf', which is just an 81 * alias for the actual shared memory allocation. 82 * 83 * The 'to' side of the connection can get a specific dataport 84 * with <from_interface>_buf(<badge>) and can enumerate badges 85 * with <from_interface>_enumerate_badge(<badge_number>) and 86 * <from_interface>_num_badges() 87 */ 88connector seL4RPCDataport { 89 from Procedures with 0 threads; 90 to Procedure; 91 92 attribute string isabelle_connector_spec = "\<lparr> 93 connector_type = NativeConnector, 94 connector_interface = RPCInterface, 95 connector_access = \<lparr> 96 access_from_to = {DeleteDerived}, 97 access_to_from = {Reply}, 98 access_from_from = {}, 99 access_to_to = {}, 100 access_from_conn = {Reset, SyncSend, Call, Read, Write}, 101 access_to_conn = {Reset, Receive, Read, Write} 102 \<rparr> \<rparr>"; 103} 104 105connector seL4RPCDataportNoThreads { 106 from Procedures with 0 threads; 107 to Procedure with 0 threads; 108 attribute bool to_global_rpc_endpoint = True; 109} 110 111 112/** 113 * RPCDataportSignal connector 114 * 115 * This connector is similar to the seL4RPCCallSignal connector, except 116 * that this connector is built on top of the seL4RPCDataport connector. 117 * 118 * The features and requirements are similar to the seL4RPCDataport connector. 119 * 120 * Additionally, the 'from' side of the connector can access the associated Notification 121 * endpoint via this exposed function: 122 * seL4_CPtr <interface name>_notification(void); 123 * 124 * The 'to' side of the connector can signal the desired connected component 125 * by passing the component's badge into the following function: 126 * void <interface_name>_emit(unsigned int badge); 127 * There is also a function to query the largest badge of all the connected 128 * components: 129 * int <interface_name>_largest_badge(void); 130 */ 131connector seL4RPCDataportSignal { 132 from Procedures; 133 to Procedure; 134 attribute bool from_global_endpoint = True; 135} 136 137/** 138 * seL4RPCOverMultiSharedData connector 139 * 140 * This connector is similar to seL4RPCCall but will use shared memory instead of 141 * the IPC buffer to transfer data between components. It supports multiple clients 142 * communicating with a single server. Each client has a separate shared memory region 143 * with the server. The size of the shared memory region can be configured on a 144 * per-client basis via setting ${client_instance}.${interface_name}_shmem_size. 145 * The default shared memory size is 4096 bytes. 146 * For a multi-threaded caller, subsequent calls to the interface will block until 147 * the first call returns in order to preserve the integrity of the shared buffer. 148 * 149 */ 150connector seL4RPCOverMultiSharedData { 151 from Procedures with 0 threads; 152 to Procedure; 153} 154 155/** 156 * seL4GlobalAsynch 157 * 158 * This is a 1-to-n global endpoint Event connector that makes the underlying 159 * seL4 Notification endpoint capability available directly to the consuming 160 * component. 161 * 162 * This Event connector does not provide the consumer with the 163 * usual wait or callback interfaces, but only provides the following function: 164 * seL4_CPtr <interface name>_notification(void); 165 * 166 * Global endpoint connectors allows an Event interface to be coupled with 167 * other interfaces in a component. The interfaces coupled with 168 * an Event will be able to access that Event's underlying Notification 169 * endpoint capability. 170 * 171 * Coupling of interfaces occurs through matching attribute values. Each global 172 * endpoint connection defines a "_global_endpoint" attribute for its associated 173 * interfaces. Those interfaces (within a component) whose "_global_endpoint" 174 * attributes match are coupled. 175 */ 176connector seL4GlobalAsynch { 177 from Event with 0 threads; 178 to Events with 0 threads; 179 attribute bool to_global_endpoint = True; 180 181 attribute string isabelle_connector_spec = "\<lparr> 182 connector_type = NativeConnector, 183 connector_interface = EventInterface, 184 connector_access = \<lparr> 185 access_from_to = {}, 186 access_to_from = {}, 187 access_from_from = {}, 188 access_to_to = {}, 189 access_from_conn = {Reset, Receive, Notify}, 190 access_to_conn = {Reset, Receive, Notify} 191 \<rparr> \<rparr>"; 192} 193 194/** 195 * seL4GlobalAsynchCallback 196 * 197 * This is a 1-to-n global endpoint Event connector that makes the underlying 198 * seL4 Notification endpoint capability available directly to the consuming 199 * component. 200 * 201 * This Event connector provides the consumer with the usual callback 202 * interface as well as the following function: 203 * seL4_CPtr <interface name>_notification(void); 204 * 205 * Global endpoint connectors allow an Event interface to be coupled with 206 * other interfaces in a component. The interfaces coupled with 207 * an Event will be able to access that Event's underlying Notification 208 * endpoint capability. 209 * 210 * Coupling of interfaces occurs through matching attribute values. Each global 211 * endpoint connection defines a "_global_endpoint" attribute for its associated 212 * interfaces. Those interfaces (within a component) whose "_global_endpoint" 213 * attributes match are coupled. 214 */ 215connector seL4GlobalAsynchCallback { 216 from Event; 217 to Events; 218 attribute bool to_global_endpoint = True; 219 220 attribute string isabelle_connector_spec = "\<lparr> 221 connector_type = NativeConnector, 222 connector_interface = EventInterface, 223 connector_access = \<lparr> 224 access_from_to = {}, 225 access_to_from = {}, 226 access_from_from = {}, 227 access_to_to = {}, 228 access_from_conn = {Reset, Receive, Notify}, 229 access_to_conn = {Reset, Receive, Notify} 230 \<rparr> \<rparr>"; 231} 232 233/* Custom connectors which use existing global connectors just with no threads configured. */ 234connector seL4TimeServer { 235 from Procedures with 0 threads; 236 to Procedure; 237 attribute bool from_global_endpoint = True; 238 239 /* TODO: double check this */ 240 attribute string isabelle_connector_spec = "\<lparr> 241 connector_type = NativeConnector, 242 connector_interface = RPCInterface, 243 connector_access = \<lparr> 244 access_from_to = {DeleteDerived}, 245 access_to_from = {Reset, Notify, Reply}, 246 access_from_from = {Reply}, \<comment> \<open>Fictitious but required by Access (Jira VER-1108)\<close> 247 access_to_to = {}, 248 access_from_conn = {Reset, Call, SyncSend, Notify, Receive}, 249 access_to_conn = {Reset, Notify, Receive} 250 \<rparr> \<rparr>"; 251} 252 253connector seL4SerialServer { 254 from Procedures with 0 threads; 255 to Procedure; 256 attribute bool from_global_endpoint = True; 257 258 /* TODO: double check this */ 259 attribute string isabelle_connector_spec = "\<lparr> 260 connector_type = NativeConnector, 261 connector_interface = RPCInterface, 262 connector_access = \<lparr> 263 access_from_to = {DeleteDerived}, 264 access_to_from = {Reply, 265 \<comment> \<open>FIXME: vm_serial_server seems to need these, but why?\<close> 266 Reset, Notify}, 267 access_from_from = {}, 268 access_to_to = {}, 269 access_from_conn = {Reset, Call, SyncSend, Read, Write}, 270 access_to_conn = {Reset, Receive, Read, Write} 271 \<rparr> \<rparr>"; 272} 273 274connector seL4PicoServerSignal { 275 from Procedures with 0 threads; 276 to Procedure with 0 threads; 277 attribute bool from_global_endpoint = True; 278 attribute bool to_global_rpc_endpoint = True; 279} 280 281connector seL4PicoServer { 282 from Procedures with 0 threads; 283 to Procedure with 0 threads; 284 attribute bool to_global_rpc_endpoint = True; 285} 286 287/** 288 * seL4Ethdriver 289 * 290 * This connector is intended to be used with the Ethdriver component. 291 * 292 * The connector itself is very similar to the seL4RPCDataportSignal connector 293 * except that it contains an additional function to query a client's assigned MAC 294 * address. 295 */ 296connector seL4Ethdriver { 297 from Procedures with 0 threads; 298 to Procedure; 299 attribute bool from_global_endpoint = True; 300} 301 302connector seL4SharedDataWithCaps { 303 from Dataports; 304 to Dataports; 305 306 attribute string isabelle_connector_spec = "\<lparr> 307 connector_type = NativeConnector, 308 connector_interface = DataportInterface, 309 connector_access = \<lparr> 310 access_from_to = {Reset, Notify}, 311 access_to_from = {}, 312 access_from_from = {}, 313 access_to_to = {}, 314 access_from_conn = {Read, Write}, 315 access_to_conn = {Read, Write} 316 \<rparr> \<rparr>"; 317} 318 319/** 320* seL4VirtQueues 321* 322* This is an n-n global endpoint connector that makes use of an seL4 323* Notification endpoint capability and shared memory region to faciliate 324* the implementation of a virtqueue-based communication protocol. 325* 326* Multiple components can participate in a virtqueue connection where 327* participating components are in the 'from' end of the connection. 328* A virtqueue connection can have only 1 component in the 'to' end, which 329* is intended to be an empty/stub component. 330*/ 331connector seL4VirtQueues { 332 from Procedures with 0 threads; 333 to Procedure with 0 threads; 334 attribute bool disable_interface_type_checking = true; 335 attribute bool from_global_endpoint = True; 336 attribute bool to_global_endpoint = True; 337 338 attribute string isabelle_connector_spec = "\<lparr> 339 connector_type = NativeConnector, 340 connector_interface = RPCInterface, 341 connector_access = \<lparr> 342 access_from_to = {}, 343 access_to_from = {}, 344 access_from_from = {Notify, Reset}, \<comment> \<open>global-endpoint ntfns are owned by clients\<close> 345 access_to_to = {}, 346 access_from_conn = {Reset, Receive, Notify, Read, Write}, 347 access_to_conn = {Reset, Receive, Notify, Read, Write} 348 \<rparr> \<rparr>"; 349} 350 351/** seL4MessageQueue 352 * 353 * This connector allows the passing of small messages from a sender to a 354 * receiver. The passing of messages is non-blocking and a number of these 355 * messages can be queued for the receiver. 356 * 357 * The block size of the messages is determined by the type associated with the 358 * dataport. 359 * 360 * The sender should be located on the 'from' side of the connection and the 361 * receivers on the 'to' side. 362 * 363 * The size of the queue can be set by the following attribute: 364 * <connection_name>.size = "<size>"; 365 * which is similar to seL4SharedDataport. 366 * 367 * Similarly, the length of the queue can be set by the following attribute: 368 * <connection_name>.length = "<length>"; 369 * 370 * To differentiate between the individual seL4MessageQueue connections in a 371 * component, an unique ID needs to be set for each connection. This can be 372 * done by setting the following attribute: 373 * <component_name>.<interface_name>_id = "<unique id>"; 374 * 375 * To interact with the message queue, use the message queue APIs in 376 * libsel4camkes. The library provides two functions to obtain a handle to use 377 * the APIs with: 378 * int camkes_msgqueue_sender_init(int msgqueue_id, camkes_msgqueue_sender_t *sender); 379 * int camkes_msgqueue_receiver_init(int msgqueue_id, camkes_msgqueue_receiver_t *receiver); 380 * which initialises either a sender or receiver msgqueue channel. The 381 * 'msgqueue_id' corresponds to the IDs that were assigned to a component's 382 * seL4MessageQueue connections. 383 */ 384connector seL4MessageQueue { 385 from Dataports; 386 to Dataports; 387} 388 389/** seL4GlobalAsynchHardwareInterrupt 390 * 391 * This connector is similar to the seL4HardwareInterrupt and has the same attributes for 392 * specifying an IRQ to allocate but doesn't allocate any threads. In order to process 393 * callback handlers for a received notification, a function provided by libsel4camkes, 394 * camkes_handle_global_endpoint_irq(), can be called. 395 * 396 */ 397connector seL4GlobalAsynchHardwareInterrupt { 398 from hardware Event; 399 to Event with 0 threads; 400 attribute bool to_global_endpoint = True; 401} 402 403/** seL4RPCNoThreads 404 * 405 * This connector is similar to the seL4RPCCall connector for performing RPC using the 406 * seL4 IPC buffer. In order to process messages, an interface function needs to be 407 * called to handle each received message. 408 * 409 * This makes it possible to tie several different interfaces to the same underlying 410 * endpoint object. 411 */ 412connector seL4RPCNoThreads { 413 from Procedures with 0 threads; 414 to Procedure with 0 threads; 415 attribute bool to_global_rpc_endpoint = True; 416} 417 418connector seL4DTBHardwareThreadless { 419 from Event with 0 threads; 420 to Events with 0 threads; 421 attribute bool to_global_endpoint = True; 422 423} 424 425connector seL4DTBHWThreadless { 426 from hardware Event; 427 to Events with 0 threads; 428 attribute bool to_global_endpoint = True; 429 430} 431 432/** seL4GPIOServer 433 * 434 * This connector is intended for the exclusive use for GPIOMUXServer. 435 * The connector is essentially the seL4RPCCall connector but with access 436 * control mechanisms for GPIO pins. The user is able to assign specific 437 * pins for clients to be used exclusively. 438 * 439 * This is done by filling out the following configuration item in the 440 * configuration block of a .camkes configuration. 441 * 442 * <component name>.<interface name>_pins = gpio({ "pins" : ["PINS", ...] }); 443 * 444 * <interface name> should be the name of the interface of the component that 445 * is connected to the GPIOMUXServer with the seL4GPIOServer connector. 446 */ 447connector seL4GPIOServer { 448 from Procedures with 0 threads; 449 to Procedure; 450} 451