Library OSMutexDelProof
Int8u ·OSMutexDel·(⌞ pevent @ OS_EVENT ∗⌟)··{
⌞
tasks_waiting @ Int8u;
pip @ Int8u;
legal @ Int8u
⌟;
1 If (pevent′ ==ₑ NULL)
{
2 RETURN ′OS_ERR_PEVENT_NULL
};ₛ
3 ENTER_CRITICAL;ₛ
4 legal′ =ᶠ OS_EventSearch(·pevent′·);ₛ
5 If (legal′ ==ₑ ′0)
{
6 EXIT_CRITICAL;ₛ
7 RETURN ′OS_ERR_PEVENT_NO_EX
};ₛ
8 If (pevent′→OSEventType !=ₑ ′OS_EVENT_TYPE_MUTEX)
{
9 EXIT_CRITICAL;ₛ
10 RETURN ′OS_ERR_EVENT_TYPE
};ₛ
11 IF (pevent′→OSEventGrp !=ₑ ′0 ||ₑ ( ( pevent′→OSEventCnt &ₑ ′OS_MUTEX_KEEP_LOWER_8 )!=ₑ ′OS_MUTEX_AVAILABLE))
{
12 tasks_waiting′ =ₑ ′1
}ELSE{
13 tasks_waiting′ =ₑ ′0
};ₛ
14 IF (tasks_waiting′ ==ₑ ′0)
{
15 pip′ =ₑ 〈Int8u〉 (pevent′→OSEventCnt ≫ ′8);ₛ
16 If ( OSTCBPrioTbl′pip′ !=ₑ 〈OS_TCB ∗〉 PlaceHolder)
{
17 EXIT_CRITICAL;ₛ
18 RETURN ′OS_ERR_MUTEXPR_NOT_HOLDER
};ₛ
19 OS_EventRemove(pevent′);ₛ
20 OSTCBPrioTbl′pip′ =ₑ NULL;ₛ
21 pevent′→OSEventType =ₑ ′OS_EVENT_TYPE_UNUSED;ₛ
22 pevent′→OSEventListPtr =ₑ OSEventFreeList′;ₛ
23 pevent′→OSEventCnt =ₑ ′0;ₛ
24 OSEventFreeList′ =ₑ pevent′;ₛ
25 EXIT_CRITICAL;ₛ
26 RETURN ′OS_NO_ERR
}ELSE{
27 EXIT_CRITICAL;ₛ
28 RETURN ′OS_ERR_TASK_WAITING
}
}· .
Require Import ucert.
Require Import lab.
Require Import common.
Require Import OSMutex_common.
Open Scope code_scope.
Theorem OSMutexDelRight:
forall vl p r,
Some p = BuildPreA´ os_api OSMutexDel mutexdelapi vl ->
Some r = BuildRetA´ os_api OSMutexDel mutexdelapi vl ->
exists t d1 d2 s,
os_api OSMutexDel = Some (t, d1, d2, s) /\ {| OSQ_spec, GetHPrio, I, r, Afalse |} |- {{ p }} s {{ Afalse }}.
Require Import mathlib.
Require Import mathlib.
Require Import lab.
Require Import common.
Require Import OSMutex_common.
Open Scope code_scope.
Theorem OSMutexDelRight:
forall vl p r,
Some p = BuildPreA´ os_api OSMutexDel mutexdelapi vl ->
Some r = BuildRetA´ os_api OSMutexDel mutexdelapi vl ->
exists t d1 d2 s,
os_api OSMutexDel = Some (t, d1, d2, s) /\ {| OSQ_spec, GetHPrio, I, r, Afalse |} |- {{ p }} s {{ Afalse }}.
Require Import mathlib.
Require Import mathlib.