Library toprule

This file defines the top rule and its soundness proofs for verifying the correctness of preemptive OS kernels.

Require Import inferules.
Require Import language.
Require Import opsem.
Require Import etraceref.
Require Import assertion.
Require Import simulation.
Require Import memory.
Require Export MapLib.
Require Import lemmasfortoptheo.
Require Import LibTactics.
Require Import soundness.
Require Import auxdef.
Require Import tst_prop.
Require Import baseTac.
Require Import seplog_tactics.
Require Import lemmasfortoptheo.
Require Import toptheorem.

To verify an OS kernel, we need to verify the following three components of OS kernels using the refinement program logic: (1) Verifying the kernel APIs (APIRule); (2) Verifying the internal functions (InterRule); (3) Verifying the interrupt handlers (ItrpRule).

The inference rule for verifying kernel APIs

Inductive APIRule: progunit -> osapispec -> funspec -> ossched -> Inv -> Prop :=
| api_rule :
    forall (P:progunit) (apispec:osapispec) (Spec:funspec) (sd : ossched) (I : Inv),
      EqDomAPI P apispec ->
      (
        forall (f:fid) ab vl p r ft,
          apispec f = Some (ab ,ft ) ->
          Some p = BuildPreA´ P f (ab ,ft ) vl ->
          Some r = BuildRetA´ P f (ab ,ft ) vl ->
          (
            exists t d1 d2 s,
              P f = Some (t, d1, d2, s) /\
              InfRules Spec sd I r Afalse p s Afalse
          )
      ) ->
      APIRule P apispec Spec sd I.

The inference rule for verifying internal functions

Inductive InterRule: progunit -> funspec -> ossched -> Inv -> Prop :=
| inter_rule :
    forall (P : progunit) (FSpec : funspec) (sd : ossched) (I : Inv),
      EqDom P FSpec ->
      (forall (f : fid) (pre : fpre) (post : fpost) (t : type) (tl : typelist),
         FSpec f = Some (pre , post , (t , tl )) ->
         exists d1 d2 s,
           P f = Some (t , d1, d2, s) /\
           tlmatch tl d1 /\
           (forall (vl : vallist) (p : asrt) (r : retasrt) (logicl : list logicvar),
              Some p = BuildPreI P f vl logicl pre ->
              Some r = BuildRetI P f vl logicl post ->
              {|FSpec , sd , I , r , Afalse |}|- {{p }}s {{Afalse }})) ->
      InterRule P FSpec sd I.

The inference rule for verifying interrupt handlers

Inductive ItrpRule: intunit -> osintspec -> funspec -> ossched -> Inv -> Prop :=
| itrp_rule: forall (P:intunit) (intspec:osintspec) (Spec:funspec) sd (I:Inv),
               EqDomInt P intspec ->
               (
                 forall i isrreg si p r,
                   Some p = BuildintPre i intspec isrreg si I ->
                   Some r = BuildintRet i intspec isrreg si I ->
                   exists s,
                     P i = Some s /\
                     {|Spec , sd , I , retfalse , r |}|- {{p }}s {{Afalse }}

               ) ->
               ItrpRule P intspec Spec sd I.

The following TopRule is used to verify the correctness of the kernel code. According to this rule, to verify the OS kernel, we need to write the specification 'funspec' for the internal functions, and define the invariants 'I' for specifying shared kernel states. Then we need to prove that the internal functions, the API implementations and the interrupt handlers at the low level refine their abstract specification code at the high level respectively. The proofs of each component take the abstract scheduler 'χ' and the invariant 'I' for reasoning about the "switch" statement and specifying the resources shared between interrupt handlers and non-handler code . The 'side_condition' is defined in 'framework/theory/toptheorem.v', 'init' ensures the initial states satisfy the invariant I0, N, the interrupt-related states are properly initialized, and the initial local variable environment is empty.

Inductive TopRule : oscode -> osspec -> InitAsrt -> Prop :=
| top_rule: forall osc A (init:InitAsrt) (I:Inv) (Spec:funspec) pa pi ip apispec intspec schedmethod,
              osc = (pa ,pi ,ip ) ->
              A = (apispec ,intspec ,schedmethod ) ->
              APIRule pa apispec Spec schedmethod I ->
              ItrpRule ip intspec Spec schedmethod I ->
              InterRule pi Spec schedmethod I ->
              side_condition I schedmethod init ->
              TopRule osc A init.

The soundness proof of TopRule, corresponding to Theorem 4.1

Theorem Soundness:
  forall osc A (init:InitAsrt),
    TopRule osc A init ->
    OS_Correctness osc A init.