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#include <autoconf.h> 14#include <sel4camkes/gen_config.h> 15#include <sel4runtime/gen_config.h> 16#include <assert.h> 17#include <camkes.h> /* generated header */ 18#include <platsupport/io.h> 19#include <sel4/types.h> 20#include <sel4/sel4.h> 21#include <sync/mutex.h> 22#include <sync/sem.h> 23#include <sync/bin_sem.h> 24#include <sel4platsupport/platsupport.h> 25#include <camkes/allocator.h> 26#include <camkes/dataport.h> 27#include <camkes/dma.h> 28#include <camkes/error.h> 29#include <camkes/fault.h> 30#include <camkes/io.h> 31#include <camkes/init.h> 32#include <camkes/pid.h> 33#include <camkes/tls.h> 34#include <camkes/vma.h> 35#include <camkes/syscalls.h> 36#include <sel4runtime.h> 37#include <stdbool.h> 38#include <stdint.h> 39#include <stdlib.h> 40#include <string.h> 41#include <strings.h> 42#include <sync/sem-bare.h> 43#include <sel4utils/mapping.h> 44#include <sys/types.h> 45#include <unistd.h> 46#include <utils/util.h> 47#include <arch_stdio.h> 48 49/*? macros.show_includes(me.type.includes) ?*/ 50 51static void (* _putchar)(int c); 52 53void set_putchar(void (*putchar)(int c)) { 54 _putchar = putchar; 55} 56 57static 58void __camkes_putchar(int c) { 59 if (_putchar != NULL) { 60 _putchar(c); 61 return; 62 } 63#ifdef CONFIG_PRINTING 64 seL4_DebugPutChar(c); 65#endif 66} 67 68static size_t 69write_buf(void *data, size_t count) 70{ 71 char* buf = data; 72 for (int i = 0; i < count; i++) { 73 __camkes_putchar(buf[i]); 74 } 75 return count; 76} 77 78const char *get_instance_name(void) { 79 static const char name[] = "/*? me.name ?*/"; 80 return name; 81} 82 83/*- set cnode_size = configuration[me.address_space].get('cnode_size_bits') -*/ 84/*- if cnode_size -*/ 85 /*- if isinstance(cnode_size, six.string_types) -*/ 86 /*- set size = int(cnode_size, 0) -*/ 87 /*- else -*/ 88 /*- set size = cnode_size -*/ 89 /*- endif -*/ 90 /*- do my_cnode.__setattr__('size_bits', size) -*/ 91/*- endif -*/ 92 93/* DTB passthrough */ 94 95 96/*# See if this component uses the DTB #*/ 97/*- set dtb_dict = [] -*/ 98/*- if configuration[me.name].get('dtb') -*/ /*# Account for the top level .camkes file case, i.e. app #*/ 99 /*- do dtb_dict.append(configuration[me.name].get('dtb')) -*/ 100/*- else -*/ /*# Account for the nested .camkes files, i.e. SerialServer/TimeServer #*/ 101 /*# Check the interfaces and see if the flag is turned on, 102 *# this assumes that the interfaces that will turn on the flag 103 *# is connected with a variant of the DTB connectors 104 #*/ 105 /*- if me.type.composition -*/ 106 /*- for c in me.type.composition.connections -*/ 107 /*- set interface_name = c.to_end.interface.name -*/ 108 /*- set interface_config_key = '%s.%s' % (me.name, interface_name) -*/ 109 /*- if configuration.get(interface_config_key) -*/ 110 /*- if configuration[interface_config_key].get('dtb') -*/ 111 /*- do dtb_dict.append(configuration[interface_config_key].get('dtb')) -*/ 112 /*- break -*/ 113 /*- endif -*/ 114 /*- endif -*/ 115 /*- endfor -*/ 116 /*- endif -*/ 117/*- endif -*/ 118 119/*# Output flags to get the loader to copy the DTB over #*/ 120/*- if len(dtb_dict) -*/ 121 /*- set dtb_size = dtb_dict[0]['dtb_size'][0] -*/ 122 /*# Calculate the multiple of 4K pages that can fit the DTB, add an extra for the bootinfo header #*/ 123 /*- set rounded_size = macros.ROUND_UP(dtb_size, 4096) + 4096 -*/ 124 char dtb_symbol[/*? rounded_size ?*/] 125 ALIGN(PAGE_SIZE_4K) SECTION("align_12bit"); 126 /*- do register_fill_frame('dtb_symbol', 'CDL_FrameFill_BootInfo CDL_FrameFill_BootInfo_FDT', rounded_size) -*/ 127/*- endif -*/ 128 129/* DMA functionality. */ 130 131/*# Determine the size of the DMA pool. Note that we make no attempt to 132 *# suppress this attribute being generated as a user-accessible variable at 133 *# the top of this file. If the component actually has a declared attribute 134 *# 'dma_pool' then they will get access to this variable at runtime. 135 #*/ 136/*- set dma_pool = macros.ROUND_UP(configuration[me.name].get('dma_pool', 0), macros.PAGE_SIZE) -*/ 137/*- set dma_pool_cache = configuration[me.name].get('dma_pool_cached', False) -*/ 138/*- set dma_pool_paddr = configuration[me.name].get('dma_pool_paddr', None) -*/ 139/*- set page_size = [macros.PAGE_SIZE] -*/ 140/*- if options.largeframe_dma -*/ 141 /*- for sz in reversed(macros.page_sizes(options.architecture)) -*/ 142 /*- if dma_pool >= sz -*/ 143 /*- do page_size.__setitem__(0, sz) -*/ 144 /*- break -*/ 145 /*- endif -*/ 146 /*- endfor -*/ 147/*- endif -*/ 148 149/*- set dma_symbol_name = "%s_dma_pool_symbol" % me.name.replace('.', '_') -*/ 150char /*? dma_symbol_name ?*/[/*? dma_pool ?*/] 151 /*- set page_size_bits = int(math.log(page_size[0], 2)) -*/ 152 SECTION("align_/*? page_size_bits ?*/bit") 153 ALIGN(/*? page_size[0] ?*/); 154 155/*- set dma_frames = [] -*/ 156/*- set num_dma_frames = int(macros.ROUND_UP(dma_pool, page_size[0]) // page_size[0]) -*/ 157 158/*- set dma_frames = [] -*/ 159/*? register_shared_variable('%s_dma' % me.name, dma_symbol_name , num_dma_frames*page_size[0], frame_size=page_size[0], label=me.label(), perm='RW', cached=dma_pool_cache, with_mapping_caps=dma_frames, paddr=dma_pool_paddr) ?*/ 160 161/*# Expose the frames backing the DMA pool #*/ 162/*- for cap in dma_frames -*/ 163 static dma_frame_t /*? me.instance.name ?*/_dma_/*? loop.index0 ?*/ = { 164 .cap = /*? cap ?*/, 165 .size = /*? page_size[0] ?*/, 166 .vaddr = (uintptr_t) &/*? dma_symbol_name ?*/[/*? loop.index0 * page_size[0] ?*/], 167 .cached = /*? int(dma_pool_cache) ?*/, 168 }; 169 USED SECTION("_dma_frames") 170 dma_frame_t * /*? me.instance.name ?*/_dma_/*? loop.index0 ?*/_ptr = &/*? me.instance.name ?*/_dma_/*? loop.index0 ?*/; 171/*- endfor -*/ 172 173/* Mutex functionality. */ 174/*- for m in me.type.mutexes -*/ 175 176/*- set mutex = c_symbol(m.name) -*/ 177static sync_mutex_t /*? mutex ?*/; 178 179static int mutex_/*? m.name ?*/_init(void) { 180 /*- set notification = alloc(m.name, seL4_NotificationObject, read=True, write=True) -*/ 181 return sync_mutex_init(&/*? mutex ?*/, /*? notification ?*/); 182} 183 184int /*? m.name ?*/_lock(void) { 185 return sync_mutex_lock(&/*? mutex ?*/); 186} 187 188int /*? m.name ?*/_unlock(void) { 189 return sync_mutex_unlock(&/*? mutex ?*/); 190} 191 192/*- endfor -*/ 193 194/* Semaphore functionality. */ 195/*- for s in me.type.semaphores -*/ 196 197/*- set semaphore = c_symbol(s.name) -*/ 198static sync_sem_t /*? semaphore ?*/; 199 200static int semaphore_/*? s.name ?*/_init(void) { 201 /*- set ep = alloc(s.name, seL4_EndpointObject, read=True, write=True) -*/ 202 return sync_sem_init(&/*? semaphore ?*/, /*? ep ?*/, 203 /*? configuration[me.name].get('%s_value' % s.name, 1) ?*/); 204} 205 206int /*? s.name ?*/_wait(void) { 207#ifndef CONFIG_KERNEL_MCS 208 camkes_protect_reply_cap(); 209#endif 210 return sync_sem_wait(&/*? semaphore ?*/); 211} 212 213int /*? s.name ?*/_trywait(void) { 214 return sync_sem_trywait(&/*? semaphore ?*/); 215} 216 217int /*? s.name ?*/_post(void) { 218 return sync_sem_post(&/*? semaphore ?*/); 219} 220 221/*- endfor -*/ 222 223/*- for b in me.type.binary_semaphores -*/ 224 225/*- set binary_semaphore = c_symbol(b.name) -*/ 226static sync_bin_sem_t /*? binary_semaphore ?*/; 227 228static int binary_semaphore_/*? b.name ?*/_init(void) { 229 /*- set notification = alloc(b.name, seL4_NotificationObject, read=True, write=True) -*/ 230 /*- set initial = configuration[me.name].get('%s_value' % b.name, 0) -*/ 231 /*? assert(initial in (0, 1), "Expected 0 or 1 as initial value for binary semaphore \"%s\". Got %d." % (b.name, initial)) ?*/ 232 return sync_bin_sem_init(&/*? binary_semaphore ?*/, /*? notification ?*/, /*? initial ?*/); 233} 234 235int /*? b.name ?*/_wait(void) { 236 return sync_bin_sem_wait(&/*? binary_semaphore ?*/); 237} 238 239int /*? b.name ?*/_post(void) { 240 return sync_bin_sem_post(&/*? binary_semaphore ?*/); 241} 242 243/*- endfor -*/ 244 245#ifdef CONFIG_CAMKES_DEFAULT_HEAP_SIZE 246/*- set heap_size = configuration[me.name].get('heap_size', 'CONFIG_CAMKES_DEFAULT_HEAP_SIZE') -*/ 247 248static char heap [/*? heap_size ?*/]; 249extern char *morecore_area; 250extern size_t morecore_size; 251#else 252/*- if configuration[me.name].get('heap_size') is not none -*/ 253 #error Set a custom heap_size for component '/*? me.name ?*/' but this has no effect if CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES is not set to 0 254/*- endif -*/ 255#endif 256 257/* Install additional syscalls in an init constructor instead of in 258 * init so that there is a way for other applications to decide whether 259 * they want to provide their syscall implementation before or after 260 * the camkes ones */ 261static void CONSTRUCTOR(CAMKES_SYSCALL_CONSTRUCTOR_PRIORITY) init_install_syscalls(void) { 262 camkes_install_syscalls(); 263} 264 265/* General CAmkES platform initialisation. Expects to be run in a 266 * single-threaded, exclusive context. On failure it does not return. 267 */ 268static void CONSTRUCTOR(CAMKES_SYSCALL_CONSTRUCTOR_PRIORITY+1) init(void) { 269#ifdef CONFIG_CAMKES_DEFAULT_HEAP_SIZE 270 /* Assign the heap */ 271 morecore_area = heap; 272 morecore_size = /*? heap_size ?*/; 273#endif 274 275 /* The user has actually had no opportunity to install any error handlers at 276 * this point, so any error triggered below will certainly be fatal. 277 */ 278 int res = camkes_dma_init(/*? dma_symbol_name ?*/, /*? dma_pool ?*/, 279 /*? page_size[0] ?*/); 280 ERR_IF(res != 0, camkes_error, ((camkes_error_t){ 281 .type = CE_ALLOCATION_FAILURE, 282 .instance = "/*? me.name ?*/", 283 .description = "DMA initialisation failed", 284 }), ({ 285 return; 286 })); 287 /*- for m in me.type.mutexes -*/ 288 res = mutex_/*? m.name ?*/_init(); 289 ERR_IF(res != 0, camkes_error, ((camkes_error_t){ 290 .type = CE_ALLOCATION_FAILURE, 291 .instance = "/*? me.name ?*/", 292 .description = "initialisation of mutex \"/*? m.name ?*/\" failed", 293 }), ({ 294 return; 295 })); 296 /*- endfor -*/ 297 /*- for s in me.type.semaphores -*/ 298 res = semaphore_/*? s.name ?*/_init(); 299 ERR_IF(res != 0, camkes_error, ((camkes_error_t){ 300 .type = CE_ALLOCATION_FAILURE, 301 .instance = "/*? me.name ?*/", 302 .description = "initialisation of semaphore \"/*? s.name ?*/\" failed", 303 }), ({ 304 return; 305 })); 306 /*- endfor -*/ 307 /*- for b in me.type.binary_semaphores -*/ 308 res = binary_semaphore_/*? b.name ?*/_init(); 309 ERR_IF(res != 0, camkes_error, ((camkes_error_t){ 310 .type = CE_ALLOCATION_FAILURE, 311 .instance = "/*? me.name ?*/", 312 .description = "initialisation of binary semaphore \"/*? b.name ?*/\" failed", 313 }), ({ 314 return; 315 })); 316 /*- endfor -*/ 317 318 /* Initialise cap allocator. */ 319 /*- set tcb_pool = configuration[me.name].get('tcb_pool', 0) -*/ 320 /*- for i in six.moves.range(tcb_pool) -*/ 321 /*- set _tcb = alloc_obj('tcb_pool_%d' % i, seL4_TCBObject) -*/ 322 /*- set tcb = alloc_cap('tcb_pool_%d' % i, _tcb) -*/ 323 /*- do _tcb.__setattr__('resume', false) -*/ 324 /*- if "tcb_pool_domains" in configuration[me.name] -*/ 325 /*- do _tcb.__setattr__('domain', configuration[me.name].get('tcb_pool_domains')[i]) -*/ 326 /*- endif -*/ 327 res = camkes_provide(seL4_TCBObject, /*? tcb ?*/, 0, 0); 328 ERR_IF(res != 0, camkes_error, ((camkes_error_t){ 329 .type = CE_ALLOCATION_FAILURE, 330 .instance = "/*? me.name ?*/", 331 .description = "failed to add TCB /*? tcb + 1 ?*/ to cap allocation pool", 332 }), ({ 333 return; 334 })); 335 /*- endfor -*/ 336 /*- set ep_pool = configuration[me.name].get('ep_pool', 0) -*/ 337 /*- for i in six.moves.range(ep_pool) -*/ 338 /*- set ep = alloc('ep_pool_%d' % i, seL4_EndpointObject, read=True, write=True) -*/ 339 res = camkes_provide(seL4_EndpointObject, /*? ep ?*/, 0, seL4_CanRead|seL4_CanWrite); 340 ERR_IF(res != 0, camkes_error, ((camkes_error_t){ 341 .type = CE_ALLOCATION_FAILURE, 342 .instance = "/*? me.name ?*/", 343 .description = "failed to add EP /*? ep + 1 ?*/ to cap allocation pool", 344 }), ({ 345 return; 346 })); 347 /*- endfor -*/ 348 /*- set notification_pool = configuration[me.name].get('notification_pool', 0) -*/ 349 /*- for i in six.moves.range(notification_pool) -*/ 350 /*- set notification = alloc('notification_pool_%d' % i, seL4_NotificationObject, read=True, write=True) -*/ 351 res = camkes_provide(seL4_NotificationObject, /*? notification ?*/, 0, seL4_CanRead.words[0]|seL4_CanWrite.words[0]); 352 ERR_IF(res != 0, camkes_error, ((camkes_error_t){ 353 .type = CE_ALLOCATION_FAILURE, 354 .instance = "/*? me.name ?*/", 355 .description = "failed to add NOTIFICATION /*? notification + 1 ?*/ to cap allocation pool", 356 }), ({ 357 return; 358 })); 359 /*- endfor -*/ 360 /*- set untyped_pool = [] -*/ 361 /*- for attribute, value in configuration[me.name].items() -*/ 362 /*- set r = re.match('untyped(\\d+)_pool$', attribute) -*/ 363 /*- if r is not none -*/ 364 /*- do untyped_pool.append((r.group(1), value)) -*/ 365 /*- endif -*/ 366 /*- endfor -*/ 367 /*- for u in untyped_pool -*/ 368 /*- for i in six.moves.range(u[1]) -*/ 369 /*- if not 4 <= int(u[0]) <= 28 -*/ 370 /*? raise(TemplateError('illegal untyped size')) ?*/ 371 /*- endif -*/ 372 /*- set untyped = alloc('untyped_%s_pool_%d' % (u[0], i), seL4_UntypedObject, size_bits=int(u[0])) -*/ 373 res = camkes_provide(seL4_UntypedObject, /*? untyped ?*/, 1U << /*? u[0] ?*/, seL4_CanRead|seL4_CanWrite); 374 ERR_IF(res != 0, camkes_error, ((camkes_error_t){ 375 .type = CE_ALLOCATION_FAILURE, 376 .instance = "/*? me.name ?*/", 377 .description = "failed to add untyped /*? untyped + 1 ?*/ of size /*? u[0] ?*/ bits to cap allocation pool", 378 }), ({ 379 return; 380 })); 381 /*- endfor -*/ 382 /*- endfor -*/ 383} 384 385/*- for i in me.type.provides + me.type.uses -*/ 386 /*? macros.show_includes(i.type.includes) ?*/ 387/*- endfor -*/ 388 389/*- set threads = macros.threads(composition, me, configuration[me.name], options) -*/ 390 391/*- if options.debug_fault_handlers -*/ 392 /*- set fault_ep = alloc_obj('fault_ep', seL4_EndpointObject) -*/ 393/*- endif -*/ 394 395/*- if options.realtime -*/ 396 /*# SC to use to initialise all passive interfaces of this instance #*/ 397 /*- set sc_passive_init = alloc('%d_0_control_%d_passive_init_sc' % (len(me.name), len('0_control')), seL4_SchedContextObject) -*/ 398 399 /*# Ntfn to use in passive init protocol #*/ 400 /*- set ntfn_passive_init = alloc('%d_0_control_%d_passive_init_ntfn' % (len(me.name), len('0_control')), seL4_NotificationObject, read=True, write=True) -*/ 401 402 /*# Dict mapping thread prefixes to tcb caps #*/ 403 /*- set passive_tcbs = {} -*/ 404 405 /*# Set of Thread objects corresponding to passive threads #*/ 406 /*- set passive_threads = set() -*/ 407/*- endif -*/ 408 409/*- set thread_names = dict() -*/ 410/*- for t in threads -*/ 411 /* Thread stacks */ 412 /*? macros.thread_stack(t.stack_symbol, t.stack_size) ?*/ 413 /*- do register_stack_symbol(t.stack_symbol, t.stack_size) -*/ 414 415 /* IPC buffers */ 416 /*? macros.ipc_buffer(t.ipc_symbol) ?*/ 417 /*- set ipc_frame = alloc_obj('frame_%s' % (t.ipc_symbol), seL4_FrameObject) -*/ 418 /*- do register_ipc_symbol(t.ipc_symbol, ipc_frame) -*/ 419 420 /*- set _tcb = alloc_obj("%s_tcb" % t.name, seL4_TCBObject) -*/ 421 /*- set tcb = alloc_cap("%s_tcb" % t.name, _tcb) -*/ 422 /*- do _tcb.__setitem__('ipc_buffer_slot', Cap(ipc_frame, read=True, write=True)) -*/ 423 /*- do _tcb.__setitem__('vspace', Cap(my_pd)) -*/ 424 /*- set cnode_cap = Cap(my_cnode) -*/ 425 /*- do my_cnode.update_guard_size_caps.append(cnode_cap) -*/ 426 /*- do _tcb.__setitem__('cspace', cnode_cap) -*/ 427 428 /*- do _tcb.__setattr__('ip', "get_vaddr(\'%s\')" % ("camkes %s _camkes_start" % me.name) ) -*/ 429 /*- do _tcb.__setattr__('sp', t.sp) -*/ 430 /*- do _tcb.__setattr__('addr', t.addr) -*/ 431 /*- do _tcb.init.append(tcb) -*/ 432 433 /*- if options.realtime -*/ 434 /*- if not t.interface or not configuration[me.name].get("%s_passive" % t.interface.name, False) -*/ 435 /*- set _sc = alloc_obj("%s_sc" % t.name, seL4_SchedContextObject) -*/ 436 /*- set sc = alloc_cap("%s_sc" % t.name, _sc) -*/ 437 /*- do _tcb.__setitem__('sc_slot', Cap(_sc)) -*/ 438 /*- if loop.first -*/ 439 /*- do macros.set_sc_properties(_sc, options, configuration[me.name], "_") -*/ 440 /*- elif options.debug_fault_handlers and loop.last -*/ 441 /*- do macros.set_sc_properties(_sc, options, configuration[me.name], "fault") -*/ 442 /*- else -*/ 443 /*- do macros.set_sc_properties(_sc, options, configuration[me.name], "%s_" % t.interface.name) -*/ 444 /*- endif -*/ 445 /*- else -*/ 446 /*# This branch is for interface threads that are passive #*/ 447 /*- do passive_tcbs.__setitem__(t.name, tcb) -*/ 448 /*- do passive_threads.add(t) -*/ 449 /*- endif -*/ 450 /*- endif -*/ 451 452 /*- if options.debug_fault_handlers and not loop.last -*/ 453 /*- if not options.realtime -*/ 454 /*- set fault_ep_cap = alloc_cap('fault_ep_%s' % t.name, fault_ep, read=True, write=True, grantreply=True, badge=tcb) -*/ 455 /*- do setattr(_tcb, 'fault_ep_slot', fault_ep_cap) -*/ 456 /*- endif -*/ 457 458 /*- if options.realtime -*/ 459 /*- do _tcb.set_fault_ep_slot(fault_ep=fault_ep.name, badge=tcb) -*/ 460 /*- endif -*/ 461 462 /*- endif -*/ 463 464 /*- if loop.first -*/ 465 /*- do macros.set_tcb_properties(_tcb, options, configuration[me.name], "_") -*/ 466 /*- do thread_names.__setitem__(tcb, "control") -*/ 467 /*- elif options.debug_fault_handlers and loop.last -*/ 468 /*- do thread_names.__setitem__(tcb, "fault_handler") -*/ 469 /*- do _tcb.__setattr__('prio', 255) -*/ 470 /*- do _tcb.__setattr__('affinity', options.default_affinity) -*/ 471 /*- do _tcb.__setattr__('max_prio', options.default_max_priority) -*/ 472 473 /*- else -*/ 474 /*- do thread_names.__setitem__(tcb, t.interface.name) -*/ 475 /*- do macros.set_tcb_properties(_tcb, options, configuration[me.name], "%s_" % t.interface.name) -*/ 476 /*- endif -*/ 477 478 479/*- endfor -*/ 480 481/* Attributes */ 482/*- set myconf = configuration[me.name] -*/ 483/*- for a in me.type.attributes -*/ 484 /*- set value = myconf.get(a.name) -*/ 485 /*- if value is not none -*/ 486 const /*? macros.show_type(a.type) ?*/ /*? a.name ?*//*- if a.array -*/ [/*?len(value)?*/] /*- endif -*/ = 487 /*? macros.show_attribute_value(a, value) ?*/ 488 ; 489 /*- endif -*/ 490/*- endfor -*/ 491 492/*- if options.debug_fault_handlers -*/ 493 /*- set fault_ep = alloc_obj('fault_ep', seL4_EndpointObject) -*/ 494/*- endif -*/ 495 496const char * get_thread_name(int thread_id) { 497 switch (thread_id) { 498 /*- for id, name in thread_names.items() -*/ 499 case /*? id ?*/: return "/*?name?*/"; 500 /*- endfor -*/ 501 } 502 return "(unknown)"; 503} 504 505static int post_main(int thread_id); 506void USED NORETURN _camkes_start_c(int thread_id) { 507 /*- set tcb_control = alloc("%s_tcb" % threads[0].name, seL4_TCBObject) -*/ 508 if (thread_id != /*? tcb_control ?*/) { 509 post_main(thread_id); 510 } else { 511 sel4muslcsys_register_stdio_write_fn(write_buf); 512 void *ipc_buf_ptr = (void *) /*? macros.ipc_buffer_address(threads[0].ipc_symbol) ?*/; 513 camkes_start_control(thread_id, ipc_buf_ptr); 514 } 515 UNREACHABLE(); 516} 517 518// a tls region for every thread except the control thread 519static void *tls_regions[/*? len(threads) - 1 ?*/]; 520// static tls regions 521static char static_tls_regions[/*? len(threads) - 1 ?*/][CONFIG_SEL4RUNTIME_STATIC_TLS]; 522 523void camkes_tls_init(int thread_id) { 524 switch (thread_id) { 525 /*- for index, t in enumerate(threads) -*/ 526 /*- set tcb = alloc('%s_tcb' % t.name, seL4_TCBObject) -*/ 527 528 case /*? tcb ?*/ : { /* Thread /*? t.name ?*/ */ 529 /*- if tcb == tcb_control -*/ 530 // the control thread has an initial tls region created for it, 531 // but this may fail if the tls region is too big. 532 ZF_LOGF_IF(!sel4runtime_initial_tls_enabled(), "Failed to init TLS"); 533 /*- else -*/ 534 void *tls_mem = tls_regions[/*? loop.index - 2?*/]; 535 assert(tls_mem != NULL); 536 uintptr_t tls_base = sel4runtime_write_tls_image(tls_mem); 537 sel4runtime_set_tls_base(tls_base); 538 ZF_LOGF_IF(!tls_base, "Failed to write new tls"); 539 __sel4_ipc_buffer = (seL4_IPCBuffer *) /*? macros.ipc_buffer_address(t.ipc_symbol) ?*/; 540 /*- endif -*/ 541 /*- if options.realtime and loop.first -*/ 542 /*- set sc_context = alloc("%s_sc" % t.name, seL4_SchedContextObject) -*/ 543 camkes_get_tls()->sc_cap = /*? sc_context ?*/; 544 /*- endif -*/ 545 camkes_get_tls()->tcb_cap = /*? tcb ?*/; 546 camkes_get_tls()->thread_index = /*? index ?*/ + 1; 547 break; 548 } 549 /*- endfor -*/ 550 551 default: 552 assert(!"invalid thread ID"); 553 } 554 555/*- if options.fprovide_tcb_caps -*/ 556#ifdef CONFIG_DEBUG_BUILD 557 char thread_name[seL4_MsgMaxLength * sizeof(seL4_Word)]; 558 snprintf(thread_name, sizeof(thread_name), "%s:%s", 559 get_instance_name(), get_thread_name(thread_id)); 560 thread_name[sizeof(thread_name) - 1] = '\0'; 561 seL4_DebugNameThread(camkes_get_tls()->tcb_cap, thread_name); 562#endif 563/*- endif -*/ 564} 565/*- if options.debug_fault_handlers -*/ 566 static void fault_handler(void) UNUSED NORETURN; 567 static void fault_handler(void) { 568 while (true) { 569 seL4_Word badge; 570 571 /* Wait for a fault from one of the component's threads. */ 572 /*- set fault_ep_cap = alloc_cap('fault_ep__fault_handler', fault_ep, read=True, write=True, grantreply=True) -*/ 573 /*- if options.realtime -*/ 574 /*- set fault_reply_cap = alloc('fault_reply__fault_handler', seL4_RTReplyObject) -*/ 575 /*- endif -*/ 576 seL4_MessageInfo_t info = /*? generate_seL4_Recv(options, fault_ep_cap, '&badge', fault_reply_cap) ?*/; 577 578 /* Various symbols that are provided by the linker script. */ 579 extern const char __executable_start[1]; 580 extern const char align_12bit[1] UNUSED; 581 extern const char _end[1] UNUSED; 582 583 /* Thread name and address space map relevant for this fault. Note 584 * that we describe a simplified version of the component's address 585 * space below (e.g. we only describe the stack of the current 586 * thread). The assumption is that the full address space will 587 * confuse the user and most likely not be relevant for diagnosing 588 * the fault. E.g. you may have faulted on another thread's guard 589 * page, which will not be revealed to you in the memory map, but 590 * it is unlikely this information will help you diagnose the cause 591 * of the fault anyway. 592 */ 593 const char *thread_name; 594 const camkes_memory_region_t *memory_map; 595 596 /* Each of the component's threads have a badged endpoint, so we 597 * can determine from the badge of the message we just received 598 * which thread was responsible for the fault. 599 */ 600 switch (badge) { 601 602 /*- for t in threads -*/ 603 /*- set tcb = alloc('%s_tcb' % t.name, seL4_TCBObject) -*/ 604 case /*? tcb ?*/ : { 605 thread_name = "/*? t.name ?*/"; 606 memory_map = (camkes_memory_region_t[]){ 607 { .start = (uintptr_t)__executable_start, 608 .end = (uintptr_t)align_12bit - 1, 609 .name = "code and data" }, 610 { .start = (uintptr_t)&/*? t.stack_symbol ?*/, 611 .end = (uintptr_t)&/*? t.stack_symbol ?*/ + PAGE_SIZE_4K - 1, 612 .name = "guard page" }, 613 { .start = (uintptr_t)&/*? t.stack_symbol ?*/ + PAGE_SIZE_4K, 614 .end = (uintptr_t)&/*? t.stack_symbol ?*/ + 615 sizeof(/*? t.stack_symbol ?*/) - PAGE_SIZE_4K - 1, 616 .name = "stack" }, 617 { .start = (uintptr_t)&/*? t.stack_symbol ?*/ + 618 sizeof(/*? t.stack_symbol ?*/) - PAGE_SIZE_4K, 619 .end = (uintptr_t)&/*? t.stack_symbol ?*/ + 620 sizeof(/*? t.stack_symbol ?*/) - 1, 621 .name = "guard page" }, 622 { .start = (uintptr_t)&/*? t.ipc_symbol ?*/, 623 .end = (uintptr_t)&/*? t.ipc_symbol ?*/ + PAGE_SIZE_4K - 1, 624 .name = "guard page" }, 625 { .start = (uintptr_t)&/*? t.ipc_symbol ?*/ + PAGE_SIZE_4K, 626 .end = (uintptr_t)&/*? t.ipc_symbol ?*/ + 627 sizeof(/*? t.ipc_symbol ?*/) - PAGE_SIZE_4K - 1, 628 .name = "IPC buffer" }, 629 { .start = (uintptr_t)&/*? t.ipc_symbol ?*/ + 630 sizeof(/*? t.ipc_symbol ?*/) - PAGE_SIZE_4K, 631 .end = (uintptr_t)&/*? t.ipc_symbol ?*/ + 632 sizeof(/*? t.ipc_symbol ?*/) - 1, 633 .name = "guard page" }, 634 { .start = 0, .end = 0, .name = NULL }, 635 }; 636 break; 637 } 638 /*- endfor -*/ 639 640 default: 641 thread_name = "<unknown>"; 642 memory_map = NULL; 643 break; 644 } 645 646 camkes_show_fault(info, (seL4_CPtr)badge, thread_name, 647 /*- if options.fprovide_tcb_caps -*/ 648 true, 649 /*- else -*/ 650 false, 651 /*- endif -*/ 652 memory_map); 653 } 654 } 655/*- endif -*/ 656 657/*# Locks for synchronising init ops. These are used by 658 pre_init_interface_sync, post_init_interface_sync and post_main 659 #*/ 660/*- set pre_init_ep = alloc('pre_init_ep', seL4_EndpointObject, read=True, write=True) -*/ 661static volatile int UNUSED pre_init_lock = 0; 662/*- set interface_init_ep = alloc('interface_init_ep', seL4_EndpointObject, read=True, write=True) -*/ 663static volatile int UNUSED interface_init_lock = 0; 664/*- set post_init_ep = alloc('post_init_ep', seL4_EndpointObject, read=True, write=True) -*/ 665static volatile int UNUSED post_init_lock = 0; 666 667int pre_init_interface_sync() { 668 int result UNUSED; 669 670 /* Wake all the non-passive interface threads. */ 671 /*- for t in threads[1:] -*/ 672 /*- if not options.realtime or t not in passive_threads -*/ 673 sync_sem_bare_post(/*? pre_init_ep ?*/, &pre_init_lock); 674 /*- endif -*/ 675 /*- endfor -*/ 676 677 /* Wait for all the non-passive interface threads to run their inits. */ 678 /*- for t in threads[1:] -*/ 679 /*- if not (options.debug_fault_handlers and loop.last) -*/ 680 /*- if not options.realtime or t not in passive_threads -*/ 681 sync_sem_bare_wait(/*? interface_init_ep ?*/, &interface_init_lock); 682 /*- endif -*/ 683 /*- endif -*/ 684 /*- endfor -*/ 685 686 /*- if options.realtime -*/ 687 /* Wake each passive thread one at a time and allow it to run its init. */ 688 /*- for prefix, tcb in passive_tcbs.items() -*/ 689 result = seL4_SchedContext_Bind(/*? sc_passive_init ?*/, /*? tcb ?*/); 690 ERR_IF(result != 0, camkes_error, ((camkes_error_t){ 691 .type = CE_SYSCALL_FAILED, 692 .instance = "/*? me.name ?*/", 693 .description = "failed to bind initialisation scheduling context for thread \"/*? prefix ?*/_tcb\"", 694 .syscall = SchedContextBind, 695 .error = result, 696 }), ({ 697 return -1; 698 })); 699 700 /*# Wake thread #*/ 701 sync_sem_bare_post(/*? pre_init_ep ?*/, &pre_init_lock); 702 703 /*# Wait for thread to run its init #*/ 704 sync_sem_bare_wait(/*? interface_init_ep ?*/, &interface_init_lock); 705 706 result = seL4_SchedContext_Unbind(/*? sc_passive_init ?*/); 707 ERR_IF(result != 0, camkes_error, ((camkes_error_t){ 708 .type = CE_SYSCALL_FAILED, 709 .instance = "/*? me.name ?*/", 710 .description = "failed to unbind initialisation scheduling context for thread \"/*? prefix ?*/_tcb\"", 711 .syscall = SchedContextUnbind, 712 .error = result, 713 }), ({ 714 return -1; 715 })); 716 /*- endfor -*/ 717 /*- endif -*/ 718 return 0; 719} 720 721int post_init_interface_sync() { 722 int result UNUSED; 723 724 /* Wake all the interface threads, including passive threads. 725 * Passive threads will receive the IPC despite not having scheduling contexts 726 * at this point. Next time they are given scheduling contexts they will be 727 * unblocked. */ 728 /*- for _ in threads[1:] -*/ 729 /*- if not (options.debug_fault_handlers and loop.last) -*/ 730 sync_sem_bare_post(/*? post_init_ep ?*/, &post_init_lock); 731 /*- endif -*/ 732 /*- endfor -*/ 733 734 /*- if options.realtime -*/ 735 /* Tempororily bind a scheduling context to each passive thread 736 * and allow it to start waiting on an endpoint. Threads will 737 * indicate that they are ready to have their sc unbound when 738 * they send on the init notification. */ 739 /*- for prefix, tcb in passive_tcbs.items() -*/ 740 741 /*# Bind the initialision scheduling context to the tcb. #*/ 742 result = seL4_SchedContext_Bind(/*? sc_passive_init ?*/, /*? tcb ?*/); 743 ERR_IF(result != 0, camkes_error, ((camkes_error_t){ 744 .type = CE_SYSCALL_FAILED, 745 .instance = "/*? me.name ?*/", 746 .description = "failed to bind initialisation scheduling context for thread \"/*? prefix ?*/_tcb\"", 747 .syscall = SchedContextBind, 748 .error = result, 749 }), ({ 750 return -1; 751 })); 752 753 /*# Wait until the passive interface is finished initialising. #*/ 754 seL4_Wait(/*? ntfn_passive_init ?*/, NULL); 755 756 /*# Unbind the sc from the tcb. #*/ 757 result = seL4_SchedContext_Unbind(/*? sc_passive_init ?*/); 758 ERR_IF(result != 0, camkes_error, ((camkes_error_t){ 759 .type = CE_SYSCALL_FAILED, 760 .instance = "/*? me.name ?*/", 761 .description = "failed to unbind initialisation scheduling context for thread \"/*? prefix ?*/_tcb\"", 762 .syscall = SchedContextUnbind, 763 .error = result, 764 }), ({ 765 return -1; 766 })); 767 /*- endfor -*/ 768 /*- endif -*/ 769 return 0; 770} 771 772static int post_main(int thread_id) { 773 int ret = 0; 774 switch (thread_id) { 775 776 case 0: 777 /* This case is just here to help debugging. If you hit this case, 778 * what is happening is probably a failure in passing arguments 779 * (thread ID) from our loader. 780 */ 781 assert(!"invalid thread ID"); 782 return -1; 783 784 case /*? tcb_control ?*/ : /* Control thread */ 785 camkes_tls_init(thread_id); 786 for (int i = 0; i < /*? len(threads) - 1 ?*/; i++) { 787 if (sel4runtime_get_tls_size() < CONFIG_SEL4RUNTIME_STATIC_TLS) { 788 tls_regions[i] = static_tls_regions[i]; 789 } else { 790 tls_regions[i] = malloc(sel4runtime_get_tls_size()); 791 ZF_LOGF_IF(tls_regions[i] == NULL, "Failed to create tls"); 792 } 793 } 794 ret = component_control_main(); 795 sync_sem_bare_wait(/*? interface_init_ep ?*/, &interface_init_lock); 796 return ret; 797 798 /*# Interface threads #*/ 799 /*- for t in threads[1:] -*/ 800 /*- if options.debug_fault_handlers and loop.last -*/ 801 /*- set tcb = alloc("%s_tcb" % t.name, seL4_TCBObject) -*/ 802 case /*? tcb ?*/ : { /* Fault handler thread */ 803 sync_sem_bare_wait(/*? pre_init_ep ?*/, &pre_init_lock); 804 camkes_tls_init(thread_id); 805 fault_handler(); 806 UNREACHABLE(); 807 return 0; 808 } 809 /*- else -*/ 810 /*- set tcb = alloc("%s_tcb" % t.name, seL4_TCBObject) -*/ 811 case /*? tcb ?*/ : { /* Interface /*? t.interface.name ?*/ */ 812 /* Wait for `pre_init` to complete. */ 813 sync_sem_bare_wait(/*? pre_init_ep ?*/, &pre_init_lock); 814 camkes_tls_init(thread_id); 815 if (/*? t.interface.name ?*/__init) { 816 /*? t.interface.name ?*/__init(); 817 } 818 /* Notify the control thread that we've completed init. */ 819 sync_sem_bare_post(/*? interface_init_ep ?*/, &interface_init_lock); 820 /* Wait for the `post_init` to complete. */ 821 sync_sem_bare_wait(/*? post_init_ep ?*/, &post_init_lock); 822 823 /*- set prefix = '%s_%s_%04d' % (me.name, t.interface.name, t.intra_index) -*/ 824 /*- if options.realtime and prefix in passive_tcbs -*/ 825 826 /*# If this is a passive interface, the __run_passive function must SignalRecv to tell the control 827 *# thread to unbind its sc, and simultaneously start waiting for rpc calls. #*/ 828 extern int /*? t.interface.name ?*/__run_passive(seL4_CPtr) WEAK; 829 if (/*? t.interface.name ?*/__run_passive) { 830 ret = /*? t.interface.name ?*/__run_passive(/*? ntfn_passive_init ?*/); 831 } else { 832 /* Inform the main component thread that we're finished initialising */ 833 seL4_Signal(/*? ntfn_passive_init ?*/); 834 835 } 836 /*- else -*/ 837 extern int /*? t.interface.name ?*/__run(void) WEAK; 838 if (/*? t.interface.name ?*/__run) { 839 ret = /*? t.interface.name ?*/__run(); 840 } 841 /*- endif -*/ 842 sync_sem_bare_wait(/*? pre_init_ep ?*/, &pre_init_lock); 843 return ret; 844 } 845 /*- endif -*/ 846 /*- endfor -*/ 847 848 849 default: 850 /* If we reach this point, the initialiser gave us a thread we 851 * weren't expecting. 852 */ 853 assert(!"Template generation failure"); 854 return -1; 855 } 856} 857 858int USED main(int argc UNUSED, char *argv[]) { 859 assert(argc == 2); 860 assert(strcmp(argv[0], "camkes") == 0); 861 862 int thread_id = (int)(uintptr_t)(argv[1]); 863 post_main(thread_id); 864 UNREACHABLE(); 865 return 0; 866} 867 868/*- for e in me.type.emits -*/ 869 void /*? e.name ?*/_emit_underlying(void) WEAK; 870 void /*? e.name ?*/_emit(void) { 871 /* If the interface is not connected, the 'underlying' function will 872 * not exist. 873 */ 874 if (/*? e.name ?*/_emit_underlying) { 875 /*? e.name ?*/_emit_underlying(); 876 } 877 } 878/*- endfor -*/ 879 880/* Prototypes for functions generated in per-interface files. */ 881/*- for d in me.type.dataports -*/ 882 extern int /*? d.name ?*/_wrap_ptr(dataport_ptr_t *p, void *ptr) 883 /*- if d.optional -*/ 884 WEAK 885 /*- endif -*/ 886 ; 887/*- endfor -*/ 888dataport_ptr_t dataport_wrap_ptr(void *ptr UNUSED) { 889 dataport_ptr_t p = { .id = -1 }; 890 /*- for d in me.type.dataports -*/ 891 if ( 892 /*- if d.optional -*/ 893 /*? d.name ?*/_wrap_ptr != NULL && 894 /*- endif -*/ 895 /*? d.name ?*/_wrap_ptr(&p, ptr) == 0) { 896 return p; 897 } 898 /*- endfor -*/ 899 return p; 900} 901 902/* Prototypes for functions generated in per-interface files. */ 903/*- for d in me.type.dataports -*/ 904 extern void * /*? d.name ?*/_unwrap_ptr(dataport_ptr_t *p) 905 /*- if d.optional -*/ 906 WEAK 907 /*- endif -*/ 908 ; 909/*- endfor -*/ 910void *dataport_unwrap_ptr(dataport_ptr_t p UNUSED) { 911 void *ptr = NULL; 912 /*- for d in me.type.dataports -*/ 913 /*- if d.optional -*/ 914 if (/*? d.name ?*/_unwrap_ptr != NULL) { 915 /*- endif -*/ 916 ptr = /*? d.name ?*/_unwrap_ptr(&p); 917 if (ptr != NULL) { 918 return ptr; 919 } 920 /*- if d.optional -*/ 921 } 922 /*- endif -*/ 923 /*- endfor -*/ 924 return ptr; 925} 926 927/* These symbols are provided by the default linker script. */ 928extern const char __executable_start[1]; /* Start of text section */ 929extern const char __etext[1]; /* End of text section, start of rodata section */ 930extern const char __preinit_array_start[1]; /* End of rodata section, start of data section */ 931extern const char _edata[1]; /* End of data section */ 932extern const char __bss_start[1]; /* Start of bss section */ 933extern const char _end[1]; /* End of bss section */ 934 935/* See vma.h in libsel4camkes for a description of this array. */ 936const struct camkes_vma camkes_vmas[] = { 937 { 938 .start = (void*)__executable_start, 939 .end = (void*)__etext, 940 .read = true, 941 .write = false, 942 .execute = true, 943 .cached = true, 944 .name = ".text", 945 }, 946 { 947 .start = (void*)__etext, 948 .end = (void*)__preinit_array_start, 949 .read = true, 950 .write = false, 951 .execute = false, 952 .cached = true, 953 .name = ".rodata", 954 }, 955 { 956 .start = (void*)__preinit_array_start, 957 .end = (void*)_edata, 958 .read = true, 959 .write = true, 960 .execute = false, 961 .cached = true, 962 .name = ".data", 963 }, 964 { 965 .start = (void*)__bss_start, 966 .end = (void*)_end, 967 .read = true, 968 .write = true, 969 .execute = false, 970 .cached = true, 971 .name = ".bss", 972 }, 973 { 974 .start = (void*)/*? dma_symbol_name ?*/, 975 .end = (void*)/*? dma_symbol_name ?*/ + sizeof(/*? dma_symbol_name ?*/), 976 .read = true, 977 .write = true, 978 .execute = false, 979 .cached = false, 980 .name = "DMA pool", 981 }, 982 /*- for t in threads -*/ 983 { 984 .start = (void*)/*? t.stack_symbol ?*/, 985 .end = (void*)/*? t.stack_symbol ?*/ + PAGE_SIZE_4K, 986 .read = false, 987 .write = false, 988 .execute = false, 989 .cached = true, 990 .name = "guard page below /*? t.name ?*/ thread's stack", 991 }, 992 { 993 .start = (void*)/*? t.stack_symbol ?*/ + PAGE_SIZE_4K, 994 .end = (void*)/*? t.stack_symbol ?*/ + sizeof(/*? t.stack_symbol ?*/) - PAGE_SIZE_4K, 995 .read = true, 996 .write = true, 997 .execute = false, 998 .cached = true, 999 .name = "/*? t.name ?*/ thread's stack", 1000 }, 1001 { 1002 .start = (void*)/*? t.stack_symbol ?*/ + sizeof(/*? t.stack_symbol ?*/) - PAGE_SIZE_4K, 1003 .end = (void*)/*? t.stack_symbol ?*/ + sizeof(/*? t.stack_symbol ?*/), 1004 .read = false, 1005 .end = false, 1006 .execute = false, 1007 .cached = true, 1008 .name = "guard page above /*? t.name ?*/ thread's stack", 1009 }, 1010 { 1011 .start = (void*)/*? t.ipc_symbol ?*/, 1012 .end = (void*)/*? t.ipc_symbol ?*/ + PAGE_SIZE_4K, 1013 .read = false, 1014 .write = false, 1015 .execute = false, 1016 .cached = true, 1017 .name = "guard page below /*? t.name ?*/ thread's IPC buffer", 1018 }, 1019 { 1020 .start = (void*)/*? t.ipc_symbol ?*/ + PAGE_SIZE_4K, 1021 .end = (void*)/*? t.ipc_symbol ?*/ + (PAGE_SIZE_4K * 2), 1022 .read = true, 1023 .write = true, 1024 .execute = false, 1025 .cached = true, 1026 .name = "/*? t.name ?*/ thread's IPC buffer", 1027 }, 1028 { 1029 .start = (void*)/*? t.ipc_symbol ?*/ + (PAGE_SIZE_4K * 2), 1030 .end = (void*)/*? t.ipc_symbol ?*/ + (PAGE_SIZE_4K * 3), 1031 .read = false, 1032 .write = false, 1033 .execute = false, 1034 .cached = true, 1035 .name = "guard page above /*? t.name ?*/ thread's IPC buffer", 1036 }, 1037 /*- endfor -*/ 1038}; 1039 1040const size_t camkes_vmas_size = sizeof camkes_vmas / sizeof camkes_vmas[0]; 1041 1042/*- for index, i in enumerate(composition.instances) -*/ 1043 /*- if id(i) == id(me) -*/ 1044 /* We consider the CapDL initialiser to have PID 1, so offset to skip over this. */ 1045 const pid_t camkes_pid = (pid_t)/*? index ?*/ + (pid_t)2; 1046 /*- break -*/ 1047 /*- endif -*/ 1048/*- endfor -*/ 1049