Require Import List.
Import ListNotations.
Require Import Relations.
Require Import util.
Require Import specification.
Require Import plf.
Require Import PLFO.
Require Import PL.
Require Import PLO.
Refinement between PL and PLO machines
We can remove the non-determinism from PL by introducing the
oracle for power-loss interrupts occurring during power-continuous
sections.
The refinement lemma is at the end of this file, stating that
forall trace t, PL.sem t -> ∃ o t', PLO.sem o t' ∧ ∃ b,
subtrace_log b t t'.
Subtrace relation
Definition of subtrace_log filtering out portions of trace
ending with a aborted power-continuous section.
Inductive subtrace_log :
bool ->
PL.trace ->
PLO.trace ->
Prop :=
|
committed_end :
forall b t t',
subtrace_log b t t' ->
subtrace_log true (
PL.LogS ::
t)
t'
|
committed_cons :
forall e t t',
subtrace_log true t t' ->
subtrace_log true (
PL.Op e ::
t) (
e ::
t')
|
ignored_nil :
subtrace_log false [] []
|
ignored_end :
forall b t t',
subtrace_log b t t' ->
subtrace_log false (
PL.LogF ::
t)
t'
|
ignored_cons :
forall e t t',
subtrace_log false t t' ->
subtrace_log false (
PL.Op e ::
t)
t'.
Unicity property for the subtrace_log relation
Lemma subtrace_log_unique:
forall b t t',
subtrace_log b t t' ->
forall b'
t'',
subtrace_log b'
t t'' ->
b' =
b /\
t'' =
t'.
Proof.
induction 1; intros.
- inv H0.
apply IHsubtrace_log in H3; auto.
intuition.
- inv H0.
+ apply IHsubtrace_log in H5; auto.
intuition.
congruence.
+ apply IHsubtrace_log in H5; auto.
intuition.
congruence.
- inv H; auto.
- inv H0.
apply IHsubtrace_log in H3; auto.
intuition.
- inv H0; auto.
apply IHsubtrace_log in H5; auto.
intuition.
congruence.
Qed.
Lemma subtrace_log_concat:
forall b t t',
subtrace_log b t t' ->
forall e,
if b then subtrace_log b (
map PL.Op e ++
t) (
e ++
t')
else subtrace_log b (
map PL.Op e ++
t)
t'.
Proof.
induction e ; intros.
- simpl. destruct b; auto.
- destruct b.
+ simpl. econstructor; eauto.
+ simpl. econstructor; eauto.
Qed.
Lemma subtrace_log_ops:
forall op,
subtrace_log false (
map PL.Op op) [].
Proof.
induction op.
- constructor.
- simpl. econstructor; eauto.
Qed.
Alternative, equivalent definition of the subtrace relation subtrace_log,
easier to use in the proof of refinement.
Inductive subtrace_log_alt :
bool ->
PL.trace ->
PLO.trace ->
Prop :=
|
committed_aend :
forall b t t',
subtrace_log_alt b t t' ->
subtrace_log_alt true (
PL.LogS ::
t)
t'
|
committed_acons :
forall e t t',
subtrace_log_alt true t t' ->
subtrace_log_alt true (
map PL.Op e ++
t) (
e ++
t')
|
ignored_anil :
subtrace_log_alt false [] []
|
ignored_aend :
forall b t t',
subtrace_log_alt b t t' ->
subtrace_log_alt false (
PL.LogF ::
t)
t'
|
ignored_acons :
forall e t t',
subtrace_log_alt false t t' ->
subtrace_log_alt false (
map PL.Op e ++
t)
t'.
Lemma subtrace_log_subtrace_log_alt :
forall b t t',
subtrace_log b t t' ->
subtrace_log_alt b t t'.
Proof.
induction 1;
intros;
try solve [
econstructor;
eauto].
-
replace (
PL.Op e ::
t)
with (
map PL.Op (
e::
nil) ++
t)
by auto with datatypes.
replace (
e::
t')
with ([
e] ++
t')
by auto with datatypes.
econstructor ;
eauto.
-
replace (
PL.Op e ::
t)
with (
map PL.Op (
e::
nil) ++
t)
by auto with datatypes.
econstructor ;
eauto.
Qed.
Lemma subtrace_log_alt_subtrace_log:
forall b t t',
subtrace_log_alt b t t' ->
subtrace_log b t t'.
Proof.
Refinement proof
Converting a PL state into a PLO state by including the oracle.
Definition lift_log (
o :
oracle) (
s:
PLstate):
PLOstate :=
match s with
|
PLF.INIT =>
PLFO.INIT o
|
PLF.USR x x0 x1 =>
PLFO.USR o x x0 x1
|
PLF.DRV x x0 x1 x2 =>
PLFO.DRV o x x0 x1 x2
|
PLF.PWR x =>
PLFO.PWR o x
|
PLF.OFF x =>
PLFO.OFF o x
end.
Helper lemma to reason about the empty oracle -- the empty trace
is produced.
Lemma empty_run:
forall s t s',
(
exists s0,
lift_log []
s0 =
s) ->
run PLO.step s t s' ->
exists s'2,
t = [] /\
lift_log []
s'2 =
s'.
Proof.
Helper lemma to exhibit the oracle generating the subtrace.
Lemma gen_logging_oracle :
forall si t sf,
run_right PL.step si t sf ->
exists
(
o :
oracle) (
t' :
list DEV.ops)
(
sf' :
PLFO.state),
run PLO.step (
lift_log o si)
t'
sf'
/\
match o with
| [] =>
subtrace_log_alt false t t'
|
true ::
_ =>
subtrace_log_alt true t t'
|
false ::
_ =>
subtrace_log_alt false t t'
end.
Proof.
intros.
induction H.
-
exists [].
exists [].
exists (
lift_log []
x).
repeat split;
try eapply run_refl;
econstructor.
-
enough (
CASE x t1 y); [|
constructor].
destruct IHrun_right as [
o [
t' [
sf' [
Hrun Hsub]]]].
destruct STEP.
+
simpl.
eexists o.
eexists t'.
eexists sf'.
repeat split;
auto.
change t'
with ([] ++
t').
eapply run_trans;
eauto.
eapply run_step;
econstructor;
eauto.
+
simpl.
eexists o.
eexists t'.
eexists sf'.
pose proof (
SPEC.axiom_usr _ _ _ _ _ INSTR)
as [-> ->].
repeat split;
auto.
change t'
with ([] ++
t').
eapply run_trans;
eauto.
eapply run_step;
econstructor;
eauto.
+
destruct o; [|
destruct b].
*
eexists.
eexists.
eexists.
pose proof (
SPEC.axiom_enter _ _ _ _ _ INSTR)
as [-> [-> ->]].
repeat split;
eauto.
eapply run_trans;
eauto.
eapply run_step.
econstructor;
eauto.
simpl.
assumption.
*
eexists.
eexists.
eexists.
pose proof (
SPEC.axiom_enter _ _ _ _ _ INSTR)
as [-> [-> ->]].
repeat split;
eauto.
eapply run_trans;
eauto.
eapply run_step.
econstructor;
eauto.
simpl.
assumption.
*
eexists.
eexists.
eexists.
pose proof (
SPEC.axiom_enter _ _ _ _ _ INSTR)
as [-> [-> ->]].
repeat split;
eauto.
eapply run_trans;
eauto.
eapply run_step.
econstructor;
eauto.
simpl.
assumption.
+
destruct o; [|
destruct b].
*
eexists [].
eexists [].
exists ((
lift_log [] (
PLF.DRV mcu dev l chkpt))).
repeat split.
--
eapply run_refl.
--
apply ignored_acons.
apply empty_run in Hrun as [
_ [->
_]];
auto.
eexists;
eauto.
*
eexists (
true ::
o).
eexists (
t ++
t').
eexists sf'.
repeat split;
eauto.
--
simpl.
eapply run_trans;
eauto.
eapply run_step.
simpl.
change t with (
if true then t else []).
eapply PLO.sem_drv;
eauto.
--
econstructor.
auto.
*
exists (
false ::
o).
exists ([] ++
t').
exists sf'.
repeat split;
eauto.
++
eapply run_trans;
eauto.
eapply run_step.
simpl.
change []
with (
if false then t else []).
eapply PLO.sem_drv;
eauto.
++
econstructor;
auto.
+
eexists.
eexists.
eexists.
pose proof (
SPEC.axiom_leave _ _ _ _ _ INSTR)
as [-> [-> ->]].
repeat split;
eauto.
eapply run_trans;
eauto.
eapply run_step.
econstructor;
eauto.
simpl.
destruct o; [|
destruct b];
(
econstructor;
eauto).
+
eexists.
eexists.
eexists.
repeat split;
eauto.
simpl.
change t'
with ([] ++
t').
eapply run_trans;
eauto.
eapply run_step.
econstructor;
eauto.
+
eexists (
false ::
o).
eexists ([] ++
t').
eexists.
repeat split;
eauto.
--
eapply run_trans;
eauto.
eapply run_step.
apply PLO.sem_pwr_drv.
--
simpl.
destruct o; [|
destruct b]; (
econstructor;
eauto).
+
eexists.
eexists.
eexists.
repeat split;
eauto.
simpl.
change t'
with ([] ++
t').
eapply run_trans;
eauto.
eapply run_step.
econstructor;
eauto.
+
eexists.
eexists.
eexists.
repeat split;
eauto.
simpl.
change t'
with ([] ++
t').
eapply run_trans;
eauto.
eapply run_step.
econstructor;
eauto.
Qed.
Validity of logging oracle.
Lemma logging_validity :
forall t,
PL.sem t ->
exists o t',
PLO.sem o t' /\
exists b,
subtrace_log b t t'.
Proof.