From 38790b241d782b547d7f77601eb63631dd01c0f1 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Wed, 28 Dec 2022 20:52:48 -0500 Subject: [PATCH] Added explanation of verifast. --- .../tasks/vTaskSwitchContext/README.md | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/README.md b/Test/VeriFast/tasks/vTaskSwitchContext/README.md index 0eef4c72b..0d73b8198 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/README.md +++ b/Test/VeriFast/tasks/vTaskSwitchContext/README.md @@ -2,6 +2,28 @@ This directory contains an unbounded memory safety and thread safety proof 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: ``` Proof Assumptions: