From e52ae501c3867b7d7d3e06b296de4d1a3e097a43 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 | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/README.md b/Test/VeriFast/tasks/vTaskSwitchContext/README.md index 561603fd659..46cfc3e3561 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/README.md +++ b/Test/VeriFast/tasks/vTaskSwitchContext/README.md @@ -198,6 +198,16 @@ 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 parts that we have to understand in order to understand what 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 files mentioned above, in the provided order 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.