begriffs open source - cmsis-freertos/blob - Test/VeriFast/queue/README.md

   1 # FreeRTOS queue proofs
   2
   3 In the queue predicates and proofs we use the following variable names.
   4
   5   - `Storage` : The concrete queue storage of `N*M` bytes. The `buffer`
   6     predicate, defined in `include/proof/queue.h` allows us to treat the
   7     storage as a list `contents` of `N` items, each of which is `M` bytes.
   8   - `N` : queue length (i.e., the maximum number of items the queue can store)
   9   - `M` : size in bytes of each element
  10   - `W` : logical index of the write pointer, necessarily between
  11     `0..(N-1)` such that the write pointer `pcWriteTo == Storage + W * M`.
  12   - `R` : logical index of the read pointer, necessarily between
  13     `0..(N-1)` such that the read pointer `pcReadFrom == Storage + R * M`.
  14   - `K` : number of items currently in the queue corresponding to
  15     `uxMessagesWaiting`
  16
  17 The `queue` predicate, defined in `include/proof/queue.h`, relates the concrete
  18 queue storage to an abstract list `abs` of `K` items. More precisely, the key
  19 queue invariant is:
  20
  21 ```
  22 abs == take(K, rotate_left((R+1)%N, contents)) &*&
  23 W == (R + 1 + K) % N
  24 ```
  25
  26 where `(R+1)%N` is the front of the queue, `W` is the back of the queue,
  27 `rotate_left` allows for the wraparound of queue storage, and `take` gives the
  28 first `K` elements.