Require Import List.
Import ListNotations.
Require Import Relations.
Require Import util.
Require Import specification.
Require Import plf.
Require Import PL.
PLFO.
Interrupt-based checkpointing with failures, with checkpointing
oracle. Non-deterministic in the way power-continuous sections get
interrupted by power-loss interrupts.
PLFO execution states are PLF states, augmented with an checkpointing oracle.
Inductive state :=
|
INIT :
oracle ->
state
|
USR :
oracle ->
MCU.t ->
DEV.t ->
CHKPT.t ->
state
|
DRV :
oracle ->
MCU.t ->
DEV.t ->
LOG.t ->
CHKPT.t ->
state
|
PWR :
oracle ->
CHKPT.t ->
state
|
OFF :
oracle ->
CHKPT.t ->
state.
PLFO observable events are the same as in the PL intermediate
model. The following notation is only here for readability.
Notation PLFOevent :=
PL.event
(
only parsing).
Definition trace :=
list PLFOevent.
Transition relation.
Inductive step :
state ->
trace ->
state ->
Prop :=
|
sem_firstboot:
forall oraclechk,
step (
INIT oraclechk)
[]
(
USR oraclechk MCU.init DEV.init CHKPT.init)
|
sem_usr:
forall oraclechk 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 oraclechk mcu dev chkpt)
(
map PL.Op t)
(
USR oraclechk mcu'
dev'
chkpt)
|
sem_enter:
forall oraclechk 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 oraclechk mcu dev chkpt)
(
map PL.Op t)
(
DRV oraclechk mcu'
dev'
l chkpt')
|
sem_drv:
forall oc oraclechk 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 (
oc::
oraclechk)
mcu dev l chkpt)
(
if oc then (
map PL.Op t)
else [])
(
DRV (
oc::
oraclechk)
mcu'
dev'
l'
chkpt)
|
sem_leave:
forall oc oraclechk 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 (
oc ::
oraclechk)
mcu dev l chkpt)
(
if oc then (
List.map PL.Op t ++ [
PL.LogS])
else [])
(
USR (
oc ::
oraclechk)
mcu'
dev'
chkpt')
|
sem_pwr_usr:
forall oraclechk mcu dev chkpt chkpt',
forall (
RUNTIME:
CHKPT.saveNextMCU chkpt mcu =
chkpt'),
step (
USR oraclechk mcu dev chkpt)
[]
(
PWR oraclechk chkpt')
|
sem_pwr_drv:
forall oc oraclechk chkpt mcu dev l,
step (
DRV (
oc ::
oraclechk)
mcu dev l chkpt)
(
if oc then [
PL.LogF]
else [])
(
PWR (
oc ::
oraclechk)
chkpt)
|
sem_chkpt_success:
forall oraclechk chkpt chkpt',
forall (
RUNTIME:
CHKPT.set chkpt =
chkpt'),
step (
PWR (
true::
oraclechk)
chkpt)
[]
(
OFF oraclechk chkpt')
|
sem_chkpt_failure:
forall oraclechk chkpt,
step (
PWR (
false::
oraclechk)
chkpt)
[]
(
OFF oraclechk chkpt)
|
sem_reboot:
forall oraclechk 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 oraclechk chkpt)
[]
(
USR oraclechk mcu dev chkpt')
|
sem_usr_off:
forall oraclechk mcu dev chkpt,
step (
USR (
false::
oraclechk)
mcu dev chkpt)
[]
(
OFF oraclechk chkpt)
|
sem_drv_off:
forall oraclechk chkpt mcu dev l,
step (
DRV (
false::
oraclechk)
mcu dev l chkpt)
[]
(
OFF oraclechk chkpt)
.
Trace semantics.
Definition sem (
o:
oracle)(
t:
list PL.event):
Prop :=
exists s,
run step (
INIT o)
t s.