Wrote more documentation.

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`
 

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

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<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(_);
 

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 */