len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-23 13:17:44 -04:00
Code Issues Projects Releases Packages Wiki Activity
FreeRTOS-Kernel/FreeRTOS/Test/VeriFast/queue/README.md
Nathan Chong 8e36bee30e
Prove buffer lemmas (#124) 
* Prove buffer lemmas

* Update queue proofs to latest kernel source

All changes were syntactic due to uncrustify code-formatting

* Strengthen prvCopyDataToQueue proof

* Add extract script for diff comparison

Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
2020-07-21 09:51:20 -07:00

1.2 KiB
Raw Blame History

FreeRTOS queue proofs

In the queue predicates and proofs we use the following variable names.

  • Storage : The concrete queue storage of N*M bytes. The buffer predicate, defined in include/proof/queue.h allows us to treat the storage as a list contents of N items, each of which is M bytes.
  • N : queue length (i.e., the maximum number of items the queue can store)
  • M : size in bytes of each element
  • W : logical index of the write pointer, necessarily between 0..(N-1) such that the write pointer pcWriteTo == Storage + W * M.
  • R : logical index of the read pointer, necessarily between 0..(N-1) such that the read pointer pcReadFrom == Storage + R * M.
  • K : number of items currently in the queue corresponding to uxMessagesWaiting

The queue predicate, defined in include/proof/queue.h, relates the concrete queue storage to an abstract list abs of K items. More precisely, the key queue invariant is:

abs == take(K, rotate_left((R+1)%N, contents)) &*&
W == (R + 1 + K) % N

where (R+1)%N is the front of the queue, W is the back of the queue, rotate_left allows for the wraparound of queue storage, and take gives the first K elements.