Require Import List.
Import ListNotations.
Require Import Relations.
Require Import util.
Require Import specification.
LOG: Device operations logging
Module LOG.
Type of operation logs, and initial log.
Parameter t :
Type.
Parameter init:
t.
Add an operation to a log.
Parameter log:
t ->
DEV.ops ->
t.
Adding a list of operations to a log.
Definition log_ops (
l:
LOG.t) (
t:
list DEV.ops) (
l':
LOG.t) :=
fold_left LOG.log t l =
l'.
Restoring a peripheral device state from a log.
Parameter restore:
t ->
DEV.t.
Below are the required and derived properties of the operation logging.
Axiom restore_init:
DEV.equiv (
restore init)
DEV.init.
Axiom restore_log:
forall l dev dev'
op,
DEV.equiv (
restore l)
dev ->
DEV.op_sem (
projT1 op)
dev (
projT2 op)
dev' ->
DEV.equiv (
restore (
log l op))
dev'.
Lemma restore_log_trace :
forall t l dev dev',
DEV.ops_sem t dev dev' ->
DEV.equiv (
restore l)
dev ->
DEV.equiv (
restore (
fold_left log t l))
dev'.
Proof.
induction t0 ;
intros.
-
simpl.
inv H.
auto.
-
simpl.
inv H.
eapply IHt0;
eauto using equiv_refl.
eapply restore_log;
eauto.
Qed.
End LOG.
CHKPT: Non-volatile checkpointing storage
Module CHKPT.
Type definition for non-volatile checkpointing storage.
Record t :=
CHKPT {
last_mcu :
MCU.t ;
last_log :
LOG.t ;
next_mcu :
MCU.t ;
next_log :
LOG.t }.
Initial non-volatile checkpointing storage.
Definition init:
t :=
CHKPT MCU.init LOG.init
MCU.init LOG.init.
Committing the next snapshot as the last valid snapshot.
Definition set (
chkpt:
t):
t :=
CHKPT chkpt.(
next_mcu)
chkpt.(
next_log)
chkpt.(
next_mcu)
chkpt.(
next_log).
Discarding the next snapshot by resetting it to the last valid snapshot.
Definition reset (
chkpt:
t):
t :=
CHKPT chkpt.(
last_mcu)
chkpt.(
last_log)
chkpt.(
last_mcu)
chkpt.(
last_log).
Updating the next log.
Definition saveNextLog (
chkpt:
t)(
l:
LOG.t):
t :=
CHKPT chkpt.(
last_mcu)
chkpt.(
last_log)
chkpt.(
next_mcu)
l.
Updating the next MCU snapshot.
Definition saveNextMCU (
chkpt:
t)(
mcu:
MCU.t):
t :=
CHKPT chkpt.(
last_mcu)
chkpt.(
last_log)
mcu chkpt.(
next_log).
End CHKPT.
PLF
Interrupt-based checkpointing model with failures. It is non-deterministic in
-
the success/failure of checkpointing
-
the occurrence of power-loss interrupts inside power-continuous sections.
Module PLF.
PLF execution states.
Inductive state :=
|
INIT :
state (* initial state *)
|
USR :
MCU.t ->
DEV.t ->
CHKPT.t ->
state (* user-mode state *)
|
DRV :
MCU.t ->
DEV.t ->
LOG.t ->
CHKPT.t ->
state (* driver mode *)
|
PWR :
CHKPT.t ->
state (* power-loss interrupt raised *)
|
OFF :
CHKPT.t ->
state.
(* power ran out *)
PLF observable events.
Inductive event :=
|
ChkptS:
event (* checkpoint success *)
|
ChkptF:
event (* checkpoint failure *)
|
LogS :
event (* power-continuous section completed *)
|
LogF :
event (* power-continuous section aborted *)
|
Op :
DEV.ops ->
event.
(* device operation *)
Definition trace :=
list event.
Transition relation.
Inductive step :
state ->
trace ->
state ->
Prop :=
|
step_firstboot:
step INIT
[]
(
USR MCU.init DEV.init CHKPT.init)
|
sem_usr:
forall mcu mcu'
dev dev'
chkpt t,
forall (
INSTR:
SPEC.step (
SPEC.STATE SPEC.Usr mcu dev)
t
(
SPEC.STATE SPEC.Usr mcu'
dev')),
step (
USR mcu dev chkpt)
(
map Op t)
(
USR mcu'
dev'
chkpt)
|
sem_enter:
forall mcu mcu'
dev dev'
chkpt chkpt'
t l,
forall (
INSTR:
SPEC.step (
SPEC.STATE SPEC.Usr mcu dev)
t
(
SPEC.STATE SPEC.Drv mcu'
dev'))
(
RUNTIME1:
CHKPT.saveNextMCU chkpt mcu =
chkpt')
(
RUNTIME2:
l =
CHKPT.next_log chkpt),
step (
USR mcu dev chkpt)
(
map Op t)
(
DRV mcu'
dev'
l chkpt')
|
sem_drv:
forall mcu mcu'
dev dev'
l l'
chkpt t,
forall (
INSTR:
SPEC.step (
SPEC.STATE SPEC.Drv mcu dev)
t
(
SPEC.STATE SPEC.Drv mcu'
dev'))
(
RUNTIME:
LOG.log_ops l t l'),
step (
DRV mcu dev l chkpt)
(
map Op t)
(
DRV mcu'
dev'
l'
chkpt)
|
sem_leave:
forall mcu mcu'
dev dev'
l chkpt chkpt'
t,
forall (
INSTR:
SPEC.step (
SPEC.STATE SPEC.Drv mcu dev)
t
(
SPEC.STATE SPEC.Usr mcu'
dev'))
(
RUNTIME:
CHKPT.saveNextLog chkpt l =
chkpt'),
step (
DRV mcu dev l chkpt)
(
map Op t ++ [
LogS])
(
USR mcu'
dev'
chkpt')
|
sem_pwr_usr:
forall mcu dev chkpt chkpt',
forall (
RUNTIME:
CHKPT.saveNextMCU chkpt mcu =
chkpt'),
step (
USR mcu dev chkpt)
[]
(
PWR chkpt')
|
sem_pwr_drv:
forall chkpt mcu dev l,
step (
DRV mcu dev l chkpt)
[
LogF]
(
PWR chkpt)
|
sem_chkpt_success:
forall chkpt chkpt',
forall (
RUNTIME:
CHKPT.set chkpt =
chkpt'),
step (
PWR chkpt)
[
ChkptS]
(
OFF chkpt')
|
sem_chkpt_failure:
forall chkpt,
step (
PWR chkpt)
[
ChkptF]
(
OFF chkpt)
|
sem_reboot:
forall chkpt dev mcu chkpt',
forall (
RUNTIME1:
mcu =
CHKPT.last_mcu chkpt)
(
RUNTIME2:
dev =
LOG.restore (
CHKPT.last_log chkpt))
(
RUNTIME3:
chkpt' =
CHKPT.reset chkpt),
step (
OFF chkpt)
[]
(
USR mcu dev chkpt')
|
sem_usr_off:
forall mcu dev chkpt,
step (
USR mcu dev chkpt)
[
ChkptF]
(
OFF chkpt)
|
sem_drv_off:
forall chkpt mcu dev l,
step (
DRV mcu dev l chkpt)
[
ChkptF]
(
OFF chkpt)
.
Trace semantics.
Definition sem (
t:
list event):
Prop :=
exists s,
run step INIT t s.
End PLF.