mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-10-14 08:47:45 -04:00
3a2f6646f0
* Use new version of CI-CD Actions, checkout@v3 instead of checkout@v2 on all jobs * Use cSpell spell check, and use ubuntu-20.04 for formatting check * Add in bot formatting action * Update freertos_demo.yml and freertos_plus_demo.yml files to increase github log readability * Add in a Qemu demo onto the workflows. |
||
|---|---|---|
| .. | ||
| 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.