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

Added explanation of verifast.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-28 20:52:48 -05:00
parent 7298a32ef2
commit 38790b241d
1 changed files with 22 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2,6 +2,28 @@
This directory contains an unbounded memory safety and thread safety proof This directory contains an unbounded memory safety and thread safety proof
for the core of the task scheduler: `vTaskSwitchContext` for the core of the task scheduler: `vTaskSwitchContext`
## VeriFast
[VeriFast](https://github.com/verifast/verifast)
is a deductive program verifier for C based on separation logic.
It supports verifying concurrent code and reasoning about complex data structures.
VeriFast proofs are *unbounded*.
That is, until explicitly specified, it does not assume any bound on the size of the involved data structures.
Hence, proofs give us unbounded guarantees.
In our case, this means that our proof holds for any number of tasks and any size of the involved data structures.
Reasoning about concurrent code can be tricky because of all the interleavings that can occur.
VeriFast does not assume anything about the occuring interleavings.
Therefore, the proven guarantees hold for every possible interleaving that might occur during runtime.
Being a deductive verifier, VeriFast requires us to manually write a proof.
In particular, we have to specify what well-formed data structures look like and to annotate the code with proof steps.
It then symbolically executes the annotated code and queries an SMT solver to check the validity of proof steps.
This directory contains all the specifications and proof steps necessary to check that the scheduler is memory and thread safe.
## Key Result
Informally, the proof guarantees the following: Informally, the proof guarantees the following:
``` ```
Proof Assumptions: Proof Assumptions: