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

Minor corrections in README.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-31 16:17:38 -05:00
parent 0adb318dd9
commit 4cc5b7dcdd
1 changed files with 11 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -105,22 +105,22 @@ FreeRTOS-Kernel
└── Test/VeriFast/tasks/vTaskSwitchContext └── Test/VeriFast/tasks/vTaskSwitchContext
│ │
├── run-verifast.sh ├── run-verifast.sh
│ Shell script to run check the proof with VeriFast. │ Shell script to check the proof with VeriFast.
│ │
├── run-vfide.sh ├── run-vfide.sh
│ Shell script to load the proof into the VeriFast IDE. │ Shell script to load the proof into the VeriFast IDE.
│ │
├── diff.sh ├── diff.sh
│ Shell script to compute flag changes in the production code that │ Shell script to flag changes in the production code that potentially
│ potentially break the validity of the VeriFast proof. An empty diff │ break the validity of the VeriFast proof. An empty diff means that the
│ means that the proof and the production code remain in sync. │ proof and the production code remain in sync.
│ │
├── preprocessing_scripts ├── preprocessing_scripts
│ Contains scripts to preprocess and rewrite the source code. │ Contains scripts to preprocess and rewrite the source code.
│ │
├── demos ├── demos
│ Contains the FreeRTOS SMP demo. Our proofs use some of its │ Contains the FreeRTOS SMP demo. Our proofs use some of its
│ configuartion files. │ configuration files.
│ │
├── include ├── include
│ Contains annotated copies of header files residing in │ Contains annotated copies of header files residing in
@ -135,7 +135,7 @@ FreeRTOS-Kernel
│ │ Headers containing VeriFast formalizations and proofs. │ │ Headers containing VeriFast formalizations and proofs.
│ │ │ │
│ ├── README.md │ ├── README.md
│ │ Contains more details about the proof. │ │ Contains overview about proof files.
│ │ │ │
│ ├── single_core_proofs │ ├── single_core_proofs
│ │ Contains the old list formalization and proofs written by │ │ Contains the old list formalization and proofs written by
@ -176,7 +176,6 @@ before it is processed by VeriFast.
This file contains a copy of all the code and annotations required to check the This file contains a copy of all the code and annotations required to check the
proof. proof.
Both scripts expect the command line arguments explained below. Both scripts expect the command line arguments explained below.
In the following we use the following variables
- #### run-verifast.sh: - #### run-verifast.sh:
Preprocesses the code and proof files and uses the Preprocesses the code and proof files and uses the
@ -185,7 +184,7 @@ In the following we use the following variables
#### run-verifast.sh \<REPO_BASE_DIR\> \<VERIFAST_DIR\> #### run-verifast.sh \<REPO_BASE_DIR\> \<VERIFAST_DIR\>
where where
- \<REPO_BASE_DIR\> is the absolute path to this repository's base directory, - \<REPO_BASE_DIR\> is the absolute path to this repository's base directory,
i.e., 'FreeRTOS-Kernel' in the repo structure depicted above. i.e., `FreeRTOS-Kernel` in the repo structure depicted above.
- \<VERIFAST_DIR\> is the absolute path to the VeriFast installation - \<VERIFAST_DIR\> is the absolute path to the VeriFast installation
directory. directory.
@ -213,7 +212,7 @@ Afterwards, it computes a diff between both versions and fails if the result is
An empty diff means that the pull request did not change anything that can affect our proof and the proof remains valid. An empty diff means that the pull request did not change anything that can affect our proof and the proof remains valid.
A non-empty diff shows which changes in the pull request potentially impact our proof. A non-empty diff shows which changes in the pull request potentially impact our proof.
In this case, the changes should also be applied to the annotated copies and the proof should be checked again. In this case, the changes should also be applied to the annotated copies and the proof should be checked again.
If the diff was not a false positive and indeed impacted the proof, the proof will likely require manual repair. If the detected divergence was not a false positive and indeed impacted the proof, the proof will likely require manual repair.
The diff can also be manually checked by running the command The diff can also be manually checked by running the command
`diff.sh <REPO_BASE_DIR>`, where the argument is the absolute path to the repository's base directory. `diff.sh <REPO_BASE_DIR>`, where the argument is the absolute path to the repository's base directory.
@ -264,7 +263,7 @@ Therefore, the proof's correctness relies on the correctness of our models.
Previously, Aalok Thakkar and Nathan Chong used VeriFast to prove functional correctness of the stand-alone list data structure for a single-core setup, c.f. [FreeRTOS Pull Request 836: Update VeriFast proofs](https://github.com/FreeRTOS/FreeRTOS/pull/836). Previously, Aalok Thakkar and Nathan Chong used VeriFast to prove functional correctness of the stand-alone list data structure for a single-core setup, c.f. [FreeRTOS Pull Request 836: Update VeriFast proofs](https://github.com/FreeRTOS/FreeRTOS/pull/836).
We reused their formalization and proofs as much as possible. We reused their formalization and proofs as much as possible.
However, we had to heavily adapt both to tailor them to the needs of the scheduler proof, cf. `Reusing List Proofs` below. However, we had to heavily adapt both to tailor them to the needs of the scheduler proof, cf. `Proof Details` below.
The reused specification resides in `proofs/single_core_proofs/`. The reused specification resides in `proofs/single_core_proofs/`.
The full ready list array is specified in `proofs/ready_list_predicates.h`. The full ready list array is specified in `proofs/ready_list_predicates.h`.
@ -294,8 +293,8 @@ Therefore, the proof's correctness relies on the correctness of our models.
- ### Locking discipline and lock invariants - ### Locking discipline and lock invariants
FreeRTOS' SMP implementation uses the following synchronization mechanisms: FreeRTOS' SMP implementation uses the following synchronization mechanisms:
- Deactivating interrupts: - Deactivating interrupts:
Some data is only meant to be accessed on a specific core C. Some data is only meant to be accessed on a specific core C.
Such data may only be accessed after interrupts on core C have been deactivated. Such data may only be accessed after interrupts on core C have been deactivated.