mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-12-07 13:45:00 -05:00
Wrote more documentation.
This commit is contained in:
Tobias Reinhard
parent
48290b9641
commit
1eb83cdb46
6 changed files with 232 additions and 89 deletions
|
|
@ -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`
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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<real, int> > lockHistory);
|
||||
@*/
|
||||
|
||||
|
|
@ -88,11 +114,13 @@ predicate locked_p(list< pair<real, int> > 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(_);
|
||||
|
||||
|
|
|
|||
|
|
@ -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 */
|
||||
|
|
@ -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 */
|
||||
|
|
@ -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"
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue