Library OSMutexCreateProof
OS_EVENT∗ ·OSMutexCreate·(⌞prio @ Int8u⌟)··{
⌞pevent @ OS_EVENT∗⌟;
1 If (prio′ ≥ ′OS_LOWEST_PRIO)
{
12 RETURN 〈OS_EVENT ∗〉 NULL
};ₛ
13 ENTER_CRITICAL;ₛ
14 If (OSTCBPrioTbl′prio′ !=ₑ NULL)
{
15 EXIT_CRITICAL;ₛ
16 RETURN 〈OS_EVENT ∗〉 NULL
};ₛ
17 pevent′ =ₑ OSEventFreeList′;ₛ
18 If (OSEventFreeList′ !=ₑ NULL)
{
19 OSEventFreeList′ =ₑ 〈OS_EVENT∗〉 OSEventFreeList′→OSEventListPtr
};ₛ
20 IF (pevent′ !=ₑ NULL)
{
21 OS_EventWaitListInit(pevent′);ₛ
22 pevent′→OSEventType =ₑ ′OS_EVENT_TYPE_MUTEX;ₛ
23 pevent′→OSEventCnt =ₑ ((〈Int16u〉prio′) ≪ ′8) |ₑ ′OS_MUTEX_AVAILABLE;ₛ
24 pevent′→OSEventPtr =ₑ NULL;ₛ
25 pevent ′ → OSEventListPtr =ₑ OSEventList ′;ₛ
26 OSTCBPrioTbl′prio′ =ₑ 〈OS_TCB ∗〉 PlaceHolder;ₛ
27 OSEventList′ =ₑ pevent′;ₛ
28 EXIT_CRITICAL;ₛ
29 RETURN pevent′
}
ELSE
{
30 EXIT_CRITICAL;ₛ
31 RETURN 〈OS_EVENT ∗〉 NULL
}
}·.
Require Import ucert.
Require Import lab.
Require Import mathlib.
Require Import OSMutex_common.
Open Scope code_scope.
Theorem OSMutexCreateRight:
forall vl p r,
Some p = BuildPreA´ os_api OSMutexCreate mutexcreapi vl ->
Some r = BuildRetA´ os_api OSMutexCreate mutexcreapi vl ->
exists t d1 d2 s,
os_api OSMutexCreate = Some (t, d1, d2, s) /\ {| OSQ_spec, GetHPrio, I, r, Afalse |} |- {{ p }} s {{ Afalse }}.
Require Import OSQCreatePure.
Require Import lab.
Require Import mathlib.
Require Import OSMutex_common.
Open Scope code_scope.
Theorem OSMutexCreateRight:
forall vl p r,
Some p = BuildPreA´ os_api OSMutexCreate mutexcreapi vl ->
Some r = BuildRetA´ os_api OSMutexCreate mutexcreapi vl ->
exists t d1 d2 s,
os_api OSMutexCreate = Some (t, d1, d2, s) /\ {| OSQ_spec, GetHPrio, I, r, Afalse |} |- {{ p }} s {{ Afalse }}.
Require Import OSQCreatePure.