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

   1 /*
   2  * FreeRTOS V202104.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
  23 #include "proof/queue.h"
  24 #define taskENTER_CRITICAL()    setInterruptMask( pxQueue )
  25 #define taskEXIT_CRITICAL()     clearInterruptMask( pxQueue )
  26
  27 /* VeriFast: we make one major change. We merge the critical regions for
  28  * decrementing `cTxLock` and `cRxLock`. */
  29
  30 static void prvUnlockQueue( Queue_t * const pxQueue )
  31 /*@requires [1/2]queuehandle(pxQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*&
  32     [1/2]pxQueue->locked |-> ?m &*&
  33     mutex_held(m, queue_locked_invariant(pxQueue), currentThread, 1/2) &*&
  34     queue_locked_invariant(pxQueue)();@*/
  35 /*@ensures [1/2]queuehandle(pxQueue, N, M, is_isr) &*&
  36     [1/2]queuelock(pxQueue);@*/
  37 {
  38     /* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. */
  39
  40     /* The lock counts contains the number of extra data items placed or
  41      * removed from the queue while the queue was locked.  When a queue is
  42      * locked items can be added or removed, but the event lists cannot be
  43      * updated. */
  44     taskENTER_CRITICAL();
  45     /*@open queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, _, ?abs);@*/
  46     {
  47         int8_t cTxLock = pxQueue->cTxLock;
  48
  49         /* See if data was added to the queue while it was locked. */
  50         while( cTxLock > queueLOCKED_UNMODIFIED )
  51         /*@invariant queuelists(pxQueue);@*/
  52         {
  53             /* Data was posted while the queue was locked.  Are any tasks
  54              * blocked waiting for data to become available? */
  55             #if ( configUSE_QUEUE_SETS == 1 )
  56                 {
  57                     if( pxQueue->pxQueueSetContainer != NULL )
  58                     {
  59                         if( prvNotifyQueueSetContainer( pxQueue ) != pdFALSE )
  60                         {
  61                             /* The queue is a member of a queue set, and posting to
  62                              * the queue set caused a higher priority task to unblock.
  63                              * A context switch is required. */
  64                             vTaskMissedYield();
  65                         }
  66                         else
  67                         {
  68                             mtCOVERAGE_TEST_MARKER();
  69                         }
  70                     }
  71                     else
  72                     {
  73                         /* Tasks that are removed from the event list will get
  74                          * added to the pending ready list as the scheduler is still
  75                          * suspended. */
  76                         if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ) == pdFALSE )
  77                         {
  78                             if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE )
  79                             {
  80                                 /* The task waiting has a higher priority so record that a
  81                                  * context switch is required. */
  82                                 vTaskMissedYield();
  83                             }
  84                             else
  85                             {
  86                                 mtCOVERAGE_TEST_MARKER();
  87                             }
  88                         }
  89                         else
  90                         {
  91                             break;
  92                         }
  93                     }
  94                 }
  95             #else /* configUSE_QUEUE_SETS */
  96                 {
  97                     /* Tasks that are removed from the event list will get added to
  98                      * the pending ready list as the scheduler is still suspended. */
  99                     if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ) == pdFALSE )
 100                     {
 101                         if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE )
 102                         {
 103                             /* The task waiting has a higher priority so record that
 104                              * a context switch is required. */
 105                             vTaskMissedYield();
 106                         }
 107                         else
 108                         {
 109                             mtCOVERAGE_TEST_MARKER();
 110                         }
 111                     }
 112                     else
 113                     {
 114                         break;
 115                     }
 116                 }
 117             #endif /* configUSE_QUEUE_SETS */
 118
 119             --cTxLock;
 120         }
 121
 122         pxQueue->cTxLock = queueUNLOCKED;
 123     }
 124 #ifndef VERIFAST /*< ***merge cTxLock and cRxLock critical regions*** */
 125     taskEXIT_CRITICAL();
 126
 127     /* Do the same for the Rx lock. */
 128     taskENTER_CRITICAL();
 129 #endif
 130     {
 131         int8_t cRxLock = pxQueue->cRxLock;
 132
 133         while( cRxLock > queueLOCKED_UNMODIFIED )
 134         /*@invariant queuelists(pxQueue);@*/
 135         {
 136             if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToSend ) ) == pdFALSE )
 137             {
 138                 if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToSend ) ) != pdFALSE )
 139                 {
 140                     vTaskMissedYield();
 141                 }
 142                 else
 143                 {
 144                     mtCOVERAGE_TEST_MARKER();
 145                 }
 146
 147                 --cRxLock;
 148             }
 149             else
 150             {
 151                 break;
 152             }
 153         }
 154
 155         pxQueue->cRxLock = queueUNLOCKED;
 156     }
 157     /*@close queue(pxQueue, Storage, N, M, W, R, K, false, abs);@*/
 158     taskEXIT_CRITICAL();
 159 #ifdef VERIFAST /*< ghost action */
 160     mutex_release( pxQueue->locked );
 161 #endif
 162 }