Require Import List.
Import ListNotations.
Require Import Relations.
Require Import util.
Require Import specification.
Require Import plf.
Import PLF.
PL
Interrupt-based checkpointing model where checkpointing always
succeeds. It is non deterministic in the occurrence of
power-loss interrupts during time-critical sections.
PL states are exactly PLF states. This notation is only here for
readability.
Notation PLstate :=
PLF.state
(
only parsing).
Observable events are the one of PLF, minus ChkptF and ChkpS.
For clarity, we device yet another data type.
Inductive event :=
|
LogS :
event
|
LogF :
event
|
Op :
DEV.ops ->
event.
Definition trace :=
list event.
Transition relation.
Inductive step :
state ->
trace ->
state ->
Prop :=
|
sem_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)
[]
(
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').
Trace semantics.
Definition sem (
t:
trace):
Prop :=
exists s,
run step INIT t s.