begriffs open source - cmsis-freertos/blob - Test/VeriFast/queue/prvUnlockQueue.c

   1 /*
   2  * FreeRTOS V202107.00
   3  * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
   4  *
   5  * Permission is hereby granted, free of charge, to any person obtaining a copy of
   6  * this software and associated documentation files (the "Software"), to deal in
   7  * the Software without restriction, including without limitation the rights to
   8  * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
   9  * the Software, and to permit persons to whom the Software is furnished to do so,
  10  * subject to the following conditions:
  11  *
  12  * The above copyright notice and this permission notice shall be included in all
  13  * copies or substantial portions of the Software.
  14  *
  15  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
  16  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
  17  * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
  18  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  19  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  20  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  21  *
  22  * https://www.FreeRTOS.org
  23  * https://github.com/FreeRTOS
  24  *
  25  */
  26
  27 #include "proof/queue.h"
  28 #define taskENTER_CRITICAL()    setInterruptMask( pxQueue )
  29 #define taskEXIT_CRITICAL()     clearInterruptMask( pxQueue )
  30
  31 /* VeriFast: we make one major change. We merge the critical regions for
  32  * decrementing `cTxLock` and `cRxLock`. */
  33
  34 static void prvUnlockQueue( Queue_t * const pxQueue )
  35
  36 /*@requires [1/2]queuehandle(pxQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*&
  37  *  [1/2]pxQueue->locked |-> ?m &*&
  38  *  mutex_held(m, queue_locked_invariant(pxQueue), currentThread, 1/2) &*&
  39  *  queue_locked_invariant(pxQueue)();@*/
  40
  41 /*@ensures [1/2]queuehandle(pxQueue, N, M, is_isr) &*&
  42  *  [1/2]queuelock(pxQueue);@*/
  43 {
  44     /* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. */
  45
  46     /* The lock counts contains the number of extra data items placed or
  47      * removed from the queue while the queue was locked.  When a queue is
  48      * locked items can be added or removed, but the event lists cannot be
  49      * updated. */
  50     taskENTER_CRITICAL();
  51     /*@open queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, _, ?abs);@*/
  52     {
  53         int8_t cTxLock = pxQueue->cTxLock;
  54
  55         /* See if data was added to the queue while it was locked. */
  56         while( cTxLock > queueLOCKED_UNMODIFIED )
  57         /*@invariant queuelists(pxQueue);@*/
  58         {
  59             /* Data was posted while the queue was locked.  Are any tasks
  60              * blocked waiting for data to become available? */
  61             #if ( configUSE_QUEUE_SETS == 1 )
  62                 {
  63                     if( pxQueue->pxQueueSetContainer != NULL )
  64                     {
  65                         if( prvNotifyQueueSetContainer( pxQueue ) != pdFALSE )
  66                         {
  67                             /* The queue is a member of a queue set, and posting to
  68                              * the queue set caused a higher priority task to unblock.
  69                              * A context switch is required. */
  70                             vTaskMissedYield();
  71                         }
  72                         else
  73                         {
  74                             mtCOVERAGE_TEST_MARKER();
  75                         }
  76                     }
  77                     else
  78                     {
  79                         /* Tasks that are removed from the event list will get
  80                          * added to the pending ready list as the scheduler is still
  81                          * suspended. */
  82                         if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ) == pdFALSE )
  83                         {
  84                             if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE )
  85                             {
  86                                 /* The task waiting has a higher priority so record that a
  87                                  * context switch is required. */
  88                                 vTaskMissedYield();
  89                             }
  90                             else
  91                             {
  92                                 mtCOVERAGE_TEST_MARKER();
  93                             }
  94                         }
  95                         else
  96                         {
  97                             break;
  98                         }
  99                     }
 100                 }
 101             #else /* configUSE_QUEUE_SETS */
 102                 {
 103                     /* Tasks that are removed from the event list will get added to
 104                      * the pending ready list as the scheduler is still suspended. */
 105                     if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ) == pdFALSE )
 106                     {
 107                         if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE )
 108                         {
 109                             /* The task waiting has a higher priority so record that
 110                              * a context switch is required. */
 111                             vTaskMissedYield();
 112                         }
 113                         else
 114                         {
 115                             mtCOVERAGE_TEST_MARKER();
 116                         }
 117                     }
 118                     else
 119                     {
 120                         break;
 121                     }
 122                 }
 123             #endif /* configUSE_QUEUE_SETS */
 124
 125             --cTxLock;
 126         }
 127
 128         pxQueue->cTxLock = queueUNLOCKED;
 129     }
 130     #ifndef VERIFAST /*< ***merge cTxLock and cRxLock critical regions*** */
 131         taskEXIT_CRITICAL();
 132
 133         /* Do the same for the Rx lock. */
 134         taskENTER_CRITICAL();
 135     #endif
 136     {
 137         int8_t cRxLock = pxQueue->cRxLock;
 138
 139         while( cRxLock > queueLOCKED_UNMODIFIED )
 140         /*@invariant queuelists(pxQueue);@*/
 141         {
 142             if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToSend ) ) == pdFALSE )
 143             {
 144                 if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToSend ) ) != pdFALSE )
 145                 {
 146                     vTaskMissedYield();
 147                 }
 148                 else
 149                 {
 150                     mtCOVERAGE_TEST_MARKER();
 151                 }
 152
 153                 --cRxLock;
 154             }
 155             else
 156             {
 157                 break;
 158             }
 159         }
 160
 161         pxQueue->cRxLock = queueUNLOCKED;
 162     }
 163     /*@close queue(pxQueue, Storage, N, M, W, R, K, false, abs);@*/
 164     taskEXIT_CRITICAL();
 165     #ifdef VERIFAST /*< ghost action */
 166         mutex_release( pxQueue->locked );
 167     #endif
 168 }