From 1eb83cdb468ab9adbb4bfc88623bdbf5bd633821 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Tue, 3 Jan 2023 17:26:12 -0500 Subject: [PATCH] Wrote more documentation. --- .../tasks/vTaskSwitchContext/README.md | 4 +- .../tasks/vTaskSwitchContext/proof/README.md | 8 +- .../proof/lock_predicates.h | 72 +++++++- .../vTaskSwitchContext/proof/port_contracts.h | 76 --------- .../proof/port_locking_contracts.h | 159 ++++++++++++++++++ .../tasks/vTaskSwitchContext/src/tasks.c | 2 +- 6 files changed, 232 insertions(+), 89 deletions(-) delete mode 100644 Test/VeriFast/tasks/vTaskSwitchContext/proof/port_contracts.h create mode 100644 Test/VeriFast/tasks/vTaskSwitchContext/proof/port_locking_contracts.h diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/README.md b/Test/VeriFast/tasks/vTaskSwitchContext/README.md index 1c57d885d3b..561603fd659 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/README.md +++ b/Test/VeriFast/tasks/vTaskSwitchContext/README.md @@ -249,7 +249,7 @@ Therefore, the proof's correctness relies on the correctness of our models. VeriFast is a program verifier for C and not designed to handle any kind of assembly. The port-specific assembly is called via macros with a port-specific definition. We redefined these macros to call dummy function prototypes instead. - We equipped these prototypes with VeriFast contracts that capture the semantics of the original assembly code, cf. `proof/port_contracts.h`. + We equipped these prototypes with VeriFast contracts that capture the semantics of the original assembly code, cf. `proof/port_locking_contracts.h`. This way, VeriFast refers to the contracts to reason about the macro calls and does not have to deal with the assembly code. @@ -333,7 +333,7 @@ Therefore, the proof's correctness relies on the correctness of our models. Otherwise, consuming `I` during the release step will fail and consequently the entire proof will fail. FreeRTOS uses macros with port-specifc definitions to acquire and release locks and to mask and unmask interrupts. - We abstracted these with VeriFast contracts defined in `proof/port_contracts.h`. + We abstracted these with VeriFast contracts defined in `proof/port_locking_contracts.h`. The contracts ensure that invoking any synchronization mechanism produces or consumes the corresponding invariant. The invariants are defined in `proof/lock_predicates.h` diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/README.md b/Test/VeriFast/tasks/vTaskSwitchContext/proof/README.md index 37d503b6dcf..f01ef2d94f4 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/README.md +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/README.md @@ -9,11 +9,11 @@ This directory contains the bulk of VeriFast formalizations and proofs. │ This file also contains the lemmas to prove that the task state updates │ in `prvSelectHighestPriorityTask` preserve the lock invariants. │ -├── port_contracts.h +├── port_locking_contracts.h │ Contains VeriFast function contracts for macros with port-specific -│ definitions, e.g., the macros to mask interrupts and to acquire AND -│ release locks. These port-specific definitions often contain contain -│ inline assembly VeriFast cannot reason about. The contracts allow us +│ definitions used to invoke synchronization mechanisms, e.g., masking +│ interrupts and acquiring locks. These port-specific definitions often +│ contain inline assembly VeriFast cannot reason about. The contracts allow us │ to abstract the semantics of the assembly. │ ├── ready_list_predicates.h diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/lock_predicates.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/lock_predicates.h index e146e9f8335..868d0ef90ec 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/lock_predicates.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/lock_predicates.h @@ -55,18 +55,37 @@ /* ---------------------------------------------------------------------- * Core local data and access restrictions. * Some data in FreeRTOS such as the pointer to TCB of the task running - * on core `C` may only be accessed from core `C`. Such core-local data + * on core `C` may only be accessed from core `C`. Such core-local data is * protected by deactivating interrupts. */ /*@ +// Represents the state of interrupts (i.e. activated or deactivated) on a +// specific core. The state corresponds to the value of the special register +// used for interrupt masking. predicate interruptState_p(uint32_t coreID, uint32_t state); +// Given an interrupt state (i.e. the value of the special register used to +// control interrupt masking), this function returns whether the state expresses +// that interrupts are deactivated. fixpoint bool interruptsDisabled_f(uint32_t); + +// This predicate expresses that the core we are currently reasoning about +// (expressed by constant `coreID_f`) is allowed to access the core-local data +// protected by interrupt masking. predicate coreLocalInterruptInv_p() = - [0.5]pointer(&pxCurrentTCBs[coreID_f], ?currentTCB) &*& - integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*& + // Read permission to the entry of `pxCurrentTCBs` that stores a pointer + // to the task currenlty running on this core + [0.5]pointer(&pxCurrentTCBs[coreID_f], ?currentTCB) + &*& + // Write permission to the entry of `xYieldPendings` for the current core + integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) + &*& + // Write permission to the "critical nesting" field of the task + // currently scheduled on this core. The field allows us to check whether + // the task is currently in a critical section. Necessary to check whether, + // we are allowed to context switch. TCB_criticalNesting_p(currentTCB, ?gCriticalNesting); @*/ @@ -76,6 +95,13 @@ predicate coreLocalInterruptInv_p() = */ /*@ +// This predicate is used to remember which locks we're currently holding. Each +// Each constists of a pair `(f,id)`. `f` is the fraction of the lock we held +// before acquiring. Remembering the fraction is important to ensure that we +// reproduce the right fraction of the lock predicate when we release the lock. +// Otherwise, we can run into inconsistencies. +// `id` is the ID of the acquired lock, i.e., either `taskLockID_f` or +// `isrLockID_f`. predicate locked_p(list< pair > lockHistory); @*/ @@ -88,11 +114,13 @@ predicate locked_p(list< pair > lockHistory); /*@ fixpoint int taskLockID_f(); -// Represents an acquired task lock. +// Represents an unacquired task lock. predicate taskLock_p(); // Represents the invariant associated with the the task lock, i.e., -// access permissions to the resources protected by the lock. +// access permissions to the resources and code regions protected by the lock. +// These are not relevant to the context-switch proof. Therefore, we leave the +// predicate abstract. predicate taskLockInv_p(); @*/ @@ -107,7 +135,9 @@ fixpoint int isrLockID_f(); predicate isrLock_p(); // Represents the invariant associated with the the ISR lock, i.e., -// access permissions to the resources protected by the lock. +// access permissions to the resources and code regions protected by the lock. +// These are not relevant to the context-switch proof. Therefore, we leave the +// predicate abstract. predicate isrLockInv_p(); @*/ @@ -120,6 +150,36 @@ predicate isrLockInv_p(); /*@ fixpoint int taskISRLockID_f(); +// Represents the access rights protected by both the task and the ISR lock. +// Note that FreeRTOS' locking discipline demands the the task lock must be +// acquired before the ISR lock. Once, both locks have been acquired in the +// right order, ths invariant can be produced by invoking the lemma +// `produce_taskISRLockInv` and it can be consumed by invoking +// `consume_taskISRLockInv`. The lemmas ensure that we follow the locking +// discipline. +// +// This invariant expresses fine grained access rights to the following: +// - some global variables: +// + Read permission to the entry of `pxCurrentTCBs` that stores a pointer +// to the task currenly running on the core `coreID_f` our proof currently +// considers. Together with the read permission from +// `coreLocalInterruptInv_p` we get write access to this entry once +// interrupts have been deactivated and both locks have been acquired. +// + Write permission to `uxSchedulerSuspended`. +// + Write permission to `xSchedulerRunning`. +// + Write permission to `uxTopReadyPriority`. This variable stores to top +// priority for which there is a task that is ready to be scheduled. +// - Write access to the ready lists. +// - Fine-grained access permissions for task run states: +// + (RP-All) Read permission for every task. +// + (RP-Current) Read permission for task currently scheduled on this core. +// Together, (RP-All) and (RP-Current) give us a write permission for +// task scheduled on this core. +// + (RP-Unsched) Read permissions for unscheduled tasks. +// Together, (RP-All) and (RP-Unsched) give us write permissions for all +// unscheduled tasks. +// Note that these permissions do not allow us to change the run state of any +// task that is currently scheduled on another core. predicate taskISRLockInv_p() = _taskISRLockInv_p(_); diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/port_contracts.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/port_contracts.h deleted file mode 100644 index a72b5759788..00000000000 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/port_contracts.h +++ /dev/null @@ -1,76 +0,0 @@ -#ifndef PORT_CONTRACTS_H -#define PORT_CONTRACTS_H - - -// We want our proofs to hold for an arbitrary number of cores. -#undef portGET_CORE_ID -#define portGET_CORE_ID() VF__get_core_num() - -/* FreeRTOS core id is always zero based.*/ -static uint VF__get_core_num(void); -//@ requires true; -/*@ ensures 0 <= result &*& result < configNUM_CORES &*& - result == coreID_f(); -@*/ - -/*@ -// Allow reference to core id in proofs. -fixpoint uint coreID_f(); - -lemma void coreID_f_range(); -requires true; -ensures 0 <= coreID_f() &*& coreID_f() < configNUM_CORES; -@*/ - - - - -#undef portDISABLE_INTERRUPTS -#define portDISABLE_INTERRUPTS VF__portDISABLE_INTERRUPTS -uint32_t VF__portDISABLE_INTERRUPTS(); -//@ requires interruptState_p(?coreID, ?state); -/*@ ensures result == state &*& - interruptState_p(coreID, ?newState) &*& - interruptsDisabled_f(newState) == true &*& - interruptsDisabled_f(state) == true - ? newState == state - : coreLocalInterruptInv_p(); -@*/ - -#undef portRESTORE_INTERRUPTS -#define portRESTORE_INTERRUPTS(ulState) VF__portRESTORE_INTERRUPTS(ulState) -void VF__portRESTORE_INTERRUPTS(uint32_t ulState); -/*@ requires interruptState_p(?coreID, ?tmpState) &*& - (interruptsDisabled_f(tmpState) == true && interruptsDisabled_f(ulState) == false) - ? coreLocalInterruptInv_p() - : true; - @*/ -/*@ ensures interruptState_p(coreID, ulState); -@*/ - -#undef portGET_TASK_LOCK -#define portGET_TASK_LOCK VF__portGET_TASK_LOCK -void VF__portGET_TASK_LOCK(); -//@ requires [?f]taskLock_p() &*& locked_p(nil); -//@ ensures taskLockInv_p() &*& locked_p( cons( pair(f, taskLockID_f()), nil) ); - -#undef portRELEASE_TASK_LOCK -#define portRELEASE_TASK_LOCK VF__portRELEASE_TASK_LOCK -void VF__portRELEASE_TASK_LOCK(); -//@ requires taskLockInv_p() &*& locked_p( cons( pair(?f, taskLockID_f()), nil) ); -//@ ensures [f]taskLock_p() &*& locked_p(nil); - -#undef portGET_ISR_LOCK -#define portGET_ISR_LOCK VF__portGET_ISR_LOCK -void VF__portGET_ISR_LOCK(); -//@ requires [?f]isrLock_p() &*& locked_p(?heldLocks); -//@ ensures isrLockInv_p() &*& locked_p( cons( pair(f, isrLockID_f()), heldLocks) ); - -#undef portRELEASE_ISR_LOCK -#define portRELEASE_ISR_LOCK VF__portRELEASE_ISR_LOCK -void VF__portRELEASE_ISR_LOCK(); -//@ requires isrLockInv_p() &*& locked_p( cons( pair(?f, isrLockID_f()), ?heldLocks) ); -//@ ensures [f]isrLock_p() &*& locked_p(heldLocks); - - -#endif /* PORT_CONTRACTS_H */ \ No newline at end of file diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/port_locking_contracts.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/port_locking_contracts.h new file mode 100644 index 00000000000..a7dc6fe7987 --- /dev/null +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/port_locking_contracts.h @@ -0,0 +1,159 @@ +#ifndef PORT_CONTRACTS_H +#define PORT_CONTRACTS_H + +/* This file defines function contracts for the macros used to invoke + * synchronization mechanisms, e.g., masking interrupts and acquiring locks. + * The definitions of these macros are port-specific and involve inline + * assembly. VeriFast cannot reason about assembly. Hence, we have to + * abstract the assembly's semantics with these contracts. + * + * Note that we cannot verify that the contracts' correctness. We have to treat + * their correctness as a proof assumption. + * + * Moreover, together with the invariants defined in the proof header + * `lock_predicates.h`, the below contracts define the locking discipline that + * our proof relies on. The file `lock_predicates.h` contains a more detailed + * explanation of the locking discipline. + * + * In short: + * - Data that is only meant to be accessed by the a specific core is protected + * by deactivating interrupts on this core. Access permissions are expressed + * by `coreLocalInterruptInv_p`. + * - The task lock and the ISR lock (i.e. interrupt lock) themselves protect + * data and code regions irrelevant to the switch-context proof. Hence, + * the respective invariants are left abstract, cf. `taskLockInv_p` and + * `isrLockInv_p`. + * - FreeRTOS' locking discipline demands that the task lock is acquired before + * and released after the ISR lock. The contracts defined below ensure that + * we follow this locking discipline. + * - The ready lists and the task run states (i.e. the data most important to + * the context-switch proof) is protected by a combination of the task lock + * and the ISR lock. That is, this data must only be accessed when both + * locks have been acquired in the right order. The invariant + * `taskISRLockInv_p` expresses these access rights. `lock_predicates.h` + * defines lemmas to produce and consume this invariant. The lemmas ensure + * that we only produce the invariant when both locks have been acquired in + * the right order. + */ + +// We want our proofs to hold for an arbitrary number of cores. +#undef portGET_CORE_ID +#define portGET_CORE_ID() VF__get_core_num() + +/* FreeRTOS core id is always zero based.*/ +static uint VF__get_core_num(void); +//@ requires true; +/*@ ensures 0 <= result &*& result < configNUM_CORES &*& + result == coreID_f(); +@*/ + +/*@ +// This contant allows proofs to talk about the ID of the core that the +// function we verify is running on. The verified function's contract must +// ensure that this constant holds the value of the current core. +fixpoint uint coreID_f(); + +lemma void coreID_f_range(); +requires true; +ensures 0 <= coreID_f() &*& coreID_f() < configNUM_CORES; +@*/ + + + + +/* In FreeRTOS interrupts are masked to protect core-local data. + * The invariant `coreLocalInterruptInv_p` expresses what data the masking + * of interrupts protects on a specific core, cf., `lock_predicates.h`. + * + * Deactivating the interrupts on the current core produces the invariant + * `coreLocalInterruptInv_p()` and thereby gives us the permission to access + * the protected data. + */ +#undef portDISABLE_INTERRUPTS +#define portDISABLE_INTERRUPTS VF__portDISABLE_INTERRUPTS +uint32_t VF__portDISABLE_INTERRUPTS(); +//@ requires interruptState_p(?coreID, ?state); +/*@ ensures result == state &*& + interruptState_p(coreID, ?newState) &*& + interruptsDisabled_f(newState) == true &*& + interruptsDisabled_f(state) == true + ? newState == state + : coreLocalInterruptInv_p(); +@*/ + + +/* This macro is used to restore the interrupt state (activated or deactivated) + * to a specific value. When an invokation sets the state from deactivated to + * activated, the invariant `coreLocalInterruptInv_p()` is consumed. + * Thereby, we lose the permission to access the core-local data protected + * by the deactivation of interrupts on this core. + */ +#undef portRESTORE_INTERRUPTS +#define portRESTORE_INTERRUPTS(ulState) VF__portRESTORE_INTERRUPTS(ulState) +void VF__portRESTORE_INTERRUPTS(uint32_t ulState); +/*@ requires interruptState_p(?coreID, ?tmpState) &*& + (interruptsDisabled_f(tmpState) == true && interruptsDisabled_f(ulState) == false) + ? coreLocalInterruptInv_p() + : true; + @*/ +/*@ ensures interruptState_p(coreID, ulState); +@*/ + + +/* This macro is used to acquire the task lock. The task lock on its own + * protects data and core regions that are not relevant to the context-switch + * proof. Hence, an invocation produces an abstract invariant `taskLockInv_p()` + * and updates the locking history `locked_p(...)` to log that the task log + * has been acquired. + * + * FreeRTOS' locking discipline requires that the task lock must be acquired + * before the ISR lock. The precondition `locked_p(nil)` only allows + * invocations of this macro when no lock has been acquired, yet. + */ +#undef portGET_TASK_LOCK +#define portGET_TASK_LOCK VF__portGET_TASK_LOCK +void VF__portGET_TASK_LOCK(); +//@ requires [?f]taskLock_p() &*& locked_p(nil); +//@ ensures taskLockInv_p() &*& locked_p( cons( pair(f, taskLockID_f()), nil) ); + + +/* This macro is used to release the task lock. An invocation consumes the + * task lock invariant `taskLockInv_p` and updates the locking history + * `locked_p(...)` to reflect the release. + * + * FreeRTOS' locking discipline demands that the task lock must be acquired + * before and released after the ISR lock. The precondition + * `locked_p( cons( pair(?f, taskLockID_f()), nil) )` only allows calls to this + * macro when we can prove that we only hold the task lock. + * */ +#undef portRELEASE_TASK_LOCK +#define portRELEASE_TASK_LOCK VF__portRELEASE_TASK_LOCK +void VF__portRELEASE_TASK_LOCK(); +//@ requires taskLockInv_p() &*& locked_p( cons( pair(?f, taskLockID_f()), nil) ); +//@ ensures [f]taskLock_p() &*& locked_p(nil); + + +/* This macro is used to acquire the ISR lock (i.e. interrupt lock). An + * invocation produces the abstract ISR lock invariant `isrLock_p` and + * updates the locking history `locked_p(...)` to reflect that the lock has + * been acquired. + */ +#undef portGET_ISR_LOCK +#define portGET_ISR_LOCK VF__portGET_ISR_LOCK +void VF__portGET_ISR_LOCK(); +//@ requires [?f]isrLock_p() &*& locked_p(?heldLocks); +//@ ensures isrLockInv_p() &*& locked_p( cons( pair(f, isrLockID_f()), heldLocks) ); + + +/* This macro is used to release the ISR lock (i.e. interrupt lock). A call + * consumes the ISR lock invariant and updates the locking history + * `locked_p(...)` to reflect the release. + */ +#undef portRELEASE_ISR_LOCK +#define portRELEASE_ISR_LOCK VF__portRELEASE_ISR_LOCK +void VF__portRELEASE_ISR_LOCK(); +//@ requires isrLockInv_p() &*& locked_p( cons( pair(?f, isrLockID_f()), ?heldLocks) ); +//@ ensures [f]isrLock_p() &*& locked_p(heldLocks); + + +#endif /* PORT_CONTRACTS_H */ \ No newline at end of file diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c index 78901121fa0..1506b11cea3 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c +++ b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c @@ -79,7 +79,7 @@ #include "task_predicates.h" #include "ready_list_predicates.h" #include "asm.h" - #include "port_contracts.h" + #include "port_locking_contracts.h" #include "lock_predicates.h" #include "verifast_lists_extended.h" #include "single_core_proofs/scp_list_predicates.h"