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