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

Wrote contracts for lock release operations.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-16 14:18:03 -05:00
parent 54523ecdce
commit 4eb2fa573e
3 changed files with 25 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
tasks.c
View file

@ -4152,7 +4152,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
portGET_TASK_LOCK(); /* Must always acquire the task lock first */ portGET_TASK_LOCK(); /* Must always acquire the task lock first */
portGET_ISR_LOCK(); portGET_ISR_LOCK();
//@ get_taskISRLockInv(); //@ produce_taskISRLockInv();
{ {
/* vTaskSwitchContext() must never be called from within a critical section. /* vTaskSwitchContext() must never be called from within a critical section.
* This is not necessarily true for vanilla FreeRTOS, but it is for this SMP port. */ * This is not necessarily true for vanilla FreeRTOS, but it is for this SMP port. */
@ -4253,6 +4253,8 @@ void vTaskSwitchContext( BaseType_t xCoreID )
#endif /* ( configUSE_NEWLIB_REENTRANT == 1 ) && ( configNEWLIB_REENTRANT_IS_DYNAMIC == 0 ) */ #endif /* ( configUSE_NEWLIB_REENTRANT == 1 ) && ( configNEWLIB_REENTRANT_IS_DYNAMIC == 0 ) */
} }
} }
//@ close taskISRLockInv();
//@ consume_taskISRLockInv();
portRELEASE_ISR_LOCK(); portRELEASE_ISR_LOCK();
portRELEASE_TASK_LOCK(); portRELEASE_TASK_LOCK();
} }

8
verification/verifast/proof/verifast_lock_predicates.h
View file

@ -103,13 +103,19 @@ predicate taskISRLockInv() =
true; true;
lemma void get_taskISRLockInv(); lemma void produce_taskISRLockInv();
requires locked(?heldLocks) &*& requires locked(?heldLocks) &*&
heldLocks == cons(?i, cons(?t, nil)) &*& heldLocks == cons(?i, cons(?t, nil)) &*&
i == pair(?f_isr, isrLockID_f()) &*& i == pair(?f_isr, isrLockID_f()) &*&
t == pair(?f_task, taskLockID_f()); t == pair(?f_task, taskLockID_f());
ensures locked( cons( pair(_, taskISRLockID_f()), heldLocks) ) &*& ensures locked( cons( pair(_, taskISRLockID_f()), heldLocks) ) &*&
taskISRLockInv(); taskISRLockInv();
lemma void consume_taskISRLockInv();
requires locked( cons( pair(_, taskISRLockID_f()), ?otherLocks) ) &*&
taskISRLockInv();
ensures locked(otherLocks);
@*/ @*/

17
verification/verifast/proof/verifast_port_contracts.h
View file

@ -53,12 +53,25 @@ void VF__portRESTORE_INTERRUPTS(uint32_t ulState);
#define portGET_TASK_LOCK VF__portGET_TASK_LOCK #define portGET_TASK_LOCK VF__portGET_TASK_LOCK
void VF__portGET_TASK_LOCK(); void VF__portGET_TASK_LOCK();
//@ requires [?f]taskLock() &*& locked(nil); //@ requires [?f]taskLock() &*& locked(nil);
//@ ensures taskLockInv() &*& locked( cons( pair(f, taskLockID_f), nil) ); //@ ensures taskLockInv() &*& locked( cons( pair(f, taskLockID_f()), nil) );
#undef portRELEASE_TASK_LOCK
#define portRELEASE_TASK_LOCK VF__portRELEASE_TASK_LOCK
void VF__portRELEASE_TASK_LOCK();
//@ requires taskLockInv() &*& locked( cons( pair(?f, taskLockID_f()), nil) );
//@ ensures [f]taskLock() &*& locked(nil);
#undef portGET_ISR_LOCK #undef portGET_ISR_LOCK
#define portGET_ISR_LOCK VF__portGET_ISR_LOCK #define portGET_ISR_LOCK VF__portGET_ISR_LOCK
void VF__portGET_ISR_LOCK(); void VF__portGET_ISR_LOCK();
//@ requires [?f]isrLock() &*& locked(?heldLocks); //@ requires [?f]isrLock() &*& locked(?heldLocks);
//@ ensures isrLockInv() &*& locked( cons( pair(f, isrLockID_f), heldLocks) ); //@ ensures isrLockInv() &*& locked( cons( pair(f, isrLockID_f()), heldLocks) );
#undef portRELEASE_ISR_LOCK
#define portRELEASE_ISR_LOCK VF__portRELEASE_ISR_LOCK
void VF__portRELEASE_ISR_LOCK();
//@ requires isrLockInv() &*& locked( cons( pair(?f, isrLockID_f()), ?heldLocks) );
//@ ensures [f]isrLock() &*& locked(heldLocks);
#endif /* VERIFAST_PORT_CONTRACTS_H */ #endif /* VERIFAST_PORT_CONTRACTS_H */