Add VeriFast thread safety proof for context switches in SMP port #908
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
The VeriFast context switch proof uses the configuration files from the Raspberry Pi Pico SMP demo.
The VeriFast context switch proof assumes a setup for Raspberry Pi Pico. In this configuration FreeRTOS includes files from the pico sdk. We need to the same in the context switch proof.
This is Nathan's list predicates and lemmas modified as required for the context switching proof. Files are renamed to avoid conflicts. For reference the files contain both Nathan's unmodified version and the modified version. To check which parts have been adapted, see instructions in README section "Comparing the Original List Proofs and Our Adaptation".
…for the context switching proof.
These files contain the code the context switching proof verifies as well as proof annotations.
tobireinhard
force-pushed
the
verifast-smp-context-switching-proof
branch
2 times, most recently
from
dee2119
to
81ae1a7
Compare
…eaders relevant for our proof. We had to modify the headers such that VeriFast can parse them.
tobireinhard
force-pushed
the
verifast-smp-context-switching-proof
branch
from
81ae1a7
to
3e9f06e
Compare
moninom1
added a commit
to moninom1/FreeRTOS
that referenced
this pull request
Jun 27, 2023
Add logs to print random number generation failure for better debugging of issue.
moninom1
added a commit
to moninom1/FreeRTOS
that referenced
this pull request
Aug 2, 2023
Add logs to print random number generation failure for better debugging of issue.
moninom1
added a commit
to moninom1/FreeRTOS
that referenced
this pull request
Aug 2, 2023
* Update mainline to reflect changes after the release. (FreeRTOS#563) * Update README.md * Update History.txt * Update version number macros * Update manifest.yml * IPv4/single SAME70 emac race condition (FreeRTOS#567) * Implemented Maty's solution * Added a new statistic 'tx_write_fail' * Uncrustify: triggered by comment. Co-authored-by: Hein Tibosch <hein@htibosch.net> Co-authored-by: GitHub Action <action@github.com> * IPv4/Single: Add a SocketID to a socket (FreeRTOS#546) * IPv4/Single: Add a SocketID to a socket * Change in comment * Applied uncrustify to format the source code * Added a few entries to lexicon.txt * Removed the 'ipconfigUSE_SetSocketID' option * Change to lexicon.txt * Add unit tests for the newly added API Co-authored-by: Hein Tibosch <hein@htibosch.net> Co-authored-by: alfred gedeon <28123637+alfred2g@users.noreply.github.com> Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> * IPv4/single: SAME70 EMAC buffer sizes (FreeRTOS#568) * Implemented Maty's solution * Added a new statistic 'tx_write_fail' * Uncrustify: triggered by comment. * Increase NETWORK_BUFFER_SIZE in order to include the 'ipBUFFER_PADDING' bytes * ICMP checksum calculated manually * Uncrustify: triggered by comment. * Update gmac_SAM.c Co-authored-by: Hein Tibosch <hein@htibosch.net> Co-authored-by: GitHub Action <action@github.com> Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> * Eliminate some warnings (FreeRTOS#578) * Eliminate some warnings related to print statements Authored-by: Pete Bone <pete-pjb@users.noreply.github.com > * Add MISRA justification for use of dynamic memory (FreeRTOS#581) * Update deprecated macros in network driver files (FreeRTOS#579) * Update deprecated macros in network driver files * Fix typo in RX driver. * Replace #warning with #error on test for deprecated macro. * Fix doxygen check Co-authored-by: PeterB <PeterB@PETE-LT.otg.local> Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> * Fix Network-interface of the Xilinx UltraScale port (FreeRTOS#588) The underlying issue was when the port would be used with Jumbo frames. During receives of Jumbo packets the data length was always set incorrectly, which then would cause buffer allocation issues and subsequently corrupted data would be sent to the IP-task. After some inspection in the Xilinx UltraScale port, I found out that when the data length would be set, the wrong mask from the Xilinx Ethernet MAC driver would be used. By using the right mask (XEMACPS_RXBUF_LEN_JUMBO_MASK) when Jumbo Frame support is enabled the issue was resolved * Fix Windows thread calling vTaskSuspendAll / xTaskResumeAll. (FreeRTOS#592) Co-authored-by: Jason Carroll <czjaso@amazon.com> * Updated comments for FreeRTOS_select return value (FreeRTOS#596) * Updated comments for FreeRTOS_select return value * Updated the function brief for FreeRTOS_select * Uncrustify: triggered by comment. * Updating FreeRTOS_select function @brief * Updated function brief for FreeRTOS_SignalSocket * Uncrustify: triggered by comment. * Update source/FreeRTOS_Sockets.c Co-authored-by: Ubuntu <ubuntu@ip-172-31-22-210.ec2.internal> Co-authored-by: GitHub Action <action@github.com> Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> * Fixed readme script to build and run unit tests (FreeRTOS#644) * Minor warning fixes (FreeRTOS#589) * Eliminate compiler unused parameter warning * Eliminate compiler unused variable warnings * Eliminate compiler unused function warning The function pcGetPHIName(...) would be called only in the FreeRTOS_printf message, however FreeRTOS_printf maybe be defined to nothing e.g. release builds, which then the warning would come up * Rework callback setups in the EMAC-driver of the Xilinx UltraScale port The calls to the function XEmacPs_SetHandler would trigger the pedantic warning: "ISO C forbids conversion of object pointer to function pointer type" The reason for this, is that the second parameter of the function XEmacPS_SetHandler is declared as pointer to a void type, but the function "expects" a function pointer, which in setup_isr rightly happens. However IMHO, this is just bad code from the side of Xilinx, as not on all architectures the size of a data pointer is identical to the size of a function pointer, which also is correctly recognised by the compiler. Instead of using the "bad" function XEmacPs_SetHandler, we can set the handlers manually to the EmacPS-instance. * Uncrustify: triggered by comment. * Update source/portable/NetworkInterface/xilinx_ultrascale/x_emacpsif_hw.c Co-authored-by: Paul Bartell <paul.bartell@gmail.com> * Apply suggestions from code review Co-authored-by: Paul Bartell <paul.bartell@gmail.com> * Address comments from reviews Co-authored-by: GitHub Action <action@github.com> Co-authored-by: Paul Bartell <paul.bartell@gmail.com> * Use CBMC XML output to enable VSCode debugger (FreeRTOS#673) Prior to this commit, CBMC would emit logging information in plain text format, which does not contain information required for the CBMC VSCode debugger. This commit makes CBMC use XML instead of plain text. Co-authored-by: Mark Tuttle <tuttle@acm.org> * Remove need of token * Use vTaskDelay for sleep in the network-interface of xilinx_ultrascale (FreeRTOS#698) The issue here is that, the FreeRTOS IP-task would block all other tasks during PHY-link speed negotiations, as it was using busy waiting. However this is not really ideal. A much more suitable function for such a task would be `vTaskDelay`. * Make sure that a TCP socket is closed only once (FreeRTOS#707) * Make sure that a TCP socket is closed only once * Fix failing test cases for FreeRTOS_TCP_IP unit test modules post PR#705 changes * Uncrustify: triggered by comment. * Fix failing test cases for FreeRTOS_TCP_IP unit test modules post PR - 705 changes --------- Co-authored-by: Hein Tibosch <hein_tibosch@yahoo.es> Co-authored-by: GitHub Action <action@github.com> * Remove Dup function HAL_ETH_SetMDIOClockRange. (FreeRTOS#711) * Update PR template to include checkbox for ut change (FreeRTOS#734) * Main/TCP4 : ACK number in TCP RESET reply to SYN packet (FreeRTOS#724) * Main/TCP4 : ACK number in TCP RESET reply to SYN packet * Typo fix * Add unit-test for coverage; Fix ntohl to htonl * Fix unit-test --------- Co-authored-by: Nikhil Kamath <110539926+amazonKamath@users.noreply.github.com> Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> * FreeRTOS#556 Initial Cmake Module definition. (FreeRTOS#557) * FreeRTOS#556 Initial Cmake Module definition. * Fixing CI builds, rely on pcap. (FreeRTOS#556) * Updating tested configurations and minor clean-up of missing network interfaces (FreeRTOS#555) * Further clean-up based on testing with build environment. (FreeRTOS#555) * Using single definition for libraries everywhere. (FreeRTOS#555) * Fixing A_CUSTOM_NETWORK_IF compile option. * Identifying and fixing compile issues. * Adding in additional warnings for GNU to ignore for now. * Fixing formatting issues with uncrustify. * More warnings for GNU used by CI/CD pipeline. * Assuming custom for build tests and using latest freertos-kernel code. Updated readme for how to consume at project level. * Fixing up issues identified in the PR. Making the build_test EXCLUDE_FROM_ALL so only compiled if requested. * Changing to support C89 instead of C99. Renaming tcp_tools to tcp_utilities to mimic the directory. * Using C90 ISO. Fixing compiler warnings. * Fixing non C90 compliant declaration after statement * Separating out CMakeLists so each port is independent. * Updating warning list in code. * Fixed formatting with uncrustify. * Fix failing tests * Fix failing unit-test * Fix a typo. --------- Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> * CMake: Fix GIT_REPOSITORY and GIT_TAG (FreeRTOS#742) * Allow use of loopback addresses in IP stack (127.0.0.0/8) (FreeRTOS#754) Authored-by: Adam St. Amand <astamand@amazon.com> * Add release candidate automation (FreeRTOS#761) This is a minimal subset of release automation which only creates a tag and verifies it. Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com> * Add CBMC-running GitHub Action; This commit adds a GitHub Action that runs the CBMC proofs in this repository upon pushes and pull requests * Copy CBMC output directory to CI location This commit ensures that the output directory for CBMC proofs is in the correct location expected by the FreeRTOS CI-CD repository. * rx: Read mac address using FreeRTOS_GetMACAddress() rather than using the defines (FreeRTOS#765) * Read mac address using FreeRTOS_GetMACAddress() rather than using the defines --------- Co-authored-by: GitHub Action <action@github.com> * cmake: Remove add_subdirectory( cbmc ) call CBMC proofs cannot currently be run using CMake. fixes FreeRTOS#753 * FreeRTOS_IP.h: Fix build error introduced by 55658e1 in FreeRTOS-Kernel * Add Nxp1060 network interface (FreeRTOS#774) * Update PR template to include checkbox for ut change * Create NetworkInterface.c * Uncrustify: triggered by comment. * Address PR comments * Uncrustify: triggered by comment. * Update NetworkInterface.c * Uncrustify: triggered by comment. * Update copyright year * Refactor the init function. Add 'brief'. Cleanup. * Uncrustify: triggered by comment. * Update global link status only when the network is quiet * Uncrustify: triggered by comment. * Update copyright yeat * Update the driver to deal with network cable disconnects * Uncrustify: triggered by comment. * Update NetworkInterface.c * Clean up and address PR comments * More cleanup and address PR comments * Uncrustify: triggered by comment. * Empty-Commit * Address issue comments * Uncrustify: triggered by comment. * Empty-Commit to trigger workflow * Remove Full-Duplex restriction * Uncrustify: triggered by comment. * Empty-Commit to trigger workflow --------- Co-authored-by: GitHub Action <action@github.com> * Correct GCC warnings (FreeRTOS#798) * Correct GCC warnings Corrects warnings with current GCC flags for GCC 7.5.0. The only suppressed warning pertains to function to object pointer conversion which is required and common for socket callbacks. * PR feedback --------- Co-authored-by: Ubuntu <ubuntu@ip-10-0-137-67.ec2.internal> Co-authored-by: Nikhil Kamath <110539926+amazonKamath@users.noreply.github.com> * Cleanup of NXP1060 network driver (FreeRTOS#801) * Update PR template to include checkbox for ut change * Empty-Commit to trigger workflow * Fix issues pointed out in PR comments * Uncrustify: triggered by comment. * Empty-Commit to trigger workflow --------- Co-authored-by: GitHub Action <action@github.com> * Fix Clang warnings (FreeRTOS#809) Corrects several warnings from Clang flags for Clang 13. Inspired by @phelter's bug report FreeRTOS/FreeRTOS-Plus-TCP#558 * uncrustify yml fix (FreeRTOS#815) * Add NetworkDown notification to NetworkInterface.c [PR: FreeRTOS#671] (FreeRTOS#812) * Add NetworkDown notification to EMAC task * Add NetworkDown notification to NetworkInterface.c * Uncrustify: triggered by comment. * Introduce ipconfigSUPPORT_NETWORK_DOWN_EVENT compile flag * Fix formatting * Uncrustify: triggered by comment. --------- Co-authored-by: Filip Oleszek <filip.oleszek@o2.pl> Co-authored-by: zipperowiec <35423392+zipperowiec@users.noreply.github.com> Co-authored-by: GitHub Action <action@github.com> * Uncrustify bot command fix (FreeRTOS#816) * fix uncrustify run command * test uncrustify * Revert "test uncrustify" This reverts commit f660ab435fa741f8767f8a2849829f02a92ecca6. * Fix uncrustify bot command - disable install prompt (FreeRTOS#819) * fix uncrustify run command * test uncrustify * Revert "test uncrustify" This reverts commit f660ab435fa741f8767f8a2849829f02a92ecca6. * removing apt-get prompt while installing git * Removing deprecated set-output command from uncrustify bot run yml (FreeRTOS#820) * fix uncrustify run command * test uncrustify * Revert "test uncrustify" This reverts commit f660ab435fa741f8767f8a2849829f02a92ecca6. * removing apt-get prompt while installing git * removing the deprecated set-output command from uncrustify bot run yml, use latest git * IPv4/Single: Let send() stop blocking after a connection reset (FreeRTOS#561) * IPv4/Single: Let send() stop after a protocol error * Remove token need * Repaired unit-testing * Added the cunftion test_FreeRTOS_send_DisconnectionOccursDuringWait() * Added a comment for unit-test function test_FreeRTOS_send_DisconnectionOccursDuringWait() * Added an item to lexicon.txt * Restored original tcp_utilities * Restored original tcp_utilities, once more --------- Co-authored-by: Hein Tibosch <hein@htibosch.net> Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Co-authored-by: Nikhil Kamath <110539926+amazonKamath@users.noreply.github.com> * Add logs to print random number generation failure (FreeRTOS#908) Add logs to print random number generation failure for better debugging of issue. * Update usage of uint64_t according to C90 standard (FreeRTOS#907) Co-authored-by: kar-rahul-aws <118818625+kar-rahul-aws@users.noreply.github.com> * Fix pragma pack in CCS compiler to push/pop (FreeRTOS#906) `#pragma pack(1)` would make it so that all structs inserted after pack_struct_start.h was included for the TI arm compiler would be packed, leading to potential unaligned memory access error. Refer: https://www.ti.com/lit/ug/spnu151w/spnu151w.pdf SECTION 5.11.23 * Modified libslirp backend file to cover different libslirp library versions (FreeRTOS#929) Authored-by: Xiaodong Li <xiaodonn@amazon.com> * Update according to devIntegration * Update links to point to main directory --------- Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com> Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Co-authored-by: Hein Tibosch <hein_tibosch@yahoo.es> Co-authored-by: Hein Tibosch <hein@htibosch.net> Co-authored-by: GitHub Action <action@github.com> Co-authored-by: alfred gedeon <28123637+alfred2g@users.noreply.github.com> Co-authored-by: Pete Bone <pete-pjb@users.noreply.github.com> Co-authored-by: PeterB <PeterB@PETE-LT.otg.local> Co-authored-by: ChristosZosi <76208460+ChristosZosi@users.noreply.github.com> Co-authored-by: jasonpcarroll <23126711+jasonpcarroll@users.noreply.github.com> Co-authored-by: Jason Carroll <czjaso@amazon.com> Co-authored-by: Tony Josi <117763118+tony-josi-aws@users.noreply.github.com> Co-authored-by: Ubuntu <ubuntu@ip-172-31-22-210.ec2.internal> Co-authored-by: Paul Bartell <paul.bartell@gmail.com> Co-authored-by: Kareem Khazem <karkhaz@amazon.com> Co-authored-by: Mark Tuttle <tuttle@acm.org> Co-authored-by: Tony Josi <tonyjosi@amazon.com> Co-authored-by: ActoryOu <jay2002824@gmail.com> Co-authored-by: Nikhil Kamath <110539926+amazonKamath@users.noreply.github.com> Co-authored-by: phelter <paulheltera@gmail.com> Co-authored-by: Adam St. Amand <adam.stamand@gmail.com> Co-authored-by: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com> Co-authored-by: sayyadumar <sayyadumar@users.noreply.github.com> Co-authored-by: Paul Bartell <pbartell@amazon.com> Co-authored-by: Kody Stribrny <89810515+kstribrnAmzn@users.noreply.github.com> Co-authored-by: Ubuntu <ubuntu@ip-10-0-137-67.ec2.internal> Co-authored-by: Filip Oleszek <filip.oleszek@o2.pl> Co-authored-by: zipperowiec <35423392+zipperowiec@users.noreply.github.com> Co-authored-by: kar-rahul-aws <118818625+kar-rahul-aws@users.noreply.github.com> Co-authored-by: Rahul Arasikere <arasikere.rahul@gmail.com> Co-authored-by: Xiaodong Li <85011700+ChaiTowKway@users.noreply.github.com>
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 described in the proof README.Related Issue
FreeRTOS/FreeRTOS-Kernel#607
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.