mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-10-15 01:07:47 -04:00
8e36bee30e
* 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> |
||
|---|---|---|
| .. | ||
| create.c | ||
| prvCopyDataFromQueue.c | ||
| prvCopyDataToQueue.c | ||
| prvIsQueueEmpty.c | ||
| prvIsQueueFull.c | ||
| prvLockQueue.c | ||
| prvUnlockQueue.c | ||
| README.md | ||
| uxQueueMessagesWaiting.c | ||
| uxQueueSpacesAvailable.c | ||
| vQueueDelete.c | ||
| xQueueGenericSend.c | ||
| xQueueGenericSendFromISR.c | ||
| xQueueIsQueueEmptyFromISR.c | ||
| xQueueIsQueueFullFromISR.c | ||
| xQueuePeek.c | ||
| xQueuePeekFromISR.c | ||
| xQueueReceive.c | ||
| xQueueReceiveFromISR.c | ||
FreeRTOS queue proofs
In the queue predicates and proofs we use the following variable names.
Storage: The concrete queue storage ofN*Mbytes. Thebufferpredicate, defined ininclude/proof/queue.hallows us to treat the storage as a listcontentsofNitems, each of which isMbytes.N: queue length (i.e., the maximum number of items the queue can store)M: size in bytes of each elementW: logical index of the write pointer, necessarily between0..(N-1)such that the write pointerpcWriteTo == Storage + W * M.R: logical index of the read pointer, necessarily between0..(N-1)such that the read pointerpcReadFrom == Storage + R * M.K: number of items currently in the queue corresponding touxMessagesWaiting
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.