Library mcertikos.conlib.conmtlib.SingleConfiguration

Configuration for single-processor linking

This file defines the class SingleConfiguration. In order to make our per-processor thread linking proof general and avoid having to deal with irrelevant details of our concrete layers, the proofs are based on an abstract interface to the logs, oracles, abstract states, thread configuration, etc. of the machines involved. This file specifies that abstract interface.

Require Export Coqlib.
Require Export Integers.
Require Export Values.
Require Export MemoryX.
Require Export Globalenvs.
Require Export Asm.
Require Export Decision.
Require Export AlgebraicMem.
Require Export SingleAbstractDataType.
Require Export SingleOracle.
Require Import GlobalOracleProp.
Require Import RealParams.

The SingleConfiguration class gathers everything.

Section SINGLE_CONF_DEF.

  Class SingleConfiguration `{spl_data: SingleData} mem
        `{spl_mem_ops: Mem.MemoryModelOps mem} :=
    {
      spl_threads_ops :> ThreadsConfigurationOps;
      spl_oracle_ops :> SingleOracleOps;
      spl_oracle_prf :> SingleOracle (single_data := spl_data) (single_oracle_ops := spl_oracle_ops)
                     (threads_conf_ops := spl_threads_ops);
      spl_threads_prf :> ThreadsConfiguration (s_oracle := spl_oracle_prf);
      spl_oracle_prf_prop :> SingleOracleProp (thread_conf_prf := spl_threads_prf);
      spl_mem_prf :> Mem.MemoryModelX mem;
      spl_algebraic_mem :> AlgebraicMemory
    }.

End SINGLE_CONF_DEF.

Derived definitions

Section WITH_SINGLE_CONFIG.

Context `{sc: SingleConfiguration}.

Initial thread states

From prim_thread_init_pc in SingleOracle and the topology of threads identifiers, we can define the following functions for computing initial states of threads.

First, we extend prim_thread_initialization to work with arbitrary log events.

  Definition thread_init_pc {F V} (ge: Genv.t F V) (e : LogEvent) :=
    match e with
      | LEvent _ (LogPrim f args new_id _) ⇒ match prim_thread_init_pc ge f args with
                                            | Some pc ⇒ Some (new_id, pc)
                                            | _ ⇒ None
                                            end
      | _ ⇒ None
    end.

  Definition thread_init_pc_of {F V} ge (i : Z) (e : LogEvent) : option val :=
    match thread_init_pc (F:=F) (V:=V) ge e with
      | Some (j, pc) ⇒ if decide (i = j) then Some pc else None
      | None ⇒ None
    end.

Using thread_init_pc, we can extract the initial program counter for a thread from any log. The initial state of the main thread is hardcoded to point to main() as set by make_program, and is already available with an empty log. For other threads, this function will compute their initial states by examining the log for a corresponding spawn event.

  Fixpoint initial_thread_pc {F V} (ge: Genv.t F V) i (l : Log) : option val :=
    match l with
      | e :: l´ ⇒
        match initial_thread_pc ge i l´ with
          | Some pc ⇒ Some pc
          | None ⇒ thread_init_pc_of ge i e
        end
      | nil ⇒
        match decide (i = main_thread) with
          | left _ ⇒ Some (symbol_offset ge 1%positive Int.zero)
          | right _ ⇒ None
        end
    end.

  Definition initial_regset_state pc :=
    (Pregmap.init Vundef) # PC <- pc # ESP <- Vzero.

  Definition initial_thread_state {F V} (ge: Genv.t F V) i l : option regset :=
    match initial_thread_pc ge i l with
      | Some pc ⇒ Some (initial_regset_state pc)
      | None ⇒ None
    end.

Before we "return" into a (non-main) thread that is scheduled for the first time, the saved context has a slightly different format, where the code pointer is stored in RA.

  Definition initial_regset_kctxt pc :=
    (Pregmap.init Vundef) # RA <- pc # ESP <- Vzero.

  Definition initial_thread_kctxt {F V} (ge: Genv.t F V) i l : option regset :=
    match initial_thread_pc ge i l with
      | Some pc ⇒ Some (initial_regset_kctxt pc)
      | None ⇒ None
    end.

The following lemma establishes the relationship between these two versions of the initial states.

  Require Import ExtensionalityAxioms.
  Require Import Conventions.

  Let do_ret rs :=
    (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
       (undef_regs (map preg_of destroyed_at_call) rs))
      # EAX <- Vundef
      # PC <- (rs RA)
      # RA <- Vundef.

  Lemma initial_regset_state_kctxt pc:
    do_ret (initial_regset_kctxt pc) = initial_regset_state pc.
  Proof.
    apply functional_extensionality.
    intros r.
    destruct r as [ | [] | [] | | [] | ]; try reflexivity.
  Qed.

  Lemma initial_thread_state_kctxt {F V} (ge: Genv.t F V) i l rs:
    initial_thread_state ge i l = Some rs →
    ∃ rs´,
      initial_thread_kctxt ge i l = Some rs´ ∧
      rs = do_ret rs´.
  Proof.
    unfold initial_thread_kctxt, initial_thread_state.
    destruct (initial_thread_pc _ _ _); try discriminate.
    intros Hrs; inversion Hrs; clear Hrs.
    eexists.
    rewrite initial_regset_state_kctxt.
    eauto.
  Qed.

As for the initial memory, in the TAsm machine and up we need to use mem_lift_nextblock in non-main threads so as to account for the effect of the initial "yield back" event.

  Definition init_mem_lift_nextblock (m: mem) :=
    match init_log with
      | nil ⇒ m
      | _::_ ⇒ mem_lift_nextblock m (Pos.to_nat (last_nb init_log) -
                                      Pos.to_nat (Mem.nextblock m))
    end.

End WITH_SINGLE_CONFIG.

Section SINGLE_Link_CONF_DEF.

  Class SingleLinkConfiguration `{spl_data: SingleData} mem
        `{spl_mem_ops: Mem.MemoryModelOps mem} :=
    {
      spl_conf_prf :> SingleConfiguration (spl_data :=spl_data) mem (spl_mem_ops:=spl_mem_ops);
      spl_oracle_link_prf_prop :> SingleOracleLinkProp (thread_conf_prf := spl_threads_prf)
    }.

End SINGLE_Link_CONF_DEF.