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 <stdio.h> 14#include <sel4/sel4.h> 15#include <vka/object.h> 16#include <vka/capops.h> 17 18#include "../test.h" 19#include "../helpers.h" 20 21static int send_func(seL4_CPtr ep, seL4_Word msg, UNUSED seL4_Word arg4, UNUSED seL4_Word arg3) 22{ 23 seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1); 24 25 /* Send the given message once. */ 26 seL4_SetMR(0, msg); 27 seL4_Send(ep, tag); 28 29 return sel4test_get_result(); 30} 31 32static int test_nbwait(env_t env) 33{ 34 35 vka_object_t notification = {0}; 36 vka_object_t endpoint = {0}; 37 vka_object_t reply = {0}; 38 int error; 39 seL4_MessageInfo_t info = {{0}}; 40 seL4_Word badge = 0; 41 42 /* allocate an endpoint and a notification */ 43 error = vka_alloc_endpoint(&env->vka, &endpoint); 44 test_eq(error, 0); 45 46 error = vka_alloc_notification(&env->vka, ¬ification); 47 test_eq(error, 0); 48 49 if (config_set(CONFIG_KERNEL_MCS)) { 50 error = vka_alloc_reply(&env->vka, &reply); 51 test_eq(error, 0); 52 } 53 54 /* bind the notification to the current thread */ 55 error = seL4_TCB_BindNotification(env->tcb, notification.cptr); 56 test_eq(error, 0); 57 58 /* create cspace paths for both objects */ 59 cspacepath_t notification_path, endpoint_path; 60 vka_cspace_make_path(&env->vka, notification.cptr, ¬ification_path); 61 vka_cspace_make_path(&env->vka, endpoint.cptr, &endpoint_path); 62 63 /* badge both caps */ 64 cspacepath_t badged_notification, badged_endpoint; 65 error = vka_cspace_alloc_path(&env->vka, &badged_notification); 66 test_eq(error, 0); 67 vka_cspace_alloc_path(&env->vka, &badged_endpoint); 68 test_eq(error, 0); 69 70 error = vka_cnode_mint(&badged_endpoint, &endpoint_path, seL4_AllRights, 1); 71 test_eq(error, 0); 72 73 error = vka_cnode_mint(&badged_notification, ¬ification_path, seL4_AllRights, 2); 74 test_eq(error, 0); 75 76 /* NBRecv on endpoint with no messages should return 0 immediately */ 77 info = api_nbrecv(endpoint.cptr, &badge, reply.cptr); 78 test_eq(badge, (seL4_Word)0); 79 80 /* Poll on a notification with no messages should return 0 immediately */ 81 info = seL4_Poll(notification.cptr, &badge); 82 test_eq(badge, (seL4_Word)0); 83 84 /* send a signal to the notification */ 85 seL4_Signal(badged_notification.capPtr); 86 87 /* Polling should return the badge from the signal we just sent */ 88 info = seL4_Poll(notification.cptr, &badge); 89 test_eq(badge, (seL4_Word)2); 90 91 /* Polling again should return nothign */ 92 info = seL4_Poll(notification.cptr, &badge); 93 test_eq(badge, (seL4_Word)0); 94 95 /* send a signal to the notification */ 96 seL4_Signal(badged_notification.capPtr); 97 98 /* This time NBRecv the endpoint - since we are bound, we should get the badge from the signal again */ 99 info = api_nbrecv(endpoint.cptr, &badge, reply.cptr); 100 test_eq(badge, (seL4_Word)2); 101 102 /* NBRecving again should return nothign */ 103 info = api_nbrecv(endpoint.cptr, &badge, reply.cptr); 104 test_eq(badge, (seL4_Word)0); 105 106 /* now start a helper to send a message on the badged endpoint */ 107 helper_thread_t thread; 108 create_helper_thread(env, &thread); 109 start_helper(env, &thread, send_func, badged_endpoint.capPtr, 0xdeadbeef, 0, 0); 110 set_helper_priority(env, &thread, env->priority); 111 /* let helper run */ 112 seL4_TCB_SetPriority(env->tcb, env->tcb, env->priority - 1); 113 114 /* NBRecving should return helpers message */ 115 info = api_nbrecv(endpoint.cptr, &badge, reply.cptr); 116 test_eq(badge, (seL4_Word)1); 117 test_eq(seL4_MessageInfo_get_length(info), (seL4_Word)1); 118 test_eq(seL4_GetMR(0), (seL4_Word)0xdeadbeef); 119 120 /* NBRecving again should return nothign */ 121 info = api_nbrecv(endpoint.cptr, &badge, reply.cptr); 122 test_eq(badge, (seL4_Word)0); 123 124 /* clean up */ 125 wait_for_helper(&thread); 126 cleanup_helper(env, &thread); 127 seL4_TCB_UnbindNotification(env->tcb); 128 vka_cnode_delete(&badged_notification); 129 vka_cnode_delete(&badged_endpoint); 130 vka_cspace_free(&env->vka, badged_endpoint.capPtr); 131 vka_cspace_free(&env->vka, badged_notification.capPtr); 132 vka_free_object(&env->vka, &endpoint); 133 vka_free_object(&env->vka, ¬ification); 134 135 return sel4test_get_result(); 136} 137DEFINE_TEST(NBWAIT0001, "Test seL4_NBRecv", test_nbwait, true) 138