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

Added some guidance on how to read the proof.

Browse source
This commit is contained in:
Tobias Reinhard 2023-01-04 12:32:28 -05:00
parent 1eb83cdb46
commit c57b62a3dc
1 changed files with 11 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -198,6 +198,17 @@ Both scripts expect the command line arguments explained below.
- \<FONT_SIZE\> is an optional argument specifying the IDE's font size.
# Reading the Proof
The most important aspects that we have to understand in order to understand the proof are the following, in this order:
- The locking discipline, cf. `proof/port_locking_contracts.h`
- The lock invariants, cf. `proof/lock_predicates.h`. The invariants use the ready list and task predicates defined in `proof/ready_list_predicates.h` and `task_predicates.h`.
- The contracts for the functions we verified, i.e., `vTaskSwitchContext` and `prvSelectHighestPriorityTask`, cf. `src/tasks.c`.
We propose to first skim the above mentioned files -- in the given order -- and the documentation they provide to get an overview of how the proof is structured.
# Maintaining the Proof
This directory contains annotated copies of FreeRTOS source and header files.
The annotations in these files tell VeriFast which functions it should verify and what the proof looks like.