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