1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
|
# FreeRTOS VeriFast Proof Signoff
Verification tool: VeriFast (code-level proof)
Proofs: `queue/` and `list`
Implementation: Kernel queue data structure (`queue.c`) and list data structure (`list.c`)
Specification / Properties:
- *Memory safety*: the implementation only accesses valid memory. In the case
of the queue, this is true under any arbitrary number of tasks or ISRs.
- *Thread safety*: in the case of the queue, tasks and ISRs only update
objects that they own via proper synchronization.
- *Functional correctness*: the queue and list implementations behave like an
abstract queue and list. In the case of the queue, this is true under any
arbitrary number of tasks or ISRs.
## Queue proof assumptions
Generally, we assume well-behaved clients; the correctness of underlying
primitives (memory allocation, task scheduling, scheduler suspension); and
assumptions about the system.
- Well-behaved client: all client tasks and ISRs use the queue API in a
manner that adheres to the specification. A badly-behaved client can
invalidate the proven properties. For example, a client that reads or
writes to the queue storage directly, without masking interrupts, is racy
and no longer thread safe. The specification forbids this behavior by
the definition of `queuehandle`, which is a handle to acquire ownership of
the queue through interrupt masking, but we cannot, in general, enforce
this behavior since we do not verify client code.
- Memory safety, thread safety and function contracts for the following
primitives. For the list and task functions we give a contract that is
maximal in terms of the queue objects that can be updated, but we do not
model their function effect (e.g., task blocking and the moving of task
control blocks between scheduler lists).
pvPortMalloc
vPortFree
memcpy
vListInitialise
xTaskRemoveFromEventList
vTaskMissedYield
xTaskCheckForTimeOut
vTaskInternalSetTimeOutState
vTaskPlaceOnEventList
- We assume interrupt masking gives strong isolation between tasks and ISRs.
See Appendix. We further assume the system is configured as required by
`configASSERT`. For example, interrupts with a priority greater than the
maximum system call priority must not call queue API functions, otherwise
the strong isolation guarantee is not maintained.
## List proof assumptions
The list proofs are sequential. We assume the caller of the list API functions
has taken appropriate synchronization steps to avoid races.
## Simplifications
A list of changes to the source code required for the proofs can be generated:
```
make proof_changes
```
A side-by-side diff with respect to the source code can be generated. See
.
The main queue changes are:
- merge cTxLock and cRxLock critical regions: under approximate queue
unlock behavior to atomically set `cTxLock` and `cRxLock` to unlocked in a
single critical region instead of two separate critical regions. In
practice, this is not an issue since no ISR function reads-from both
cTxLock and cRxLock.
- model single malloc of struct and buffer: split the single malloc of the
queue struct and storage into two separate mallocs.
- xQueueGenericReset happens-before concurrent behavior: assume that queue
initialisation is not concurrent.
- do not model pxIndex and xListEnd of xLIST struct: ignore these fields in
the list structs of the queue implementation
The main list changes are:
- change `MiniList_t` to `ListItem_t`: simplifying assumption on the list
structure.
- over-approximate list insert loop: replace a loop in the insert function
that finds the insertion point with an over-approximating function call.
The following minor changes due to the stricter typing and parser of VeriFast:
- replacing a union declaration with a struct
- const pointer declaration
- stricter casting
- void cast of unused return value
- void cast of unused var
The following minor changes due to the modeling of interrupts and scheduler
suspension in the proofs as ghost state.
- ghost action
- leak ghost state on deletion
## Configuration
We do not verify across the full configuration space of FreeRTOS. In
particular, the queue proofs do not apply when the following options are
enabled:
- `configUSE_QUEUE_SETS`
- `configSUPPORT_STATIC_ALLOCATION`
For both the queue and list proofs we assume that coverage and tracing
macros are no-ops.
## Trusted computing base
- Soundness of verification tools: VeriFast, Redux prover
- C Compiler, because the verification is at the C code-level and the
properties proved may not be preserved by compilation.
## References
[N1570] ISO/IEC. Programming languages – C. International standard 9899:201x,
2011
## Appendix
Assumption on strong isolation induced by interrupt masking and scheduler
suspension for queue proofs. Informally, we need the following:
```
// Initially *data == 0
// Task 1
taskENTER_CRITICAL()
*data = 1;
*data = 2;
taskEXIT_CRITICAL()
// ISR or Task 2
r0 = *data; //< guaranteed to read 0 or 2, never 1
```
|
