# 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/