mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-10-15 09:17:44 -04:00
4f87f485d5
* Undo syntax changes preventing VeriFast parsing * Update proofs inline with source changes Outstanding: - xQueueGenericReset return code - Not using prvIncrementQueueTxLock or prvIncrementQueueRxLock macros * Remove git hash check * Document new changes between proven code and implementation * Update copyright header * VeriFast proofs: turn off uncrustify checks Uncrustify requires formatting of comments that is at odds with VeriFast's proof annotations, which are contained within comments. * Update ci.yml Co-authored-by: Joseph Julicher <jjulicher@mac.com> Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@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.