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.
Require Import PLF_PLFO.
Require Import PLFO_PL.
Require Import PL_PLO.
Require Import PLO_SPEC.
Require PLF_SPEC.
Final correctness theorem, with explicit trace filtering
The final correctness result can be alternatively stated using an
operational characterization of the subtrace relation.
Given the trace emitted by the PLF machine, the corresponding
subtrace emitted by the SPEC machine can be explicitly built with
the filter function:
∀ t. PLF.sem t -> SPEC.sem (filter t).
Defining the filter function
Filtering portions of trace from failing checkpointing
Fixpoint split_at_chkpt_events (
t:
PLF.trace) :
list (
bool *
PL.trace) :=
match t with
| [] => []
|
PLF.ChkptS::
t => (
true, []) :: (
split_at_chkpt_events t)
|
PLF.ChkptF::
t => (
false, []) :: (
split_at_chkpt_events t)
|
e::
t =>
match split_at_chkpt_events t with
| [] => [(
false,
match e with
|
PLF.LogS => [
PL.LogS]
|
PLF.LogF => [
PL.LogF]
|
PLF.Op op => [
PL.Op op]
|
_ => []
end)]
| (
b,
x)::
m => (
b,
match e with
|
PLF.LogS =>
PL.LogS::
x
|
PLF.LogF =>
PL.LogF::
x
|
PLF.Op op => (
PL.Op op)::
x
|
_ => []
end)::
m
end
end.
Fixpoint x_filter_chkpt (
t:
list (
bool *
PL.trace)) :
PL.trace :=
match t with
| [] => []
| (
true,
t')::
t =>
t'++
x_filter_chkpt t
| (
false,
_ )::
t =>
x_filter_chkpt t
end.
Definition filter_chkpt (
t:
PLF.trace) :
PL.trace :=
x_filter_chkpt (
split_at_chkpt_events t).
Filtering portions of PL.trace from aborted power-continuous sections.
Fixpoint split_at_log_events (
t:
PL.trace) :
list (
bool *
SPEC.trace) :=
match t with
| [] => []
|
PL.LogS::
t => (
true, []) :: (
split_at_log_events t)
|
PL.LogF::
t => (
false, []) :: (
split_at_log_events t)
|
PL.Op op::
t =>
match split_at_log_events t with
| [] => [(
false, [
op])]
| (
b,
x)::
m => (
b,
op::
x)::
m
end
end.
Fixpoint x_filter_log (
t:
list (
bool *
SPEC.trace)) :
SPEC.trace :=
match t with
| [] => []
| (
true,
t')::
t =>
t' ++
x_filter_log t
| (
false,
_ )::
t =>
x_filter_log t
end.
Definition filter_log (
t:
PL.trace) :
SPEC.trace :=
x_filter_log (
split_at_log_events t).
The final filter function
Definition filter (
t:
PLF.trace) :
SPEC.trace :=
filter_log (
filter_chkpt t).
Properties of the filter_chkpt function.
Properties of the auxiliary split_at_chkpt_events function.
Lemma split_at_chkpt_events_ops_nil :
forall top,
forall b pt,
In (
b,
pt) (
split_at_chkpt_events (
map PLFevent top)) ->
b =
false.
Proof.
induction top;
intros.
-
inv H.
-
destruct a;
simpl in *.
+
destruct split_at_chkpt_events.
*
inv H;
try congruence.
inv H0.
*
destruct p.
inv H.
--
inv H0.
eapply IHtop;
eauto with datatypes.
--
eapply IHtop;
eauto with datatypes.
+
destruct split_at_chkpt_events.
*
inv H;
try congruence.
inv H0.
*
destruct p.
inv H.
--
inv H0.
eapply IHtop;
eauto with datatypes.
--
eapply IHtop;
eauto with datatypes.
+
destruct split_at_chkpt_events.
*
inv H;
try congruence.
inv H0.
*
destruct p.
inv H.
--
inv H0.
eapply IHtop;
eauto with datatypes.
--
eapply IHtop;
eauto with datatypes.
Qed.
Lemma split_at_chkpt_events_split_F :
forall top tend,
split_at_chkpt_events (
map PLFevent top ++
PLF.ChkptF ::
tend) =
(
false,
top)::
split_at_chkpt_events tend.
Proof.
Lemma split_at_chkpt_events_split_S :
forall top tend,
split_at_chkpt_events (
map PLFevent top ++
PLF.ChkptS ::
tend) =
(
true,
top)::
split_at_chkpt_events tend.
Proof.
Lemma x_filter_chkpt_false :
forall l,
(
forall b x,
In (
b,
x)
l ->
b =
false) ->
x_filter_chkpt l = [].
Proof.
induction l ; intros.
- auto.
- simpl. destruct a.
rewrite (H b t); eauto with datatypes.
Qed.
Lemmas characterizing the filtering action of filter_chkpt
Lemma filter_chkpt_ops_nil:
forall top,
filter_chkpt (
map PLFevent top) = [].
Proof.
Lemma filter_chkpt_false :
forall top tend,
filter_chkpt (
map PLFevent top ++
PLF.ChkptF ::
tend) =
filter_chkpt tend.
Proof.
Lemma filter_chkpt_true :
forall top tend,
filter_chkpt (
map PLFevent top ++
PLF.ChkptS ::
tend) =
top ++
filter_chkpt tend.
Proof.
Alternative induction principle to reason about PLF traces.
Inductive PLFtrace :
PLF.trace ->
Prop :=
|
plftrace_op :
forall op,
PLFtrace (
map PLFevent op)
|
plftrace_chkptS :
forall op tend,
PLFtrace tend ->
PLFtrace ((
map PLFevent op)++
PLF.ChkptS::
tend)
|
plftrace_chkptF :
forall op tend,
PLFtrace tend ->
PLFtrace ((
map PLFevent op)++
PLF.ChkptF::
tend).
Lemma PLFtrace_ind' :
forall t,
PLFtrace t.
Proof.
The filter_chkpt is correct for the subtrace_chk relation
Lemma filter_chkpt_correct:
forall t,
exists b,
subtrace_chk b t (
filter_chkpt t).
Proof.
The subtrace_chk co-domain is populated with traces filtered
with filter_chkpt.
Lemma filter_chkpt_complete :
forall t b t',
subtrace_chk b t t' ->
t' =
filter_chkpt t.
Proof.
Properties of the filter_log function.
Properties of the auxiliary split_at_log_events function.
Lemma split_at_log_events_ops_nil :
forall top,
forall b pt,
In (
b,
pt) (
split_at_log_events (
map Op top)) ->
b =
false.
Proof.
induction top;
intros.
-
inv H.
-
simpl in *.
destruct split_at_log_events.
+
inv H;
inv H0.
auto.
+
destruct p.
inv H.
--
inv H0.
eapply IHtop;
eauto with datatypes.
--
eapply IHtop;
eauto with datatypes.
Qed.
Lemma split_at_log_events_split_F :
forall top tend,
split_at_log_events (
map Op top ++
LogF ::
tend) =
(
false,
top)::
split_at_log_events tend.
Proof.
induction top;
intros.
-
simpl.
auto.
-
simpl.
case_eq (
split_at_log_events (
map Op top ++
LogF ::
tend));
intros.
*
rewrite IHtop in H;
eauto.
congruence.
*
rewrite IHtop in H;
eauto.
inv H.
auto.
Qed.
Lemma split_at_log_events_split_S :
forall top tend,
split_at_log_events (
map Op top ++
LogS ::
tend) =
(
true,
top)::
split_at_log_events tend.
Proof.
induction top;
intros.
-
simpl.
auto.
-
simpl.
case_eq (
split_at_log_events (
map Op top ++
LogS ::
tend));
intros.
*
rewrite IHtop in H;
eauto.
congruence.
*
rewrite IHtop in H;
eauto.
inv H.
auto.
Qed.
Lemma x_filter_log_false :
forall l,
(
forall b x,
In (
b,
x)
l ->
b =
false) ->
x_filter_log l = [].
Proof.
induction l ; intros.
- auto.
- simpl. destruct a.
rewrite (H b t); eauto with datatypes.
Qed.
Lemmas characterizing the filtering action of filter_log.
Lemma filter_log_ops_nil:
forall top,
filter_log (
map Op top) = [].
Proof.
Lemma filter_log_false :
forall top tend,
filter_log (
map Op top ++
LogF ::
tend) =
filter_log tend.
Proof.
Lemma filter_log_true :
forall top tend,
filter_log (
map Op top ++
LogS ::
tend) =
top ++
filter_log tend.
Proof.
Alternative induction principle to reason about PL traces.
Inductive PLtrace :
PL.trace ->
Prop :=
|
pltrace_op :
forall op,
PLtrace (
map PL.Op op)
|
pltrace_LogS :
forall op tend,
PLtrace tend ->
PLtrace ((
map PL.Op op)++
LogS::
tend)
|
pltrace_LogF :
forall op tend,
PLtrace tend ->
PLtrace ((
map PL.Op op)++
LogF::
tend).
Lemma PLtrace_ind' :
forall t,
PLtrace t.
Proof.
The filter_log is correct for the subtrace_log relation
Lemma filter_log_correct:
forall t,
exists b,
subtrace_log b t (
filter_log t).
Proof.
The subtrace_log co-domain is populated with traces filtered
with filter_log.
Lemma filter_log_complete :
forall t b t',
subtrace_log b t t' ->
t' =
filter_log t.
Proof.
filter functionally characterizes the subtrace relation
filter is a correct implementation of subtrace
Lemma filter_correct:
forall t,
PLF_SPEC.subtrace t (
filter t).
Proof.
filter is a complete implementation of subtrace
Lemma filter_complete:
forall t t',
PLF_SPEC.subtrace t t' ->
t' =
filter t.
Proof.
Final correctness result, with explicit trace filtering
Theorem correctness_final:
forall t,
PLF.sem t ->
SPEC.sem (
filter t).
Proof.