Module PL

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.