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