Add VeriFast thread safety proof for context switches in SMP port #608
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
- const pointers
- inline assembler
- statements blocks consisting of multiple elements used in expression contexts, e.g., `({e1 e2;})`
- multiple pointer declarations to user-defined types in single line, i.e., `A *p1, *p2;`
- VeriFast does not support nested union definitions. Removed those temporarily. - VeriFast does not support duplicate function prototypes. Prevented include of unguarded system header file.
…ort-specific implementation.
… to justify `memset`-ing the stack.
…overflows and underflows.
…und for over/underflows.
Fields: `pxNewTCB->ucNotifyState` and `pxNewTCB->ulNotifiedValue`
…erification of contract from portable.h
…tack` impl from RP2040 port.
…nternship-AWS-2022/FreeRTOS-Kernel into verifast_switch_context
tobireinhard
force-pushed
the
verifast_switch_context
branch
from
e52ae50
to
c57b62a
Compare
Closed
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Add VeriFast thread safety proof for context switches in SMP port
Description
The SMP implementation of the scheduler suffers from a buffer underflow, cf. the fix proposed in PR 607. We used VeriFast, a deductive program verifier for C, to prove that once the fix from PR 607 has been applied, context switches are memory safe (i.e. no memory error) and mutually thread safe (i.e. no race condition).
The proof is an unbounded proof. That is, it considers any possible number of tasks and any possible sizes for the involved data structures. Further, it considers any possible task interleavings and any possible interrupt schedule that may occur during runtime. Taking all this into account, it ensure that no memory error and no race condition can occur during runtime, when we run multiple concurrent context switches on different cores.
See the proof README for a more detailed explanation.
Test Steps
Run one of the scripts
run-verifast.shorrun-vfide.shas descripted in the proof README.Related Issue
#607
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.