Library sem_common
Require Import absop_rules.
Require Import include.
Require Import memory.
Require Import memdata.
Require Import assertion.
Require Import absop.
Require Import simulation.
Require Import language.
Require Import opsem.
Require Import os_program.
Require Import os_spec.
Require Import inferules.
Require Import os_code_notations.
Require Import os_code_defs.
Require Import os_ucos_h.
Require Import os_time.
Require Import baseTac.
Require Import auxdef.
Require Import seplog_lemmas.
Require Import seplog_tactics.
Require Import derivedrules.
Require Import hoare_conseq.
Require Import symbolic_execution.
Require Import hoare_assign.
Require Import hoare_lemmas.
Require Import BaseAsrtDef.
Require Import inv_prop.
Require Import InternalFunSpec.
Require Import IntLib.
Require Import List.
Require Import can_change_aop_proof.
Require Import cancel_absdata.
Require Import sep_pure.
Require Import type_val_match.
Require Import hoare_tactics.
Require Export mathlib.
Require Export ucert.
Require Export sem_absop_rule.
Require Export sem_lab.
Open Scope code_scope.
Lemma sem_H_get_none:
forall els eid,
EcbMod.get els eid = None ->
~(exists n wls, EcbMod.get els eid = Some (abssem n, wls)).
Lemma eventsearch_after_get_H:
forall p ectrl1 a b ectrl2 msgqls1 msgq msgqls2 mqls tcbls qid mqls1 mqls´ mq mqls2,
length ectrl1 = length msgqls1 ->
ECBList_P p Vnull
(ectrl1 ++ ((a,b)::nil) ++ ectrl2)
(msgqls1 ++ (msgq::nil) ++ msgqls2)
mqls tcbls ->
ECBList_P p (Vptr qid) ectrl1 msgqls1 mqls1 tcbls ->
EcbMod.join mqls1 mqls´ mqls ->
EcbMod.joinsig qid mq mqls2 mqls´ ->
EcbMod.get mqls qid = Some mq.
Lemma semacc_eventtype_neq_sem:
forall s P p ectrl1 a b ectrl2 msgqls1 msgq msgqls2 mqls tcbls qid mqls1 mqls´ mq mqls2 t,
s |= AEventData a msgq ** P ->
RLH_ECBData_P msgq mq ->
length ectrl1 = length msgqls1 ->
ECBList_P p Vnull
(ectrl1 ++ ((a,b)::nil) ++ ectrl2)
(msgqls1 ++ (msgq::nil) ++ msgqls2)
mqls tcbls ->
ECBList_P p (Vptr qid) ectrl1 msgqls1 mqls1 tcbls ->
EcbMod.join mqls1 mqls´ mqls ->
EcbMod.joinsig qid mq mqls2 mqls´ ->
V_OSEventType a = Some (Vint32 t) ->
Int.eq t ($ OS_EVENT_TYPE_SEM) = false ->
s |= AEventData a msgq **
[| ~ exists n wls, EcbMod.get mqls qid = Some (abssem n, wls)|] ** P.
Lemma semacc_triangle_sem:
forall s P a msgq mq n,
s |= AEventData a msgq ** P ->
RLH_ECBData_P msgq mq ->
V_OSEventType a = Some (V$OS_EVENT_TYPE_SEM) ->
V_OSEventCnt a = Some (Vint32 n) ->
s |= AEventData a msgq **
[| exists wls, msgq = DSem n /\ mq = (abssem n, wls) |] ** P.
Lemma semacc_ltu_trans:
forall x y,
Int.ltu Int.zero x = true ->
Int.ltu x y = true ->
Int.ltu (Int.sub x Int.one) y = true.
Lemma semacc_compose_EcbList_P:
forall p qid a b tcbls i n x2 x3 vn msgq mq ectrl1 msgqls1 mqls1 ectrl2 msgqls2 mqls2 mqls´ mqls,
R_ECB_ETbl_P qid (a,b) tcbls ->
a = (V$OS_EVENT_TYPE_SEM :: Vint32 i :: Vint32 n :: x2 :: x3 :: vn :: nil) ->
RLH_ECBData_P msgq mq ->
ECBList_P p (Vptr qid) ectrl1 msgqls1 mqls1 tcbls ->
ECBList_P vn Vnull ectrl2 msgqls2 mqls2 tcbls ->
EcbMod.joinsig qid mq mqls2 mqls´ ->
EcbMod.join mqls1 mqls´ mqls ->
ECBList_P p Vnull (ectrl1 ++ ((a,b)::nil) ++ ectrl2)
(msgqls1 ++ (msgq::nil) ++ msgqls2)
mqls tcbls.
Lemma sem_eventtype_neq_sem:
forall s P a msgq mq t,
s |= AEventData a msgq ** P ->
RLH_ECBData_P msgq mq ->
V_OSEventType a = Some (Vint32 t) ->
Int.eq t ($ OS_EVENT_TYPE_SEM) = false ->
s |= AEventData a msgq **
[| (~ exists n wls, mq = (abssem n, wls)) |] ** P.
Lemma Mutex_owner_set: forall x y z t, (~exists aa bb cc, t = (absmutexsem aa bb, cc))-> RH_TCBList_ECBList_MUTEX_OWNER x y -> RH_TCBList_ECBList_MUTEX_OWNER (EcbMod.set x z t) y.
Lemma Mutex_owner_hold_for_set_tcb: forall x y pcur a b c, RH_TCBList_ECBList_MUTEX_OWNER x y -> RH_TCBList_ECBList_MUTEX_OWNER x (TcbMod.set y pcur (a, b, c)).
Definition semcre_RL_Tbl_init_prop:
RL_Tbl_Grp_P INIT_EVENT_TBL (Vint32 Int.zero).
Lemma semcre_ECBList_P:
forall mqls tcbls ct sid ecbls p l i v1,
RH_TCBList_ECBList_P mqls tcbls ct ->
EcbMod.get mqls sid = None ->
ECBList_P p Vnull l ecbls mqls tcbls ->
ECBList_P (Vptr sid) Vnull
((V$OS_EVENT_TYPE_SEM
:: Vint32 Int.zero :: Vint32 i :: Vnull :: v1 :: p :: nil,
INIT_EVENT_TBL) :: l) (DSem i :: ecbls)
(EcbMod.set mqls sid (abssem i, nil))
tcbls.
Lemma semcre_RH_TCBList_ECBList_P:
forall v´37 x i v´38 v´40,
EcbMod.get v´37 x = None ->
RH_TCBList_ECBList_P v´37 v´38 v´40 ->
RH_TCBList_ECBList_P
(EcbMod.set v´37 x (abssem i, nil))
v´38 v´40.
Lemma semcre_ecblist_star_not_inh :
forall v´28 v´24 eid v´27 v´37 v´38 s vl P,
ECBList_P v´24 Vnull v´28 v´27 v´37 v´38 ->
s |= Astruct eid OS_EVENT vl **
evsllseg v´24 Vnull v´28 v´27 ** P ->
EcbMod.get v´37 eid = None.
Lemma sempend_ltu_ass1:
forall x, Int.ltu x x = false.
Lemma sempend_ltu_ass2:
Int.ltu Int.zero Int.one = true.
Lemma join_prop2_my´:
forall m1 m2 m12 b1 prio st msg m3 ma3 m4 msg´,
TcbMod.join m1 m2 m12 ->
TcbJoin (b1, Int.zero) (prio, st, msg) m3 ma3 ->
TcbMod.join m4 ma3 m2 ->
TcbMod.join m1
(TcbMod.set m2 (b1, Int.zero) (prio, rdy, msg´))
(TcbMod.set m12 (b1, Int.zero) (prio, rdy, msg´)).
Lemma statsem_and_not_statsem_eq_rdy : Int.eq ($ OS_STAT_SEM&Int.not ($ OS_STAT_SEM)) ($ OS_STAT_RDY) = true.
Require Import include.
Require Import memory.
Require Import memdata.
Require Import assertion.
Require Import absop.
Require Import simulation.
Require Import language.
Require Import opsem.
Require Import os_program.
Require Import os_spec.
Require Import inferules.
Require Import os_code_notations.
Require Import os_code_defs.
Require Import os_ucos_h.
Require Import os_time.
Require Import baseTac.
Require Import auxdef.
Require Import seplog_lemmas.
Require Import seplog_tactics.
Require Import derivedrules.
Require Import hoare_conseq.
Require Import symbolic_execution.
Require Import hoare_assign.
Require Import hoare_lemmas.
Require Import BaseAsrtDef.
Require Import inv_prop.
Require Import InternalFunSpec.
Require Import IntLib.
Require Import List.
Require Import can_change_aop_proof.
Require Import cancel_absdata.
Require Import sep_pure.
Require Import type_val_match.
Require Import hoare_tactics.
Require Export mathlib.
Require Export ucert.
Require Export sem_absop_rule.
Require Export sem_lab.
Open Scope code_scope.
Lemma sem_H_get_none:
forall els eid,
EcbMod.get els eid = None ->
~(exists n wls, EcbMod.get els eid = Some (abssem n, wls)).
Lemma eventsearch_after_get_H:
forall p ectrl1 a b ectrl2 msgqls1 msgq msgqls2 mqls tcbls qid mqls1 mqls´ mq mqls2,
length ectrl1 = length msgqls1 ->
ECBList_P p Vnull
(ectrl1 ++ ((a,b)::nil) ++ ectrl2)
(msgqls1 ++ (msgq::nil) ++ msgqls2)
mqls tcbls ->
ECBList_P p (Vptr qid) ectrl1 msgqls1 mqls1 tcbls ->
EcbMod.join mqls1 mqls´ mqls ->
EcbMod.joinsig qid mq mqls2 mqls´ ->
EcbMod.get mqls qid = Some mq.
Lemma semacc_eventtype_neq_sem:
forall s P p ectrl1 a b ectrl2 msgqls1 msgq msgqls2 mqls tcbls qid mqls1 mqls´ mq mqls2 t,
s |= AEventData a msgq ** P ->
RLH_ECBData_P msgq mq ->
length ectrl1 = length msgqls1 ->
ECBList_P p Vnull
(ectrl1 ++ ((a,b)::nil) ++ ectrl2)
(msgqls1 ++ (msgq::nil) ++ msgqls2)
mqls tcbls ->
ECBList_P p (Vptr qid) ectrl1 msgqls1 mqls1 tcbls ->
EcbMod.join mqls1 mqls´ mqls ->
EcbMod.joinsig qid mq mqls2 mqls´ ->
V_OSEventType a = Some (Vint32 t) ->
Int.eq t ($ OS_EVENT_TYPE_SEM) = false ->
s |= AEventData a msgq **
[| ~ exists n wls, EcbMod.get mqls qid = Some (abssem n, wls)|] ** P.
Lemma semacc_triangle_sem:
forall s P a msgq mq n,
s |= AEventData a msgq ** P ->
RLH_ECBData_P msgq mq ->
V_OSEventType a = Some (V$OS_EVENT_TYPE_SEM) ->
V_OSEventCnt a = Some (Vint32 n) ->
s |= AEventData a msgq **
[| exists wls, msgq = DSem n /\ mq = (abssem n, wls) |] ** P.
Lemma semacc_ltu_trans:
forall x y,
Int.ltu Int.zero x = true ->
Int.ltu x y = true ->
Int.ltu (Int.sub x Int.one) y = true.
Lemma semacc_compose_EcbList_P:
forall p qid a b tcbls i n x2 x3 vn msgq mq ectrl1 msgqls1 mqls1 ectrl2 msgqls2 mqls2 mqls´ mqls,
R_ECB_ETbl_P qid (a,b) tcbls ->
a = (V$OS_EVENT_TYPE_SEM :: Vint32 i :: Vint32 n :: x2 :: x3 :: vn :: nil) ->
RLH_ECBData_P msgq mq ->
ECBList_P p (Vptr qid) ectrl1 msgqls1 mqls1 tcbls ->
ECBList_P vn Vnull ectrl2 msgqls2 mqls2 tcbls ->
EcbMod.joinsig qid mq mqls2 mqls´ ->
EcbMod.join mqls1 mqls´ mqls ->
ECBList_P p Vnull (ectrl1 ++ ((a,b)::nil) ++ ectrl2)
(msgqls1 ++ (msgq::nil) ++ msgqls2)
mqls tcbls.
Lemma sem_eventtype_neq_sem:
forall s P a msgq mq t,
s |= AEventData a msgq ** P ->
RLH_ECBData_P msgq mq ->
V_OSEventType a = Some (Vint32 t) ->
Int.eq t ($ OS_EVENT_TYPE_SEM) = false ->
s |= AEventData a msgq **
[| (~ exists n wls, mq = (abssem n, wls)) |] ** P.
Lemma Mutex_owner_set: forall x y z t, (~exists aa bb cc, t = (absmutexsem aa bb, cc))-> RH_TCBList_ECBList_MUTEX_OWNER x y -> RH_TCBList_ECBList_MUTEX_OWNER (EcbMod.set x z t) y.
Lemma Mutex_owner_hold_for_set_tcb: forall x y pcur a b c, RH_TCBList_ECBList_MUTEX_OWNER x y -> RH_TCBList_ECBList_MUTEX_OWNER x (TcbMod.set y pcur (a, b, c)).
Definition semcre_RL_Tbl_init_prop:
RL_Tbl_Grp_P INIT_EVENT_TBL (Vint32 Int.zero).
Lemma semcre_ECBList_P:
forall mqls tcbls ct sid ecbls p l i v1,
RH_TCBList_ECBList_P mqls tcbls ct ->
EcbMod.get mqls sid = None ->
ECBList_P p Vnull l ecbls mqls tcbls ->
ECBList_P (Vptr sid) Vnull
((V$OS_EVENT_TYPE_SEM
:: Vint32 Int.zero :: Vint32 i :: Vnull :: v1 :: p :: nil,
INIT_EVENT_TBL) :: l) (DSem i :: ecbls)
(EcbMod.set mqls sid (abssem i, nil))
tcbls.
Lemma semcre_RH_TCBList_ECBList_P:
forall v´37 x i v´38 v´40,
EcbMod.get v´37 x = None ->
RH_TCBList_ECBList_P v´37 v´38 v´40 ->
RH_TCBList_ECBList_P
(EcbMod.set v´37 x (abssem i, nil))
v´38 v´40.
Lemma semcre_ecblist_star_not_inh :
forall v´28 v´24 eid v´27 v´37 v´38 s vl P,
ECBList_P v´24 Vnull v´28 v´27 v´37 v´38 ->
s |= Astruct eid OS_EVENT vl **
evsllseg v´24 Vnull v´28 v´27 ** P ->
EcbMod.get v´37 eid = None.
Lemma sempend_ltu_ass1:
forall x, Int.ltu x x = false.
Lemma sempend_ltu_ass2:
Int.ltu Int.zero Int.one = true.
Lemma join_prop2_my´:
forall m1 m2 m12 b1 prio st msg m3 ma3 m4 msg´,
TcbMod.join m1 m2 m12 ->
TcbJoin (b1, Int.zero) (prio, st, msg) m3 ma3 ->
TcbMod.join m4 ma3 m2 ->
TcbMod.join m1
(TcbMod.set m2 (b1, Int.zero) (prio, rdy, msg´))
(TcbMod.set m12 (b1, Int.zero) (prio, rdy, msg´)).
Lemma statsem_and_not_statsem_eq_rdy : Int.eq ($ OS_STAT_SEM&Int.not ($ OS_STAT_SEM)) ($ OS_STAT_RDY) = true.