Library OSMutexPostProof
Int8u ·OSMutexPost·(⌞pevent @ OS_EVENT∗ ⌟)··{
⌞
x @ Int8u;
pip @ Int8u;
prio @ 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 pip′ =ₑ 〈Int8u〉(pevent′→OSEventCnt ≫ ′8);ₛ
12 prio′ =ₑ 〈Int8u〉(pevent′→OSEventCnt &ₑ ′OS_MUTEX_KEEP_LOWER_8);ₛ
13 If (OSTCBCur′ !=ₑ pevent′→OSEventPtr)
{ 14 EXIT_CRITICAL;ₛ
15 RETURN ′OS_ERR_NOT_MUTEX_OWNER
};ₛ
16 If (OSTCBCur′→OSTCBPrio <ₑ pip′)
{
17 EXIT_CRITICAL;ₛ
18 RETURN ′OS_ERR_MUTEX_PRIO
};ₛ
19 If (OSTCBCur′→OSTCBPrio ==ₑ pip′)
{
20 If ( OSTCBPrioTbl′prio′ !=ₑ 〈OS_TCB ∗〉 PlaceHolder)
{
21 EXIT_CRITICAL;ₛ
22 RETURN ′OS_ERR_ORIGINAL_NOT_HOLDER
};ₛ
23 OSRdyTbl′OSTCBCur′→OSTCBY =ₑ OSRdyTbl′OSTCBCur′→OSTCBY &ₑ (∼OSTCBCur′→OSTCBBitX);ₛ
24 If ( OSRdyTbl′OSTCBCur′→OSTCBY ==ₑ ′0)
{
25 OSRdyGrp′ =ₑ OSRdyGrp′ &ₑ ∼OSTCBCur′→OSTCBBitY
};ₛ
26 OSTCBCur′→OSTCBPrio =ₑ prio′;ₛ
27 OSTCBCur′→OSTCBY =ₑ prio′ ≫ ′3;ₛ
28 OSTCBCur′→OSTCBBitY =ₑ OSMapTbl′OSTCBCur′→OSTCBY;ₛ
29 OSTCBCur′→OSTCBX =ₑ prio′ &ₑ ′7;ₛ
30 OSTCBCur′→OSTCBBitX =ₑ OSMapTbl′OSTCBCur′→OSTCBX;ₛ
31 OSRdyGrp′ =ₑ OSRdyGrp′ |ₑ OSTCBCur′→OSTCBBitY;ₛ
32 OSRdyTbl′OSTCBCur′→OSTCBY =ₑ OSRdyTbl′OSTCBCur′→OSTCBY |ₑ OSTCBCur′→OSTCBBitX;ₛ
33 OSTCBPrioTbl′prio′ =ₑ 〈OS_TCB ∗〉 OSTCBCur′;ₛ
34 OSTCBPrioTbl′pip′ =ₑ 〈OS_TCB ∗〉 PlaceHolder
};ₛ
35 If (pevent′→OSEventGrp !=ₑ ′0)
{
36 x′ =ₑ ′OS_STAT_MUTEX;ₛ
37 prio′ =ᶠ OS_EventTaskRdy(·pevent′, pevent′, x′·);ₛ
38 pevent′→OSEventCnt =ₑ pevent′→OSEventCnt &ₑ ′OS_MUTEX_KEEP_UPPER_8;ₛ 39 pevent′→OSEventCnt =ₑ pevent′→OSEventCnt |ₑ prio′;ₛ
40 pevent′→OSEventPtr =ₑ OSTCBPrioTbl′prio′;ₛ 41 EXIT_CRITICAL;ₛ
42 OS_Sched();ₛ
43 RETURN ′OS_NO_ERR
};ₛ
44 pevent′→OSEventCnt =ₑ pevent′→OSEventCnt |ₑ ′OS_MUTEX_AVAILABLE;ₛ 45 pevent′→OSEventPtr =ₑ NULL;ₛ
46 EXIT_CRITICAL;ₛ
47 RETURN ′OS_NO_ERR
Require Import ucert.
Require Import os_code_defs.
Require Import mathlib.
Require Import OSMutex_common.
Require Import lab.
Open Scope code_scope.
Theorem OSMutexPostRight:
forall vl p r,
Some p = BuildPreA´ os_api OSMutexPost mutexpostapi vl ->
Some r = BuildRetA´ os_api OSMutexPost mutexpostapi vl ->
exists t d1 d2 s,
os_api OSMutexPost = Some (t, d1, d2, s) /\ {| OSQ_spec, GetHPrio, I, r, Afalse |} |- {{ p }} s {{ Afalse }}.
Open Scope code_scope.
Hint Resolve OS_EVENT_TBL_SIZE : tlib.
Hint Resolve intlt2nat : tlib.
Hint Resolve int8ule255 : tlib.
Hint Resolve array_type_vallist_match_imp_rule_type_val_match : tlib.
Ltac mew2 := match goal with
| |- (if _ then true else false) = true => rewrite ifE
| |- (_ <=? _ = true) => apply Zle_imp_le_bool
| |- (_ <= _ ) => apply Zle_bool_imp_le
end.
Hint Resolve ifE : tlib.
Hint Resolve Zle_imp_le_bool : tlib.
Hint Resolve OSUnMapVallist_type_vallist_match: tlib.
Ltac copy H1 H2 :=
match type of H1 with
| ?T =>
assert(T) as H2 by (apply H1)
end.
Require Import OSMutexPostPart2.
Require Import os_code_defs.
Require Import mathlib.
Require Import OSMutex_common.
Require Import lab.
Open Scope code_scope.
Theorem OSMutexPostRight:
forall vl p r,
Some p = BuildPreA´ os_api OSMutexPost mutexpostapi vl ->
Some r = BuildRetA´ os_api OSMutexPost mutexpostapi vl ->
exists t d1 d2 s,
os_api OSMutexPost = Some (t, d1, d2, s) /\ {| OSQ_spec, GetHPrio, I, r, Afalse |} |- {{ p }} s {{ Afalse }}.
Open Scope code_scope.
Hint Resolve OS_EVENT_TBL_SIZE : tlib.
Hint Resolve intlt2nat : tlib.
Hint Resolve int8ule255 : tlib.
Hint Resolve array_type_vallist_match_imp_rule_type_val_match : tlib.
Ltac mew2 := match goal with
| |- (if _ then true else false) = true => rewrite ifE
| |- (_ <=? _ = true) => apply Zle_imp_le_bool
| |- (_ <= _ ) => apply Zle_bool_imp_le
end.
Hint Resolve ifE : tlib.
Hint Resolve Zle_imp_le_bool : tlib.
Hint Resolve OSUnMapVallist_type_vallist_match: tlib.
Ltac copy H1 H2 :=
match type of H1 with
| ?T =>
assert(T) as H2 by (apply H1)
end.
Require Import OSMutexPostPart2.