Library sem_absop_rule
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 Import absop_rules.
Require Import lab.
Open Scope code_scope.
Lemma semcre_absimp_no_free:
forall P n,
can_change_aop P ->
(Z.leb (Int.unsigned n) Int16.max_unsigned) = true ->
absinfer ( <|| semcre (Vint32 n :: nil) ||> ** P)
( <|| END (Some Vnull) ||> ** P).
Lemma semcre_absimp_succ:
forall P sid n els tcbls tm curtid,
can_change_aop P ->
(Z.leb (Int.unsigned n) Int16.max_unsigned) = true ->
EcbMod.get els sid = None ->
absinfer ( <|| semcre (Vint32 n :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vptr sid)) ||> **
HECBList (EcbMod.set els sid (abssem n, nil:list tid)) **
HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma semacc_absimp_null:
forall sid P,
sid = Vnull ->
can_change_aop P ->
absinfer ( <|| semacc (sid :: nil) ||> ** P)
( <|| END (Some (Vint32 Int.zero)) ||> ** P ).
Lemma semacc_absimp_no_sem:
forall P els tcbls tm curtid sid,
can_change_aop P ->
(~ exists n wls, EcbMod.get els sid = Some (abssem n, wls)) ->
absinfer
( <|| semacc (Vptr sid :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 Int.zero)) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma semacc_absimp_no_source:
forall P els tcbls tm curtid sid wls,
can_change_aop P ->
EcbMod.get els sid = Some (abssem Int.zero, wls) ->
absinfer
( <|| semacc (Vptr sid :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 Int.zero)) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma semacc_absimp_succ:
forall P wls els sid n v1 v3 v4,
can_change_aop P ->
EcbMod.get els sid = Some (abssem n, wls) ->
Int.ltu Int.zero n = true ->
absinfer
( <|| semacc (Vptr sid :: nil) ||> **
HECBList els **
HTCBList v1 **
HTime v3 **
HCurTCB v4 ** P)
( <|| END (Some (Vint32 n)) ||> **
HECBList (EcbMod.set els sid (abssem (Int.sub n Int.one), wls)) **
HTCBList v1 **
HTime v3 **
HCurTCB v4 ** P).
Lemma semdel_absimp_null:
forall sid P,
sid = Vnull ->
can_change_aop P ->
absinfer ( <|| semdel (sid :: nil) ||> ** P)
( <|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL))) ||> ** P ).
Lemma semdel_absimp_no_sem:
forall P els tcbls tm curtid sid,
can_change_aop P ->
(~ exists n wls, EcbMod.get els sid = Some (abssem n, wls)) ->
absinfer
( <|| semdel (Vptr sid :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL))) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma semdel_absimp_type_err:
forall P els tcbls tm curtid sid,
can_change_aop P ->
(~ exists n wls, EcbMod.get els sid = Some (abssem n, wls)) ->
absinfer
( <|| semdel (Vptr sid :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 (Int.repr OS_ERR_EVENT_TYPE))) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma semdel_absimp_task_waiting:
forall P els tcbls tm curtid n sid w wls,
can_change_aop P ->
EcbMod.get els sid = Some (abssem n, w::wls) ->
absinfer
( <|| semdel (Vptr sid :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 (Int.repr OS_ERR_TASK_WAITING))) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma semdel_absimp_succ:
forall P els els´ sid n v1 v3 v4,
can_change_aop P ->
EcbMod.get els sid = Some (abssem n, nil) ->
EcbMod.join els´ (EcbMod.sig sid (abssem n,nil)) els ->
absinfer
( <|| semdel (Vptr sid :: nil) ||> **
HECBList els **
HTCBList v1 **
HTime v3 **
HCurTCB v4 ** P)
( <|| END (Some (Vint32 (Int.repr NO_ERR))) ||> **
HECBList els´ **
HTCBList v1 **
HTime v3 **
HCurTCB v4 ** P).
Lemma absimp_sem_post_null_return:
forall sid P,
sid = Vnull ->
can_change_aop P ->
absinfer ( <|| sem_post (sid :: nil) ||> ** P)
( <|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL))) ||> ** P ).
Lemma absimp_sem_post_p_not_legal_return:
forall P els tcbls tm curtid sid,
can_change_aop P ->
EcbMod.get els sid = None ->
absinfer ( <|| sem_post ((Vptr sid) :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL))) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma absimp_sem_post_wrong_type_return:
forall P els tcbls tm curtid sid,
can_change_aop P ->
(exists d,
EcbMod.get els sid = Some d /\ ~ (exists n wls, d = (abssem n, wls))) ->
absinfer
( <|| sem_post ((Vptr sid) :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL))) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma absimp_sem_post_ovf_err_return:
forall P els tcbls tm curtid sid n wls,
can_change_aop P ->
EcbMod.get els sid = Some (abssem n, wls) ->
Int.ltu n (Int.repr 65535) = false ->
absinfer
( <|| sem_post ((Vptr sid) :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 (Int.repr OS_SEM_OVF))) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma absimp_sem_post_put_sem_return:
forall P els sid n wls tcbls t ct,
can_change_aop P ->
EcbMod.get els sid = Some (abssem n, wls) ->
Int.ltu n (Int.repr 65535) = true ->
absinfer
( <|| sem_post ((Vptr sid) :: nil) ||> **
HECBList els **
HTCBList tcbls **
HTime t ** HCurTCB ct ** P)
( <|| END (Some (Vint32 (Int.repr OS_NO_ERR))) ||> **
HECBList (EcbMod.set els sid (abssem (Int.add n Int.one), wls)) **
HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma absimp_sem_post_ex_wt_succ_return:
forall P els sid tls t t´ n wls p st m ct mid,
can_change_aop P ->
EcbMod.get els sid = Some (abssem n, wls) ->
~ wls = nil ->
GetHWait tls wls t´ ->
TcbMod.get tls t´ = Some (p, st, m) ->
absinfer
( <|| sem_post ((Vptr sid) :: nil) ||> **
HECBList els ** HTCBList tls ** HTime t ** HCurTCB ct ** P )
( <|| isched;;END (Some (Vint32 (Int.repr OS_NO_ERR))) ||> **
HECBList (EcbMod.set els sid (abssem n, (remove_tid t´ wls))) **
HTCBList (TcbMod.set tls t´ (p, rdy, Vptr mid)) **
HTime t ** HCurTCB ct ** P ).
Lemma absinfer_sem_pend_null_return :
forall P x,
can_change_aop P ->
tl_vl_match (Tint16 :: nil) x = true ->
absinfer
(<|| sem_pend (Vnull :: x) ||> ** P)
(<|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL))) ||> ** P).
Lemma absinfer_sem_pend_p_not_legal_return :
forall x a P b v´33 v´16 v´35,
can_change_aop P ->
Int.unsigned b<=65535 ->
EcbMod.get x a = None ->
absinfer
(<|| sem_pend (Vptr a ::Vint32 b:: nil) ||> **
HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 ** P)
(<|| END (Some (V$ OS_ERR_PEVENT_NULL)) ||> **
HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 ** P).
Lemma absinfer_sem_pend_wrong_type_return :
forall x a b P v´33 v´16 v´35,
can_change_aop P ->
Int.unsigned b <= 65535 ->
(exists d,
EcbMod.get x a = Some d /\ ~ (exists x wls, d = (abssem x, wls))) ->
absinfer
(<|| sem_pend (Vptr a :: Vint32 b :: nil) ||> **
HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 ** P)
(<|| END (Some (V$ OS_ERR_PEVENT_NULL)) ||> **
HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 ** P).
Lemma absinfer_sem_pend_from_idle_return :
forall x a b P y t ct,
can_change_aop P ->
Int.unsigned b <= 65535 ->
(exists st msg, TcbMod.get y ct = Some (Int.repr OS_IDLE_PRIO, st, msg)) ->
absinfer
(<|| sem_pend (Vptr a :: Vint32 b :: nil) ||> **
HECBList x **
HTCBList y **
HTime t **
HCurTCB ct ** P)
( <|| END (Some (V$ OS_ERR_PEVENT_NULL)) ||> **
HECBList x **
HTCBList y **
HTime t **
HCurTCB ct ** P).
Lemma absinfer_sem_pend_not_ready_return :
forall P ecbls tcbls t ct st msg v x prio,
Int.unsigned v <= 65535 ->
TcbMod.get tcbls ct = Some (prio, st, msg) ->
~ st = rdy ->
can_change_aop P ->
absinfer
(<|| sem_pend (Vptr x :: Vint32 v :: nil) ||> **
HECBList ecbls **
HTCBList tcbls **
HTime t **
HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL)))||> **
HECBList ecbls **
HTCBList tcbls **
HTime t **
HCurTCB ct ** P).
Lemma absinfer_sem_pend_inst_get_return:
forall P wls els sid n v1 v3 v4 v,
can_change_aop P ->
Int.unsigned v <= 65535 ->
EcbMod.get els sid = Some (abssem n, wls) ->
Int.ltu Int.zero n = true ->
absinfer
( <|| sem_pend (Vptr sid :: Vint32 v :: nil) ||> **
HECBList els **
HTCBList v1 **
HTime v3 **
HCurTCB v4 ** P)
( <|| END (Some (Vint32 (Int.repr OS_NO_ERR))) ||> **
HECBList (EcbMod.set els sid (abssem (Int.sub n Int.one), wls)) **
HTCBList v1 **
HTime v3 **
HCurTCB v4 ** P).
Lemma absinfer_sem_pend_msg_not_null_return :
forall P ecbls tcbls t ct st msg v x prio,
Int.unsigned v <= 65535 ->
TcbMod.get tcbls ct = Some (prio, st, msg) ->
~ msg = Vnull ->
can_change_aop P ->
absinfer
(<|| sem_pend (Vptr x :: Vint32 v :: nil) ||> **
HECBList ecbls **
HTCBList tcbls **
HTime t **
HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL)))||> **
HECBList ecbls **
HTCBList tcbls **
HTime t **
HCurTCB ct ** P).
Lemma absinfer_sem_pend_block:
forall P mqls qid v wl p m t ct tls,
Int.unsigned v <= 65535 ->
can_change_aop P ->
EcbMod.get mqls qid = Some (abssem Int.zero, wl) ->
TcbMod.get tls ct = Some (p,rdy,m) ->
absinfer
( <|| sem_pend (Vptr qid :: Vint32 v :: nil) ||> **
HECBList mqls **
HTCBList tls **
HTime t **
HCurTCB ct ** P)
(<|| isched;;
(sem_pend_timeout_err (|Vptr qid :: Vint32 v :: nil|) ??
sem_pend_block_get_succ (|Vptr qid :: Vint32 v :: nil|)) ||> **
HECBList (EcbMod.set mqls qid (abssem Int.zero ,ct::wl)) **
HTCBList (TcbMod.set tls ct (p,wait (os_stat_sem qid) v, m) ) **
HTime t **
HCurTCB ct ** P).
Lemma absinfer_sem_pend_to_timeout :
forall P mqls qid t ct tls v st prio m,
Int.unsigned v <= 65535 ->
TcbMod.get tls ct = Some (prio, st, m) ->
m = Vnull ->
can_change_aop P ->
absinfer
( <|| sem_pend_timeout_err (|Vptr qid :: Vint32 v :: nil|)
?? sem_pend_block_get_succ (|Vptr qid :: Vint32 v :: nil|) ||> **
HECBList mqls **
HTCBList tls **
HTime t **
HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr OS_TIMEOUT)))||> **
HECBList mqls **
HTCBList tls **
HTime t **
HCurTCB ct ** P).
Lemma absinfer_sem_pend_to_succ:
forall (P : asrt) (mqls : EcbMod.map) (qid : addrval)
(v : int32) (p : priority) (t : ostime) (ct : tidspec.A)
(tls : TcbMod.map) (m : msg) (st : taskstatus),
Int.unsigned v <= 65535 ->
can_change_aop P ->
TcbMod.get tls ct = Some (p, st, m) ->
~ (m = Vnull) ->
absinfer
( <|| sem_pend_timeout_err (|Vptr qid :: Vint32 v :: nil|)
?? sem_pend_block_get_succ (|Vptr qid :: Vint32 v :: nil|) ||> **
HECBList mqls **
HTCBList tls **
HTime t **
HCurTCB ct ** P)
( <|| END (Some (V$ OS_NO_ERR)) ||> **
HECBList mqls **
HTCBList tls **
HTime t **
HCurTCB ct ** P).
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 Import absop_rules.
Require Import lab.
Open Scope code_scope.
Lemma semcre_absimp_no_free:
forall P n,
can_change_aop P ->
(Z.leb (Int.unsigned n) Int16.max_unsigned) = true ->
absinfer ( <|| semcre (Vint32 n :: nil) ||> ** P)
( <|| END (Some Vnull) ||> ** P).
Lemma semcre_absimp_succ:
forall P sid n els tcbls tm curtid,
can_change_aop P ->
(Z.leb (Int.unsigned n) Int16.max_unsigned) = true ->
EcbMod.get els sid = None ->
absinfer ( <|| semcre (Vint32 n :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vptr sid)) ||> **
HECBList (EcbMod.set els sid (abssem n, nil:list tid)) **
HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma semacc_absimp_null:
forall sid P,
sid = Vnull ->
can_change_aop P ->
absinfer ( <|| semacc (sid :: nil) ||> ** P)
( <|| END (Some (Vint32 Int.zero)) ||> ** P ).
Lemma semacc_absimp_no_sem:
forall P els tcbls tm curtid sid,
can_change_aop P ->
(~ exists n wls, EcbMod.get els sid = Some (abssem n, wls)) ->
absinfer
( <|| semacc (Vptr sid :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 Int.zero)) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma semacc_absimp_no_source:
forall P els tcbls tm curtid sid wls,
can_change_aop P ->
EcbMod.get els sid = Some (abssem Int.zero, wls) ->
absinfer
( <|| semacc (Vptr sid :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 Int.zero)) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma semacc_absimp_succ:
forall P wls els sid n v1 v3 v4,
can_change_aop P ->
EcbMod.get els sid = Some (abssem n, wls) ->
Int.ltu Int.zero n = true ->
absinfer
( <|| semacc (Vptr sid :: nil) ||> **
HECBList els **
HTCBList v1 **
HTime v3 **
HCurTCB v4 ** P)
( <|| END (Some (Vint32 n)) ||> **
HECBList (EcbMod.set els sid (abssem (Int.sub n Int.one), wls)) **
HTCBList v1 **
HTime v3 **
HCurTCB v4 ** P).
Lemma semdel_absimp_null:
forall sid P,
sid = Vnull ->
can_change_aop P ->
absinfer ( <|| semdel (sid :: nil) ||> ** P)
( <|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL))) ||> ** P ).
Lemma semdel_absimp_no_sem:
forall P els tcbls tm curtid sid,
can_change_aop P ->
(~ exists n wls, EcbMod.get els sid = Some (abssem n, wls)) ->
absinfer
( <|| semdel (Vptr sid :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL))) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma semdel_absimp_type_err:
forall P els tcbls tm curtid sid,
can_change_aop P ->
(~ exists n wls, EcbMod.get els sid = Some (abssem n, wls)) ->
absinfer
( <|| semdel (Vptr sid :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 (Int.repr OS_ERR_EVENT_TYPE))) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma semdel_absimp_task_waiting:
forall P els tcbls tm curtid n sid w wls,
can_change_aop P ->
EcbMod.get els sid = Some (abssem n, w::wls) ->
absinfer
( <|| semdel (Vptr sid :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 (Int.repr OS_ERR_TASK_WAITING))) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma semdel_absimp_succ:
forall P els els´ sid n v1 v3 v4,
can_change_aop P ->
EcbMod.get els sid = Some (abssem n, nil) ->
EcbMod.join els´ (EcbMod.sig sid (abssem n,nil)) els ->
absinfer
( <|| semdel (Vptr sid :: nil) ||> **
HECBList els **
HTCBList v1 **
HTime v3 **
HCurTCB v4 ** P)
( <|| END (Some (Vint32 (Int.repr NO_ERR))) ||> **
HECBList els´ **
HTCBList v1 **
HTime v3 **
HCurTCB v4 ** P).
Lemma absimp_sem_post_null_return:
forall sid P,
sid = Vnull ->
can_change_aop P ->
absinfer ( <|| sem_post (sid :: nil) ||> ** P)
( <|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL))) ||> ** P ).
Lemma absimp_sem_post_p_not_legal_return:
forall P els tcbls tm curtid sid,
can_change_aop P ->
EcbMod.get els sid = None ->
absinfer ( <|| sem_post ((Vptr sid) :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL))) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma absimp_sem_post_wrong_type_return:
forall P els tcbls tm curtid sid,
can_change_aop P ->
(exists d,
EcbMod.get els sid = Some d /\ ~ (exists n wls, d = (abssem n, wls))) ->
absinfer
( <|| sem_post ((Vptr sid) :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL))) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma absimp_sem_post_ovf_err_return:
forall P els tcbls tm curtid sid n wls,
can_change_aop P ->
EcbMod.get els sid = Some (abssem n, wls) ->
Int.ltu n (Int.repr 65535) = false ->
absinfer
( <|| sem_post ((Vptr sid) :: nil) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
( <|| END (Some (Vint32 (Int.repr OS_SEM_OVF))) ||> **
HECBList els ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma absimp_sem_post_put_sem_return:
forall P els sid n wls tcbls t ct,
can_change_aop P ->
EcbMod.get els sid = Some (abssem n, wls) ->
Int.ltu n (Int.repr 65535) = true ->
absinfer
( <|| sem_post ((Vptr sid) :: nil) ||> **
HECBList els **
HTCBList tcbls **
HTime t ** HCurTCB ct ** P)
( <|| END (Some (Vint32 (Int.repr OS_NO_ERR))) ||> **
HECBList (EcbMod.set els sid (abssem (Int.add n Int.one), wls)) **
HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma absimp_sem_post_ex_wt_succ_return:
forall P els sid tls t t´ n wls p st m ct mid,
can_change_aop P ->
EcbMod.get els sid = Some (abssem n, wls) ->
~ wls = nil ->
GetHWait tls wls t´ ->
TcbMod.get tls t´ = Some (p, st, m) ->
absinfer
( <|| sem_post ((Vptr sid) :: nil) ||> **
HECBList els ** HTCBList tls ** HTime t ** HCurTCB ct ** P )
( <|| isched;;END (Some (Vint32 (Int.repr OS_NO_ERR))) ||> **
HECBList (EcbMod.set els sid (abssem n, (remove_tid t´ wls))) **
HTCBList (TcbMod.set tls t´ (p, rdy, Vptr mid)) **
HTime t ** HCurTCB ct ** P ).
Lemma absinfer_sem_pend_null_return :
forall P x,
can_change_aop P ->
tl_vl_match (Tint16 :: nil) x = true ->
absinfer
(<|| sem_pend (Vnull :: x) ||> ** P)
(<|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL))) ||> ** P).
Lemma absinfer_sem_pend_p_not_legal_return :
forall x a P b v´33 v´16 v´35,
can_change_aop P ->
Int.unsigned b<=65535 ->
EcbMod.get x a = None ->
absinfer
(<|| sem_pend (Vptr a ::Vint32 b:: nil) ||> **
HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 ** P)
(<|| END (Some (V$ OS_ERR_PEVENT_NULL)) ||> **
HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 ** P).
Lemma absinfer_sem_pend_wrong_type_return :
forall x a b P v´33 v´16 v´35,
can_change_aop P ->
Int.unsigned b <= 65535 ->
(exists d,
EcbMod.get x a = Some d /\ ~ (exists x wls, d = (abssem x, wls))) ->
absinfer
(<|| sem_pend (Vptr a :: Vint32 b :: nil) ||> **
HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 ** P)
(<|| END (Some (V$ OS_ERR_PEVENT_NULL)) ||> **
HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 ** P).
Lemma absinfer_sem_pend_from_idle_return :
forall x a b P y t ct,
can_change_aop P ->
Int.unsigned b <= 65535 ->
(exists st msg, TcbMod.get y ct = Some (Int.repr OS_IDLE_PRIO, st, msg)) ->
absinfer
(<|| sem_pend (Vptr a :: Vint32 b :: nil) ||> **
HECBList x **
HTCBList y **
HTime t **
HCurTCB ct ** P)
( <|| END (Some (V$ OS_ERR_PEVENT_NULL)) ||> **
HECBList x **
HTCBList y **
HTime t **
HCurTCB ct ** P).
Lemma absinfer_sem_pend_not_ready_return :
forall P ecbls tcbls t ct st msg v x prio,
Int.unsigned v <= 65535 ->
TcbMod.get tcbls ct = Some (prio, st, msg) ->
~ st = rdy ->
can_change_aop P ->
absinfer
(<|| sem_pend (Vptr x :: Vint32 v :: nil) ||> **
HECBList ecbls **
HTCBList tcbls **
HTime t **
HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL)))||> **
HECBList ecbls **
HTCBList tcbls **
HTime t **
HCurTCB ct ** P).
Lemma absinfer_sem_pend_inst_get_return:
forall P wls els sid n v1 v3 v4 v,
can_change_aop P ->
Int.unsigned v <= 65535 ->
EcbMod.get els sid = Some (abssem n, wls) ->
Int.ltu Int.zero n = true ->
absinfer
( <|| sem_pend (Vptr sid :: Vint32 v :: nil) ||> **
HECBList els **
HTCBList v1 **
HTime v3 **
HCurTCB v4 ** P)
( <|| END (Some (Vint32 (Int.repr OS_NO_ERR))) ||> **
HECBList (EcbMod.set els sid (abssem (Int.sub n Int.one), wls)) **
HTCBList v1 **
HTime v3 **
HCurTCB v4 ** P).
Lemma absinfer_sem_pend_msg_not_null_return :
forall P ecbls tcbls t ct st msg v x prio,
Int.unsigned v <= 65535 ->
TcbMod.get tcbls ct = Some (prio, st, msg) ->
~ msg = Vnull ->
can_change_aop P ->
absinfer
(<|| sem_pend (Vptr x :: Vint32 v :: nil) ||> **
HECBList ecbls **
HTCBList tcbls **
HTime t **
HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL)))||> **
HECBList ecbls **
HTCBList tcbls **
HTime t **
HCurTCB ct ** P).
Lemma absinfer_sem_pend_block:
forall P mqls qid v wl p m t ct tls,
Int.unsigned v <= 65535 ->
can_change_aop P ->
EcbMod.get mqls qid = Some (abssem Int.zero, wl) ->
TcbMod.get tls ct = Some (p,rdy,m) ->
absinfer
( <|| sem_pend (Vptr qid :: Vint32 v :: nil) ||> **
HECBList mqls **
HTCBList tls **
HTime t **
HCurTCB ct ** P)
(<|| isched;;
(sem_pend_timeout_err (|Vptr qid :: Vint32 v :: nil|) ??
sem_pend_block_get_succ (|Vptr qid :: Vint32 v :: nil|)) ||> **
HECBList (EcbMod.set mqls qid (abssem Int.zero ,ct::wl)) **
HTCBList (TcbMod.set tls ct (p,wait (os_stat_sem qid) v, m) ) **
HTime t **
HCurTCB ct ** P).
Lemma absinfer_sem_pend_to_timeout :
forall P mqls qid t ct tls v st prio m,
Int.unsigned v <= 65535 ->
TcbMod.get tls ct = Some (prio, st, m) ->
m = Vnull ->
can_change_aop P ->
absinfer
( <|| sem_pend_timeout_err (|Vptr qid :: Vint32 v :: nil|)
?? sem_pend_block_get_succ (|Vptr qid :: Vint32 v :: nil|) ||> **
HECBList mqls **
HTCBList tls **
HTime t **
HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr OS_TIMEOUT)))||> **
HECBList mqls **
HTCBList tls **
HTime t **
HCurTCB ct ** P).
Lemma absinfer_sem_pend_to_succ:
forall (P : asrt) (mqls : EcbMod.map) (qid : addrval)
(v : int32) (p : priority) (t : ostime) (ct : tidspec.A)
(tls : TcbMod.map) (m : msg) (st : taskstatus),
Int.unsigned v <= 65535 ->
can_change_aop P ->
TcbMod.get tls ct = Some (p, st, m) ->
~ (m = Vnull) ->
absinfer
( <|| sem_pend_timeout_err (|Vptr qid :: Vint32 v :: nil|)
?? sem_pend_block_get_succ (|Vptr qid :: Vint32 v :: nil|) ||> **
HECBList mqls **
HTCBList tls **
HTime t **
HCurTCB ct ** P)
( <|| END (Some (V$ OS_NO_ERR)) ||> **
HECBList mqls **
HTCBList tls **
HTime t **
HCurTCB ct ** P).