begriffs open source - cmsis-freertos/blob - Test/VeriFast/docs/signoff.md

   1 # FreeRTOS VeriFast Proof Signoff
   2
   3 Verification tool: VeriFast (code-level proof)
   4
   5 Proofs: `queue/` and `list`
   6
   7 Implementation: Kernel queue data structure (`queue.c`) and list data structure (`list.c`)
   8
   9 Specification / Properties:
  10   - *Memory safety*: the implementation only accesses valid memory. In the case
  11     of the queue, this is true under any arbitrary number of tasks or ISRs.
  12   - *Thread safety*: in the case of the queue, tasks and ISRs only update
  13     objects that they own via proper synchronization.
  14   - *Functional correctness*: the queue and list implementations behave like an
  15     abstract queue and list. In the case of the queue, this is true under any
  16     arbitrary number of tasks or ISRs.
  17
  18 ## Queue proof assumptions
  19
  20 Generally, we assume well-behaved clients; the correctness of underlying
  21 primitives (memory allocation, task scheduling, scheduler suspension); and
  22 assumptions about the system.
  23
  24   - Well-behaved client: all client tasks and ISRs use the queue API in a
  25     manner that adheres to the specification. A badly-behaved client can
  26     invalidate the proven properties. For example, a client that reads or
  27     writes to the queue storage directly, without masking interrupts, is racy
  28     and no longer thread safe. The specification forbids this behavior by
  29     the definition of `queuehandle`, which is a handle to acquire ownership of
  30     the queue through interrupt masking, but we cannot, in general, enforce
  31     this behavior since we do not verify client code.
  32
  33   - Memory safety, thread safety and function contracts for the following
  34     primitives. For the list and task functions we give a contract that is
  35     maximal in terms of the queue objects that can be updated, but we do not
  36     model their function effect (e.g., task blocking and the moving of task
  37     control blocks between scheduler lists).
  38
  39         pvPortMalloc
  40         vPortFree
  41         memcpy
  42         vListInitialise
  43         xTaskRemoveFromEventList
  44         vTaskMissedYield
  45         xTaskCheckForTimeOut
  46         vTaskInternalSetTimeOutState
  47         vTaskPlaceOnEventList
  48
  49   - We assume interrupt masking gives strong isolation between tasks and ISRs.
  50     See Appendix. We further assume the system is configured as required by
  51     `configASSERT`. For example, interrupts with a priority greater than the
  52     maximum system call priority must not call queue API functions, otherwise
  53     the strong isolation guarantee is not maintained.
  54
  55 ## List proof assumptions
  56
  57 The list proofs are sequential. We assume the caller of the list API functions
  58 has taken appropriate synchronization steps to avoid races.
  59
  60 ## Simplifications
  61
  62 A list of changes to the source code required for the proofs can be generated:
  63
  64 ```
  65 make proof_changes
  66 ```
  67
  68 A side-by-side diff with respect to the source code can be generated. See
  69 ![`scripts/diff_files.md`](../scripts/diff_files.md).
  70
  71 The main queue changes are:
  72
  73   - merge cTxLock and cRxLock critical regions: under approximate queue
  74         unlock behavior to atomically set `cTxLock` and `cRxLock` to unlocked in a
  75     single critical region instead of two separate critical regions. In
  76         practice, this is not an issue since no ISR function reads-from both
  77     cTxLock and cRxLock.
  78   - model single malloc of struct and buffer: split the single malloc of the
  79     queue struct and storage into two separate mallocs.
  80   - xQueueGenericReset happens-before concurrent behavior: assume that queue
  81     initialisation is not concurrent.
  82   - do not model pxIndex and xListEnd of xLIST struct: ignore these fields in
  83     the list structs of the queue implementation
  84
  85 The main list changes are:
  86
  87   - change `MiniList_t` to `ListItem_t`: simplifying assumption on the list
  88     structure.
  89   - over-approximate list insert loop: replace a loop in the insert function
  90     that finds the insertion point with an over-approximating function call.
  91
  92 The following minor changes due to the stricter typing and parser of VeriFast:
  93
  94   - replacing a union declaration with a struct
  95   - const pointer declaration
  96   - stricter casting
  97   - void cast of unused return value
  98   - void cast of unused var
  99
 100 The following minor changes due to the modeling of interrupts and scheduler
 101 suspension in the proofs as ghost state.
 102
 103   - ghost action
 104   - leak ghost state on deletion
 105
 106 ## Configuration
 107
 108 We do not verify across the full configuration space of FreeRTOS. In
 109 particular, the queue proofs do not apply when the following options are
 110 enabled:
 111
 112   - `configUSE_QUEUE_SETS`
 113   - `configSUPPORT_STATIC_ALLOCATION`
 114
 115 For both the queue and list proofs we assume that coverage and tracing
 116 macros are no-ops.
 117
 118 ## Trusted computing base
 119
 120   - Soundness of verification tools: VeriFast, Redux prover
 121   - C Compiler, because the verification is at the C code-level and the
 122     properties proved may not be preserved by compilation.
 123
 124 ## References
 125
 126 [N1570] ISO/IEC. Programming languages – C. International standard 9899:201x,
 127 2011
 128
 129 ## Appendix
 130
 131 Assumption on strong isolation induced by interrupt masking and scheduler
 132 suspension for queue proofs. Informally, we need the following:
 133
 134 ```
 135 // Initially *data == 0
 136 // Task 1
 137 taskENTER_CRITICAL()
 138 *data = 1;
 139 *data = 2;
 140 taskEXIT_CRITICAL()
 141
 142 // ISR or Task 2
 143 r0 = *data; //< guaranteed to read 0 or 2, never 1
 144 ```