| 34 | * decrementing `cTxLock` and `cRxLock`. */ |
| 35 | |
| 36 | static void prvUnlockQueue( Queue_t * const pxQueue ) |
| 37 | /*@requires [1/2]queuehandle(pxQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& |
| 38 | [1/2]pxQueue->locked |-> ?m &*& |
| 39 | mutex_held(m, queue_locked_invariant(pxQueue), currentThread, 1/2) &*& |
| 40 | queue_locked_invariant(pxQueue)();@*/ |
| 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 | } |
no test coverage detected