len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-12 06:35:19 -05:00
Code Issues Projects Releases Packages Wiki Activity

Introduced initial formulation of predicate to capture shared ready lists.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-18 09:22:31 -05:00
parent 6dcaef48d6
commit c9e61fce49
3 changed files with 80 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
tasks.c
View file

@ -982,6 +982,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
}
#endif
//@ open taskISRLockInv();
//@ open readyLists_p();
//@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority);
if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE )
{

42
verification/verifast/proof/nathan/list_predicates.h
View file

@ -30,6 +30,48 @@ predicate xList_gen(struct xLIST *l) =
l->uxNumberOfItems |-> _ &*&
l->pxIndex |-> _;
predicate List_p(List_t* l);
@*/
/* Ferreira et al. (STTT'14) doubly-linked list segment (DLS). */
/* @
predicate DLS(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells,
list<TickType_t > vals,
struct xLIST *pxContainer) =
n == m
? cells == cons(n, nil) &*&
vals == cons(?v, nil) &*&
xLIST_ITEM(n, v, mnext, nprev, pxContainer)
: cells == cons(n, ?cells0) &*&
vals == cons(?v, ?vals0) &*&
xLIST_ITEM(n, v, ?o, nprev, pxContainer) &*& DLS(o, n, mnext, m, cells0, vals0, pxContainer);
@*/
/* @
predicate xLIST(
struct xLIST *l,
int uxNumberOfItems,
struct xLIST_ITEM *pxIndex,
struct xLIST_ITEM *xListEnd,
list<struct xLIST_ITEM *>cells,
list<TickType_t >vals) =
l->uxNumberOfItems |-> uxNumberOfItems &*&
l->pxIndex |-> pxIndex &*&
mem(pxIndex, cells) == true &*&
xListEnd == &(l->xListEnd) &*&
xListEnd == head(cells) &*&
portMAX_DELAY == head(vals) &*&
struct_xLIST_ITEM_padding(&l->xListEnd) &*&
length(cells) == length(vals) &*&
uxNumberOfItems + 1 == length(cells) &*&
DLS(xListEnd, ?endprev, xListEnd, endprev, cells, vals, l);
@*/
#endif /* LIST_PREDICATES_H */

36
verification/verifast/proof/ready_list_predicates.h
View file

@ -1,8 +1,42 @@
#ifndef READY_LIST_PREDICATES_H
#define READY_LIST_PREDICATES_H
/*@
predicate readyLists_p();
// TODO: Replace List_p by Aaloks list predicate
predicate List_array_p(List_t* array, int size) =
pointer_within_limits(array) == true &*&
size > 0 &*&
List_p(array) &*&
size > 1
? List_array_p(array + 1, size - 1)
: true;
// For testing purposes only!
// TODO: Replace by Aaloks list predicate
predicate List_p(List_t* l);
@*/
/*@
predicate readyLists_p() =
List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES);
@*/
/*@
lemma void List_array_p_index_within_limits(List_t* array, int index)
requires List_array_p(array, ?size) &*&
0 <= index &*& index < size;
ensures List_array_p(array, size) &*&
pointer_within_limits(&array[index]) == true;
{
open List_array_p(array, size);
if( index > 0) {
List_array_p_index_within_limits(&array[1], index-1);
}
close List_array_p(array, size);
}
@*/
#endif /* READY_LIST_PREDICATES_H */