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/* The following SPIN model attempts to represent the semantics of the 14 * seL4Notification connector code and its relevant correctness properties. It is not 15 * intended to be exhaustive, but is intended to give some confidence of the 16 * concurrency correctness of the connector's glue code. To execute: 17 * 18 * # Verify safety 19 * spin -a sel4notification.pml 20 * gcc -o pan-safety -O3 -DREACH -DSAFETY pan.c 21 * ./pan-safety | tee /dev/stderr | grep -q 'errors: 0' 22 * 23 * # Verify liveness 24 * spin -a sel4notification.pml 25 * gcc -o pan-liveness -O3 -DNP -DNOREDUCE pan.c 26 * ./pan-liveness -l -m100000 | tee /dev/stderr | grep -q 'errors: 0' 27 */ 28 29#define NULL 0 30 31/* The NOTIFICATION underlying the connection itself (`notification` in the template). */ 32chan connection = [1] of {bool}; 33 34/* Models of seL4 NOTIFICATION functions. */ 35inline NOTIFICATION_WAIT(notification) { 36 notification ? 1; 37} 38inline NOTIFICATION_NOTIFY(notification) { 39 atomic { 40 if 41 :: notification ? [1] -> skip; 42 :: !(notification ? [1]) -> notification ! 1; 43 fi; 44 } 45} 46 47/* Models of sync_sem_bare_*. We don't attempt to model the internals of the 48 * semaphore with any accuracy, and just assume we have some external evidence 49 * of the correctness of the libsel4sync-provided implementation. 50 */ 51byte handoff = 0; 52inline SEM_WAIT(result, sem) { 53 atomic { 54 if 55 :: sem > 0 -> 56 sem--; 57 result = 0; 58 /* We over approximate `wait` and assume it can fail at any time 59 * for no reason. 60 */ 61 :: result = 1; 62 fi; 63 } 64} 65inline SEM_TRYWAIT(result, sem) { 66 atomic { 67 if 68 :: sem > 0 -> 69 sem--; 70 result = 1; 71 :: else -> 72 result = 0; 73 fi; 74 } 75} 76inline SEM_POST(sem) { 77 sem++; 78} 79 80/* Model of a binary semaphore. Similarly, we don't attempt to accurately model 81 * its internals. 82 */ 83int lock_count = 1; 84inline lock() { 85 atomic { 86 lock_count == 1 -> 87 lock_count--; 88 } 89} 90inline unlock() { 91 assert(lock_count == 0); 92 lock_count++; 93} 94 95/* The slot for registered callbacks. */ 96bool callback = NULL; 97 98/* A process representing the glue code thread. This code is intended to model 99 * the glue code execution as closely as possible. 100 */ 101active [1] proctype inf_run() { 102 do 103 :: 104 NOTIFICATION_WAIT(connection); 105 lock(); 106 bool cb = callback; 107 callback = NULL; 108 if 109 :: cb == NULL -> 110 if 111 /* We cap the semaphore at 10, though the 112 * implementation caps it at `INT_MAX`. It is unlikely 113 * we mask any bugs with this under approximation, but 114 * we could increase this value to reduce the risk in 115 * future. 116 */ 117 :: handoff < 10 -> 118 SEM_POST(handoff); 119 :: else -> 120 skip; 121 fi; 122 :: else -> 123 skip; 124 fi; 125 /* A claim of the correctness of the connector code is that, at 126 * this point, no one else can be concurrently modifying the 127 * callback slot, so we ought to know it is empty. 128 */ 129 assert(callback == NULL); 130 unlock(); 131 if 132 :: cb != NULL -> 133 /* Here is where we invoke the callback function. We don't 134 * model execution of the callback function. 135 */ 136 skip; 137 :: else -> 138 skip; 139 fi; 140progress: 141 od; 142} 143 144/* The various API functions from the 'to' side of the connector follow. */ 145 146inline inf_poll() { 147 /* For the purposes of this model, we don't care whether the polled 148 * endpoint contained a message or not. 149 */ 150 bool ignored; 151 SEM_TRYWAIT(ignored, handoff); 152} 153 154inline inf_wait() { 155 /* Similarly, we don't care whether a `wait` failed or not. */ 156 bool ignored; 157 SEM_WAIT(ignored, handoff); 158} 159 160inline inf_reg_callback() { 161 bool result; 162 SEM_TRYWAIT(result, handoff); 163 if 164 :: result -> goto done; 165 :: else -> skip; 166 fi; 167 lock(); 168 SEM_TRYWAIT(result, handoff); 169 if 170 :: result -> 171 unlock(); 172 /* At this point in the implementation, we invoke the callback 173 * function. We don't model the actual execution of the callback 174 * function here. 175 */ 176 :: !result && callback -> 177 unlock(); 178 :: else -> 179 /* The following captures a desired correctness property of the 180 * connector code. Namely, that we are not overwriting an existing 181 * registered callback and there is no pending message. 182 */ 183 assert(callback == NULL && handoff == 0); 184 /* The value of the callback pointer itself is irrelevant, so we 185 * just use 1 to indicate that the slot is occupied. 186 */ 187 callback = 1; 188 unlock(); 189 fi; 190done:; 191} 192 193/* A process to represent the user making calls into glue code on the 'to' 194 * side. The model is processed in a reasonable time with 4 processes, but we 195 * may wish to increase this limit to be more thorough in future. 196 */ 197active [4] proctype user() { 198 if 199 :: inf_poll(); 200 :: inf_wait(); 201 :: inf_reg_callback(); 202 fi; 203progress: 204} 205 206/* A process to represent the user making calls into glue code on the 'from' 207 * side. Note that we only ever need 1 process for this to capture all possible 208 * interleavings. 209 */ 210active [1] proctype inf_emit() { 211 do 212 :: 213 NOTIFICATION_NOTIFY(connection); 214progress: 215 od; 216} 217