578 lines
21 KiB
C
578 lines
21 KiB
C
/*
|
|
* FreeRTOS V202111.00
|
|
* Copyright (C) Amazon.com, Inc. or its affiliates. All Rights Reserved.
|
|
*
|
|
* Permission is hereby granted, free of charge, to any person obtaining a copy of
|
|
* this software and associated documentation files (the "Software"), to deal in
|
|
* the Software without restriction, including without limitation the rights to
|
|
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
|
|
* the Software, and to permit persons to whom the Software is furnished to do so,
|
|
* subject to the following conditions:
|
|
*
|
|
* The above copyright notice and this permission notice shall be included in all
|
|
* copies or substantial portions of the Software.
|
|
*
|
|
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
|
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
|
|
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
|
|
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
|
|
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
|
|
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
|
*
|
|
* https://www.FreeRTOS.org
|
|
* https://github.com/FreeRTOS
|
|
*
|
|
*/
|
|
|
|
#ifndef QUEUE_H
|
|
#define QUEUE_H
|
|
|
|
#define VERIFAST
|
|
#include <stdlib.h>
|
|
#include <stdint.h>
|
|
#include <string.h>
|
|
#include <threading.h>
|
|
/*@#include "common.gh"@*/
|
|
|
|
typedef size_t TickType_t;
|
|
typedef size_t UBaseType_t;
|
|
typedef ssize_t BaseType_t;
|
|
|
|
/* Empty/no-op macros */
|
|
/* Tracing */
|
|
#define traceBLOCKING_ON_QUEUE_PEEK( x )
|
|
#define traceBLOCKING_ON_QUEUE_RECEIVE( x )
|
|
#define traceBLOCKING_ON_QUEUE_SEND( x )
|
|
#define traceQUEUE_CREATE( x )
|
|
#define traceQUEUE_CREATE_FAILED( x )
|
|
#define traceQUEUE_DELETE( x )
|
|
#define traceQUEUE_PEEK( x )
|
|
#define traceQUEUE_PEEK_FAILED( x )
|
|
#define traceQUEUE_PEEK_FROM_ISR( x )
|
|
#define traceQUEUE_PEEK_FROM_ISR_FAILED( x )
|
|
#define traceQUEUE_RECEIVE( x )
|
|
#define traceQUEUE_RECEIVE_FAILED( x )
|
|
#define traceQUEUE_RECEIVE_FROM_ISR( x )
|
|
#define traceQUEUE_RECEIVE_FROM_ISR_FAILED( x )
|
|
#define traceQUEUE_SEND( x )
|
|
#define traceQUEUE_SEND_FAILED( x )
|
|
#define traceQUEUE_SEND_FROM_ISR( x )
|
|
#define traceQUEUE_SEND_FROM_ISR_FAILED( x )
|
|
/* Coverage */
|
|
#define mtCOVERAGE_TEST_MARKER()
|
|
/* Asserts */
|
|
#define configASSERT( x )
|
|
#define portASSERT_IF_INTERRUPT_PRIORITY_INVALID()
|
|
|
|
/* Map portable memory management functions */
|
|
#define pvPortMalloc malloc
|
|
#define vPortFree free
|
|
|
|
#define queueSEND_TO_BACK ( ( BaseType_t ) 0 )
|
|
#define queueSEND_TO_FRONT ( ( BaseType_t ) 1 )
|
|
#define queueOVERWRITE ( ( BaseType_t ) 2 )
|
|
|
|
#define pdTRUE 1
|
|
#define pdFALSE 0
|
|
|
|
#define pdPASS pdTRUE
|
|
#define pdFAIL pdFALSE
|
|
#define errQUEUE_FULL 0
|
|
#define errQUEUE_EMPTY 0
|
|
|
|
/* Constants used with the cRxLock and cTxLock structure members. */
|
|
#define queueUNLOCKED ( ( int8_t ) -1 )
|
|
#define queueLOCKED_UNMODIFIED ( ( int8_t ) 0 )
|
|
#define queueINT8_MAX ( ( int8_t ) 127 )
|
|
|
|
typedef struct QueuePointers
|
|
{
|
|
int8_t * pcTail; /*< Points to the byte at the end of the queue storage area. Once more byte is allocated than necessary to store the queue items, this is used as a marker. */
|
|
int8_t * pcReadFrom; /*< Points to the last place that a queued item was read from when the structure is used as a queue. */
|
|
} QueuePointers_t;
|
|
|
|
typedef struct SemaphoreData
|
|
{
|
|
#ifdef VERIFAST /*< do not model xMutexHolder */
|
|
void * xMutexHolder;
|
|
#else
|
|
TaskHandle_t xMutexHolder; /*< The handle of the task that holds the mutex. */
|
|
#endif
|
|
UBaseType_t uxRecursiveCallCount; /*< Maintains a count of the number of times a recursive mutex has been recursively 'taken' when the structure is used as a mutex. */
|
|
} SemaphoreData_t;
|
|
|
|
/* VeriFast does not support unions so we replace with a struct */
|
|
struct fake_union_t
|
|
{
|
|
QueuePointers_t xQueue;
|
|
SemaphoreData_t xSemaphore;
|
|
};
|
|
|
|
typedef struct xLIST
|
|
{
|
|
UBaseType_t uxNumberOfItems;
|
|
#ifndef VERIFAST /*< do not model pxIndex and xListEnd of xLIST struct */
|
|
struct xLIST_ITEM * pxIndex;
|
|
MiniListItem_t xListEnd;
|
|
#endif
|
|
} List_t;
|
|
|
|
typedef struct QueueDefinition /* The old naming convention is used to prevent breaking kernel aware debuggers. */
|
|
{
|
|
int8_t * pcHead; /*< Points to the beginning of the queue storage area. */
|
|
int8_t * pcWriteTo; /*< Points to the free next place in the storage area. */
|
|
|
|
#ifdef VERIFAST /*< VeriFast does not model unions */
|
|
struct fake_union_t u;
|
|
#else
|
|
union
|
|
{
|
|
QueuePointers_t xQueue; /*< Data required exclusively when this structure is used as a queue. */
|
|
SemaphoreData_t xSemaphore; /*< Data required exclusively when this structure is used as a semaphore. */
|
|
} u;
|
|
#endif
|
|
|
|
List_t xTasksWaitingToSend; /*< List of tasks that are blocked waiting to post onto this queue. Stored in priority order. */
|
|
List_t xTasksWaitingToReceive; /*< List of tasks that are blocked waiting to read from this queue. Stored in priority order. */
|
|
|
|
volatile UBaseType_t uxMessagesWaiting; /*< The number of items currently in the queue. */
|
|
UBaseType_t uxLength; /*< The length of the queue defined as the number of items it will hold, not the number of bytes. */
|
|
UBaseType_t uxItemSize; /*< The size of each items that the queue will hold. */
|
|
|
|
volatile int8_t cRxLock; /*< Stores the number of items received from the queue (removed from the queue) while the queue was locked. Set to queueUNLOCKED when the queue is not locked. */
|
|
volatile int8_t cTxLock; /*< Stores the number of items transmitted to the queue (added to the queue) while the queue was locked. Set to queueUNLOCKED when the queue is not locked. */
|
|
|
|
#if ( ( configSUPPORT_STATIC_ALLOCATION == 1 ) && ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) )
|
|
uint8_t ucStaticallyAllocated; /*< Set to pdTRUE if the memory used by the queue was statically allocated to ensure no attempt is made to free the memory. */
|
|
#endif
|
|
|
|
#if ( configUSE_QUEUE_SETS == 1 )
|
|
struct QueueDefinition * pxQueueSetContainer;
|
|
#endif
|
|
|
|
#if ( configUSE_TRACE_FACILITY == 1 )
|
|
UBaseType_t uxQueueNumber;
|
|
uint8_t ucQueueType;
|
|
#endif
|
|
|
|
/*@struct mutex *irqMask;@*/ /*< Ghost mutex simulates the effect of irq masking */
|
|
/*@struct mutex *schedulerSuspend;@*/ /*< Ghost mutex simulates the effect of scheduler suspension */
|
|
/*@struct mutex *locked;@*/ /*< Ghost mutex simulates the effect of queue locking */
|
|
} xQUEUE;
|
|
|
|
typedef xQUEUE Queue_t;
|
|
|
|
typedef struct QueueDefinition * QueueHandle_t;
|
|
|
|
/*@
|
|
#define QUEUE_SHAPE(q, Storage, N, M, K) \
|
|
* malloc_block_QueueDefinition(q) &*& \
|
|
* q->pcHead |-> Storage &*& \
|
|
* q->pcWriteTo |-> ?WPtr &*& \
|
|
* q->u.xQueue.pcTail |-> ?End &*& \
|
|
* q->u.xQueue.pcReadFrom |-> ?RPtr &*& \
|
|
* q->uxItemSize |-> M &*& \
|
|
* q->uxLength |-> N &*& \
|
|
* q->uxMessagesWaiting |-> K &*& \
|
|
* q->cRxLock |-> ?rxLock &*& \
|
|
* q->cTxLock |-> ?txLock &*& \
|
|
* struct_QueuePointers_padding(&q->u.xQueue) &*& \
|
|
* struct_SemaphoreData_padding(&q->u.xSemaphore) &*& \
|
|
* struct_fake_union_t_padding(&q->u) &*& \
|
|
* struct_xLIST_padding(&q->xTasksWaitingToSend) &*& \
|
|
* struct_xLIST_padding(&q->xTasksWaitingToReceive) &*& \
|
|
* q->u.xSemaphore.xMutexHolder |-> _ &*& \
|
|
* q->u.xSemaphore.uxRecursiveCallCount |-> _ &*& \
|
|
* true
|
|
*
|
|
* predicate queue(QueueHandle_t q, int8_t *Storage, size_t N, size_t M, size_t W, size_t R, size_t K, bool is_locked; list<list<char> >abs) =
|
|
* QUEUE_SHAPE(q, Storage, N, M, K) &*&
|
|
* 0 < N &*&
|
|
* 0 < M &*&
|
|
* 0 <= W &*& W < N &*&
|
|
* 0 <= R &*& R < N &*&
|
|
* 0 <= K &*& K <= N &*&
|
|
* W == (R + 1 + K) % N &*&
|
|
* (-1) <= rxLock &*&
|
|
* (-1) <= txLock &*&
|
|
* (is_locked ? 0 <= rxLock : (-1) == rxLock) &*&
|
|
* (is_locked ? 0 <= txLock : (-1) == txLock) &*&
|
|
* WPtr == Storage + (W*M) &*&
|
|
* RPtr == Storage + (R*M) &*&
|
|
* End == Storage + (N*M) &*&
|
|
* buffer(Storage, N, M, ?contents) &*&
|
|
* length(contents) == N &*&
|
|
* abs == take(K, rotate_left((R+1)%N, contents)) &*&
|
|
* malloc_block(Storage, N*M) &*&
|
|
* true
|
|
* ;
|
|
* @*/
|
|
|
|
/* A buffer allows us to interpret a flat character array of `N*M` bytes as a
|
|
* list of `N` elements where each element is `M` bytes */
|
|
|
|
/*@
|
|
* predicate buffer(char *buffer, size_t N, size_t M; list<list<char> > elements) =
|
|
* N == 0
|
|
* ? elements == nil
|
|
* : chars(buffer, M, ?x) &*& buffer(buffer + M, N - 1, M, ?xs) &*& elements == cons(x, xs);
|
|
*
|
|
* lemma void buffer_length(char *buffer, size_t N, size_t M)
|
|
* requires buffer(buffer, N, M, ?elements);
|
|
* ensures buffer(buffer, N, M, elements) &*& length(elements) == N;
|
|
* {
|
|
* if (N == 0) {
|
|
* open buffer(buffer, N, M, elements);
|
|
* close buffer(buffer, N, M, elements);
|
|
* } else {
|
|
* open buffer(buffer, N, M, elements);
|
|
* buffer_length(buffer+M, N-1, M);
|
|
* }
|
|
* }
|
|
* @*/
|
|
|
|
/*
|
|
* There is no need in the queue proofs to preserve a relationship between `cs`
|
|
* and `elements` (i.e., `flatten(elements) == cs`) because we only move in one
|
|
* direction from `cs` to `elements` during queue creation when the contents is
|
|
* fresh from `malloc` (i.e., uninitialized). If we needed to do a roundtrip from
|
|
* elements back to cs then this would require a stronger lemma.
|
|
*/
|
|
|
|
/*@
|
|
* lemma void buffer_from_chars(char *buffer, size_t N, size_t M)
|
|
* requires chars(buffer, N*M, ?cs) &*& 0 <= N &*& 0 < M;
|
|
* ensures exists<list<list<char> > >(?elements) &*& buffer(buffer, N, M, elements) &*& length(elements) == N;
|
|
* {
|
|
* if (N == 0) {
|
|
* close exists(nil);
|
|
* } else {
|
|
* int i = 0;
|
|
* while (i < N)
|
|
* invariant 0 <= i &*& i <= N &*&
|
|
* chars(buffer, (N-i)*M, ?xs) &*& xs == take((N-i)*M, cs) &*&
|
|
* buffer(buffer + (N-i)*M, i, M, ?ys);
|
|
* decreases N-i;
|
|
* {
|
|
* mul_mono_l(0, N-i-1, M);
|
|
* chars_split(buffer, (N-i-1)*M);
|
|
* mul_mono_l(i, N, M);
|
|
* mul_mono_l(N-i, N, M);
|
|
* take_take((N-i-1)*M, (N-i)*M, cs);
|
|
* i++;
|
|
* }
|
|
* close exists(ys);
|
|
* buffer_length(buffer, N, M);
|
|
* }
|
|
* }
|
|
*
|
|
* lemma void append_buffer(char *buffer, size_t N1, size_t N2, size_t M)
|
|
* requires
|
|
* buffer(buffer, N1, M, ?elements1) &*&
|
|
* buffer(buffer + N1 * M, N2, M, ?elements2) &*&
|
|
* 0 <= N1 &*& 0 <= N2;
|
|
* ensures buffer(buffer, N1+N2, M, append(elements1, elements2));
|
|
* {
|
|
* if (N1 == 0) {
|
|
* open buffer(buffer, 0, M, _);
|
|
* } else if (N2 == 0) {
|
|
* open buffer(buffer + N1 * M, 0, M, _);
|
|
* } else {
|
|
* open buffer(buffer, N1, M, elements1);
|
|
* append_buffer(buffer + M, N1-1, N2, M);
|
|
* close buffer(buffer, N1+N2, M, cons(?x, append(xs, elements2)));
|
|
* }
|
|
* }
|
|
*
|
|
* lemma void split_element<t>(char *buffer, size_t N, size_t M, size_t i)
|
|
* requires buffer(buffer, N, M, ?elements) &*& 0 <= i &*& i < N;
|
|
* ensures
|
|
* buffer(buffer, i, M, take(i, elements)) &*&
|
|
* chars(buffer + i * M, M, nth(i, elements)) &*&
|
|
* buffer(buffer + (i + 1) * M, (N-1-i), M, drop(i+1, elements));
|
|
* {
|
|
* if (i == 0) {
|
|
* // straightforward
|
|
* } else {
|
|
* buffer_length(buffer, N, M);
|
|
* int j = 0;
|
|
* while (j < i)
|
|
* invariant 0 <= j &*& j <= i &*&
|
|
* buffer(buffer, j, M, take(j, elements)) &*&
|
|
* buffer(buffer + j * M, N-j, M, drop(j, elements));
|
|
* decreases i-j;
|
|
* {
|
|
* drop_drop(1, j, elements);
|
|
* nth_drop2(elements, j);
|
|
* open buffer(buffer + j * M, N-j, M, drop(j, elements));
|
|
* assert chars(buffer + j * M, M, ?x) &*& x == nth(j, elements);
|
|
* close buffer(buffer + j * M, 1, M, singleton(x));
|
|
* append_buffer(buffer, j, 1, M);
|
|
* take_plus_one(j, elements);
|
|
* j++;
|
|
* }
|
|
* drop_drop(1, j, elements);
|
|
* nth_drop2(elements, i);
|
|
* }
|
|
* }
|
|
*
|
|
* lemma void join_element(char *buffer, size_t N, size_t M, size_t i)
|
|
* requires
|
|
* 0 <= i &*& i < N &*&
|
|
* buffer(buffer, i, M, ?prefix) &*&
|
|
* chars(buffer + i * M, M, ?element) &*&
|
|
* buffer(buffer + (i + 1) * M, (N-1-i), M, ?suffix);
|
|
* ensures buffer(buffer, N, M, append(prefix, cons(element, suffix)));
|
|
* {
|
|
* if (i == 0) {
|
|
* open buffer(buffer, i, M, prefix);
|
|
* assert prefix == nil;
|
|
* close buffer(buffer, N, M, cons(element, suffix));
|
|
* } else {
|
|
* close buffer(buffer + i * M, N-i, M, cons(element, suffix));
|
|
* append_buffer(buffer, i, N-i, M);
|
|
* }
|
|
* }
|
|
*
|
|
* predicate list(List_t *l;) =
|
|
* l->uxNumberOfItems |-> _;
|
|
*
|
|
* predicate queuelists(QueueHandle_t q;) =
|
|
* list(&q->xTasksWaitingToSend) &*&
|
|
* list(&q->xTasksWaitingToReceive);
|
|
* @*/
|
|
|
|
/* Because prvCopyDataFromQueue does *not* decrement uxMessagesWaiting (K) the
|
|
* queue predicate above does not hold as a postcondition. If the caller
|
|
* subsequently decrements K then the queue predicate can be reinstated. */
|
|
|
|
/*@
|
|
* predicate queue_after_prvCopyDataFromQueue(QueueHandle_t q, int8_t *Storage, size_t N, size_t M, size_t W, size_t R, size_t K, bool is_locked; list<list<char> >abs) =
|
|
* QUEUE_SHAPE(q, Storage, N, M, K) &*&
|
|
* 0 < N &*&
|
|
* 0 < M &*&
|
|
* 0 <= W &*& W < N &*&
|
|
* 0 <= R &*& R < N &*&
|
|
* 0 <= K &*& K <= N &*&
|
|
* W == (R + K) % N &*& //< Differs from queue predicate
|
|
* (-1) <= rxLock &*&
|
|
* (-1) <= txLock &*&
|
|
* (is_locked ? 0 <= rxLock : (-1) == rxLock) &*&
|
|
* (is_locked ? 0 <= txLock : (-1) == txLock) &*&
|
|
* WPtr == Storage + (W*M) &*&
|
|
* RPtr == Storage + (R*M) &*&
|
|
* End == Storage + (N*M) &*&
|
|
* buffer(Storage, N, M, ?contents) &*&
|
|
* length(contents) == N &*&
|
|
* abs == take(K, rotate_left(R, contents)) &*& //< Differs from queue predicate
|
|
* malloc_block(Storage, N*M) &*&
|
|
* true
|
|
* ;
|
|
* @*/
|
|
|
|
/* Can't be called `mutex` as this clashes with VeriFast's predicate */
|
|
|
|
/*@
|
|
* predicate freertos_mutex(QueueHandle_t q, int8_t *Storage, size_t N, size_t K;) =
|
|
* QUEUE_SHAPE(q, Storage, N, 0, K) &*&
|
|
* queuelists(q) &*&
|
|
* 0 < N &*&
|
|
* 0 <= K &*& K <= N &*&
|
|
* (-1) <= rxLock &*&
|
|
* (-1) <= txLock &*&
|
|
* WPtr == Storage &*&
|
|
* RPtr == Storage &*&
|
|
* End == Storage &*&
|
|
* malloc_block(Storage, 0) &*&
|
|
* chars(Storage, 0, _) &*&
|
|
* true
|
|
* ;
|
|
* @*/
|
|
|
|
/* A queuehandle can be shared between tasks and ISRs. Acquiring the ghost
|
|
* `irqMask` gives access to the core queue resources. The permissions granted
|
|
* after masking interrupts depends on the caller:
|
|
* - A task has access to the queue and the queuelists
|
|
* - An ISR has access to the queue and, if the queue is unlocked, the queuelists */
|
|
|
|
/*@
|
|
* predicate queuehandle(QueueHandle_t q, size_t N, size_t M, bool is_isr;) =
|
|
* q->irqMask |-> ?m &*& mutex(m, irqs_masked_invariant(q, N, M, is_isr));
|
|
*
|
|
* predicate_ctor irqs_masked_invariant(QueueHandle_t queue, size_t N, size_t M, bool is_isr)() =
|
|
* queue(queue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
|
|
* (is_isr && is_locked ? true : queuelists(queue));
|
|
* @*/
|
|
|
|
/* A queuesuspend can be shared between tasks. Acquiring the ghost `schedulerSuspend` gives access to the `locked` mutex. */
|
|
|
|
/*@
|
|
* predicate_ctor scheduler_suspended_invariant(QueueHandle_t queue)() =
|
|
* queue->locked |-> ?m &*&
|
|
* mutex(m, queue_locked_invariant(queue));
|
|
*
|
|
* predicate queuesuspend(QueueHandle_t q;) =
|
|
* q->schedulerSuspend |-> ?m &*&
|
|
* mutex(m, scheduler_suspended_invariant(q));
|
|
* @*/
|
|
|
|
/* A queuelock is exclusively acquired by a task. Acquiring the ghost `queuelock` gives access to the queue list resources. */
|
|
|
|
/*@
|
|
* predicate queuelock(QueueHandle_t q;) =
|
|
* q->locked |-> ?m &*&
|
|
* mutex(m, queue_locked_invariant(q));
|
|
*
|
|
* predicate_ctor queue_locked_invariant(QueueHandle_t queue)() =
|
|
* queuelists(queue);
|
|
* @*/
|
|
|
|
BaseType_t vListInitialise( List_t * list );
|
|
/*@requires list(list);@*/
|
|
/*@ensures list(list);@*/
|
|
|
|
BaseType_t listLIST_IS_EMPTY( List_t * list );
|
|
/*@requires list->uxNumberOfItems |-> ?len;@*/
|
|
/*@ensures list->uxNumberOfItems |-> len &*& result == (len == 0 ? pdTRUE : pdFALSE);@*/
|
|
|
|
typedef struct xTIME_OUT
|
|
{
|
|
BaseType_t xOverflowCount;
|
|
TickType_t xTimeOnEntering;
|
|
} TimeOut_t;
|
|
|
|
/*@
|
|
* predicate xTIME_OUT(struct xTIME_OUT *to;) =
|
|
* to->xOverflowCount |-> _ &*&
|
|
* to->xTimeOnEntering |-> _ &*&
|
|
* struct_xTIME_OUT_padding(to);
|
|
* @*/
|
|
|
|
void vTaskInternalSetTimeOutState( TimeOut_t * x );
|
|
/*@requires xTIME_OUT(x);@*/
|
|
/*@ensures xTIME_OUT(x);@*/
|
|
|
|
BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut,
|
|
TickType_t * const pxTicksToWait );
|
|
/*@requires xTIME_OUT(pxTimeOut) &*& u_integer(pxTicksToWait, _);@*/
|
|
/*@ensures xTIME_OUT(pxTimeOut) &*& u_integer(pxTicksToWait, _);@*/
|
|
|
|
BaseType_t xTaskRemoveFromEventList( List_t * list );
|
|
/*@requires list(list);@*/
|
|
/*@ensures list(list);@*/
|
|
|
|
void vTaskPlaceOnEventList( List_t * const pxEventList,
|
|
const TickType_t xTicksToWait );
|
|
/*@requires list(pxEventList);@*/
|
|
/*@ensures list(pxEventList);@*/
|
|
|
|
void vTaskMissedYield();
|
|
/*@requires true;@*/
|
|
/*@ensures true;@*/
|
|
|
|
void vTaskSuspendAll();
|
|
|
|
/*@requires exists<QueueHandle_t>(?xQueue) &*&
|
|
* [1/2]xQueue->schedulerSuspend |-> ?m &*&
|
|
* [1/2]mutex(m, scheduler_suspended_invariant(xQueue));@*/
|
|
|
|
/*@ensures [1/2]xQueue->schedulerSuspend |-> m &*&
|
|
* mutex_held(m, scheduler_suspended_invariant(xQueue), currentThread, 1/2) &*&
|
|
* xQueue->locked |-> ?m2 &*&
|
|
* mutex(m2, queue_locked_invariant(xQueue));@*/
|
|
|
|
BaseType_t xTaskResumeAll( void );
|
|
|
|
/*@requires exists<QueueHandle_t>(?xQueue) &*&
|
|
* [1/2]xQueue->schedulerSuspend |-> ?m &*&
|
|
* mutex_held(m, scheduler_suspended_invariant(xQueue), currentThread, 1/2) &*&
|
|
* xQueue->locked |-> ?m2 &*&
|
|
* mutex(m2, queue_locked_invariant(xQueue));@*/
|
|
|
|
/*@ensures [1/2]xQueue->schedulerSuspend |-> m &*&
|
|
* [1/2]mutex(m, scheduler_suspended_invariant(xQueue));@*/
|
|
|
|
void prvLockQueue( QueueHandle_t xQueue );
|
|
|
|
/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*&
|
|
* [1/2]queuelock(xQueue); @*/
|
|
|
|
/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*&
|
|
* [1/2]xQueue->locked |-> ?m &*&
|
|
* mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*&
|
|
* queue_locked_invariant(xQueue)();@*/
|
|
|
|
void prvUnlockQueue( QueueHandle_t xQueue );
|
|
|
|
/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*&
|
|
* [1/2]xQueue->locked |-> ?m &*&
|
|
* mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*&
|
|
* queue_locked_invariant(xQueue)();@*/
|
|
|
|
/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*&
|
|
* [1/2]queuelock(xQueue);@*/
|
|
|
|
void setInterruptMask( QueueHandle_t xQueue )
|
|
/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/
|
|
|
|
/*@ensures [1/2]xQueue->irqMask |-> ?m &*&
|
|
* mutex_held(m, irqs_masked_invariant(xQueue, N, M, is_isr), currentThread, 1/2) &*&
|
|
* queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
|
|
* queuelists(xQueue);@*/
|
|
{
|
|
/*@open queuehandle(xQueue, N, M, is_isr);@*/
|
|
mutex_acquire( xQueue->irqMask );
|
|
/*@open irqs_masked_invariant(xQueue, N, M, is_isr)();@*/
|
|
}
|
|
|
|
void clearInterruptMask( QueueHandle_t xQueue )
|
|
|
|
/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
|
|
* [1/2]xQueue->irqMask |-> ?m &*&
|
|
* mutex_held(m, irqs_masked_invariant(xQueue, N, M, false), currentThread, 1/2) &*&
|
|
* queuelists(xQueue);@*/
|
|
/*@ensures [1/2]queuehandle(xQueue, N, M, false);@*/
|
|
{
|
|
/*@close irqs_masked_invariant(xQueue, N, M, false)();@*/
|
|
mutex_release( xQueue->irqMask );
|
|
/*@close [1/2]queuehandle(xQueue, N, M, false);@*/
|
|
}
|
|
|
|
#define taskENTER_CRITICAL() setInterruptMask( xQueue )
|
|
#define taskEXIT_CRITICAL() clearInterruptMask( xQueue )
|
|
#define portYIELD_WITHIN_API()
|
|
#define queueYIELD_IF_USING_PREEMPTION()
|
|
|
|
UBaseType_t setInterruptMaskFromISR( QueueHandle_t xQueue )
|
|
/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == true;@*/
|
|
|
|
/*@ensures [1/2]xQueue->irqMask |-> ?m &*&
|
|
* mutex_held(m, irqs_masked_invariant(xQueue, N, M, is_isr), currentThread, 1/2) &*&
|
|
* queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
|
|
* (is_locked ? true : queuelists(xQueue));@*/
|
|
{
|
|
/*@open queuehandle(xQueue, N, M, is_isr);@*/
|
|
mutex_acquire( xQueue->irqMask );
|
|
/*@open irqs_masked_invariant(xQueue, N, M, is_isr)();@*/
|
|
return 0;
|
|
}
|
|
|
|
void clearInterruptMaskFromISR( QueueHandle_t xQueue,
|
|
UBaseType_t uxSavedInterruptStatus )
|
|
|
|
/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
|
|
* [1/2]xQueue->irqMask |-> ?m &*&
|
|
* mutex_held(m, irqs_masked_invariant(xQueue, N, M, true), currentThread, 1/2) &*&
|
|
* (is_locked ? true : queuelists(xQueue));@*/
|
|
/*@ensures [1/2]queuehandle(xQueue, N, M, true);@*/
|
|
{
|
|
/*@close irqs_masked_invariant(xQueue, N, M, true)();@*/
|
|
mutex_release( xQueue->irqMask );
|
|
/*@close [1/2]queuehandle(xQueue, N, M, true);@*/
|
|
}
|
|
|
|
#define portSET_INTERRUPT_MASK_FROM_ISR() setInterruptMaskFromISR( xQueue )
|
|
#define portCLEAR_INTERRUPT_MASK_FROM_ISR( uxSavedInterruptStatus ) clearInterruptMaskFromISR( xQueue, uxSavedInterruptStatus )
|
|
|
|
#endif /* QUEUE_H */
|