Library simulation
This file defines the simulation relations, which are employed
as the meta theory for proving the soundness of the verification framework.
Require Import include.
Require Import memdata.
Require Import memory.
Require Import Lists.ListSet.
Require Import language.
Require Import opsem.
Require Import assertion.
whole-program simulation relation
The whole-program simulation relation (ProgSim) between concrete
and abstract levels is co-inductively defined as below. It implies
that the set of observable behaviors of the low level program is a subset
of those of the high-level program (see /framework/theory/oscorrectness.v);
CoInductive ProgSim : lprog -> tasks -> osstate -> hprog -> tasks ->
osabst -> clientst -> tid -> Prop:=
| prog_sim:
forall (pl:lprog) (ph:hprog) (Tl Th:tasks) (S:osstate) (O:osabst) (cst:clientst) t,
OSAbstMod.get O curtid = Some (oscurt t) ->
(forall Tl´ S´ cst´ t´, lpstep pl Tl cst S t Tl´ cst´ S´ t´->
exists Th´ O´, hpstepstar ph Th cst O Th´ cst´ O´ /\
(ProgSim pl Tl´ S´ ph Th´ O´ cst´ t´)) ->
(forall Tl´ S´ cst´ ev t´, lpstepev pl Tl cst S t Tl´ cst´ S´ t´ ev ->
exists Th´ O´, hpstepevstar ph Th cst O Th´ cst´ O´ ev /\
(ProgSim pl Tl´ S´ ph Th´ O´ cst´ t´ ))->
(lpstepabt pl Tl cst S t-> hpstepabtstar ph Th cst O )
-> ProgSim pl Tl S ph Th O cst t.
Definition reltaskpred := prod taskst osabst -> Prop.
Import OSAbstMod.
task-local simulation relations
The task-local simulation relations (TaskSim) between the low-level task and
the high-level task is co-inductively defined as below. It is compositional by
parametrizing with the global invariants for specifying interleavings.
The whole program simulation relation can be obtained by composing all the task-local
simulation relations together (see Lemma 'tsimtopsim' in /framework/theory/lemmasfortopthem.v).
CoInductive TaskSim: lprog -> code -> taskst -> hprog -> code -> osabst ->
tid -> Inv -> reltaskpred -> Prop :=
| task_sim : forall (pl:lprog) (ph:hprog) (Cl Ch:code) (o:taskst) (O:osabst)
(t:tid) (I:Inv) (P:reltaskpred),
(
forall Cl´ Ms Mf cst cst´ o´´ Os o1 o2,
(forall ab, sat (((substaskst o Ms), Os),ab) (INV I))->
joinmem o Ms o1 ->
joinmem o1 Mf o2 ->
disj O Os ->
ltstep pl t Cl cst o2 Cl´ cst´ o´´ ->
(
exists Ms´ Ch´ O´ Os´ o1´ o´,
joinmem o1´ Mf o´´/\
joinmem o´ Ms´ o1´ /\
(forall ab,sat (((substaskst o´ Ms´), Os´),ab) (INV I))/\
disj O´ Os´ /\
htstepstar ph t Ch cst (merge O Os) Ch´ cst´ (merge O´ Os´)/\
TaskSim pl Cl´ o´ ph Ch´ O´ t I P
)
)->
(
forall cst Cl´ Ms Mf Os o1 o2 ev,
(forall ab,sat (((substaskst o Ms), Os),ab) (INV I))->
joinmem o Ms o1 ->
joinmem o1 Mf o2 ->
disj O Os ->
ltstepev pl t Cl cst o2 Cl´ cst o2 ev->
(
exists Ch´ O´ Os´,
(forall ab,sat (((substaskst o Ms), Os´),ab) (INV I))/\
disj O´ Os´ /\
htstepevstar ph t Ch cst (merge O Os) Ch´ cst (merge O´ Os´) ev/\
TaskSim pl Cl´ o ph Ch´ O´ t I P
)
)->
(
forall cst Cl´ Ms ks x Os,
Cl = (curs (sprim (switch x)), (kenil, ks)) ->
Cl´ =(SKIP, (kenil, ks)) ->
MemMod.disj (get_mem (get_smem o)) Ms ->
(forall ab, sat (((substaskst o Ms), Os),ab) (INV I))->
disj O Os ->
InOS Cl (pumerge (fst (fst (snd pl))) (snd (fst (snd pl))) )->
(
exists O´ Os´ Mc ol Ch´ ke ks s,
joinmem ol Mc o /\
htstepstar ph t Ch cst (merge O Os) Ch´ cst (merge O´ Os´)/\
Ch´ = (curs (hapi_code (spec_seq sched s)),(ke,ks)) /\
disj O´ Os´/\
(forall ab,sat (((substaskst o Ms), Os´),ab) (INV I))/\
(forall ab, sat (((substaskst ol Mc), O´),ab) (SWPRE (snd (snd ph))x))/\
(forall ab,sat (((substaskst ol Mc), O´),ab) (SWINV I))/\
(
forall Mc´ O´´ o´,
joinmem ol Mc´ o´ ->
(forall ab,sat (((substaskst ol Mc´), O´´),ab) (SWINV I)) ->
TaskSim pl Cl´ o´ ph (curs (hapi_code s),(ke,ks)) O´´ t I P
)
)
)
->
(
forall cst Ms Os,
IsEnd Cl ->
disj O Os ->
MemMod.disj (get_mem (get_smem o)) Ms ->
(forall ab,sat (((substaskst o Ms), Os),ab) (INV I))->
(
exists O´ Os´ Ch,
IsEnd Ch /\
htstepstar ph t Ch cst (merge O Os) Ch cst (merge O´ Os´)/\
disj O´ Os´/\
(forall ab, sat (((substaskst o Ms), Os´),ab) (INV I))/\
P (o, O´)
)
)->
(
forall cst o´ o´´ Ms Os Mf,
~(IsEnd Cl) ->
~(exists x ks, Cl = (curs (sprim (switch x)), (kenil, ks)))->
joinmem o Ms o´ ->
joinmem o´ Mf o´´->
(forall ab,sat (((substaskst o Ms), Os),ab) (INV I)) ->
ltstepabt pl t Cl cst o´´ ->
disj O Os ->
htstepabtstar ph t Ch cst (merge O Os)
)->
TaskSim pl Cl o ph Ch O t I P.
Definition TaskSimAsrt (pl:lprog) (Cl:code) (ph:hprog) (Ch:code)
(t:tid) (I:Inv) (P:reltaskpred):Prop:=
forall (o:taskst) (O:osabst),
P (o, O) -> TaskSim pl Cl o ph Ch O t I P.
Notation hmstep := spec_step.
Notation hmstepstar:=spec_stepstar.
Definition TcbBJ tls:= (forall t t´ pr a pr´ a´ msg msg´, t<>t´ -> TcbMod.get tls t = Some (pr,a,msg) -> TcbMod.get tls t´ = Some (pr´,a´,msg´) -> (Vint32 pr) <> (Vint32 pr´)) /\ (forall t t´ pr a pr´ a´ msg msg´, pr<>pr´ -> TcbMod.get tls t = Some (pr,a,msg) -> TcbMod.get tls t´ = Some (pr´,a´,msg´) -> t <> t´).
Definition notabortm (C:code):= ~IsFcall C/\~IsSwitch C /\ ~IsEnd C /\
~ IsRet C /\ ~IsRetE C /\ ~IsIRet C.
Definition eqenv (o o´: taskst) : Prop := match o, o´ with
| (G,E,M,isr,aux),(G´,E´,M´,isr´,aux´) => G =G´ /\ E = E´
end.
CoInductive MethSimMod : funspec -> ossched -> code -> taskst -> absop -> osabst ->
Inv -> retasrt -> asrt -> retasrt -> Prop :=
| meth_sim_mod : forall (spec :funspec) sd (C:code)
(gamma:absop) (O:osabst) (I:Inv)
(r q : retasrt) (ri: asrt) (o:taskst),
(
forall p C´ Ms Mf Os o1 o2 o2´ ab,
~IsFcall C ->
sat (((substaskst o Ms), Os),ab) (INV I) ->
joinmem o Ms o1 ->
joinmem o1 Mf o2 ->
loststep p C o2 C´ o2´ ->
disj O Os ->
(
exists Os´ gamma´ O´ o´ o1´ Ms´,
joinmem o1´ Mf o2´ /\
joinmem o´ Ms´ o1´ /\
disj O´ Os´ /\
hmstepstar gamma (merge O Os) gamma´ (merge O´ Os´) /\
sat (((substaskst o´ Ms´), Os´),ab) (INV I)/\
MethSimMod spec sd C´ o´ gamma´ O´ I r ri q
)
)->
(
forall Ms Os ab ks f vl tl,
C = (curs (sfexec f vl tl), (kenil,ks)) ->
MemMod.disj (get_mem (get_smem o)) Ms ->
sat (((substaskst o Ms), Os),ab) (INV I)->
disj O Os ->
(
exists om M Ot Of O´ Os´,
exists gamma´ pre post tp logicl,
tl_vl_match tl vl = true /\
spec f = Some (pre, post, (tp ,List.rev tl)) /\
joinmem om M o /\
hmstepstar gamma (merge O Os) gamma´ (merge O´ Os´)/\
sat (om, Ot, gamma´) (getasrt (pre (rev vl) logicl)) /\
disj O´ Os´/\
OSAbstMod.join Ot Of O´/\
sat (((substaskst o Ms), Os´),ab) (INV I)/\
(
forall o1 o´ O1 O´´ v gamma´´,
eqenv o o´ ->
sat (o1,O1,gamma´´) (getasrt (post (rev vl) v logicl)) ->
joinmem o1 M o´ ->
OSAbstMod.join O1 Of O´´ ->
MethSimMod spec sd (curs (sskip v), (kenil,ks)) o´
gamma´´ O´´ I r ri q
)
)
)->
(
forall C´ Ms ks x Os ab,
C = (curs (sprim (switch x)), (kenil, ks)) ->
C´ =(SKIP, (kenil, ks)) ->
MemMod.disj (get_mem (get_smem o)) Ms ->
sat (((substaskst o Ms), Os),ab) (INV I)->
disj O Os ->
(
exists O´ Os´ Mc ol gamma´ s,
joinmem ol Mc o /\
hmstepstar gamma (merge O Os) gamma´ (merge O´ Os´) /\
gamma´ = spec_seq sched s /\
disj O´ Os´/\
sat (((substaskst o Ms), Os´),ab) (INV I)/\
sat (((substaskst ol Mc), O´),ab) (SWPRE sd x)/\
sat (((substaskst ol Mc), O´),ab) (SWINV I)/\
(
forall Mc´ O´´ o´,
joinmem ol Mc´ o´ ->
sat (((substaskst ol Mc´), O´´),ab) (SWINV I)->
MethSimMod spec sd C´ o´ s O´´ I r ri q
)
)
)->
(
forall v ab Ms Os ,
C = (curs (sskip v), (kenil, kstop)) ->
MemMod.disj (get_mem (get_smem o)) Ms ->
sat (((substaskst o Ms), Os),ab) (INV I)->
disj O Os ->
(
exists gamma´ Os´ O´,
disj O´ Os´/\
hmstepstar gamma (merge O Os) gamma´ (merge O´ Os´) /\
sat (((substaskst o Ms), Os´),ab) (INV I)/\
sat ((o, O´),gamma´) (q v)
)
)->
(
forall ks Os Ms ab,
C = (curs sret, (kenil, ks)) ->
callcont ks = None ->
intcont ks =None ->
MemMod.disj (get_mem (get_smem o)) Ms ->
sat (((substaskst o Ms), Os),ab) (INV I)->
disj O Os ->
(
exists O´ Os´ gamma´,
disj O´ Os´ /\
hmstepstar gamma (merge O Os) gamma´
(merge O´ Os´) /\
sat (((substaskst o Ms), Os´),ab) (INV I)/\
sat ((o, O´),gamma´) (r None)
)
)->
(
forall ks Os Ms v ab,
C = ([v], (kenil, (kret ks))) ->
callcont ks = None ->
intcont ks =None ->
MemMod.disj (get_mem (get_smem o)) Ms ->
sat (((substaskst o Ms), Os),ab) (INV I) ->
disj O Os ->
(
exists O´ Os´ gamma´,
disj O´ Os´ /\
hmstepstar gamma (merge O Os) gamma´
(merge O´ Os´) /\
sat (((substaskst o Ms), Os´),ab) (INV I)/\
sat ((o, O´), gamma´) (r (Some v))
)
)->
(
forall ab ks Os Ms,
C = (curs (sprim exint), (kenil, ks)) ->
callcont ks = None ->
intcont ks =None ->
MemMod.disj (get_mem (get_smem o)) Ms ->
sat (((substaskst o Ms), Os),ab) (INV I) ->
disj O Os ->
(
exists O´ Os´ gamma´,
disj O´ Os´ /\
hmstepstar gamma (merge O Os) gamma´ (merge O´ Os´) /\
sat (((substaskst o Ms), Os´),ab) (INV I)/\
sat ((o, O´),gamma´) ri
)
)->
(
forall p ab Os Ms Mf o1 o2 ,
notabortm C ->
joinmem o Ms o1 ->
joinmem o1 Mf o2 ->
sat (((substaskst o Ms), Os),ab) (INV I) ->
disj O Os ->
~ (loststepabt p C o2)
)->
MethSimMod spec sd C o gamma O I r ri q.
Notation " ´{[´ p , sd , I , r , ri , q ´]}´ ´||-´ ´(´ C , o ´)´ ´<_msim´ ´(´ gamma , O ´)´ "
:= (MethSimMod p sd C o gamma O I r ri q) (at level 200).
Definition notabort (C:code):=~IsSwitch C /\ ~IsEnd C /\
~ IsRet C /\ ~IsRetE C /\ ~IsIRet C.
The method simulation is similar as the modular one (MethSimMod), and it is defined only
for simplifying the soundness proofs. Instead of using function specifications to
ignore the function calls, it steps into the the function bodies of
internal functions. It could be implied by modular method simulation(MethSimMod)
(see Lemma 'MethSim_to_Methsim'_aux' in /framework/logic/methsimlift.v).
CoInductive MethSim : progunit -> ossched -> code -> taskst -> absop -> osabst ->
Inv -> retasrt -> asrt -> retasrt -> Prop :=
| meth_sim : forall (p:progunit) sd (C:code)
(gamma:absop) (O:osabst) (I:Inv)
(r q: retasrt) (ri: asrt) (o:taskst),
(
forall C´ Ms Mf Os o1 o2 o2´ ab,
sat (((substaskst o Ms), Os),ab) (INV I) ->
joinmem o Ms o1 ->
joinmem o1 Mf o2 ->
loststep p C o2 C´ o2´ ->
disj O Os ->
(
exists Os´ gamma´ O´ o´ o1´ Ms´,
joinmem o1´ Mf o2´ /\
joinmem o´ Ms´ o1´ /\
disj O´ Os´ /\
hmstepstar gamma (merge O Os) gamma´ (merge O´ Os´) /\
sat (((substaskst o´ Ms´), Os´),ab) (INV I)/\
MethSim p sd C´ o´ gamma´ O´ I r ri q
)
)->
(
forall C´ Ms ks x Os ab,
C = (curs (sprim (switch x)), (kenil, ks)) ->
C´ =(SKIP, (kenil, ks)) ->
MemMod.disj (get_mem (get_smem o)) Ms ->
sat (((substaskst o Ms), Os),ab) (INV I)->
disj O Os ->
(
exists O´ Os´ Mc ol gamma´ s,
joinmem ol Mc o /\
hmstepstar gamma (merge O Os) gamma´ (merge O´ Os´) /\
gamma´ = spec_seq sched s /\
disj O´ Os´/\
sat (((substaskst o Ms), Os´),ab) (INV I)/\
sat (((substaskst ol Mc), O´),ab) (SWPRE sd x)/\
sat (((substaskst ol Mc), O´),ab) (SWINV I)/\
(
forall Mc´ O´´ o´,
joinmem ol Mc´ o´ ->
sat (((substaskst ol Mc´), O´´),ab) (SWINV I)->
MethSim p sd C´ o´ s O´´ I r ri q
)
)
)->
(
forall v ab Ms Os ,
C = (curs (sskip v), (kenil, kstop)) ->
MemMod.disj (get_mem (get_smem o)) Ms ->
sat (((substaskst o Ms), Os),ab) (INV I)->
disj O Os ->
(
exists gamma´ Os´ O´,
disj O´ Os´/\
hmstepstar gamma (merge O Os) gamma´ (merge O´ Os´) /\
sat (((substaskst o Ms), Os´),ab) (INV I)/\
sat ((o, O´),gamma´) (q v)
)
)->
(
forall ks Os Ms ab,
C = (curs sret, (kenil, ks)) ->
callcont ks = None ->
intcont ks =None ->
MemMod.disj (get_mem (get_smem o)) Ms ->
sat (((substaskst o Ms), Os),ab) (INV I)->
disj O Os ->
(
exists O´ Os´ gamma´,
disj O´ Os´ /\
hmstepstar gamma (merge O Os) gamma´
(merge O´ Os´) /\
sat (((substaskst o Ms), Os´),ab) (INV I)/\
sat ((o, O´),gamma´) (r None)
)
)->
(
forall ks Os Ms v ab,
C = ([v], (kenil, (kret ks))) ->
callcont ks = None ->
intcont ks =None ->
MemMod.disj (get_mem (get_smem o)) Ms ->
sat (((substaskst o Ms), Os),ab) (INV I) ->
disj O Os ->
(
exists O´ Os´ gamma´,
disj O´ Os´ /\
hmstepstar gamma (merge O Os) gamma´
(merge O´ Os´) /\
sat (((substaskst o Ms), Os´),ab) (INV I)/\
sat ((o, O´), gamma´) (r (Some v))
)
)->
(
forall ab ks Os Ms,
C = (curs (sprim exint), (kenil, ks)) ->
callcont ks = None ->
intcont ks =None ->
MemMod.disj (get_mem (get_smem o)) Ms ->
sat (((substaskst o Ms), Os),ab) (INV I) ->
disj O Os ->
(
exists O´ Os´ gamma´,
disj O´ Os´ /\
hmstepstar gamma (merge O Os) gamma´ (merge O´ Os´) /\
sat (((substaskst o Ms), Os´),ab) (INV I)/\
sat ((o, O´),gamma´) ri
)
)->
(
forall ab Os Ms Mf o1 o2 ,
notabort C ->
joinmem o Ms o1 ->
joinmem o1 Mf o2 ->
sat (((substaskst o Ms), Os),ab) (INV I) ->
disj O Os ->
~ (loststepabt p C o2)
)->
MethSim p sd C o gamma O I r ri q.
Definition EqDom (P : progunit) (F : funspec) : Prop :=
forall f, (exists a, P f = Some a) <-> (exists b, F f = Some b).
Fixpoint getlenvdom (dl:decllist) : edom :=
match dl with
| dnil => nil
| dcons x t dl´ => (x,t)::(getlenvdom dl´)
end.
Fixpoint in_decllist (x:var) (dl : decllist) : bool :=
match dl with
| dnil => false
| dcons x´ t´ dl´ => orb (Zeq_bool x x´) (in_decllist x dl´)
end.
Fixpoint good_decllist (dl: decllist) : bool :=
match dl with
| dnil => true
| dcons x t dl´ => andb ( negb (in_decllist x dl´)) (good_decllist dl´)
end.
Fixpoint buildp (dl:decllist) (vl:vallist) :option asrt:=
match good_decllist dl with
| true =>
match dl, vl with
| dnil,nil => Some Aemp
| dcons x t dl´,cons v vl´ => match buildp dl´ vl´ with
| Some p => Some (Astar (Alvarmapsto x t v) p)
| None => None
end
| dcons x t dl´,nil => match buildp dl´ nil with
| Some p => Some (Astar (Aexists (fun (v:val) =>
Alvarmapsto x t v)) p)
| None => None
end
| _,_ => None
end
| false => None
end.
Lemma buldp_some_imp_gooddecl : forall dl vl p, buildp dl vl = Some p -> good_decllist dl = true .
Fixpoint buildq (dl:decllist) : option asrt:=
if good_decllist dl then
match dl with
| dnil => Some Aemp
| dcons x t dl´ => match buildq dl´ with
| Some p => Some (Astar (Aexists (fun (v:val)
=> Alvarmapsto x t v)) p)
| None => None
end
end
else None.
Parameter InitG:env.
Fixpoint dl_vl_match (dl:decllist) (vl:vallist) :=
match dl with
| dnil => match vl with
| nil => true
| _ => false
end
| dcons x t dl´ => match vl with
| v :: vl´ => if type_val_match t v then dl_vl_match dl´ vl´ else false
| _ => false
end
end.
Definition BuildPreA (p:progunit) (f:fid) (abs:osapi) (vl:vallist) G:option asrt:=
match p f with
| Some (t, d1, d2, s) =>
match dl_vl_match d1 (rev vl) with
| true =>
match buildp (revlcons d1 d2) vl with
| Some p =>Some (Aconj (Agenv G)
(Aconj
(Astar (p ** Aie true ** Ais nil ** Acs nil ** Aisr empisr)
(A_dom_lenv (getlenvdom (revlcons d1 d2))))
(Aop (fst abs (rev vl)))))
| _ => None
end
| false => None
end
| _ => None
end.
Definition BuildRetA (p:progunit) (f:fid) (abs:osapi) (vl:vallist) G:option retasrt:=
match p f with
| Some (t, d1, d2, s) => match buildq (revlcons d1 d2) with
| Some p =>
Some
(fun (v:option val) =>
(Aconj (Agenv G)
(Aconj (Astar
(p** Aie true ** Ais nil ** Acs nil ** Aisr empisr)
(A_dom_lenv (getlenvdom (revlcons d1 d2))))
(Aop (spec_done v)))))
|_ => None
end
| _ => None
end.
Definition BuildPreI (p:progunit) (f:fid) (vl:vallist) (logicl:list logicvar) (fp:vallist -> list logicvar -> funasrt): option asrt:=
match p f with
| Some (t, d1, d2, s) =>
match dl_vl_match d1 (rev vl) with
| true =>
match buildp (revlcons d1 d2) vl with
| Some p => Some (Astar (Astar p (getasrt (fp (rev vl) logicl)))
(A_dom_lenv (getlenvdom (revlcons d1 d2))))
| _ => None
end
| false => None
end
| _ => None
end.
Definition BuildRetI (p:progunit) (f:fid) (vl:vallist) (logicl:list logicvar) (fq:vallist -> option val -> list logicvar -> funasrt):option retasrt:=
match p f with
| Some (t, d1 , d2, s) =>
match buildq (revlcons d1 d2) with
| Some p => Some (fun (v:option val) =>
(Astar (Astar p (getasrt (fq (rev vl) v logicl)))
(A_dom_lenv (getlenvdom (revlcons d1 d2)))))
| _ => None
end
| _ => None
end.
Definition lift (q : asrt): retasrt := fun _ => q.
The judgement semantics of the refinement logic.
Definition RuleSem (spec : funspec) (sd : ossched) (I:Inv) (r:retasrt) (ri:asrt)
(p:asrt) (s:stmts) (q:asrt) :Prop:=
forall o O aop, sat ((o, O),aop) p ->
MethSimMod spec sd (nilcont s) o aop O I r ri (lift q).
Definition MethSimAsrt (P : progunit) (sd:ossched) (I:Inv) (r:retasrt) (ri:asrt)
(p:asrt) (s:stmts) (q:asrt) :Prop:=
forall o O aop, sat ((o, O),aop) p -> MethSim P sd (nilcont s) o aop O I r ri (lift q).
Definition WFFuncsSim (P:progunit) (FSpec:funspec) (sd:ossched ) (I:Inv) :Prop:=
EqDom P FSpec /\
forall f pre post t tl, FSpec f = Some (pre, post, (t, tl)) ->
exists d1 d2 s, P f = Some (t, d1, d2, s)/\
tlmatch tl d1 /\
good_decllist (revlcons d1 d2) = true /\
(
forall vl p r logicl,
Some p = BuildPreI P f vl logicl pre ->
Some r = BuildRetI P f vl logicl post ->
RuleSem FSpec sd I r Afalse p s Afalse
).
Notation " ´[´ Spec , sd , I , r , ri , n ´]´ ´|=´ ´{{´ pre ´}}´ s ´{{´ post ´}}´ "
:= (RuleSem Spec sd I r ri pre s post n) (at level 200).
Notation " ´{[´ p , sd , I , r , ri , q ´]}´ ´||-´ ´(´ C , o ´)´ ´<_msim´ ´(´ gamma , O ´)´ "
:= (MethSimMod p sd C o gamma O I r ri q) (at level 200).