70 lines
2.0 KiB
Markdown
70 lines
2.0 KiB
Markdown
# FreeRTOS list proofs
|
|
|
|
The list predicates and proofs are inspired by and based on the work from
|
|
Ferreira et al. (STTT'14).
|
|
|
|
The main shape predicate is a doubly-linked list segment (DLS), as defined
|
|
by Ferreira et al. in Fig 15. A DLS is defined by two `xLIST_ITEM` struct
|
|
pointers `n` and `m` (possibly pointing to the same item) which are the start
|
|
and end of the segment. We track the item pointers and values within the DLS in
|
|
the lists `cells` and `vals`, respectively. Therefore `n` and `m` are the first
|
|
and last items of `cells`.
|
|
|
|
```
|
|
+--+ +--+
|
|
-----n-> |*n| ... |*m| -mnext->
|
|
<-nprev- | | | | <-m-----
|
|
+--+ +--+
|
|
^-----------^
|
|
DLS(n, nprev, mnext, m)
|
|
```
|
|
|
|
With base case: `n == m` (single item case)
|
|
|
|
```
|
|
+--+
|
|
-----n-> |*n| -mnext->
|
|
<-nprev- | | <-n-----
|
|
+--+
|
|
^--^
|
|
xLIST_ITEM
|
|
DLS(n, nprev, mnext, n)
|
|
```
|
|
|
|
Cons case:
|
|
|
|
```
|
|
+--+ +--+ +--+
|
|
-----n-> |*n| -o-> |*o| ... |*m| -mnext->
|
|
<-nprev- | | <-n- | | | | <-m-----
|
|
+--+ +--+ +--+
|
|
^--^ ^-----------^
|
|
xLIST_ITEM DLS(o, n, mnext, m)
|
|
|
|
^---------------------^
|
|
DLS(n, nprev, mnext, m)
|
|
```
|
|
|
|
A DLS can be made into a well-formed list by joining `n` and `m` into a cycle.
|
|
Note that unlike Ferreira et al.'s list shape predicate, we always start with
|
|
the sentinel end item to avoid a top-level case-split. So in the following
|
|
diagram the start and end of the DLS are `end` and the item-before-end
|
|
`endprev`.
|
|
|
|
```
|
|
.-----------------------------------.
|
|
| +--------+ +--------+ |
|
|
`--> |*end | ... |*endprev| ----'
|
|
.---- | | | | <---.
|
|
| +--------+ +--------+ |
|
|
`----------------------------------'
|
|
^-----------------------^
|
|
DLS(end, endprev, end, endprev)
|
|
```
|
|
|
|
## References
|
|
|
|
- Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK\
|
|
João F. Ferreira, Cristian Gherghina, Guanhua He, Shengchao Qin, Wei-Ngan Chin\
|
|
https://joaoff.com/publication/2014/sttt/
|