Module PLO

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.