Library assertion
This file gives the defintions of the assertion language used in the
refinement program logic. The assertion language follows the separation
logic assertions, and it extends separation logic assertions to support
reasoning about relational states. (Corresponding to Sec.4 of the paper)
Require Import include.
Require Import memory.
Require Import memdata.
Require Import Lists.ListSet.
Require Import language.
Require Import opsem.
Set Implicit Arguments.
Definition EventCtr:=( vallist * vallist).
Definition edom := list (var*type).
Definition absop:= spec_code.
The syntax of the assertion langauge.
Inductive asrt : Type :=
Aemp
| Aconj (p1: asrt) (p2: asrt)
| Afalse
| Atrue
| Adisj (p1: asrt) (p2: asrt)
| Astar (p1: asrt) (p2: asrt)
| Anot : asrt -> asrt
| Apure : Prop -> asrt
| Aexists (ty:Type) (P:ty->asrt)
| Amapsto : addr -> type -> val -> asrt
| Amapstolsval : addr -> type -> vallist ->asrt
| Alvarenv : var -> type -> addr -> asrt
| Agvarenv : var -> type -> addr -> asrt
| Agenv : env -> asrt
| A_eval_expr : expr -> type -> val -> asrt
| A_eval_list : exprlist -> typelist -> vallist -> asrt
| A_dom_lenv : edom -> asrt
| A_notin_lenv : var -> asrt
| Alval : expr -> type -> addrval -> asrt
| Aistrue : expr -> asrt
| Aisfalse : expr -> asrt
| AHprio : ossched -> tid -> asrt
| Aie : ie -> asrt
| Ais : is -> asrt
| ATopis : hid -> asrt
| Aisr : isr -> asrt
| Acs : cs -> asrt
| Aabsdata : absdataid -> absdata -> asrt
| Aop : absop -> asrt.
Notation "´[|´ P ´|]´" := (Apure P) (at level 29, no associativity).
Infix "**" := Astar (at level 30, right associativity).
Infix "//\\" := Aconj (at level 31, right associativity).
Infix "\\//" := Adisj (at level 31, right associativity).
Notation "´Rv´ e ´@´ t ´==´ v" := (A_eval_expr e t v) (at level 20).
Notation "´Lv´ e ´@´ t ´==´ a" := (Alval e t a) (at level 20).
Notation "´Rvl´ el ´@´ tl ´==´ vl" := (A_eval_list el tl vl)(at level 20).
Notation " <| op |> " := (Aop op) (at level 20).
Notation "l # t |-> v " := (Amapsto l t v) (at level 20).
Definition Agvarenv´ x t l := Agvarenv x t (addrval_to_addr l).
Definition Alvarenv´ x t l := Alvarenv x t (addrval_to_addr l).
Aemp
| Aconj (p1: asrt) (p2: asrt)
| Afalse
| Atrue
| Adisj (p1: asrt) (p2: asrt)
| Astar (p1: asrt) (p2: asrt)
| Anot : asrt -> asrt
| Apure : Prop -> asrt
| Aexists (ty:Type) (P:ty->asrt)
| Amapsto : addr -> type -> val -> asrt
| Amapstolsval : addr -> type -> vallist ->asrt
| Alvarenv : var -> type -> addr -> asrt
| Agvarenv : var -> type -> addr -> asrt
| Agenv : env -> asrt
| A_eval_expr : expr -> type -> val -> asrt
| A_eval_list : exprlist -> typelist -> vallist -> asrt
| A_dom_lenv : edom -> asrt
| A_notin_lenv : var -> asrt
| Alval : expr -> type -> addrval -> asrt
| Aistrue : expr -> asrt
| Aisfalse : expr -> asrt
| AHprio : ossched -> tid -> asrt
| Aie : ie -> asrt
| Ais : is -> asrt
| ATopis : hid -> asrt
| Aisr : isr -> asrt
| Acs : cs -> asrt
| Aabsdata : absdataid -> absdata -> asrt
| Aop : absop -> asrt.
Notation "´[|´ P ´|]´" := (Apure P) (at level 29, no associativity).
Infix "**" := Astar (at level 30, right associativity).
Infix "//\\" := Aconj (at level 31, right associativity).
Infix "\\//" := Adisj (at level 31, right associativity).
Notation "´Rv´ e ´@´ t ´==´ v" := (A_eval_expr e t v) (at level 20).
Notation "´Lv´ e ´@´ t ´==´ a" := (Alval e t a) (at level 20).
Notation "´Rvl´ el ´@´ tl ´==´ vl" := (A_eval_list el tl vl)(at level 20).
Notation " <| op |> " := (Aop op) (at level 20).
Notation "l # t |-> v " := (Amapsto l t v) (at level 20).
Definition Agvarenv´ x t l := Agvarenv x t (addrval_to_addr l).
Definition Alvarenv´ x t l := Alvarenv x t (addrval_to_addr l).
Assertion notations
Notation "´G&´ x ´@´ t ´==´ l " := (Agvarenv´ x t l) (at level 20).
Notation "´L&´ x ´@´ t ´==´ l " := (Alvarenv´ x t l) (at level 20).
Notation "´EX´ x , p " :=
(Aexists (fun x => p))
(at level 32, x ident, right associativity).
Notation "´EX´ x : t , p " :=
(Aexists (fun x : t => p))
(at level 32, x ident, right associativity).
Notation "´EX´ x .. y , p" :=
(Aexists (fun x => .. (Aexists (fun y => p)) ..))
(at level 32, x binder, right associativity).
Definition Aptrmapsto (l : addrval) (t : type) (v : val) : asrt :=
(addrval_to_addr l) # t |-> v.
Definition Agvarmapsto (x :var) (tp :type) (v :val) : asrt :=
EX b : block, G& x @ tp == (b,Int.zero) ** Aptrmapsto (b, Int.zero) tp v.
Definition Alvarmapsto (x :var) (tp :type) (v :val) : asrt :=
EX b : block, L& x @ tp == (b,Int.zero) ** Aptrmapsto (b, Int.zero) tp v.
Notation "´PV´ l ´@´ t ´|->´ v " := (Aptrmapsto l t v) (at level 20).
Notation "´GV´ x ´@´ t ´|->´ l " := (Agvarmapsto x t l) (at level 20).
Notation "´LV´ x ´@´ t ´|->´ l " := (Alvarmapsto x t l) (at level 20).
Definition retasrt := option val -> asrt.
Definition reltaskst := prod taskst osabst.
Definition RstateOP := prod reltaskst absop.
Notation empenv := EnvMod.emp.
Notation empmem := MemMod.emp.
Definition emptaskst := fun (ts : taskst) =>
match ts with
| ((_,_,M),_,_) => M = empmem
end.
Notation empabst := OSAbstMod.emp.
Definition emposabst := fun st => st =empabst.
Definition empst (s : RstateOP) := match s with
| ((lo, ho), op) => emptaskst lo /\ emposabst ho
end.
Definition getmem (s : RstateOP) : mem :=
match s with
| ((lo, ho), op) => get_mem (get_smem lo)
end.
Definition getlenv (s : RstateOP) : env :=
match s with
| ((lo, ho), op) => get_lenv (get_smem lo)
end.
Definition getgenv (s : RstateOP) : env :=
match s with
| ((lo, ho), op) => get_genv (get_smem lo)
end.
Definition getabst (s : RstateOP) : osabst :=
match s with
| ((lo, ho), op) => ho
end.
Definition substabst (s : RstateOP) (o : osabst): RstateOP :=
match s with
| ((lo, ho), op) => ((lo ,o),op)
end.
Definition substaskst (st : taskst) (M : mem) : taskst :=
match st with
| ((G,E,M´),ir,aux) => ((G,E,M),ir,aux)
end.
Definition substaskstm (st:taskst) (M:mem):taskst:=
match st with
| ((G,E,M´),ir,aux) => ((G,E,M),ir,aux)
end.
Definition substmem (s : RstateOP) (M : mem): RstateOP :=
match s with
| ((lo, ho), op) => ((substaskst lo M ,ho),op)
end.
Definition substmo (s : RstateOP) (M : mem) (o : osabst): RstateOP :=
match s with
| ((lo, ho), op) => ((substaskst lo M , o),op)
end.
Definition getsmem (s : RstateOP) : smem := match s with
| ((lo, ho), op) => (get_smem lo)
end.
Definition gettaskst (s : RstateOP) : taskst :=
match s with
| ((lo, ho), op) => lo
end.
Definition getie (ts :taskst) :=
match ts with
| (_,_,(ie,_,_)) => ie
end.
Definition getis (ts :taskst) :=
match ts with
| (_,_,(_,is,_)) => is
end.
Definition getcs (ts :taskst) :=
match ts with
| (_,_,(_,_,cs)) => cs
end.
Definition getisr (ts :taskst) :=
match ts with
| (_,isr,_) => isr
end.
Definition getabsop (s : RstateOP) : absop :=
match s with
| ((lo, ho), op) => op
end.
Definition subabsop (s : RstateOP) (op : absop) : RstateOP :=
match s with
| (rs,_) => (rs ,op)
end.
Definition SysmemJoinM (m:smem) (M1:mem) (m´:smem):=
exists G E M0 M´, m = (G, E, M0) /\ m´ = (G,E,M´) /\ MemMod.join M0 M1 M´.
Definition joinmem (ts : taskst)(M : mem)(ts´ : taskst) : Prop :=
exists G E M1 M2 ir ls, ts = ((G, E, M1), ir, ls) /\
ts´ = ((G, E, M2), ir, ls) /\
MemMod.join M1 M M2.
Definition rval (e : expr) (v : val) (m : smem) := evalval e m = Some v /\ v <> Vundef.
Definition lval (e :expr) (v : val) (m : smem) := evaladdr e m = Some v /\ exists l, v = Vptr l.
Definition typecheck (e :expr) (t : type ) (m : smem) := evaltype e m = Some t.
Fixpoint typechklist (el : exprlist) (tl : typelist) (vl : vallist) (m : smem){struct el} :=
match el, tl, vl with
| nil,nil, nil => True
| cons e el´, cons t tl´, cons v vl´ => (rval e v) m /\ (typecheck e t) m /\ (typechklist el´ tl´ vl´) m
| _,_,_ => False
end.
Fixpoint evalexprlist (el : exprlist) (tl : typelist) (vl : vallist) (m : smem) {struct el} :=
match el, tl, vl with
| nil,nil, nil => True
| cons e el´, cons t tl´, cons v vl´ =>
evalval e m = Some v /\ evaltype e m = Some t
/\ evalexprlist el´ tl´ vl´ m /\ v <> Vundef
| _,_,_ => False
end.
Definition ptomval (l : addr) (v : memval) (M : mem) := M = MemMod.sig l v.
Open Local Scope Z_scope.
Fixpoint ptomvallist (l : addr) ( vl : mvallist) (M: mem) {struct vl} : Prop :=
match vl, l with
| nil, _ => M = MemMod.emp
| u:: vl´, (b, i) =>
exists M1 M2, MemMod.join M1 M2 M /\
ptomval l u M1 /\ ptomvallist ( b, (Z.add i 1%Z)) vl´ M2
end.
Definition mapstoval (l : addr) (t : type) (v : val) (m : mem) :=
exists vl, encode_val t v = vl /\ (ptomvallist l vl m).
Fixpoint arraymapstovallist (l : addr) (t : type) (vl : vallist) (m : mem){struct vl} :=
match vl with
| nil => m = MemMod.emp
| v :: vl´ => exists m1 m2,
MemMod.join m1 m2 m /\
(mapstoval l t v m1) /\
exists b i,
l = (b, i) /\ arraymapstovallist (b, (Z.add i (Z_of_nat (typelen t)))) t vl´ m2
end.
Fixpoint structmapstovallist (l : addr)(dls : decllist)
(vl : vallist) (m : mem){struct vl} :=
match vl, dls with
| nil,dnil => m = empmem
| v :: vl´, dcons id t dls´ =>
exists m1 m2,
MemMod.join m1 m2 m /\
(mapstoval l t v m1) /\
exists b i,
l = (b, i) /\ structmapstovallist
(b, (Z.add i (Z_of_nat (typelen t)))) dls´ vl´ m2
| _, _ => False
end.
Definition gettopis (ii : is) : hid := match ii with
| nil => INUM
| i :: is´ => i
end.
Definition eq_dom_env (E :env) (d : edom) : Prop :=
forall x t, set_In (x,t) d <-> exists l, EnvMod.get E x =Some (l,t).
Notation "´L&´ x ´@´ t ´==´ l " := (Alvarenv´ x t l) (at level 20).
Notation "´EX´ x , p " :=
(Aexists (fun x => p))
(at level 32, x ident, right associativity).
Notation "´EX´ x : t , p " :=
(Aexists (fun x : t => p))
(at level 32, x ident, right associativity).
Notation "´EX´ x .. y , p" :=
(Aexists (fun x => .. (Aexists (fun y => p)) ..))
(at level 32, x binder, right associativity).
Definition Aptrmapsto (l : addrval) (t : type) (v : val) : asrt :=
(addrval_to_addr l) # t |-> v.
Definition Agvarmapsto (x :var) (tp :type) (v :val) : asrt :=
EX b : block, G& x @ tp == (b,Int.zero) ** Aptrmapsto (b, Int.zero) tp v.
Definition Alvarmapsto (x :var) (tp :type) (v :val) : asrt :=
EX b : block, L& x @ tp == (b,Int.zero) ** Aptrmapsto (b, Int.zero) tp v.
Notation "´PV´ l ´@´ t ´|->´ v " := (Aptrmapsto l t v) (at level 20).
Notation "´GV´ x ´@´ t ´|->´ l " := (Agvarmapsto x t l) (at level 20).
Notation "´LV´ x ´@´ t ´|->´ l " := (Alvarmapsto x t l) (at level 20).
Definition retasrt := option val -> asrt.
Definition reltaskst := prod taskst osabst.
Definition RstateOP := prod reltaskst absop.
Notation empenv := EnvMod.emp.
Notation empmem := MemMod.emp.
Definition emptaskst := fun (ts : taskst) =>
match ts with
| ((_,_,M),_,_) => M = empmem
end.
Notation empabst := OSAbstMod.emp.
Definition emposabst := fun st => st =empabst.
Definition empst (s : RstateOP) := match s with
| ((lo, ho), op) => emptaskst lo /\ emposabst ho
end.
Definition getmem (s : RstateOP) : mem :=
match s with
| ((lo, ho), op) => get_mem (get_smem lo)
end.
Definition getlenv (s : RstateOP) : env :=
match s with
| ((lo, ho), op) => get_lenv (get_smem lo)
end.
Definition getgenv (s : RstateOP) : env :=
match s with
| ((lo, ho), op) => get_genv (get_smem lo)
end.
Definition getabst (s : RstateOP) : osabst :=
match s with
| ((lo, ho), op) => ho
end.
Definition substabst (s : RstateOP) (o : osabst): RstateOP :=
match s with
| ((lo, ho), op) => ((lo ,o),op)
end.
Definition substaskst (st : taskst) (M : mem) : taskst :=
match st with
| ((G,E,M´),ir,aux) => ((G,E,M),ir,aux)
end.
Definition substaskstm (st:taskst) (M:mem):taskst:=
match st with
| ((G,E,M´),ir,aux) => ((G,E,M),ir,aux)
end.
Definition substmem (s : RstateOP) (M : mem): RstateOP :=
match s with
| ((lo, ho), op) => ((substaskst lo M ,ho),op)
end.
Definition substmo (s : RstateOP) (M : mem) (o : osabst): RstateOP :=
match s with
| ((lo, ho), op) => ((substaskst lo M , o),op)
end.
Definition getsmem (s : RstateOP) : smem := match s with
| ((lo, ho), op) => (get_smem lo)
end.
Definition gettaskst (s : RstateOP) : taskst :=
match s with
| ((lo, ho), op) => lo
end.
Definition getie (ts :taskst) :=
match ts with
| (_,_,(ie,_,_)) => ie
end.
Definition getis (ts :taskst) :=
match ts with
| (_,_,(_,is,_)) => is
end.
Definition getcs (ts :taskst) :=
match ts with
| (_,_,(_,_,cs)) => cs
end.
Definition getisr (ts :taskst) :=
match ts with
| (_,isr,_) => isr
end.
Definition getabsop (s : RstateOP) : absop :=
match s with
| ((lo, ho), op) => op
end.
Definition subabsop (s : RstateOP) (op : absop) : RstateOP :=
match s with
| (rs,_) => (rs ,op)
end.
Definition SysmemJoinM (m:smem) (M1:mem) (m´:smem):=
exists G E M0 M´, m = (G, E, M0) /\ m´ = (G,E,M´) /\ MemMod.join M0 M1 M´.
Definition joinmem (ts : taskst)(M : mem)(ts´ : taskst) : Prop :=
exists G E M1 M2 ir ls, ts = ((G, E, M1), ir, ls) /\
ts´ = ((G, E, M2), ir, ls) /\
MemMod.join M1 M M2.
Definition rval (e : expr) (v : val) (m : smem) := evalval e m = Some v /\ v <> Vundef.
Definition lval (e :expr) (v : val) (m : smem) := evaladdr e m = Some v /\ exists l, v = Vptr l.
Definition typecheck (e :expr) (t : type ) (m : smem) := evaltype e m = Some t.
Fixpoint typechklist (el : exprlist) (tl : typelist) (vl : vallist) (m : smem){struct el} :=
match el, tl, vl with
| nil,nil, nil => True
| cons e el´, cons t tl´, cons v vl´ => (rval e v) m /\ (typecheck e t) m /\ (typechklist el´ tl´ vl´) m
| _,_,_ => False
end.
Fixpoint evalexprlist (el : exprlist) (tl : typelist) (vl : vallist) (m : smem) {struct el} :=
match el, tl, vl with
| nil,nil, nil => True
| cons e el´, cons t tl´, cons v vl´ =>
evalval e m = Some v /\ evaltype e m = Some t
/\ evalexprlist el´ tl´ vl´ m /\ v <> Vundef
| _,_,_ => False
end.
Definition ptomval (l : addr) (v : memval) (M : mem) := M = MemMod.sig l v.
Open Local Scope Z_scope.
Fixpoint ptomvallist (l : addr) ( vl : mvallist) (M: mem) {struct vl} : Prop :=
match vl, l with
| nil, _ => M = MemMod.emp
| u:: vl´, (b, i) =>
exists M1 M2, MemMod.join M1 M2 M /\
ptomval l u M1 /\ ptomvallist ( b, (Z.add i 1%Z)) vl´ M2
end.
Definition mapstoval (l : addr) (t : type) (v : val) (m : mem) :=
exists vl, encode_val t v = vl /\ (ptomvallist l vl m).
Fixpoint arraymapstovallist (l : addr) (t : type) (vl : vallist) (m : mem){struct vl} :=
match vl with
| nil => m = MemMod.emp
| v :: vl´ => exists m1 m2,
MemMod.join m1 m2 m /\
(mapstoval l t v m1) /\
exists b i,
l = (b, i) /\ arraymapstovallist (b, (Z.add i (Z_of_nat (typelen t)))) t vl´ m2
end.
Fixpoint structmapstovallist (l : addr)(dls : decllist)
(vl : vallist) (m : mem){struct vl} :=
match vl, dls with
| nil,dnil => m = empmem
| v :: vl´, dcons id t dls´ =>
exists m1 m2,
MemMod.join m1 m2 m /\
(mapstoval l t v m1) /\
exists b i,
l = (b, i) /\ structmapstovallist
(b, (Z.add i (Z_of_nat (typelen t)))) dls´ vl´ m2
| _, _ => False
end.
Definition gettopis (ii : is) : hid := match ii with
| nil => INUM
| i :: is´ => i
end.
Definition eq_dom_env (E :env) (d : edom) : Prop :=
forall x t, set_In (x,t) d <-> exists l, EnvMod.get E x =Some (l,t).
The semantics of relational assertions.
Assertions are interpreted over relational states 'RstateOP',
which consist of the low-level task-local states 'taskst', the high-level
abstract states 'osabst', and the abstract statements 'absop' that the
low-level code needs to refine. 'osabst' and 'absop(spec_code)' are defined in
'/machine/language.v'. 'taskst' consists of a task-local view 'smem' of
program variables and memory, and also the global isr register and the
task-local interrupt states 'localst'. Here 'smem' contains the global
and local variables (G and E respectively) and the memory M.
Assertion 'Aemp' says the low-level memory and the high-level abstract state
are both empty. 'empE' further requires that the local variable environment be
empty too. 'Amapsto' specifies a singleton memory cell with 'v' stored in it.
'Aisr', 'Aie', 'Acs' and 'Ais' specify the value of the corresponding interrupt
status. 'ATopis' means that the currently running interrupt handler is at level k
(or k = N , meaning no running handlers). 'AHprio x t' says that, based on the
high-level abstract state, the abstract scheduler 'x' picks 't' as the target task.
'Aabsdata a b' specifies a singleton high-level abstract state mapping the data name
'a' to the abstract data 'b'. 'Aop s' means the current abstract statement remaining
to be refined is 's'. The separating conjunction 'Astar p1 p2' means 'p1' and 'p2'
hold over disjoint parts of a relational state. 'Alvarenv x t l' means variable 'x'
has type 't' and its location in memory is 'l'.
Fixpoint sat (s : RstateOP)(p : asrt) {struct p}:=
match p with
| Aemp => empst s
| [| vp |] => vp /\ empst s
| p //\\ q => sat s p /\ sat s q
| p \\// q => sat s p \/ sat s q
| Afalse => False
| Atrue => True
| Anot p => ~ sat s p
| p ** q => exists M1 M2 M o1 o2 o ,
M = getmem s /\ MemMod.join M1 M2 M
/\ o = getabst s /\ OSAbstMod.join o1 o2 o
/\ sat (substmo s M1 o1) p
/\ sat (substmo s M2 o2) q
| A_eval_expr e t v => evalval e (getsmem s) = Some v /\ evaltype e (getsmem s) = Some t /\ v <> Vundef
| A_eval_list el tl vl => evalexprlist el tl vl (getsmem s)
| Alval e t l => evaladdr e (getsmem s) = Some (Vptr l) /\
evaltype e (getsmem s) = Some t
| Alvarenv x t l => exists b,
EnvMod.get (getlenv s) x = Some (b,t) /\ l = (b,0%Z)/\
getmem s = empmem /\ emposabst (getabst s)
| Agvarenv x t l => exists b,
EnvMod.get (getgenv s) x = Some (b,t)/\ l = (b,0%Z) /\
getmem s = empmem /\ emposabst (getabst s)
| l # t |-> v => (mapstoval l t v) (getmem s) /\ emposabst (getabst s)
| Amapstolsval l t vl => match t with
| Tarray t´ n => n = length vl /\
arraymapstovallist l t´ vl (getmem s)/\ emposabst (getabst s)
| Tstruct id dls =>
structmapstovallist l dls vl (getmem s) /\ emposabst (getabst s)
| _ => False
end
| Agenv G => G = getgenv s
| A_dom_lenv d => eq_dom_env (getlenv s) d /\ empst s
| A_notin_lenv x => (~EnvMod.indom (getlenv s) x) /\ empst s
| Aistrue e => exists v, evalval e (getsmem s) = Some v /\
istrue v = Some true
| Aisfalse e => exists v, evalval e (getsmem s) = Some v /\
istrue v = Some false
| Aexists t p´ => exists (x : t), sat s (p´ x)
| AHprio sd tid => sd (getabst s) tid /\ emptaskst (gettaskst s)
| Aie i => getie (gettaskst s) = i /\ empst s
| Ais i => getis (gettaskst s) = i /\ empst s
| ATopis i => gettopis (getis (gettaskst s)) = i /\ empst s
| Aisr i => getisr (gettaskst s) = i /\ empst s
| Acs i => getcs (gettaskst s) = i /\ empst s
| <| op |> => getabsop s = op
| Aabsdata id absdata => OSAbstMod.sig id absdata = getabst s /\
emptaskst (gettaskst s)
end.
Notation "s ´|=´ P" := (sat s P) (at level 33, no associativity).
Notation "P ==> Q" :=
(forall s, s |= P -> s |= Q)
(at level 33, right associativity).
Notation "P <==> Q" :=
(forall s, s |= P <-> s |= Q)
(at level 33, right associativity).
Definition Aop´ a := Aop a //\\ Aemp.
Notation " <|| op ||> " := (Aop´ op) (at level 20).
Notation ieon := (Aie true) (only parsing).
Notation ieoff := (Aie false) (only parsing).
Notation "´OS´ [ isr , ie , is , cs ] " := ((Aisr isr) ** (Aie ie) ** (Ais is) ** (Acs cs))(at level 20).
Definition arfalse := fun (v : option val) => Afalse.
Fixpoint GoodInvAsrt (p : asrt ) {struct p}: Prop :=
match p with
| Aemp => True
| [| vp |] => True
| p´ //\\ q´ => GoodInvAsrt p´ /\ GoodInvAsrt q´
| p´ \\// q´ => GoodInvAsrt p´ /\ GoodInvAsrt q´
| p´ ** q´ => GoodInvAsrt p´ /\ GoodInvAsrt q´
| Afalse => True
| Atrue => True
| l # t |-> v => True
| Amapstolsval l t vl => True
| Aexists t p´ => forall x, GoodInvAsrt (p´ x)
| Aabsdata id absdata => True
| Agvarenv x t l => True
| Aisr _ => True
| Ais _ => True
| ATopis _ => True
| _ => False
end.
Fixpoint AbsOsEmpAsrt (p : asrt ) {struct p}: Prop :=
match p with
| Aemp => True
| [| vp |] => True
| p´ //\\ q´ => AbsOsEmpAsrt p´ /\ AbsOsEmpAsrt q´
| p´ \\// q´ => AbsOsEmpAsrt p´ /\ AbsOsEmpAsrt q´
| p´ ** q´ => AbsOsEmpAsrt p´ /\ AbsOsEmpAsrt q´
| l # t |-> v => True
| Aexists t p´ => forall x, AbsOsEmpAsrt (p´ x)
| Agvarenv x t l => True
| Alvarenv x t l => True
| Amapstolsval l t vl => True
| A_dom_lenv d => True
| A_notin_lenv x => True
| _ => False
end.
Fixpoint Emp_AbsOs_Asrt (p : asrt ) {struct p}: Prop :=
match p with
| Aemp => True
| [| vp |] => True
| p´ //\\ q´ => Emp_AbsOs_Asrt p´ /\ Emp_AbsOs_Asrt q´
| p´ \\// q´ => Emp_AbsOs_Asrt p´ /\ Emp_AbsOs_Asrt q´
| p´ ** q´ => Emp_AbsOs_Asrt p´ /\ Emp_AbsOs_Asrt q´
| l # t |-> v => True
| Aexists t p´ => forall x, Emp_AbsOs_Asrt (p´ x)
| Agvarenv x t l => True
| Alvarenv x t l => True
| Amapstolsval l t vl => True
| Aie i => True
| Ais i => True
| ATopis i => True
| Aisr i => True
| Acs i => True
| A_dom_lenv d => True
| A_notin_lenv x => True
| _ => False
end.
Definition get_isr_s (s:RstateOP):= match s with
| ((_, _, _, isr, _),_,_) => isr
end.
Definition get_is_s (s:RstateOP):= match s with
| ((_, _, _, _, (_,si,_)),_,_) => si
end.
Definition set_isr_s (s:RstateOP) (ir:isr) :=
match s with
| ((a,b,c,d,e),x,aop)=> ((a,b,c,ir,e),x,aop)
end.
Definition set_is_s (s:RstateOP) (si:is):=
match s with
| ((a,b,c,d,(ie,is,cs)),x,aop)=> ((a,b,c,d,(ie,si,cs)),x,aop)
end.
Definition set_isisr_s (s:RstateOP) (ir:isr) (si:is):=
match s with
| ((a,b,c,d,(ie,is,cs)),x,aop)=> ((a,b,c,ir,(ie,si,cs)),x,aop)
end.
Definition inv_isr_prop p:= (forall s, s |= p ->
forall i,(set_isr_s s (isrupd (get_isr_s s) i false)) |= p ) /\
(forall s, s|=p -> forall i, (set_isisr_s s (isrupd (get_isr_s s) i true) (i::(get_is_s s)))|=p) /\
(forall s i is, s|=p -> (get_isr_s s) i = false -> get_is_s s =i::is -> (set_is_s s is) |= p) /\
(forall s is ,s|=p -> (get_isr_s s = empisr) -> (set_is_s s is) |= p).
Definition precise (p : asrt) : Prop := forall s M1 M2 o1 o2 ,
sat (substmo s M1 o1) p -> sat (substmo s M2 o2) p ->
(forall M, MemMod.sub M1 M -> MemMod.sub M2 M -> M1 = M2) /\
(forall o, OSAbstMod.sub o1 o -> OSAbstMod.sub o2 o -> o1 = o2).
Definition inv_prop p := precise p /\ inv_isr_prop p.
Record invasrt := mkinvasrt {getinv : asrt; invp : GoodInvAsrt getinv; prec : inv_prop getinv}.
The defintion of the global invariant.
Share resoures are divided into N parts, Interrupt handlers at levels 0 to N −1
are assigned with resource blocks B0 , . . . , B n−1 respectively, and the
resource shared only by non-handler code is represented as B N . 'Inv' is
a mapping form {0,...,N} to the invaiant of each block respectively. The block
B k is specified by Inv k. We require that each invariate satisfying properties
'precise', 'inv_isr_prop' and 'GoodInvAsrt'. 'precise' means that invariate needs
to be precise which is similar to the definition fo separation logic. 'inv_isr_prop'
are some restrict of the invariate if it specifies 'localst'. 'GoodInvAsrt' is a
syntax checker which says that the invariant will not specify local symbol table and
the abstract statement.
Definition Inv:= hid -> invasrt.
Fixpoint starinv_isr (I : Inv) (low : hid) (n : hid){struct n} : asrt :=
match n with
| 0%nat =>
EX r : isr,
([|r low = true|] //\\ Aisr r) \\//
([|r low = false|] //\\ Aisr r) ** getinv (I low)
| S n´ =>
(EX r : isr,
([|r low = true|] //\\ Aisr r) \\//
([|r low = false|] //\\ Aisr r) ** getinv (I low)) **
starinv_isr I (S low) n´
end.
Definition II := fun (i : hid) => Aemp.
Fixpoint starinv_noisr (I : Inv) (low : hid) (n : hid){struct n} : asrt :=
match n with
| 0%nat => getinv (I low)
| S n´ => getinv (I low) ** starinv_noisr I (S low) n´
end.
Open Local Scope nat_scope.
Definition invlth_noisr (I : Inv) (low : hid) (high : hid) : asrt
:= starinv_noisr I low (high - low).
Definition invlth_isr (I : Inv) (low : hid) (high : hid) : asrt :=
starinv_isr I low (high- low).
Definition isrclr : asrt := EX r : isr, Aisr r //\\ [|forall i : hid, r i = false|].
Definition isr_inv : asrt :=
EX r : isr,
Aisr r //\\
(EX k : hid, ATopis k //\\ [|forall j : nat, 0 <= j < k -> r j = false|]).
Definition inv_ieon (I : Inv): asrt := Aie true ** invlth_isr I 0 INUM.
Definition inv_ieoff (I : Inv) : asrt :=
Aie false ** (EX k : hid, ATopis k ** (([| k < INUM|] ** (invlth_isr I (k + 1) INUM))\\// [|k = INUM|])) .
Definition iret_ieon : asrt := isr_inv //\\ (Aie true).
Definition iret_ieoff (I : Inv) : asrt :=
(isr_inv //\\ Aie false) **
(EX (ii : is) (k : nat), [|hd_error ii = Some k|] ** Ais ii ** invlth_isr I 0 k).
Definition INV (I : Inv) : asrt :=
getinv (I (S INUM)) ** (inv_ieon I \\// inv_ieoff I).
Definition SWPRE (sd : ossched )(x: var) : asrt :=
EX t tc: tid, AHprio sd t ** isrclr ** (EX tp : type, Agvarmapsto x (Tptr tp) (Vptr t)) ** (EX tp : type, Agvarmapsto OSTCBCur (Tptr tp) (Vptr tc)) ** Atrue.
Definition SWINV(I : Inv) : asrt :=
(isrclr ** Aie false) ** (EX k : hid, ATopis k ** invlth_isr I 0 k).
Definition RDYINV(I : Inv) : asrt :=
(Aie true //\\ isrclr) \\// SWINV I.
Definition IRINV (I : Inv) : asrt :=
iret_ieon \\// iret_ieoff I.
Definition InitTaskAsrt : asrt :=
(Aie true //\\ Ais nil) //\\ Acs nil.
Fixpoint GoodFrame (p : asrt){struct p}: Prop :=
match p with
| Aemp => True
| [| vp |] => True
| p´ //\\ q´ => GoodFrame p´ /\ GoodFrame q´
| p´ \\// q´ => GoodFrame p´ /\ GoodFrame q´
| p´ ** q´ => GoodFrame p´ /\ GoodFrame q´
| l # t |-> v => True
| Amapstolsval l t vl => True
| Aexists t p´ => forall x, GoodFrame (p´ x)
| _ => False
end.
Fixpoint GoodFunAsrt (p : asrt) : Prop :=
match p with
| Aemp => True
| [| P |] => True
| Afalse => True
| Atrue => True
| l # t |-> v => True
| Amapstolsval l t vl => True
| Agvarenv x t l => True
| AHprio sd t => True
| Aie ie => True
| Ais is => True
| ATopis id => True
| Aisr isr => True
| Acs cs => True
| Aabsdata id data => True
| Aconj p´ q´ => GoodFunAsrt p´ /\ GoodFunAsrt q´
| Adisj p´ q´ => GoodFunAsrt p´ /\ GoodFunAsrt q´
| Astar p´ q´ => GoodFunAsrt p´ /\ GoodFunAsrt q´
| Aexists t p´ => forall x, GoodFunAsrt (p´ x)
| Aop _ => True
| _ => False
end.
Fixpoint can_change_aop (p:asrt) :=
match p with
| Astar p1 p2 => (can_change_aop p1) /\ (can_change_aop p2)
| p1 //\\ p2 => (can_change_aop p1) /\ (can_change_aop p2)
| p1 \\// p2 => (can_change_aop p1) /\ (can_change_aop p2)
| Aop aop => False
| Anot p´ => False
| Aexists t p´ => forall x : t, can_change_aop (p´ x)
| _ => True
end.
Theorem change_aop_rule:
forall o O aop aop´ P,
(o,O,aop) |= P -> can_change_aop P -> (o,O,aop´) |= P.
Inductive EventData :=
| DMsgQ : val -> vallist->vallist->vallist-> EventData
| DSem : int32 -> EventData
| DMbox: msg -> EventData
| DMutex: val -> val -> EventData.
The logical variables.
Inductive logicvar:=
| logic_isr: isr -> logicvar
| logic_is: is -> logicvar
| logic_ie: ie -> logicvar
| logic_cs: cs -> logicvar
| logic_hid: hid -> logicvar
| logic_val: val -> logicvar
| logic_lv: vallist -> logicvar
| logic_llv: list vallist -> logicvar
| logic_leventd: list EventData -> logicvar
| logic_leventc:list EventCtr -> logicvar
| logic_abstcb: TcbMod.map -> logicvar
| logic_absecb: EcbMod.map -> logicvar
| logic_code : spec_code -> logicvar.
| logic_isr: isr -> logicvar
| logic_is: is -> logicvar
| logic_ie: ie -> logicvar
| logic_cs: cs -> logicvar
| logic_hid: hid -> logicvar
| logic_val: val -> logicvar
| logic_lv: vallist -> logicvar
| logic_llv: list vallist -> logicvar
| logic_leventd: list EventData -> logicvar
| logic_leventc:list EventCtr -> logicvar
| logic_abstcb: TcbMod.map -> logicvar
| logic_absecb: EcbMod.map -> logicvar
| logic_code : spec_code -> logicvar.
The specifications of internal functions.
The specification of each internal function 'fspec' consists of a funcion
precondition 'fpre', a function post condition 'fpost' and the function's type 'ftype'.
'fpre' is mapping from a value list and a logic variable list to a funcion assertion.
the value list is used to specify the values of function arguments, the logic variable
list is used to extend expressibility of funcion specs, like we can use the same list
in pre and post condition to say that some global variable will not be change by the
function. 'ftype' consists of the type of return value and the type of arguments.
We require that the function assertion will not specify local variable table.
Record funasrt: Type := mkfunasrt{getasrt : asrt ; getprop : GoodFunAsrt getasrt}.
Definition fpre := vallist -> list logicvar -> funasrt.
Definition fpost := vallist -> option val -> list logicvar -> funasrt.
Open Scope type_scope.
Definition fspec := (fpre * fpost * funtype ).
Definition funspec := fid -> option fspec.
Notation "´PRE´ [ p , vl , logicl ]" := (getasrt (p vl logicl))(at level 20).
Notation "´POST´ [ p , vl , v , logicl ] " := (getasrt (p vl v logicl))(at level 20, vl at next level).