Require Import List.
Import ListNotations.
Require Import Relations.
Require Import util.
Require Import specification.
Require Import plf.
Require Import PLFO.
Require Import PL.
PLO
Interrupt-based checkpointing without checkpointing failures. An
oracle dictates power-loss interrupts occurring during
power-continuous sections.
PLO state are the same as for PLFO machines. This
notation is only here for readability.
Notation PLOstate :=
PLFO.state.
PLO observable events are the same as in the SPEC machine.
Definition trace :=
SPEC.trace.
Transition relation.
Inductive step :
state ->
trace ->
state ->
Prop :=
|
sem_firstboot:
forall oracle,
step (
INIT oracle)
[]
(
USR oracle MCU.init DEV.init CHKPT.init)
|
sem_usr:
forall oracle 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 oracle mcu dev chkpt)
t
(
USR oracle mcu'
dev'
chkpt)
|
sem_enter:
forall oracle 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 oracle mcu dev chkpt)
t
(
DRV oracle mcu'
dev'
l chkpt')
|
sem_drv:
forall oracle b 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 (
b ::
oracle)
mcu dev l chkpt)
(
if b then t else [])
(
DRV (
b ::
oracle)
mcu'
dev'
l'
chkpt)
|
sem_leave:
forall oracle 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 (
true ::
oracle)
mcu dev l chkpt)
t
(
USR oracle mcu'
dev'
chkpt')
|
sem_pwr_usr:
forall oracle mcu dev chkpt chkpt',
forall (
RUNTIME:
CHKPT.saveNextMCU chkpt mcu =
chkpt'),
step (
USR oracle mcu dev chkpt)
[]
(
PWR oracle chkpt')
|
sem_pwr_drv:
forall oracle chkpt mcu dev l,
step (
DRV (
false ::
oracle)
mcu dev l chkpt)
[]
(
PWR oracle chkpt)
|
sem_chkpt_success:
forall oracle chkpt chkpt',
forall (
RUNTIME:
CHKPT.set chkpt =
chkpt'),
step (
PWR oracle chkpt)
[]
(
OFF oracle chkpt')
|
sem_reboot:
forall oracle 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 oracle chkpt)
[]
(
USR oracle mcu dev chkpt').
Trace semantics.
Definition sem (
o:
oracle)(
t:
trace):
Prop :=
exists s,
run step (
INIT o)
t s.