From c57b62a3dc7031fb80044b802f632c4fb98061e4 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Wed, 4 Jan 2023 12:32:28 -0500 Subject: [PATCH] Added some guidance on how to read the proof. --- Test/VeriFast/tasks/vTaskSwitchContext/README.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/README.md b/Test/VeriFast/tasks/vTaskSwitchContext/README.md index 561603fd659..630c8a79539 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/README.md +++ b/Test/VeriFast/tasks/vTaskSwitchContext/README.md @@ -198,6 +198,17 @@ Both scripts expect the command line arguments explained below. - \ is an optional argument specifying the IDE's font size. +# Reading the Proof +The most important aspects that we have to understand in order to understand the proof are the following, in this order: + - The locking discipline, cf. `proof/port_locking_contracts.h` + - The lock invariants, cf. `proof/lock_predicates.h`. The invariants use the ready list and task predicates defined in `proof/ready_list_predicates.h` and `task_predicates.h`. + - The contracts for the functions we verified, i.e., `vTaskSwitchContext` and `prvSelectHighestPriorityTask`, cf. `src/tasks.c`. + +We propose to first skim the above mentioned files -- in the given order -- and the documentation they provide to get an overview of how the proof is structured. + + + + # Maintaining the Proof This directory contains annotated copies of FreeRTOS source and header files. The annotations in these files tell VeriFast which functions it should verify and what the proof looks like.