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/*# This defines a 'connector' that attempts to have an coherent API that can be implemented
14  # differently by different connectors to change how data/control transfer happens between
15  # components. By using the public interfaces defined here a template need only concern
16  # itself with particular details of doing the marshalling/unmarshalling with the component
17  # and leave the connector implementation free to determine how to communicate between
18  # components. This connector specifically uses synchronous endpoints with Call+ReplyRecv,
19  # but it could use shared memory and notifications just as easily without changing the
20  # specific interfaces that use this.
21  # Currently this connector has some rough edges and should potentially be split into two
22  # connectors as it tries to support both dataport message passing as well as IPC buffer
23  # message passing.
24  #
25  # For state the connectors rely on a namespace being given that they instantiate and then
26  # should be given in every subsequent invocation. *some* members of this namespace are
27  # explicitly documented as being public and can be used directly by the template code,
28  # others are internal and not guaranteed to exist or be consistent across different
29  # connector instantiations.
30  #
31  # The individual methods document their interactions and requirements
32  #*/
33
34/*# *** Internal helpers *** #*/
35
36/*- macro allocate_badges(namespace) -*/
37    /*# Find any badges that have been explicitly assigned for this connection. That
38     *# is, any badge identifiers that are not valid for us to assign automatically
39     *# to other ends.
40      #*/
41    /*- set namespace.badges = [] -*/
42    /*- for e in me.parent.from_ends -*/
43        /*- set badge_attribute = '%s_attributes' % e.interface.name -*/
44        /*- set badge = configuration[e.instance.name].get(badge_attribute) -*/
45        /*- if isinstance(badge, six.integer_types) -*/
46            /*- do namespace.badges.append(badge) -*/
47        /*- elif isinstance(badge, six.string_types) and re.match('\\d+$', badge) is not none -*/
48            /*- do namespace.badges.append(int(badge)) -*/
49        /*- elif badge is not none -*/
50            /*? raise(TemplateError('%s.%s must be either an integer or string encoding an integer' % (e.instance.name, badge_attribute), configuration.settings_dict[e.instance.name][badge_attribute])) ?*/
51        /*- else -*/
52            /*- do namespace.badges.append(none) -*/
53        /*- endif -*/
54    /*- endfor -*/
55
56    /*# Now fill in any missing badges, skipping any already assigned badge values #*/
57    /*- set next = [1] -*/
58    /*- for _ in me.parent.from_ends -*/
59        /*- if namespace.badges[loop.index0] is none -*/
60            /*- for _ in namespace.badges -*/
61                /*- if next[0] in namespace.badges -*/
62                    /*- do next.__setitem__(0, next[0] + 1) -*/
63                /*- endif -*/
64            /*- endfor -*/
65            /*- do namespace.badges.__setitem__(loop.index0, next[0]) -*/
66        /*- endif -*/
67    /*- endfor -*/
68/*- endmacro -*/
69
70/*- macro _establish_buffer(namespace, buffer, recv) -*/
71    /*- if namespace.language == 'c' -*/
72        /*- if buffer is none -*/
73            /*- set namespace.userspace_ipc = False -*/
74            /*- set base = '((void*)&seL4_GetIPCBuffer()->msg[0])' -*/
75            /*- set buffer_size = '(seL4_MsgMaxLength * sizeof(seL4_Word))' -*/
76            /*- set namespace.lock = False -*/
77        /*- else -*/
78            /*- set namespace.userspace_ipc = True -*/
79            /*- set base = buffer[0] -*/
80            /*- set buffer_size = buffer[1] -*/
81        /*- if not recv -*/
82                /*- set lock = buffer[2] -*/
83                /*- set namespace.lock = lock -*/
84                /*- if lock -*/
85                    /*- set namespace.lock_symbol = c_symbol() -*/
86                    /*- set namespace.lock_ep = alloc('userspace_buffer_ep', seL4_EndpointObject, label=me.instance.name, write=True, read=True) -*/
87                    static volatile int /*? namespace.lock_symbol ?*/ = 1;
88                /*- else -*/
89                    /*- set namespace.lock = False -*/
90                /*- endif -*/
91            /*- endif -*/
92        /*- endif -*/
93    /*- elif namespace.language == 'cakeml' -*/
94        open camkesUtilsLib;
95        /*- set word_size = macros.get_word_size(options.architecture) -*/
96        /*- if buffer is not none -*/
97            /*? raise(TemplateError('CakeML connector only supports using the IPC buffer')) ?*/
98        /*- endif -*/
99        /*- set base = 'ConInternal.ipcbuf' -*/
100        /*- set buffer_size = 120 * word_size -*/
101        (* Add '2 * word_size + 1' because the protocol with the ffi IPC functions requires 1 byte for
102           success and two words for data *)
103        /*- set bsize = buffer_size + 2 * word_size + 1 -*/
104        val ipcbuf_e = ``(App Aw8alloc [Lit (IntLit /*? bsize ?*/); Lit (Word8 0w)])``
105        /*- set namespace.cakeml_reserved_buf = 2 * word_size + 1 -*/
106        val eval_thm = derive_eval_thm_bytes false "ipcbuf_loc" ipcbuf_e /*? bsize ?*/;
107        val _ = ml_prog_update (add_Dlet eval_thm "ipcbuf" []);
108    /*- endif -*/
109    /*- set namespace.send_buffer = base -*/
110    /*- set namespace.recv_buffer = base -*/
111    /*- set namespace.send_buffer_size = buffer_size -*/
112    /*- set namespace.recv_buffer_size = buffer_size -*/
113    /*- set namespace.recv_buffer_size_fixed = namespace.userspace_ipc -*/
114/*- endmacro -*/
115
116/*- macro _make_get_sender_id_symbol(namespace, interface_name) -*/
117    /*- set namespace.badge_symbol = '%s_badge' % interface_name -*/
118    #include <sel4/sel4.h>
119    static seL4_Word /*? namespace.badge_symbol ?*/ = 0;
120
121    seL4_Word /*? interface_name ?*/_get_sender_id(void) {
122        return /*? namespace.badge_symbol ?*/;
123    }
124/*- endmacro -*/
125
126/*- macro _extract_size(namespace, info, size, recv) -*/
127    /*? size ?*/ =
128        /*-- if namespace.userspace_ipc -*/
129            /*-- if recv -*/
130                /*? namespace.recv_buffer_size ?*/
131            /*-- else -*/
132                /*? namespace.send_buffer_size ?*/
133            /*-- endif -*/
134        /*-- else --*/
135            seL4_MessageInfo_get_length(/*? info ?*/) * sizeof(seL4_Word);
136            assert(/*? size ?*/ <= seL4_MsgMaxLength * sizeof(seL4_Word))
137        /*-- endif --*/
138        ;
139/*- endmacro -*/
140
141/*- macro _save_reply_cap(namespace, might_block) -*/
142    /*- if not options.realtime and might_block -*/
143        /*# We need to save the reply cap because the user's implementation may
144         * perform operations that overwrite or discard it.
145         #*/
146        /*? assert(namespace.reply_cap_slot is defined and namespace.reply_cap_slot > 0) ?*/
147        /*- if namespace.language == 'c' -*/
148            camkes_declare_reply_cap(/*? namespace.reply_cap_slot ?*/);
149        /*- elif namespace.language == 'cakeml' -*/
150            val _ = Utils.camkes_declare_reply_cap /*? namespace.reply_cap_slot ?*/;
151        /*- endif -*/
152    /*- endif -*/
153/*- endmacro -*/
154
155/*- macro _begin_cakeml_module(namespace) -*/
156    val _ = ml_prog_update (open_module "ConInternal")
157/*- endmacro -*/
158
159/*- macro _end_cakeml_module(namespace) -*/
160    val _ = ml_prog_update (close_module NONE);
161/*- endmacro -*/
162
163/*# *** Public interfaces *** #*/
164
165/*# Instantiates a 'from' side of this connector for doing RPC using the 'default'
166  # memory sharing policy, or the dataport if one is given.
167  # This may generate symbols and other globals and should appear in the same namespace
168  # as the rest of the instantiated template.
169  # Will produce the follow values in the namespace that may be referenced
170  #  send_buffer: Buffer to marshal inputs into for sending
171  #  send_buffer_size: Size of the send buffer
172  #  recv_buffer: Buffer to unmarsh outputs from
173  #  recv_buffer_size: Size of the recv buffer
174  #  recv_buffer_size_fixed: If fixed a received message has an 'unknown' size as the entire buffer is always transfered
175  #  badges: List of the badge assigned to each incoming edge of the connector
176  #*/
177/*- macro establish_from_rpc(namespace, buffer=none) -*/
178    /*- set namespace.language = 'c' -*/
179    /*# Establish the buffer for message contents #*/
180    /*? _establish_buffer(namespace, buffer, False) ?*/
181
182    /*# Ensure the endpoint is allocated #*/
183    /*- set ep_obj = alloc_obj('ep', seL4_EndpointObject) -*/
184    /*- set ep = alloc_cap('ep_%s' % me.interface.name, ep_obj, write=True, grantreply=True) -*/
185
186    /*? allocate_badges(namespace) ?*/
187    /*# Badge our capability #*/
188    /*- do cap_space.cnode[ep].set_badge(namespace.badges[me.parent.from_ends.index(me)]) -*/
189
190    /*# Store the EP for later messaging #*/
191    /*- set namespace.ep = ep -*/
192/*- endmacro -*/
193
194/*# Establish the recv side of this connector for doing RPC.
195  # Has the same requirements as establish_from_rpc and produces the same namespace items
196  #*/
197/*- macro establish_recv_rpc(namespace, interface_name, buffer=none, language='c') -*/
198    /*- set namespace.language = language -*/
199    /*- if namespace.language == 'cakeml' -*/
200        /*? _begin_cakeml_module(namespace) ?*/
201    /*- endif -*/
202    /*# Establish the buffer for message contents #*/
203    /*? _establish_buffer(namespace, buffer, True) ?*/
204
205    /*# Ensure the endpoint is allocated #*/
206    /*- set ep_obj = alloc_obj('ep', seL4_EndpointObject) -*/
207    /*- set namespace.ep = alloc_cap('ep_%s' % me.interface.name, ep_obj, read=True) -*/
208
209    /*? allocate_badges(namespace) ?*/
210
211    /*- if language == 'c' -*/
212        /*? _make_get_sender_id_symbol(namespace, interface_name) ?*/
213    /*- elif language == 'cakeml' -*/
214        /*- set namespace.badge_symbol = 'badge' -*/
215    /*- endif -*/
216
217    /*# Allocate reply cap #*/
218    /*- if options.realtime -*/
219            /*- set namespace.reply_cap_slot = alloc('reply_cap_slot', seL4_RTReplyObject) -*/
220    /*- else -*/
221        /*- if me.might_block() -*/
222            /*# We're going to need a CNode cap in order to save our pending reply
223             * caps in the future.
224             #*/
225            /*- set namespace.cnode = alloc_cap('cnode', my_cnode) -*/
226            /*- set namespace.reply_cap_slot = alloc_cap('reply_cap_slot', None) -*/
227        /*- endif -*/
228    /*- endif -*/
229    /*- if namespace.language == 'cakeml' -*/
230    /*- endif -*/
231    /*- if namespace.language == 'cakeml' -*/
232        /*? _end_cakeml_module(namespace) ?*/
233    /*- endif -*/
234/*- endmacro -*/
235
236/*# *** The following functions all generated *code* that must be executed *** #*/
237
238/*# The code output by this macro must be *executed* once prior to the code generated by
239  # any of the other messaging macros for the recv side. This is special as a connector
240  # may need to do something special to setup for the first RPC
241  # Otherwise this is same as begin_recv
242  #*/
243/*- macro recv_first_rpc(namespace, size, might_block, notify_cptr=none, namespace_prefix='') -*/
244    /*- if not options.realtime and might_block -*/
245        /*- if namespace.language == 'cakeml' -*/
246            val _ = #(set_tls_cnode_cap) "" (Utils.int_to_bytes /*? namespace.cnode ?*/ 8);
247        /*- else -*/
248            camkes_get_tls()->cnode_cap = /*? namespace.cnode ?*/;
249        /*- endif -*/
250    /*- endif -*/
251    /*- if namespace.language == 'c' -*/
252        /*- set info = "%sinfo" % namespace_prefix -*/
253        /*- if notify_cptr is not none -*/
254            /* This interface has a passive thread, must let the control thread know before waiting */
255            seL4_MessageInfo_t /*? info ?*/ = {0};
256            /*? generate_seL4_SignalRecv(options,
257                                         info,
258                                         notify_cptr,
259                                         info, namespace.ep,
260                                         '&%s' % namespace.badge_symbol,
261                                         namespace.reply_cap_slot) ?*/;
262        /*- else -*/
263            /* This interface has an active thread, just wait for an RPC */
264            seL4_MessageInfo_t /*? info ?*/ = /*? generate_seL4_Recv(options, namespace.ep,
265                                                                    '&%s' % namespace.badge_symbol,
266                                                                     namespace.reply_cap_slot) ?*/;
267        /*- endif -*/
268        /*? _extract_size(namespace, info, size, True) ?*/
269    /*- elif namespace.language == 'cakeml' -*/
270        /*- if notify_cptr is not none -*/
271            /*? raise(TemplateError('CakeML connector does not support notification')) ?*/
272        /*- endif -*/
273        val (/*? size ?*/, /*? namespace.badge_symbol ?*/) =
274            Utils.seL4_Recv /*? namespace.ep ?*/ ConInternal.ipcbuf;
275    /*- endif -*/
276    /*? _save_reply_cap(namespace, might_block) ?*/
277/*- endmacro -*/
278
279/*# Releases ownership of the recv buffer #*/
280/*- macro complete_recv(namespace) -*/
281    /*#- nothing needs to be done for us -#*/
282/*- endmacro -*/
283
284/*# Takes ownership of the send buffer #*/
285/*- macro begin_reply(namespace) -*/
286    /*#- nothing needs to be done for us -#*/
287/*- endmacro -*/
288
289/*# Releases ownership of the send buffer #*/
290/*- macro complete_reply(namespace) -*/
291    /*#- nothing needs to be done for us -#*/
292/*- endmacro -*/
293
294/*# Recieves a message storing its length into the 'size' symbol and takes ownership
295  # of the recv buffer #*/
296/*- macro begin_recv(namespace, size, might_block, namespace_prefix='') -*/
297    /*-- set info = "%sinfo" % namespace_prefix -*/
298    seL4_MessageInfo_t /*? info ?*/ = /*? generate_seL4_Recv(options, namespace.ep,
299                                                             '&%s' % namespace.badge_symbol,
300                                                             namespace.reply_cap_slot) ?*/;
301    /*? _extract_size(namespace, info, size, True) ?*/
302    /*? _save_reply_cap(namespace, might_block) ?*/
303/*- endmacro -*/
304
305/*# Sends whatever message is in the send buffer with the given `length`, and then
306  # does begin_recv. This implicitly does complete_reply #*/
307/*- macro reply_recv(namespace, length, size, might_block, namespace_prefix='') -*/
308    /*- if namespace.language == 'c' -*/
309        /*-- set info = "%sinfo" % namespace_prefix -*/
310        seL4_MessageInfo_t /*? info ?*/ = seL4_MessageInfo_new(0, 0, 0, /* length */
311            /*-- if namespace.userspace_ipc --*/
312                0
313            /*-- else --*/
314                ROUND_UP_UNSAFE(/*? length ?*/, sizeof(seL4_Word)) / sizeof(seL4_Word)
315            /*-- endif --*/
316        );
317
318        /* Send the response */
319        /*-- if not options.realtime and might_block -*/
320            /*-- set tls = "%stls" % namespace_prefix -*/
321            camkes_tls_t * /*? tls ?*/ UNUSED = camkes_get_tls();
322            assert(/*? tls ?*/ != NULL);
323            if (/*? tls ?*/->reply_cap_in_tcb) {
324                /*? tls ?*/->reply_cap_in_tcb = false;
325                /*? info ?*/ = /*? generate_seL4_ReplyRecv(options, namespace.ep,
326                                                        info,
327                                                        '&%s' % namespace.badge_symbol,
328                                                        namespace.reply_cap_slot) ?*/;
329            } else {
330                camkes_unprotect_reply_cap();
331                seL4_Send(/*? namespace.reply_cap_slot ?*/, /*? info ?*/);
332                /*? info ?*/ = /*? generate_seL4_Recv(options, namespace.ep,
333                                                    '&%s' % namespace.badge_symbol,
334                                                    namespace.reply_cap_slot) ?*/;
335            }
336        /*-- elif options.realtime -*/
337            /*? info ?*/ = /*? generate_seL4_ReplyRecv(options, namespace.ep,
338                                                    info,
339                                                    '&%s' % namespace.badge_symbol,
340                                                    namespace.reply_cap_slot) ?*/;
341        /*-- else -*/
342            /*? info ?*/ = /*? generate_seL4_ReplyRecv(options, namespace.ep,
343                                                    info,
344                                                    '&%s' % namespace.badge_symbol,
345                                                    namespace.reply_cap_slot) ?*/;
346        /*-- endif -*/
347        /*? _extract_size(namespace, info, size, True) ?*/
348    /*- elif namespace.language == 'cakeml' -*/
349        /*- if options.realtime -*/
350            /*? raise(TemplateError('CakeML connector does not support realtime')) ?*/
351        /*- endif -*/
352        val (/*? size ?*/, /*? namespace.badge_symbol ?*/) =
353        /*- if might_block -*/
354                if Utils.clear_tls_reply_cap_in_tcb () then
355                    Utils.seL4_ReplyRecv /*? namespace.ep ?*/ /*? length ?*/ ConInternal.ipcbuf
356                else let
357                    val _ = Utils.seL4_Send /*? namespace.reply_cap_slot ?*/ /*? length ?*/ ConInternal.ipcbuf;
358                    in Utils.seL4_Recv /*? namespace.ep ?*/ ConInternal.ipcbuf end
359        /*- else -*/
360            Utils.seL4_ReplyRecv /*? namespace.ep ?*/ /*? length ?*/ ConInternal.ipcbuf
361        /*- endif -*/
362        ;
363    /*- endif -*/
364    /*? _save_reply_cap(namespace, might_block) ?*/
365/*- endmacro -*/
366
367/*# Takes ownership of the send buffer #*/
368/*- macro begin_send(namespace) -*/
369   /*- if namespace.lock -*/
370        /*- if me.might_block() and not options.realtime -*/
371        /* Save any pending reply cap as the lock will call seL4_Recv on an endpoint which
372         * will overwrite it. Note that we do this here before marshalling
373         * parameters to ensure we don't inadvertently overwrite any marshalled
374         * data with this call.
375         */
376        camkes_protect_reply_cap();
377        /*- endif -*/
378        sync_sem_bare_wait(/*? namespace.lock_ep ?*/,
379            &/*? namespace.lock_symbol ?*/);
380    /*- endif -*/
381/*- endmacro -*/
382
383/*# Sends a message and receives a reply. Implicitly does complete_reply and
384  # takes ownership of the recv buffer #*/
385/*- macro perform_call(namespace, size, length, namespace_prefix='') -*/
386    /* Call the endpoint */
387    /*-- set info = "%sinfo" % namespace_prefix -*/
388    seL4_MessageInfo_t /*? info ?*/ = seL4_MessageInfo_new(0, 0, 0,
389        /*-- if namespace.userspace_ipc --*/
390                0
391        /*-- else --*/
392                ROUND_UP_UNSAFE(/*? length ?*/, sizeof(seL4_Word)) / sizeof(seL4_Word)
393        /*-- endif --*/
394        );
395    /*? info ?*/ = seL4_Call(/*? namespace.ep ?*/, /*? info ?*/);
396
397    /*? size ?*/ =
398    /*-- if namespace.userspace_ipc -*/
399        /*? namespace.recv_buffer_size ?*/;
400    /*-- else -*/
401        seL4_MessageInfo_get_length(/*? info ?*/) * sizeof(seL4_Word);
402        assert(/*? size ?*/ <= seL4_MsgMaxLength * sizeof(seL4_Word));
403    /*-- endif -*/
404/*- endmacro -*/
405
406/*# Releases the recv buffer #*/
407/*- macro release_recv(namespace) -*/
408    /*- if namespace.lock -*/
409        sync_sem_bare_post(/*? namespace.lock_ep ?*/,
410            &/*? namespace.lock_symbol ?*/);
411    /*- endif -*/
412/*- endmacro -*/
413