Library mcertikos.driver.CertiKOSproof
Require Import CertiKOSAux.
Require mcertikos.ticketlog.CurIDGenLink.
Require mcertikos.ticketlog.TicketLockIntroGenLink.
Require mcertikos.ticketlog.TicketLockOpGenLink.
Require mcertikos.ticketlog.QTicketLockOpGenLink.
Require mcertikos.ticketlog.HTicketLockOpGenLink.
Require mcertikos.ticketlog.QTicketLockGenLink.
Require mcertikos.devdrivers.ConsoleBuffIntroGenLink.
Require mcertikos.devdrivers.AbsConsoleBuffIntroGenLink.
Require mcertikos.devdrivers.SerialIntroGenLink.
Require mcertikos.devdrivers.SerialGenLink.
Require mcertikos.devdrivers.IoApicGenLink.
Require mcertikos.devdrivers.LApicGenLink.
Require mcertikos.devdrivers.ConsoleGenLink.
Require mcertikos.devdrivers.HandlerIntroGenLink.
Require mcertikos.devdrivers.HandlerSwGenLink.
Require mcertikos.devdrivers.HandlerAsmGenLink.
Require mcertikos.devdrivers.HandlerCxtGenLink.
Require mcertikos.devdrivers.HandlerOpGenLink.
Require mcertikos.devdrivers.HandlerGenLink.
Require mcertikos.devdrivers.AbsHandlerGenLink.
Require mcertikos.mm.ContainerIntroGenLink.
Require mcertikos.mm.ContainerGenLink.
Require mcertikos.mm.ALInitGenLink.
Require mcertikos.mm.ALOpGenLink.
Require mcertikos.mm.ALGenLink.
Require mcertikos.mm.ALHGenLink.
Require mcertikos.mm.PTIntroGenLink.
Require mcertikos.mm.PTOpGenLink.
Require mcertikos.mm.PTCommGenLink.
Require mcertikos.mm.PTKernGenLink.
Require mcertikos.mm.PTInitGenLink.
Require mcertikos.mm.PTNewGenLink.
Require mcertikos.mm.ShareIntroGenLink.
Require mcertikos.mm.ShareOpGenLink.
Require mcertikos.mm.ShareGenLink.
Require mcertikos.proc.KContextGenLink.
Require mcertikos.proc.KContextNewGenLink.
Require mcertikos.proc.SleeperGenLink.
Require mcertikos.proc.QueueIntroGenLink.
Require mcertikos.proc.QueueInitGenLink.
Require mcertikos.proc.AbQueueGenLink.
Require mcertikos.proc.AbQueueAtomicGenLink.
Require mcertikos.proc.CVIntroGenLink.
Require mcertikos.proc.CVOpGenLink.
Require mcertikos.proc.ThreadSchedGenLink.
Require mcertikos.proc.ThreadGenLink.
Require mcertikos.proc.QThreadGenLink.
Require mcertikos.proc.EPTIntroGenLink.
Require mcertikos.proc.EPTOpGenLink.
Require mcertikos.proc.EPTInitGenLink.
Require mcertikos.proc.VMCSIntroGenLink.
Require mcertikos.proc.VMCSInitGenLink.
Require mcertikos.proc.VMXIntroGenLink.
Require mcertikos.proc.VMXInitGenLink.
Require mcertikos.proc.UCtxtIntroGenLink.
Require mcertikos.proc.ProcGenLink.
Require mcertikos.proc.BThreadGenLink.
Require mcertikos.ipc.IPCIntroGenLink.
Require mcertikos.ipc.IPCGenLink.
Require mcertikos.trap.TrapArgGenLink.
Require mcertikos.trap.TrapGenLink.
Require mcertikos.trap.DispatchGenLink.
Require mcertikos.trap.SysCallGenLink.
Require Import GlobalOracleProp.
Require Import AlgebraicMemImpl.
Require Import SingleOracle.
Require Import SingleConfiguration.
Require Import SingleOracleImpl.
Require Import StencilImpl.
Require Import CompCertiKOSproof.
Remove Hints
MemimplX.memory_model_ops
MemimplX.memory_model
MemimplX.memory_model_x
StencilImpl.ptree_stencil_ops
StencilImpl.ptree_stencil_prf
: typeclass_instances.
Existing Instance CompCertiKOSproof.memory_model_ops.
Inductive exists_program_simulation
(s : stencil)
(CTXT : LAsm.module)
{CDATA}
(HLayer : CompatLayerDef.compatlayer CDATA)
(HSem LSem : LAsm.program → Smallstep.semantics Integers.Int.int)
(pl : LAsm.program) : Prop :=
exists_program_simulation_intro :
∀ ph : LAsm.program,
backward_simulation (HSem ph) (LSem pl) →
make_program s CTXT HLayer = OK ph →
exists_program_simulation s CTXT HLayer HSem LSem pl.
Require Import LAsmAbsDataProperty.
Require Import PHThread2TGenDef.
Require Import PHThread2TGen.
Require Import E2PBThreadGenDef.
Require Import E2PBThreadGen.
Require Import SingleProcessor_Refinement.
Require Import Concurrent_Linking.
Section PERTHREADCERTIKOSCORRECT.
Context `{multi_oracle_prop : MultiOracleProp}.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Existing Instance SingleOracleImpl.s_oracle_prf.
Existing Instance SingleOracleImpl.s_oracle_prop_prf.
Existing Instance SingleOracleImpl.s_config.
Context `{s_oracle_basic_link_prop_prf: !SingleOracleBasicLinkProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Existing Instance SingleOracleImpl.s_link_config.
Context `{multi_oracle_link: !MultiOracleLink}.
Theorem Per_Thread_CertiKOS_correct´:
∀ (s: stencil) (CTXT: LAsm.module) combined_module combined
(builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
CertiKOS.per_thread_certikos_plus_ctxt CTXT = OK combined_module →
make_program s combined_module (PHThread.phthread ⊕ L64) = OK combined →
exists_program_simulation
s CTXT (TSysCall.tsyscall ⊕ L64)
(HAsm.semantics (TSysCall.tsyscall ⊕ L64))
(HAsm.semantics (PHThread.phthread ⊕ L64))
combined.
Proof.
intros s CTXT cM combined ? Hkern Hcomb.
assert (pl_single_events :
single_events (HAsm.semantics (PHThread.phthread ⊕ L64) combined)).
{ apply LAsmModuleSemEvent.LAsm_single_events;
[ Decision.decision | assumption ].
}
unfold CertiKOS.per_thread_certikos_plus_ctxt in ×.
unfold CertiKOS.add_loc in ×.
inv_monad´ Hkern.
unfold ret, res_monad_ops in ×.
unfold_all_into_link_impl.
destruct_mpe IPCIntroGenLink.make_program_exists.
destruct_mpe IPCGenLink.make_program_exists.
destruct_mpe TrapArgGenLink.make_program_exists.
destruct_mpe TrapGenLink.make_program_exists.
destruct_mpe DispatchGenLink.make_program_exists.
destruct_mpe SysCallGenLink.make_program_exists.
eapply exists_program_simulation_intro; [ | eassumption].
compose_backward_simulation SysCallGenLink.cl_backward_simulation.
compose_backward_simulation DispatchGenLink.cl_backward_simulation.
compose_backward_simulation TrapGenLink.cl_backward_simulation.
compose_backward_simulation TrapArgGenLink.cl_backward_simulation.
compose_backward_simulation IPCGenLink.cl_backward_simulation.
last_backward_simulation IPCIntroGenLink.cl_backward_simulation.
Qed.
Correctness Theorem
Theorem Per_Thread_CertiKOS_correct:
∀ (s: stencil) (CTXT: LAsm.module) kernel combined_program user_program
(builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
CertiKOS.per_thread_certikos = OK kernel →
make_program s (CTXT ⊕ kernel) (PHThread.phthread ⊕ L64) = OK combined_program →
make_program s CTXT (TSysCall.tsyscall ⊕ L64) = OK user_program →
inhabited
(backward_simulation
(HAsm.semantics (TSysCall.tsyscall ⊕ L64) user_program)
(HAsm.semantics (PHThread.phthread ⊕ L64) combined_program)).
Proof.
intros s CTXT kernel combined_program user_program ? Hkernel Hcp Hup.
edestruct (per_thread_CertiKOS_plus_context CTXT) as (comb & Hcomb & Heqv); [ eassumption | ].
eapply make_program_equiv in Hcp; [ | eassumption].
edestruct Per_Thread_CertiKOS_correct´; try eassumption.
constructor.
setoid_rewrite H in Hup.
congruence.
Qed.
End PERTHREADCERTIKOSCORRECT.
Section PERCPUCERTIKOSCORRECT.
Context `{multi_oracle_prop : MultiOracleProp}.
Context `{multi_oracle_link: !MultiOracleLink}.
Theorem Per_CPU_CertiKOS_correct´:
∀ (s: stencil) (CTXT: LAsm.module) combined_module combined
(builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
CertiKOS.per_cpu_certikos_plus_ctxt CTXT = OK combined_module →
make_program s combined_module (MBoot.mboot ⊕ L64) = OK combined →
exists_program_simulation
s CTXT (PBThread.pbthread ⊕ L64)
(LAsm.semantics (lcfg_ops := LC (PBThread.pbthread ⊕ L64)))
(LAsm.semantics (lcfg_ops := LC (MBoot.mboot ⊕ L64)))
combined.
Proof.
intros s CTXT cM combined ? Hkern Hcomb.
assert (pl_single_events :
single_events (LAsm.semantics (lcfg_ops := LC (MBoot.mboot ⊕ L64)) combined)).
{ apply LAsmModuleSemEvent.LAsm_single_events;
[ Decision.decision | assumption ].
}
unfold CertiKOS.per_cpu_certikos_plus_ctxt in ×.
unfold CertiKOS.add_loc in ×.
inv_monad´ Hkern.
unfold ret, res_monad_ops in ×.
unfold_all_into_link_impl.
destruct_mpe CurIDGenLink.make_program_exists.
destruct_mpe TicketLockIntroGenLink.make_program_exists.
destruct_mpe TicketLockOpGenLink.make_program_exists.
destruct_mpe QTicketLockOpGenLink.make_program_exists.
destruct_mpe HTicketLockOpGenLink.make_program_exists.
destruct_mpe QTicketLockGenLink.make_program_exists.
destruct_mpe ConsoleBuffIntroGenLink.make_program_exists.
destruct_mpe AbsConsoleBuffIntroGenLink.make_program_exists.
destruct_mpe SerialIntroGenLink.make_program_exists.
destruct_mpe SerialGenLink.make_program_exists.
destruct_mpe IoApicGenLink.make_program_exists.
destruct_mpe LApicGenLink.make_program_exists.
destruct_mpe ConsoleGenLink.make_program_exists.
destruct_mpe HandlerIntroGenLink.make_program_exists.
destruct_mpe HandlerSwGenLink.make_program_exists.
destruct_mpe HandlerAsmGenLink.make_program_exists.
destruct_mpe HandlerCxtGenLink.make_program_exists.
destruct_mpe HandlerOpGenLink.make_program_exists.
destruct_mpe HandlerGenLink.make_program_exists.
destruct_mpe AbsHandlerGenLink.make_program_exists.
destruct_mpe ContainerIntroGenLink.make_program_exists.
destruct_mpe ContainerGenLink.make_program_exists.
destruct_mpe ALInitGenLink.make_program_exists.
destruct_mpe ALOpGenLink.make_program_exists.
destruct_mpe ALGenLink.make_program_exists.
destruct_mpe ALHGenLink.make_program_exists.
destruct_mpe PTIntroGenLink.make_program_exists.
destruct_mpe PTOpGenLink.make_program_exists.
destruct_mpe PTCommGenLink.make_program_exists.
destruct_mpe PTKernGenLink.make_program_exists.
destruct_mpe PTInitGenLink.make_program_exists.
destruct_mpe PTNewGenLink.make_program_exists.
destruct_mpe ShareIntroGenLink.make_program_exists.
destruct_mpe ShareOpGenLink.make_program_exists.
destruct_mpe ShareGenLink.make_program_exists.
destruct_mpe KContextGenLink.make_program_exists.
destruct_mpe KContextNewGenLink.make_program_exists.
destruct_mpe SleeperGenLink.make_program_exists.
destruct_mpe QueueIntroGenLink.make_program_exists.
destruct_mpe QueueInitGenLink.make_program_exists.
destruct_mpe AbQueueGenLink.make_program_exists.
destruct_mpe AbQueueAtomicGenLink.make_program_exists.
destruct_mpe CVIntroGenLink.make_program_exists.
destruct_mpe CVOpGenLink.make_program_exists.
destruct_mpe ThreadSchedGenLink.make_program_exists.
destruct_mpe ThreadGenLink.make_program_exists.
destruct_mpe QThreadGenLink.make_program_exists.
destruct_mpe UCtxtIntroGenLink.make_program_exists.
destruct_mpe ProcGenLink.make_program_exists.
destruct_mpe EPTIntroGenLink.make_program_exists.
destruct_mpe EPTOpGenLink.make_program_exists.
destruct_mpe EPTInitGenLink.make_program_exists.
destruct_mpe VMCSIntroGenLink.make_program_exists.
destruct_mpe VMCSInitGenLink.make_program_exists.
destruct_mpe VMXIntroGenLink.make_program_exists.
destruct_mpe VMXInitGenLink.make_program_exists.
destruct_mpe BThreadGenLink.make_program_exists.
eapply exists_program_simulation_intro; [ | eassumption].
compose_backward_simulation BThreadGenLink.cl_backward_simulation.
compose_backward_simulation VMXInitGenLink.cl_backward_simulation.
compose_backward_simulation VMXIntroGenLink.cl_backward_simulation.
compose_backward_simulation VMCSInitGenLink.cl_backward_simulation.
compose_backward_simulation VMCSIntroGenLink.cl_backward_simulation.
compose_backward_simulation EPTInitGenLink.cl_backward_simulation.
compose_backward_simulation EPTOpGenLink.cl_backward_simulation.
compose_backward_simulation EPTIntroGenLink.cl_backward_simulation.
compose_backward_simulation ProcGenLink.cl_backward_simulation.
compose_backward_simulation UCtxtIntroGenLink.cl_backward_simulation.
compose_backward_simulation QThreadGenLink.cl_backward_simulation.
compose_backward_simulation ThreadGenLink.cl_backward_simulation.
compose_backward_simulation ThreadSchedGenLink.cl_backward_simulation.
compose_backward_simulation CVOpGenLink.cl_backward_simulation.
compose_backward_simulation CVIntroGenLink.cl_backward_simulation.
compose_backward_simulation AbQueueAtomicGenLink.cl_backward_simulation.
compose_backward_simulation AbQueueGenLink.cl_backward_simulation.
compose_backward_simulation QueueInitGenLink.cl_backward_simulation.
compose_backward_simulation QueueIntroGenLink.cl_backward_simulation.
compose_backward_simulation SleeperGenLink.cl_backward_simulation.
compose_backward_simulation KContextNewGenLink.cl_backward_simulation.
compose_backward_simulation KContextGenLink.cl_backward_simulation.
compose_backward_simulation ShareGenLink.cl_backward_simulation.
compose_backward_simulation ShareOpGenLink.cl_backward_simulation.
compose_backward_simulation ShareIntroGenLink.cl_backward_simulation.
compose_backward_simulation PTNewGenLink.cl_backward_simulation.
compose_backward_simulation PTInitGenLink.cl_backward_simulation.
compose_backward_simulation PTKernGenLink.cl_backward_simulation.
compose_backward_simulation PTCommGenLink.cl_backward_simulation.
compose_backward_simulation PTOpGenLink.cl_backward_simulation.
compose_backward_simulation PTIntroGenLink.cl_backward_simulation.
compose_backward_simulation ALHGenLink.cl_backward_simulation.
compose_backward_simulation ALGenLink.cl_backward_simulation.
compose_backward_simulation ALOpGenLink.cl_backward_simulation.
compose_backward_simulation ALInitGenLink.cl_backward_simulation.
compose_backward_simulation ContainerGenLink.cl_backward_simulation.
compose_backward_simulation ContainerIntroGenLink.cl_backward_simulation.
compose_backward_simulation AbsHandlerGenLink.cl_backward_simulation.
compose_backward_simulation HandlerGenLink.cl_backward_simulation.
compose_backward_simulation HandlerOpGenLink.cl_backward_simulation.
compose_backward_simulation HandlerCxtGenLink.cl_backward_simulation.
compose_backward_simulation HandlerAsmGenLink.cl_backward_simulation.
compose_backward_simulation HandlerSwGenLink.cl_backward_simulation.
compose_backward_simulation HandlerIntroGenLink.cl_backward_simulation.
compose_backward_simulation ConsoleGenLink.cl_backward_simulation.
compose_backward_simulation LApicGenLink.cl_backward_simulation.
compose_backward_simulation IoApicGenLink.cl_backward_simulation.
compose_backward_simulation SerialGenLink.cl_backward_simulation.
compose_backward_simulation SerialIntroGenLink.cl_backward_simulation.
compose_backward_simulation AbsConsoleBuffIntroGenLink.cl_backward_simulation.
compose_backward_simulation ConsoleBuffIntroGenLink.cl_backward_simulation.
compose_backward_simulation QTicketLockGenLink.cl_backward_simulation.
compose_backward_simulation HTicketLockOpGenLink.cl_backward_simulation.
compose_backward_simulation QTicketLockOpGenLink.cl_backward_simulation.
compose_backward_simulation TicketLockOpGenLink.cl_backward_simulation.
compose_backward_simulation TicketLockIntroGenLink.cl_backward_simulation.
last_backward_simulation CurIDGenLink.cl_backward_simulation.
Qed.
∀ (s: stencil) (CTXT: LAsm.module) kernel combined_program user_program
(builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
CertiKOS.per_thread_certikos = OK kernel →
make_program s (CTXT ⊕ kernel) (PHThread.phthread ⊕ L64) = OK combined_program →
make_program s CTXT (TSysCall.tsyscall ⊕ L64) = OK user_program →
inhabited
(backward_simulation
(HAsm.semantics (TSysCall.tsyscall ⊕ L64) user_program)
(HAsm.semantics (PHThread.phthread ⊕ L64) combined_program)).
Proof.
intros s CTXT kernel combined_program user_program ? Hkernel Hcp Hup.
edestruct (per_thread_CertiKOS_plus_context CTXT) as (comb & Hcomb & Heqv); [ eassumption | ].
eapply make_program_equiv in Hcp; [ | eassumption].
edestruct Per_Thread_CertiKOS_correct´; try eassumption.
constructor.
setoid_rewrite H in Hup.
congruence.
Qed.
End PERTHREADCERTIKOSCORRECT.
Section PERCPUCERTIKOSCORRECT.
Context `{multi_oracle_prop : MultiOracleProp}.
Context `{multi_oracle_link: !MultiOracleLink}.
Theorem Per_CPU_CertiKOS_correct´:
∀ (s: stencil) (CTXT: LAsm.module) combined_module combined
(builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
CertiKOS.per_cpu_certikos_plus_ctxt CTXT = OK combined_module →
make_program s combined_module (MBoot.mboot ⊕ L64) = OK combined →
exists_program_simulation
s CTXT (PBThread.pbthread ⊕ L64)
(LAsm.semantics (lcfg_ops := LC (PBThread.pbthread ⊕ L64)))
(LAsm.semantics (lcfg_ops := LC (MBoot.mboot ⊕ L64)))
combined.
Proof.
intros s CTXT cM combined ? Hkern Hcomb.
assert (pl_single_events :
single_events (LAsm.semantics (lcfg_ops := LC (MBoot.mboot ⊕ L64)) combined)).
{ apply LAsmModuleSemEvent.LAsm_single_events;
[ Decision.decision | assumption ].
}
unfold CertiKOS.per_cpu_certikos_plus_ctxt in ×.
unfold CertiKOS.add_loc in ×.
inv_monad´ Hkern.
unfold ret, res_monad_ops in ×.
unfold_all_into_link_impl.
destruct_mpe CurIDGenLink.make_program_exists.
destruct_mpe TicketLockIntroGenLink.make_program_exists.
destruct_mpe TicketLockOpGenLink.make_program_exists.
destruct_mpe QTicketLockOpGenLink.make_program_exists.
destruct_mpe HTicketLockOpGenLink.make_program_exists.
destruct_mpe QTicketLockGenLink.make_program_exists.
destruct_mpe ConsoleBuffIntroGenLink.make_program_exists.
destruct_mpe AbsConsoleBuffIntroGenLink.make_program_exists.
destruct_mpe SerialIntroGenLink.make_program_exists.
destruct_mpe SerialGenLink.make_program_exists.
destruct_mpe IoApicGenLink.make_program_exists.
destruct_mpe LApicGenLink.make_program_exists.
destruct_mpe ConsoleGenLink.make_program_exists.
destruct_mpe HandlerIntroGenLink.make_program_exists.
destruct_mpe HandlerSwGenLink.make_program_exists.
destruct_mpe HandlerAsmGenLink.make_program_exists.
destruct_mpe HandlerCxtGenLink.make_program_exists.
destruct_mpe HandlerOpGenLink.make_program_exists.
destruct_mpe HandlerGenLink.make_program_exists.
destruct_mpe AbsHandlerGenLink.make_program_exists.
destruct_mpe ContainerIntroGenLink.make_program_exists.
destruct_mpe ContainerGenLink.make_program_exists.
destruct_mpe ALInitGenLink.make_program_exists.
destruct_mpe ALOpGenLink.make_program_exists.
destruct_mpe ALGenLink.make_program_exists.
destruct_mpe ALHGenLink.make_program_exists.
destruct_mpe PTIntroGenLink.make_program_exists.
destruct_mpe PTOpGenLink.make_program_exists.
destruct_mpe PTCommGenLink.make_program_exists.
destruct_mpe PTKernGenLink.make_program_exists.
destruct_mpe PTInitGenLink.make_program_exists.
destruct_mpe PTNewGenLink.make_program_exists.
destruct_mpe ShareIntroGenLink.make_program_exists.
destruct_mpe ShareOpGenLink.make_program_exists.
destruct_mpe ShareGenLink.make_program_exists.
destruct_mpe KContextGenLink.make_program_exists.
destruct_mpe KContextNewGenLink.make_program_exists.
destruct_mpe SleeperGenLink.make_program_exists.
destruct_mpe QueueIntroGenLink.make_program_exists.
destruct_mpe QueueInitGenLink.make_program_exists.
destruct_mpe AbQueueGenLink.make_program_exists.
destruct_mpe AbQueueAtomicGenLink.make_program_exists.
destruct_mpe CVIntroGenLink.make_program_exists.
destruct_mpe CVOpGenLink.make_program_exists.
destruct_mpe ThreadSchedGenLink.make_program_exists.
destruct_mpe ThreadGenLink.make_program_exists.
destruct_mpe QThreadGenLink.make_program_exists.
destruct_mpe UCtxtIntroGenLink.make_program_exists.
destruct_mpe ProcGenLink.make_program_exists.
destruct_mpe EPTIntroGenLink.make_program_exists.
destruct_mpe EPTOpGenLink.make_program_exists.
destruct_mpe EPTInitGenLink.make_program_exists.
destruct_mpe VMCSIntroGenLink.make_program_exists.
destruct_mpe VMCSInitGenLink.make_program_exists.
destruct_mpe VMXIntroGenLink.make_program_exists.
destruct_mpe VMXInitGenLink.make_program_exists.
destruct_mpe BThreadGenLink.make_program_exists.
eapply exists_program_simulation_intro; [ | eassumption].
compose_backward_simulation BThreadGenLink.cl_backward_simulation.
compose_backward_simulation VMXInitGenLink.cl_backward_simulation.
compose_backward_simulation VMXIntroGenLink.cl_backward_simulation.
compose_backward_simulation VMCSInitGenLink.cl_backward_simulation.
compose_backward_simulation VMCSIntroGenLink.cl_backward_simulation.
compose_backward_simulation EPTInitGenLink.cl_backward_simulation.
compose_backward_simulation EPTOpGenLink.cl_backward_simulation.
compose_backward_simulation EPTIntroGenLink.cl_backward_simulation.
compose_backward_simulation ProcGenLink.cl_backward_simulation.
compose_backward_simulation UCtxtIntroGenLink.cl_backward_simulation.
compose_backward_simulation QThreadGenLink.cl_backward_simulation.
compose_backward_simulation ThreadGenLink.cl_backward_simulation.
compose_backward_simulation ThreadSchedGenLink.cl_backward_simulation.
compose_backward_simulation CVOpGenLink.cl_backward_simulation.
compose_backward_simulation CVIntroGenLink.cl_backward_simulation.
compose_backward_simulation AbQueueAtomicGenLink.cl_backward_simulation.
compose_backward_simulation AbQueueGenLink.cl_backward_simulation.
compose_backward_simulation QueueInitGenLink.cl_backward_simulation.
compose_backward_simulation QueueIntroGenLink.cl_backward_simulation.
compose_backward_simulation SleeperGenLink.cl_backward_simulation.
compose_backward_simulation KContextNewGenLink.cl_backward_simulation.
compose_backward_simulation KContextGenLink.cl_backward_simulation.
compose_backward_simulation ShareGenLink.cl_backward_simulation.
compose_backward_simulation ShareOpGenLink.cl_backward_simulation.
compose_backward_simulation ShareIntroGenLink.cl_backward_simulation.
compose_backward_simulation PTNewGenLink.cl_backward_simulation.
compose_backward_simulation PTInitGenLink.cl_backward_simulation.
compose_backward_simulation PTKernGenLink.cl_backward_simulation.
compose_backward_simulation PTCommGenLink.cl_backward_simulation.
compose_backward_simulation PTOpGenLink.cl_backward_simulation.
compose_backward_simulation PTIntroGenLink.cl_backward_simulation.
compose_backward_simulation ALHGenLink.cl_backward_simulation.
compose_backward_simulation ALGenLink.cl_backward_simulation.
compose_backward_simulation ALOpGenLink.cl_backward_simulation.
compose_backward_simulation ALInitGenLink.cl_backward_simulation.
compose_backward_simulation ContainerGenLink.cl_backward_simulation.
compose_backward_simulation ContainerIntroGenLink.cl_backward_simulation.
compose_backward_simulation AbsHandlerGenLink.cl_backward_simulation.
compose_backward_simulation HandlerGenLink.cl_backward_simulation.
compose_backward_simulation HandlerOpGenLink.cl_backward_simulation.
compose_backward_simulation HandlerCxtGenLink.cl_backward_simulation.
compose_backward_simulation HandlerAsmGenLink.cl_backward_simulation.
compose_backward_simulation HandlerSwGenLink.cl_backward_simulation.
compose_backward_simulation HandlerIntroGenLink.cl_backward_simulation.
compose_backward_simulation ConsoleGenLink.cl_backward_simulation.
compose_backward_simulation LApicGenLink.cl_backward_simulation.
compose_backward_simulation IoApicGenLink.cl_backward_simulation.
compose_backward_simulation SerialGenLink.cl_backward_simulation.
compose_backward_simulation SerialIntroGenLink.cl_backward_simulation.
compose_backward_simulation AbsConsoleBuffIntroGenLink.cl_backward_simulation.
compose_backward_simulation ConsoleBuffIntroGenLink.cl_backward_simulation.
compose_backward_simulation QTicketLockGenLink.cl_backward_simulation.
compose_backward_simulation HTicketLockOpGenLink.cl_backward_simulation.
compose_backward_simulation QTicketLockOpGenLink.cl_backward_simulation.
compose_backward_simulation TicketLockOpGenLink.cl_backward_simulation.
compose_backward_simulation TicketLockIntroGenLink.cl_backward_simulation.
last_backward_simulation CurIDGenLink.cl_backward_simulation.
Qed.
Correctness Theorem
Theorem Per_CPU_CertiKOS_correct:
∀ (s: stencil) (CTXT: LAsm.module) kernel combined_program user_program
(builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
CertiKOS.per_cpu_certikos = OK kernel →
make_program s (CTXT ⊕ kernel) (MBoot.mboot ⊕ L64) = OK combined_program →
make_program s CTXT (PBThread.pbthread ⊕ L64) = OK user_program →
inhabited
(backward_simulation
(LAsm.semantics (lcfg_ops := LC (PBThread.pbthread ⊕ L64)) user_program)
(LAsm.semantics (lcfg_ops := LC (MBoot.mboot ⊕ L64)) combined_program)).
Proof.
intros s CTXT kernel combined_program user_program ? Hkernel Hcp Hup.
edestruct (per_cpu_CertiKOS_plus_context CTXT) as (comb & Hcomb & Heqv); [ eassumption | ].
eapply make_program_equiv in Hcp; [ | eassumption].
edestruct Per_CPU_CertiKOS_correct´; try eassumption.
constructor.
setoid_rewrite H in Hup.
congruence.
Qed.
End PERCPUCERTIKOSCORRECT.
Section CERTIKOSCORRECT.
Context `{multi_oracle_prop : MultiOracleProp}.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Existing Instance SingleOracleImpl.s_oracle_prf.
Existing Instance SingleOracleImpl.s_oracle_prop_prf.
Existing Instance SingleOracleImpl.s_config.
Context `{s_oracle_basic_link_prop_prf: !SingleOracleBasicLinkProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Existing Instance SingleOracleImpl.s_link_config.
Context `{multi_oracle_link: !MultiOracleLink}.
Context `{phthread2tgen_prop: !PHThraed2TGenProp s_oracle_prf}.
Existing Instance ptree_stencil_ops.
Context `{e2pbthread_gen_prop: !E2PBThreadGenProp s_oracle_prf}.
Existing Instance PHThread2TGen.abs_relT.
Existing Instance algebraicmem.
Existing Instance E2PBThreadGen.abs_rel.
Require Import lsamep_PHBThread_PHThread.
Lemma pbthread_phthread_lsamep:
lsamep (Fm:=LAsm.function) (Vm:=Ctypes.type) (Fp:=LAsm.fundef) (Vp:=unit)
(PBThread.pbthread ⊕ L64)
(PHThread.phthread ⊕ L64).
Proof.
repeat apply conj.
- apply lsamepp_iff.
split; apply elements_lsamepp; reflexivity.
- apply lsamepv_iff.
split; apply elements_lsamepv; reflexivity.
- decision.
- decision.
- decision.
- decision.
Qed.
Context `{zset_op: !Concurrent_Linking_Lib.ZSet_operation}.
Context `{pmap: !Concurrent_Linking_Lib.PartialMap}.
Context `{mc_link_oracle: !ConcurrentOracle.MCLinkOracle}.
Context `{mc_link_fairness: !Concurrent_Linking_Def.Fairness}.
Context `{mc_oracle_cond: !ConcurrentOracle.MCLinkOracleCond}.
Context `{Hpp1: !PrimcallProperties (TAsm.sprimitive_call (L:=PHBThread.phbthread ⊕ L64))}.
Context `{Hpp2: !PrimcallProperties (IIEAsm.sprimitive_call (L:=PHBThread.phbthread ⊕ L64))}.
Context `{Hpp3: !PrimcallProperties (EAsm.sprimitive_call (L:=PHBThread.phbthread ⊕ L64))}.
Context `{Hrel: !AsmIIE2IIE.IE2IERel (L := PHBThread.phbthread ⊕ L64)}.
Context `{Hdataprop: !LAsmAbsDataProp (L := PHBThread.phbthread ⊕ L64)}.
Theorem CertiKOS_correct:
∀ (s: stencil) (CTXT: LAsm.module) k1 k2 p combined_program user_program,
genv_next s = init_nb →
CertiKOS.per_thread_certikos = OK k1 →
CertiKOS.per_cpu_certikos = OK k2 →
∀ Hmp: make_program s ((CTXT ⊕ k1) ⊕ k2) (MBoot.mboot ⊕ L64) = OK combined_program,
make_program s (CTXT ⊕ k1) (PHThread.phthread ⊕ L64) = OK p →
make_program s CTXT (TSysCall.tsyscall ⊕ L64) = OK user_program →
noglobvar p →
inhabited
(backward_simulation
(HAsm.semantics (TSysCall.tsyscall ⊕ L64) user_program)
(HWStepSemImpl.hwstep_semantics
(Hmakege := make_program_globalenv _ _ _ _ Hmp)
(Genv.globalenv combined_program) s
((CTXT ⊕ k1) ⊕ k2)
combined_program)).
Proof.
intros.
assert (Hpb: make_program s (CTXT ⊕ k1) (PBThread.pbthread ⊕ L64) = OK p).
{
erewrite make_program_lsamep.
eapply H2.
eapply pbthread_phthread_lsamep.
}
assert (Hpbh: make_program s (CTXT ⊕ k1) (PHBThread.phbthread ⊕ L64) = OK p).
{
erewrite make_program_lsamep.
eapply H2.
apply phbthread_phthread_lsamep.
}
edestruct Per_Thread_CertiKOS_correct as [PER_THREAD_CORRECT]; try eassumption.
edestruct Per_CPU_CertiKOS_correct as [PER_CPU_CORRECT]; try eassumption.
constructor.
eapply compose_backward_simulation.
eapply HWStepSemImpl.hwstep_semantics_single_events.
eexact PER_THREAD_CORRECT.
eapply compose_backward_simulation.
eapply HWStepSemImpl.hwstep_semantics_single_events.
eapply @SingleCore_backward_simulation; eauto 2.
{ decision. }
simpl in Hpbh.
eexact Hpbh.
eapply compose_backward_simulation.
eapply HWStepSemImpl.hwstep_semantics_single_events.
exact PER_CPU_CORRECT.
apply concurrent_backward_simulation.
Qed.
End CERTIKOSCORRECT.
∀ (s: stencil) (CTXT: LAsm.module) kernel combined_program user_program
(builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
CertiKOS.per_cpu_certikos = OK kernel →
make_program s (CTXT ⊕ kernel) (MBoot.mboot ⊕ L64) = OK combined_program →
make_program s CTXT (PBThread.pbthread ⊕ L64) = OK user_program →
inhabited
(backward_simulation
(LAsm.semantics (lcfg_ops := LC (PBThread.pbthread ⊕ L64)) user_program)
(LAsm.semantics (lcfg_ops := LC (MBoot.mboot ⊕ L64)) combined_program)).
Proof.
intros s CTXT kernel combined_program user_program ? Hkernel Hcp Hup.
edestruct (per_cpu_CertiKOS_plus_context CTXT) as (comb & Hcomb & Heqv); [ eassumption | ].
eapply make_program_equiv in Hcp; [ | eassumption].
edestruct Per_CPU_CertiKOS_correct´; try eassumption.
constructor.
setoid_rewrite H in Hup.
congruence.
Qed.
End PERCPUCERTIKOSCORRECT.
Section CERTIKOSCORRECT.
Context `{multi_oracle_prop : MultiOracleProp}.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Existing Instance SingleOracleImpl.s_oracle_prf.
Existing Instance SingleOracleImpl.s_oracle_prop_prf.
Existing Instance SingleOracleImpl.s_config.
Context `{s_oracle_basic_link_prop_prf: !SingleOracleBasicLinkProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Existing Instance SingleOracleImpl.s_link_config.
Context `{multi_oracle_link: !MultiOracleLink}.
Context `{phthread2tgen_prop: !PHThraed2TGenProp s_oracle_prf}.
Existing Instance ptree_stencil_ops.
Context `{e2pbthread_gen_prop: !E2PBThreadGenProp s_oracle_prf}.
Existing Instance PHThread2TGen.abs_relT.
Existing Instance algebraicmem.
Existing Instance E2PBThreadGen.abs_rel.
Require Import lsamep_PHBThread_PHThread.
Lemma pbthread_phthread_lsamep:
lsamep (Fm:=LAsm.function) (Vm:=Ctypes.type) (Fp:=LAsm.fundef) (Vp:=unit)
(PBThread.pbthread ⊕ L64)
(PHThread.phthread ⊕ L64).
Proof.
repeat apply conj.
- apply lsamepp_iff.
split; apply elements_lsamepp; reflexivity.
- apply lsamepv_iff.
split; apply elements_lsamepv; reflexivity.
- decision.
- decision.
- decision.
- decision.
Qed.
Context `{zset_op: !Concurrent_Linking_Lib.ZSet_operation}.
Context `{pmap: !Concurrent_Linking_Lib.PartialMap}.
Context `{mc_link_oracle: !ConcurrentOracle.MCLinkOracle}.
Context `{mc_link_fairness: !Concurrent_Linking_Def.Fairness}.
Context `{mc_oracle_cond: !ConcurrentOracle.MCLinkOracleCond}.
Context `{Hpp1: !PrimcallProperties (TAsm.sprimitive_call (L:=PHBThread.phbthread ⊕ L64))}.
Context `{Hpp2: !PrimcallProperties (IIEAsm.sprimitive_call (L:=PHBThread.phbthread ⊕ L64))}.
Context `{Hpp3: !PrimcallProperties (EAsm.sprimitive_call (L:=PHBThread.phbthread ⊕ L64))}.
Context `{Hrel: !AsmIIE2IIE.IE2IERel (L := PHBThread.phbthread ⊕ L64)}.
Context `{Hdataprop: !LAsmAbsDataProp (L := PHBThread.phbthread ⊕ L64)}.
Theorem CertiKOS_correct:
∀ (s: stencil) (CTXT: LAsm.module) k1 k2 p combined_program user_program,
genv_next s = init_nb →
CertiKOS.per_thread_certikos = OK k1 →
CertiKOS.per_cpu_certikos = OK k2 →
∀ Hmp: make_program s ((CTXT ⊕ k1) ⊕ k2) (MBoot.mboot ⊕ L64) = OK combined_program,
make_program s (CTXT ⊕ k1) (PHThread.phthread ⊕ L64) = OK p →
make_program s CTXT (TSysCall.tsyscall ⊕ L64) = OK user_program →
noglobvar p →
inhabited
(backward_simulation
(HAsm.semantics (TSysCall.tsyscall ⊕ L64) user_program)
(HWStepSemImpl.hwstep_semantics
(Hmakege := make_program_globalenv _ _ _ _ Hmp)
(Genv.globalenv combined_program) s
((CTXT ⊕ k1) ⊕ k2)
combined_program)).
Proof.
intros.
assert (Hpb: make_program s (CTXT ⊕ k1) (PBThread.pbthread ⊕ L64) = OK p).
{
erewrite make_program_lsamep.
eapply H2.
eapply pbthread_phthread_lsamep.
}
assert (Hpbh: make_program s (CTXT ⊕ k1) (PHBThread.phbthread ⊕ L64) = OK p).
{
erewrite make_program_lsamep.
eapply H2.
apply phbthread_phthread_lsamep.
}
edestruct Per_Thread_CertiKOS_correct as [PER_THREAD_CORRECT]; try eassumption.
edestruct Per_CPU_CertiKOS_correct as [PER_CPU_CORRECT]; try eassumption.
constructor.
eapply compose_backward_simulation.
eapply HWStepSemImpl.hwstep_semantics_single_events.
eexact PER_THREAD_CORRECT.
eapply compose_backward_simulation.
eapply HWStepSemImpl.hwstep_semantics_single_events.
eapply @SingleCore_backward_simulation; eauto 2.
{ decision. }
simpl in Hpbh.
eexact Hpbh.
eapply compose_backward_simulation.
eapply HWStepSemImpl.hwstep_semantics_single_events.
exact PER_CPU_CORRECT.
apply concurrent_backward_simulation.
Qed.
End CERTIKOSCORRECT.