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

Minor layout corrections in README.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-31 16:43:10 -05:00
parent f335145676
commit 4f80a727d9
1 changed files with 11 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -303,19 +303,19 @@ Therefore, the proof's correctness relies on the correctness of our models.
Core C is always allowed to read `pxCurrentTCBs[C]`. Core C is always allowed to read `pxCurrentTCBs[C]`.
However, writing requires the interrupts on core C to be deactivated. However, writing requires the interrupts on core C to be deactivated.
- task lock: - task lock:
The task lock is used to protect ciritical sections and resources from being accessed by multiple tasks simultaneously. The task lock is used to protect ciritical sections and resources from being accessed by multiple tasks simultaneously.
- ISR lock: - ISR lock:
The ISR/ interrupt lock is used to protect critical sections and resources from being accessed by multiple interrupts simultaneously. The ISR/ interrupt lock is used to protect critical sections and resources from being accessed by multiple interrupts simultaneously.
- task lock + ISR lock: - task lock + ISR lock:
Access to certain resources and ciritical sections are protected by both the task lock and the ISR lock. Access to certain resources and ciritical sections are protected by both the task lock and the ISR lock.
For these, it is crucial that we first acquire the task lock and then the ISR lock. For these, it is crucial that we first acquire the task lock and then the ISR lock.
Likewise, we must release them in opposite order. Likewise, we must release them in opposite order.
Failure to comply with this order may lead to deadlocks. Failure to comply with this order may lead to deadlocks.
The resources protected by both locks are the main resources this proof deals with. The resources protected by both locks are the main resources this proof deals with.
These include the ready lists and the certain access rights to the tasks' run states. These include the ready lists and the certain access rights to the tasks' run states.
#### Lock Invariants #### Lock Invariants
Every synchronization mechanism protects specific data structures and sections of code. Every synchronization mechanism protects specific data structures and sections of code.