len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-10 05:35:17 -05:00
Code Issues Projects Releases Packages Wiki Activity

Explained found bug in README.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-30 14:45:42 -05:00
parent 53d3062e2c
commit e644877f7f
1 changed files with 18 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

18
Test/VeriFast/tasks/vTaskSwitchContext/README.md
View file

@ -54,6 +54,24 @@ The proof ensures that every concurrent execution of `vTaskSwitchContext` on any
That is, when we execute multiple instances of the function on different cores, we won't get any memory errors or data races, no matter how these instances interleave or when interrupts occur.
# Found Buffer Underflow
During the verification of `vTaskSwitchContext` we found a buffer underflow, fixed it and verified that our fix works.
The guarantees stated in the section above concern the fixed-up code.
We submitted the fix as a pull request: [Fixed buffer underflow in prvSelectHighestPriorityTask. #607](https://github.com/FreeRTOS/FreeRTOS-Kernel/pull/607)
Our verification target `vTaskSwitchContext` calls the auxiliary function `prvSelectHighestPriorityTask` to choose the task that will be scheduled next.
This works as long as the idle tasks have already been created.
The idle tasks are tasks whose only purpose is to run and do nothing in case there is no other task that can be scheduled.
However, `prvSelectHighestPriorityTask` can also be called before the idle tasks have been created.
When that happens, the function decrements the global variable `uxTopReadyPriority` to -1.
This variable is supposed to store the highest priority for which we know that there is a ready task.
Priorities start at 0, so -1 is an invalid value.
During the next regular context switch, `vTaskSwitchContext` calls `prvSelectHighestPriorityTask`.
The latter looks at `uxTopReadyPriority` to detect at which priority level it should start its search.
Hence, it accesses the global ready list array at index -1, i.e., `pxReadyTasksLists[ uxCurrentPriority ]`.
This causes a memory error.
# Proof Directory Structure
```