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