kernel/src/sk-kernel.adb

   1 --
   2 --  Copyright (C) 2013, 2015  Reto Buerki <reet@codelabs.ch>
   3 --  Copyright (C) 2013, 2015  Adrian-Ken Rueegsegger <ken@codelabs.ch>
   4 --
   5 --  This program is free software: you can redistribute it and/or modify
   6 --  it under the terms of the GNU General Public License as published by
   7 --  the Free Software Foundation, either version 3 of the License, or
   8 --  (at your option) any later version.
   9 --
  10 --  This program is distributed in the hope that it will be useful,
  11 --  but WITHOUT ANY WARRANTY; without even the implied warranty of
  12 --  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  13 --  GNU General Public License for more details.
  14 --
  15 --  You should have received a copy of the GNU General Public License
  16 --  along with this program.  If not, see <http://www.gnu.org/licenses/>.
  17 --
  18
  19 with Skp.Events;
  20 with Skp.Interrupts;
  21 with Skp.Kernel;
  22 with Skp.Subjects;
  23
  24 with SK.Apic;
  25 with SK.Bitops;
  26 with SK.CPU;
  27 with SK.Constants;
  28 with SK.Dump;
  29 with SK.KC;
  30 with SK.Version;
  31 with SK.Power;
  32 with SK.Strings;
  33 with SK.Subjects.Debug;
  34 with SK.System_State;
  35 with SK.VTd.Debug;
  36 with SK.VTd.Interrupts;
  37 with SK.Interrupts;
  38 with SK.Crash_Audit_Types;
  39
  40 package body SK.Kernel
  41 is
  42
  43    --  Initialize subject with given ID.
  44    procedure Init_Subject (ID : Skp.Global_Subject_ID_Type)
  45    with
  46       Global =>
  47         (Input  => (CPU_Info.APIC_ID, Interrupt_Tables.State,
  48                     VMX.Exit_Address),
  49          In_Out => (Crash_Audit.State, FPU.State, Subjects.State,
  50                     Subjects_Events.State, Subjects_Interrupts.State,
  51                     Subjects_MSR_Store.State, Timed_Events.State,
  52                     VMX.VMCS_State, X86_64.State));
  53
  54    -------------------------------------------------------------------------
  55
  56    use type Crash_Audit_Types.Reason_Type;
  57
  58    --  Allocate crash audit entry for given error and trigger system restart.
  59    procedure Error
  60      (Reason   : Crash_Audit_Types.Reason_Type;
  61       Subj_Ctx : Crash_Audit_Types.Subj_Context_Type
  62       := Crash_Audit_Types.Null_Subj_Context;
  63       MCE_Ctx  : Crash_Audit_Types.MCE_Context_Type
  64       := Crash_Audit_Types.Null_MCE_Context)
  65    with
  66       Pre => Reason /= Crash_Audit_Types.Reason_Undefined,
  67       No_Return
  68    is
  69       use type Crash_Audit_Types.Subj_Context_Type;
  70       use type Crash_Audit_Types.MCE_Context_Type;
  71
  72       A : Crash_Audit.Entry_Type;
  73    begin
  74       Crash_Audit.Allocate (Audit => A);
  75       Crash_Audit.Set_Reason
  76         (Audit  => A,
  77          Reason => Reason);
  78       if Subj_Ctx /= Crash_Audit_Types.Null_Subj_Context then
  79          Crash_Audit.Set_Subject_Context
  80            (Audit   => A,
  81             Context => Subj_Ctx);
  82       end if;
  83       if MCE_Ctx /= Crash_Audit_Types.Null_MCE_Context then
  84          Crash_Audit.Set_MCE_Context
  85            (Audit   => A,
  86             Context => MCE_Ctx);
  87       end if;
  88       Crash_Audit.Finalize (Audit => A);
  89    end Error;
  90
  91    -------------------------------------------------------------------------
  92
  93    --  Inject pending interrupt into subject identified by ID. Sets interrupt
  94    --  window if interrupt(s) remain pending.
  95    --D @Section Id => impl_inject_interrupt, Label => Interrupt Injection, Parent => impl_exit_handler, Priority => 70
  96    procedure Inject_Interrupt (Subject_ID : Skp.Global_Subject_ID_Type)
  97    with
  98       Global => (Input  => CPU_Info.APIC_ID,
  99                  In_Out => (Crash_Audit.State, Subjects_Interrupts.State,
 100                             Subjects.State, X86_64.State))
 101    is
 102       Vector            : Byte;
 103       Interrupt_Pending : Boolean;
 104    begin
 105       if Subjects.Accepts_Interrupts (ID => Subject_ID) then
 106          --D @Text Section => impl_inject_interrupt, Priority => 10
 107          --D If a subject is ready to accept interrupts, check if it has a
 108          --D pending interrupt.
 109          Subjects_Interrupts.Consume_Interrupt
 110            (Subject => Subject_ID,
 111             Found   => Interrupt_Pending,
 112             Vector  => Vector);
 113
 114          if Interrupt_Pending then
 115             --D @Text Section => impl_inject_interrupt, Priority => 10
 116             --D Consume the pending interrupt by writing the corresponding
 117             --D vector to the VM-entry interruption-information and setting the
 118             --D valid bit, see Intel SDM Vol. 3C, "26.6 Event Injection".
 119             VMX.VMCS_Write
 120               (Field => Constants.VM_ENTRY_INTERRUPT_INFO,
 121                Value => Constants.VM_INTERRUPT_INFO_VALID + Word64 (Vector));
 122
 123             if not Subjects.Is_Running (ID => Subject_ID) then
 124                --D @Text Section => impl_inject_interrupt, Priority => 10
 125                --D If the subject is currently sleeping, then set it to running.
 126                Subjects.Set_Running (ID    => Subject_ID,
 127                                      Value => True);
 128             end if;
 129          end if;
 130       end if;
 131
 132       --D @Text Section => impl_inject_interrupt, Priority => 10
 133       --D Then, check if the subject has more pending interrupts and activate
 134       --D interrupt window exiting if required, see Intel SDM Vol. 3C, "26.7.5
 135       --D Interrupt-Window Exiting and Virtual-Interrupt Delivery".
 136       Interrupt_Pending := Subjects_Interrupts.Has_Pending_Interrupt
 137         (Subject => Subject_ID);
 138       if Interrupt_Pending then
 139          VMX.VMCS_Set_Interrupt_Window (Value => True);
 140       end if;
 141    end Inject_Interrupt;
 142
 143    -------------------------------------------------------------------------
 144
 145    --D @Section Id => impl_handle_target_event, Label => Target Event Handling, Parent => impl_exit_handler, Priority => 60
 146    --D @Text Section => impl_handle_target_event
 147    --D Target events are actions performed prior to resuming execution of a
 148    --D given subject.
 149    procedure Handle_Pending_Target_Event
 150      (Subject_ID : Skp.Global_Subject_ID_Type)
 151    with
 152       Global =>
 153         (Input  => (CPU_Info.APIC_ID, Interrupt_Tables.State,
 154                     VMX.Exit_Address),
 155          In_Out => (Crash_Audit.State, FPU.State, Subjects.State,
 156                     Subjects_Events.State, Subjects_Interrupts.State,
 157                     Subjects_MSR_Store.State, Timed_Events.State,
 158                     VMX.VMCS_State, X86_64.State))
 159    is
 160       Found         : Boolean;
 161       Event_Handled : Boolean := False;
 162       Event_ID      : Skp.Events.Event_Range;
 163    begin
 164       for I in Skp.Events.Event_Range loop
 165          --D @Text Section => impl_handle_target_event
 166          --D First, check if the subject specified by ID has a target event
 167          --D pending by consulting the subject events data.
 168          Subjects_Events.Consume_Event
 169            (Subject => Subject_ID,
 170             Found   => Found,
 171             Event   => Event_ID);
 172
 173          exit when not Found;
 174
 175          Event_Handled := True;
 176
 177          --D @Text Section => impl_handle_target_event
 178          --D If an event is pending, it is consumed by looking up the target
 179          --D event and its action as specified by the policy.
 180          --D @UL Id => impl_handle_target_event_actions, Section => impl_handle_target_event
 181          declare
 182             Cur_Event : constant Skp.Events.Target_Event_Type
 183               := Skp.Events.Get_Target_Event (Subject_ID => Subject_ID,
 184                                               Event_Nr   => Event_ID);
 185          begin
 186             case Skp.Events.Get_Kind (Target_Event => Cur_Event)
 187             is
 188                when Skp.Events.No_Action        => null;
 189                   --D @Item List => impl_handle_target_event_actions
 190                   --D If the designated action is no action, then nothing is
 191                   --D done.
 192                when Skp.Events.Inject_Interrupt =>
 193                   --D @Item List => impl_handle_target_event_actions
 194                   --D If the designated action is interrupt injection, then the
 195                   --D interrupt with the vector specified in the policy is
 196                   --D marked as pending for the subject.
 197                   Subjects_Interrupts.Insert_Interrupt
 198                     (Subject => Subject_ID,
 199                      Vector  => Byte (Skp.Events.Get_Vector
 200                        (Target_Event => Cur_Event)));
 201                when Skp.Events.Reset            =>
 202                   --D @Item List => impl_handle_target_event_actions
 203                   --D If the designated action is subject reset, then the
 204                   --D subject state is initialized, see \ref{impl_subject_init}.
 205                   Init_Subject (ID => Subject_ID);
 206             end case;
 207          end;
 208          --D @Text Section => impl_handle_target_event, Priority => 10
 209          --D At most 64 target events are processed since that is the maximum
 210          --D number of events that can be pending.
 211       end loop;
 212
 213       if Event_Handled and not Subjects.Is_Running (ID => Subject_ID) then
 214          --D @Text Section => impl_handle_target_event, Priority => 10
 215          --D If an event was handled and the subject is currently sleeping, set
 216          --D it to running.
 217          Subjects.Set_Running (ID    => Subject_ID,
 218                                Value => True);
 219       end if;
 220    end Handle_Pending_Target_Event;
 221
 222    -------------------------------------------------------------------------
 223
 224    --D @Section Id => impl_handle_system_panic, Label => System Panic Action Handling, Parent => impl_handle_source_event, Priority => 10
 225    procedure Handle_System_Panic (Subject : Skp.Global_Subject_ID_Type)
 226    with
 227        Global => (Input  => (CPU_Info.APIC_ID, FPU.State, Subjects.State),
 228                   In_Out => (Crash_Audit.State, X86_64.State)),
 229        No_Return
 230    is
 231       S : Crash_Audit_Types.Subj_Context_Type;
 232    begin
 233       --D @Text Section => impl_handle_system_panic
 234       --D A system panic action triggered by a source event of a given subject
 235       --D is handled by creating a crash audit entry with the state of the
 236       --D triggering subject and invoking the crash audit facility.
 237       Subjects.Create_Context (ID  => Subject,
 238                                Ctx => S);
 239       FPU.Get_Registers (ID   => Subject,
 240                          Regs => S.FPU_Registers);
 241       pragma Debug (Dump.Print_Message (Msg => ">>> System Panic triggered"));
 242       pragma Debug (Subjects.Debug.Print_State (S => S));
 243       Error (Reason   => Crash_Audit_Types.Subj_System_Panic,
 244              Subj_Ctx => S);
 245    end Handle_System_Panic;
 246
 247    -------------------------------------------------------------------------
 248
 249    --D @Section Id => impl_handle_source_event, Label => Source Event Handling, Parent => impl_exit_handler, Priority => 50
 250    --D @Text Section => impl_handle_source_event
 251    --D Source events are actions performed when a given subject triggers a trap
 252    --D or a hypercall. Source events can also be triggered by the timed event
 253    --D mechanism. The increment RIP parameter specifies that the RIP of the
 254    --D subject should be incremented if necessary, as part of the event
 255    --D handling (e.g. sleep action).
 256    procedure Handle_Source_Event
 257      (Subject       :     Skp.Global_Subject_ID_Type;
 258       Event         :     Skp.Events.Source_Event_Type;
 259       Increment_RIP :     Boolean;
 260       Next_Subject  : out Skp.Global_Subject_ID_Type)
 261    with
 262       Global =>
 263         (Input  => (CPU_Info.APIC_ID, CPU_Info.CPU_ID, FPU.State,
 264                     Subjects_Interrupts.State,
 265                     Timed_Events.State),
 266          In_Out => (Crash_Audit.State, IO_Apic.State,
 267                     Scheduler.State, Scheduler.Group_Activity_Indicator,
 268                     Subjects.State, Subjects_Events.State, X86_64.State))
 269    is
 270       use type Skp.CPU_Range;
 271       use type Skp.Events.Target_Event_Range;
 272
 273       Dst_CPU : Skp.CPU_Range;
 274    begin
 275       --D @Text Section => impl_handle_source_event
 276       --D \paragraph*{}
 277       --D First, the next subject to be executed is initialized to the current
 278       --D one. A handover event may change this but otherwise the same subject
 279       --D is to be executed next.
 280       Next_Subject := Subject;
 281
 282       --D @Text Section => impl_handle_source_event
 283       --D Then the operation corresponding to the given source event action is
 284       --D performed.
 285       --D @UL Id => impl_handle_source_event_actions, Section => impl_handle_source_event, Priority => 10
 286       case Event.Source_Action
 287       is
 288          when Skp.Events.No_Action       => null;
 289             --D @Item List => impl_handle_source_event_actions
 290             --D If the designated action is no action, then nothing is
 291             --D done.
 292          when Skp.Events.Subject_Sleep   =>
 293             --D @Item List => impl_handle_source_event_actions
 294             --D If the designated action is subject sleep, then a rescheduling
 295             --D of the partition with parameter \verb!Sleep! set to \verb!True!
 296             --D is performed, see \ref{impl_scheduling_resched_sp}.
 297             Scheduler.Reschedule_Partition
 298               (Subject_ID    => Subject,
 299                Increment_RIP => Increment_RIP,
 300                Sleep         => True,
 301                Next_Subject  => Next_Subject);
 302          when Skp.Events.Subject_Yield   =>
 303             --D @Item List => impl_handle_source_event_actions
 304             --D If the designated action is subject yield, then a rescheduling
 305             --D of the partition with parameter \verb!Sleep! set to \verb!False!
 306             --D is performed, see \ref{impl_scheduling_resched_sp}.
 307             Scheduler.Reschedule_Partition
 308               (Subject_ID    => Subject,
 309                Increment_RIP => Increment_RIP,
 310                Sleep         => False,
 311                Next_Subject  => Next_Subject);
 312          when Skp.Events.System_Reboot   =>
 313             --D @Item List => impl_handle_source_event_actions
 314             --D If the designated action is system reboot, then a reboot with
 315             --D power-cycle is initiated.
 316             Power.Reboot (Power_Cycle => True);
 317          when Skp.Events.System_Poweroff =>
 318             --D @Item List => impl_handle_source_event_actions
 319             --D If the designated action is system poweroff, then a shutdown is
 320             --D initiated.
 321             Power.Shutdown;
 322          when Skp.Events.System_Panic =>
 323             --D @Item List => impl_handle_source_event_actions
 324             --D If the designated action is system panic, then the system panic
 325             --D handler is invoked.
 326             Handle_System_Panic (Subject => Subject);
 327          when Skp.Events.Unmask_Irq      =>
 328             --D @Item List => impl_handle_source_event_actions
 329             --D If the designated action is unmask IRQ, then use I/O APIC to
 330             --D unmask the IRQ designated by the event's IRQ number.
 331             IO_Apic.Unmask_IRQ
 332               (RTE_Index => Skp.Interrupts.RTE_Index_Type (Event.IRQ_Number));
 333       end case;
 334
 335       if Event.Target_Subject /= Skp.Invalid_Subject then
 336          if Event.Target_Event /= Skp.Events.Invalid_Target_Event then
 337             --D @Text Section => impl_handle_source_event, Priority => 20
 338             --D If the source event has a valid target subject and target event
 339             --D set, then mark the target event pending for the designated
 340             --D subject.
 341             Subjects_Events.Set_Event_Pending
 342               (Subject  => Event.Target_Subject,
 343                Event_ID => Event.Target_Event);
 344
 345             Dst_CPU := Skp.Subjects.Get_CPU_ID
 346               (Subject_ID => Event.Target_Subject);
 347
 348             --D @Text Section => impl_handle_source_event, Priority => 20
 349             --D Indicate activity for the target subject which may lead to a
 350             --D subject being woken up if it is currently sleeping, see
 351             --D \ref{impl_scheduling_indicate_activity}.
 352             Scheduler.Indicate_Activity
 353               (Subject_ID => Event.Target_Subject,
 354                Same_CPU   => Dst_CPU = CPU_Info.CPU_ID);
 355
 356             if Event.Send_IPI then
 357                --D @Text Section => impl_handle_source_event, Priority => 20
 358                --D Additionally, send an IPI to the CPU running the target
 359                --D subject if specified by the policy.
 360                Apic.Send_IPI (Vector => Constants.IPI_Vector,
 361                               CPU_ID => Dst_CPU);
 362             end if;
 363          end if;
 364
 365          if Event.Handover then
 366             --D @Text Section => impl_handle_source_event, Priority => 20
 367             --D If the source event has a valid target subject and it is a
 368             --D handover event, then set the target subject as the next subject
 369             --D to run.
 370             Next_Subject := Event.Target_Subject;
 371             Scheduler.Set_Current_Subject_ID (Subject_ID => Next_Subject);
 372          end if;
 373       end if;
 374    end Handle_Source_Event;
 375
 376    -------------------------------------------------------------------------
 377
 378    --  Handle hypercall with given event number.
 379    --D @Section Id => hypercall_handling, Label => Hypercall Handling, Parent => impl_exit_handler, Priority => 20
 380    --D @Text Section => hypercall_handling
 381    --D Hypercalls can be triggered by subjects executing the \verb!vmcall!
 382    --D instruction in guest privilege level 0, which is assured by means of a
 383    --D precondition check. If subject user space/ring-3 tries to invoke
 384    --D hypercalls, the VM-Exit is handled as a trap with exit reason
 385    --D \verb!VMCALL!, see \verb!Handle_Trap!.
 386    procedure Handle_Hypercall
 387      (Current_Subject    : Skp.Global_Subject_ID_Type;
 388       Unchecked_Event_Nr : Word64)
 389    with
 390       Global =>
 391         (Input  => (CPU_Info.APIC_ID, CPU_Info.CPU_ID, FPU.State,
 392                     Subjects_Interrupts.State, Timed_Events.State),
 393          In_Out => (Crash_Audit.State, IO_Apic.State, Scheduler.State,
 394                     Scheduler.Group_Activity_Indicator,
 395                     Subjects.State, Subjects_Events.State, X86_64.State)),
 396       Pre    => Subjects.Is_CPL_0 (ID => Current_Subject)
 397    is
 398       --  XXX: Only current wavefronts report that use type clause has no
 399       --       effect. To keep compatibility with earlier toolchains disable
 400       --       all warnings.
 401       pragma $Release_Warnings (Off, -- "use clause for type * has no effect",
 402                                 Reason => "Only used for debug output");
 403       use type Skp.Events.Source_Event_Type;
 404       pragma $Release_Warnings (On);
 405
 406       --  The following code operating on Unchecked_Event_Nr was specifically
 407       --  constructed to defend against Spectre Variant 1 attacks
 408       --  (CVE-2017-5753), i.e. it is important NOT to use the unchecked
 409       --  user-supplied value as index into an array after a conditional
 410       --  checking this variable.
 411
 412       Event_Nr        : constant Skp.Events.Event_Range
 413         := Skp.Events.Event_Range
 414           (Unchecked_Event_Nr and Skp.Events.Event_Mask);
 415       Valid_Event_Nr  : constant Boolean
 416         := Word64 (Event_Nr) = Unchecked_Event_Nr;
 417       Event           : Skp.Events.Source_Event_Type;
 418       Next_Subject_ID : Skp.Global_Subject_ID_Type := Current_Subject;
 419    begin
 420       --D @Text Section => hypercall_handling
 421       --D First the event number of the hypercall is checked. If it is valid
 422       --D then the corresponding subject source event as specified by the
 423       --D policy is looked up and processed, see
 424       --D \ref{impl_handle_source_event}. Note that events that are not
 425       --D specified in the policy are ignored since these are initialized to
 426       --D source events that have no action and an invalid target subject.
 427       if Valid_Event_Nr then
 428          Event := Skp.Events.Get_Source_Event
 429            (Subject_ID => Current_Subject,
 430             Event_Nr   => Event_Nr);
 431          Handle_Source_Event
 432            (Subject       => Current_Subject,
 433             Event         => Event,
 434             Increment_RIP => False,
 435             Next_Subject  => Next_Subject_ID);
 436       end if;
 437
 438       pragma Debug (not Valid_Event_Nr or else
 439                     Event = Skp.Events.Null_Source_Event,
 440                     Dump.Print_Spurious_Event
 441                       (Current_Subject => Current_Subject,
 442                        Event_Nr        => Unchecked_Event_Nr));
 443
 444       --D @Text Section => hypercall_handling
 445       --D After handling the source event, the instruction pointer of the
 446       --D current subject is incremented so execution resumes after the
 447       --D \texttt{vmcall} instruction.
 448       Subjects.Increment_RIP (ID => Current_Subject);
 449
 450       --D @Text Section => hypercall_handling, Priority => 20
 451       --D If the hypercall triggered a handover event, load the new VMCS.
 452       if Current_Subject /= Next_Subject_ID then
 453          VMX.Load (VMCS_Address => Skp.Subjects.Get_VMCS_Address
 454                    (Subject_ID => Next_Subject_ID));
 455       end if;
 456    end Handle_Hypercall;
 457
 458    -------------------------------------------------------------------------
 459
 460    --  Handle external interrupt request with given vector.
 461    --D @Section Id => impl_handle_irq, Label => External Interrupt Handling, Parent => impl_exit_handler, Priority => 10
 462    procedure Handle_Irq (Vector : Byte)
 463    with
 464       Global => (Input  => Scheduler.State,
 465                  In_Out => (IO_Apic.State, Scheduler.Group_Activity_Indicator,
 466                             Subjects_Interrupts.State, X86_64.State))
 467    is
 468       Vect_Nr : Skp.Interrupts.Remapped_Vector_Type;
 469       Route   : Skp.Interrupts.Vector_Route_Type;
 470    begin
 471       --D @Text Section => impl_handle_irq
 472       --D First the vector of the external interrupt is validated. If it is an
 473       --D IPI or VT-d fault vector, no further action is taken since the purpose
 474       --D was to force a VM exit of the currently executing subject. A
 475       --D subsequent subject VM entry leads to the evaluation of pending target
 476       --D events and subject interrupts.
 477       if Vector >= Skp.Interrupts.Remap_Offset
 478         and then Vector < Constants.VTd_Fault_Vector
 479       then
 480          --D @Text Section => impl_handle_irq
 481          --D \paragraph{}
 482          --D If the vector is valid and neither an IPI nor VT-d fault vector,
 483          --D consult the vector routing table to determine the target subject
 484          --D and vector as specified by the policy and insert the target
 485          --D vector by marking it as pending. Note that there is no
 486          --D switching to the destination of the IRQ. The interrupt will be
 487          --D delivered whenever the target subject is executed according to the
 488          --D scheduling plan (i.e. IRQs are not preemptive).
 489          Vect_Nr := Skp.Interrupts.Remapped_Vector_Type (Vector);
 490          Route   := Skp.Interrupts.Vector_Routing (Vect_Nr);
 491          if Route.Subject in Skp.Global_Subject_ID_Type then
 492             Subjects_Interrupts.Insert_Interrupt
 493               (Subject => Route.Subject,
 494                Vector  => Byte (Route.Vector));
 495             --D \paragraph{}
 496             --D Then, indicate activity for the subject in order to make sure
 497             --D that potentially sleeping target subjects are woken up. Note
 498             --D that IRQs are always routed to CPUs executing the target
 499             --D subject.
 500             Scheduler.Indicate_Activity
 501               (Subject_ID => Route.Subject,
 502                Same_CPU   => True);
 503          end if;
 504
 505          --D @Text Section => impl_handle_irq
 506          --D \paragraph{}
 507          --D If the interrupt vector designates an IRQ that must be masked,
 508          --D instruct the I/O APIC to mask the corresponding redirection
 509          --D table entry.
 510          if Vect_Nr in Skp.Interrupts.Mask_IRQ_Type then
 511             IO_Apic.Mask_IRQ
 512               (RTE_Index => Skp.Interrupts.RTE_Index_Type (Vector - 32));
 513          end if;
 514
 515          pragma Debug (Route.Subject not in Skp.Global_Subject_ID_Type,
 516                        Dump.Print_Message
 517                          (Msg => "Spurious IRQ vector "
 518                           & Strings.Img (Vector)));
 519       end if;
 520
 521       pragma Debug (Vector = Constants.VTd_Fault_Vector,
 522                     VTd.Debug.Process_Fault);
 523       pragma Debug (Vector < Skp.Interrupts.Remap_Offset,
 524                     Dump.Print_Message
 525                       (Msg => "IRQ with invalid vector "
 526                        & Strings.Img (Vector)));
 527
 528       --D @Text Section => impl_handle_irq
 529       --D \paragraph{}
 530       --D Finally, signal to the local APIC that the interrupt servicing has
 531       --D completed and other IRQs may be issued once interrupts are re-enabled.
 532       Apic.EOI;
 533    end Handle_Irq;
 534
 535    -------------------------------------------------------------------------
 536
 537    --  Handle Xsetbv trap of current subject by validating new XCR0 value and
 538    --  setting the corresponding register in the associated FPU state.
 539    --D @Section Id => impl_handle_xsetbv, Label => Xsetbv handling, Parent => impl_exit_handler, Priority => 80
 540    procedure Handle_Xsetbv
 541      (Current_Subject : Skp.Global_Subject_ID_Type;
 542       RAX, RDX, RCX   : Word64)
 543    is
 544       Supported : constant Word64 := FPU.Get_Active_XCR0_Features;
 545       Index     : constant Word32 := Word32'Mod (RCX);
 546       New_Value : constant Word64 := Word64 (Word32'Mod (RDX)) * 2 ** 32
 547         + Word64 (Word32'Mod (RAX));
 548    begin
 549       --D @Text Section => impl_handle_xsetbv
 550       --D Subjects can toggle FPU features by writing to XCR0 using the
 551       --D \verb!xsetbv! instruction. The provided value is validated according
 552       --D to Intel SDM Vol. 1,
 553       --D "13.3 Enabling the XSAVE Feature Set and XSAVE-Enabled Features":
 554       --D @OL Id => impl_handle_xsetbv_checks, Section => impl_handle_xsetbv, Priority => 10
 555       --D @Item List => impl_handle_xsetbv_checks
 556       --D Privilege Level (CPL0) must be 0.
 557       if not Subjects.Is_CPL_0 (ID => Current_Subject)
 558         --D @Item List => impl_handle_xsetbv_checks
 559         --D Register index must be 0, only XCR0 is supported.
 560         or else Index /= 0
 561         --D @Item List => impl_handle_xsetbv_checks
 562         --D Only bits that we support must be set.
 563         or else (Supported or New_Value) /= Supported
 564           --D @Item List => impl_handle_xsetbv_checks
 565           --D \verb!XCR0_FPU_STATE_FLAG! must always be set
 566         or else not Bitops.Bit_Test
 567           (Value => New_Value,
 568            Pos   => Constants.XCR0_FPU_STATE_FLAG)
 569         --D @Item List => impl_handle_xsetbv_checks
 570         --D If \verb!XCR0_AVX_STATE_FLAG! is set then \verb!XCR0_SSE_STATE_FLAG!
 571         --D must be set as well.
 572         or else (Bitops.Bit_Test
 573                  (Value => New_Value,
 574                   Pos   => Constants.XCR0_AVX_STATE_FLAG)
 575                  and not Bitops.Bit_Test
 576                    (Value => New_Value,
 577                     Pos   => Constants.XCR0_SSE_STATE_FLAG))
 578         --D @Item List => impl_handle_xsetbv_checks
 579         --D If any of \verb!XCR0_OPMASK_STATE_FLAG! or
 580         --D \verb!XCR0_ZMM_HI256_STATE_FLAG! or \\
 581         --D \verb!XCR0_HI16_ZMM_STATE_FLAG! are set then all must be set.
 582         or else ((Bitops.Bit_Test
 583                   (Value => New_Value,
 584                    Pos   => Constants.XCR0_OPMASK_STATE_FLAG)
 585                   or Bitops.Bit_Test
 586                     (Value => New_Value,
 587                      Pos   => Constants.XCR0_ZMM_HI256_STATE_FLAG)
 588                   or Bitops.Bit_Test
 589                     (Value => New_Value,
 590                      Pos   => Constants.XCR0_ZMM_HI256_STATE_FLAG))
 591                  and not
 592                    (Bitops.Bit_Test
 593                         (Value => New_Value,
 594                          Pos   => Constants.XCR0_OPMASK_STATE_FLAG)
 595                     and Bitops.Bit_Test
 596                       (Value => New_Value,
 597                        Pos   => Constants.XCR0_ZMM_HI256_STATE_FLAG)
 598                     and Bitops.Bit_Test
 599                       (Value => New_Value,
 600                        Pos   => Constants.XCR0_ZMM_HI256_STATE_FLAG)))
 601         --D @Item List => impl_handle_xsetbv_checks
 602         --D If \verb!AVX512! is set then \verb!XCR0_AVX_STATE_FLAG! must be set
 603         --D as well.
 604         or else (Bitops.Bit_Test
 605                  (Value => New_Value,
 606                   Pos   => Constants.XCR0_OPMASK_STATE_FLAG)
 607                  and not Bitops.Bit_Test
 608                    (Value => New_Value,
 609                     Pos   => Constants.XCR0_AVX_STATE_FLAG))
 610       then
 611
 612          --D @Text Section => impl_handle_xsetbv
 613          --D If the value is invalid, inject a \#GP exception. Note that
 614          --D effectively the inserted event has type \emph{external interrupt}.
 615          --D While it would not work in general but in this specific case the
 616          --D exception error code is 0.
 617
 618          Subjects_Interrupts.Insert_Interrupt
 619            (Subject => Current_Subject,
 620             Vector  => Constants.GP_Exception_Vector);
 621       else
 622
 623          --D @Text Section => impl_handle_xsetbv
 624          --D If the value is valid, set the corresponding subject XCR0 value,
 625          --D increment the subject RIP and resume execution.
 626
 627          FPU.Set_XCR0 (ID    => Current_Subject,
 628                        Value => New_Value);
 629          Subjects.Increment_RIP (ID => Current_Subject);
 630       end if;
 631    end Handle_Xsetbv;
 632
 633    -------------------------------------------------------------------------
 634
 635    --D @Section Id => impl_handle_timer_expiry, Label => Timer Expiry, Parent => impl_exit_handler, Priority => 40
 636    --D @Text Section => impl_handle_timer_expiry
 637    --D The VMX timer expiration designates the end of a minor frame. Handle the
 638    --D timer expiry by updating the current scheduling information and checking
 639    --D if a timed event has expired as well.
 640    procedure Handle_Timer_Expiry (Current_Subject : Skp.Global_Subject_ID_Type)
 641      with
 642        Global =>
 643          (Input  => (CPU_Info.APIC_ID, CPU_Info.CPU_ID, CPU_Info.Is_BSP,
 644                      FPU.State, Subjects_Interrupts.State,
 645                      Tau0_Interface.State),
 646           In_Out => (Crash_Audit.State, IO_Apic.State, MP.Barrier,
 647                      Scheduler.State, Scheduler.Group_Activity_Indicator,
 648                      Scheduling_Info.State, Subjects.State,
 649                      Subjects_Events.State, Timed_Events.State, X86_64.State))
 650    is
 651       Next_Subject_ID : Skp.Global_Subject_ID_Type;
 652    begin
 653       Scheduler.Update_Scheduling_Info (Next_Subject => Next_Subject_ID);
 654
 655       --  Check and possibly handle timed event of subject.
 656
 657       declare
 658          Event_Subj    : constant Skp.Global_Subject_ID_Type
 659            := Next_Subject_ID;
 660          Trigger_Value : Word64;
 661          Event_Nr      : Skp.Events.Event_Range;
 662          TSC_Now       : constant Word64 := CPU.RDTSC;
 663       begin
 664
 665          --D @Text Section => impl_handle_timer_expiry, Priority => 20
 666          --D \paragraph{}
 667          --D Check if timed event has expired and handle source event if
 668          --D necessary.
 669          Timed_Events.Get_Event (Subject           => Event_Subj,
 670                                  TSC_Trigger_Value => Trigger_Value,
 671                                  Event_Nr          => Event_Nr);
 672          if Trigger_Value <= TSC_Now then
 673             Handle_Source_Event
 674               (Subject       => Event_Subj,
 675                Event         => Skp.Events.Get_Source_Event
 676                  (Subject_ID => Event_Subj,
 677                   Event_Nr   => Skp.Events.Target_Event_Range (Event_Nr)),
 678                Increment_RIP => False,
 679                Next_Subject  => Next_Subject_ID);
 680             Timed_Events.Clear_Event (Subject => Event_Subj);
 681          end if;
 682       end;
 683
 684       --D @Text Section => impl_handle_timer_expiry, Priority => 20
 685       --D If the new minor frame designates a different subject, load its VMCS.
 686       if Current_Subject /= Next_Subject_ID then
 687
 688          --  New minor frame contains different subject -> Load VMCS.
 689
 690          VMX.Load (VMCS_Address => Skp.Subjects.Get_VMCS_Address
 691                    (Subject_ID => Next_Subject_ID));
 692       end if;
 693    end Handle_Timer_Expiry;
 694
 695    -------------------------------------------------------------------------
 696
 697    --  Handle trap with given number using trap table of current subject.
 698    --D @Section Id => impl_handle_trap, Label => Trap Handling, Parent => impl_exit_handler, Priority => 30
 699    procedure Handle_Trap
 700      (Current_Subject : Skp.Global_Subject_ID_Type;
 701       Trap_Nr         : Word16)
 702    with
 703       Global =>
 704         (Input  => (CPU_Info.APIC_ID, CPU_Info.CPU_ID, FPU.State,
 705                     Subjects_Interrupts.State, Timed_Events.State),
 706          In_Out => (Crash_Audit.State, IO_Apic.State, Scheduler.State,
 707                     Scheduler.Group_Activity_Indicator,
 708                     Subjects.State, Subjects_Events.State, X86_64.State))
 709    is
 710       Trap_Entry      : Skp.Events.Source_Event_Type;
 711       Next_Subject_ID : Skp.Global_Subject_ID_Type;
 712       Valid_Trap_Nr   : Boolean;
 713
 714       ----------------------------------------------------------------------
 715
 716       procedure Panic_Unknown_Trap
 717       with
 718          Global => (Input  => (Current_Subject, CPU_Info.APIC_ID, FPU.State,
 719                                Subjects.State),
 720                     In_Out => (Crash_Audit.State, X86_64.State)),
 721          No_Return
 722       is
 723          S : Crash_Audit_Types.Subj_Context_Type;
 724       begin
 725          Subjects.Create_Context (ID  => Current_Subject,
 726                                   Ctx => S);
 727          FPU.Get_Registers (ID   => Current_Subject,
 728                             Regs => S.FPU_Registers);
 729          pragma Debug (Dump.Print_Message (Msg => ">>> Unknown trap "
 730                                            & Strings.Img (Trap_Nr)));
 731          pragma Debug (Subjects.Debug.Print_State (S => S));
 732          Error (Reason   => Crash_Audit_Types.Subj_Unknown_Trap,
 733                 Subj_Ctx => S);
 734       end Panic_Unknown_Trap;
 735    begin
 736       --D @Text Section => impl_handle_trap
 737       --D First the trap number is checked. If it is outside the valid trap
 738       --D range an appropriate crash audit record is written and an error
 739       --D condition is signaled.
 740       Valid_Trap_Nr := Trap_Nr <= Word16 (Skp.Events.Trap_Range'Last);
 741       if not Valid_Trap_Nr then
 742          Panic_Unknown_Trap;
 743       end if;
 744
 745       --D @Text Section => impl_handle_trap
 746       --D \paragraph{}
 747       --D If the trap number is valid then the corresponding subject trap entry
 748       --D as specified by the policy is looked up. Note that the policy
 749       --D validation tools enforce that an event must be specified for each
 750       --D trap ID.
 751       Trap_Entry := Skp.Events.Get_Trap
 752         (Subject_ID => Current_Subject,
 753          Trap_Nr    => Skp.Events.Trap_Range (Trap_Nr));
 754
 755       --D @Text Section => impl_handle_trap
 756       --D The source event designated by the policy trap entry is processed,
 757       --D see \ref{impl_handle_source_event}.
 758       Handle_Source_Event
 759         (Subject       => Current_Subject,
 760          Event         => Trap_Entry,
 761          Increment_RIP => True,
 762          Next_Subject  => Next_Subject_ID);
 763
 764       --D @Text Section => impl_handle_trap, Priority => 20
 765       --D If the trap triggered a handover event, load the new VMCS.
 766       if Current_Subject /= Next_Subject_ID then
 767          VMX.Load (VMCS_Address => Skp.Subjects.Get_VMCS_Address
 768                    (Subject_ID => Next_Subject_ID));
 769       end if;
 770    end Handle_Trap;
 771
 772    -------------------------------------------------------------------------
 773
 774    --D @Section Id => impl_exit_handler, Label => VMX Exit Handling, Parent => implementation, Priority => -5
 775    --D @Text Section => impl_exit_handler
 776    --D The VMX exit handle procedure \texttt{Handle\_Vmx\_Exit} is the main
 777    --D subprogram of the kernel.
 778    --D It is invoked whenever the execution of a subject stops and an exit into
 779    --D VMX root mode is performed by the hardware. The register state of the
 780    --D current subject is passed to the procedure by the
 781    --D \texttt{vmx\_exit\_handler} assembly code (which is set as kernel entry
 782    --D point/\verb!HOST_RIP! in the VMCS of the trapping subject, see
 783    --D \ref{impl_vmcs_setup_host}).
 784    procedure Handle_Vmx_Exit (Subject_Registers : in out CPU_Registers_Type)
 785    is
 786       --  See Intel SDM Vol. 3C, "27.2.2 Information for VM Exits Due to
 787       --  Vectored Events".
 788       Exception_Mask : constant := 16#07ff#;
 789       Exception_NMI  : constant := 16#0202#;
 790       Exception_MCE  : constant := 16#0312#;
 791
 792       Exit_Reason            : Word64;
 793       Exit_Interruption_Info : Word64;
 794       Basic_Exit_Reason      : Word16;
 795       Current_Subject        : Skp.Global_Subject_ID_Type;
 796    begin
 797       Current_Subject := Scheduler.Get_Current_Subject_ID;
 798
 799       VMX.VMCS_Read (Field => Constants.VMX_EXIT_REASON,
 800                      Value => Exit_Reason);
 801       Basic_Exit_Reason := Word16 (Exit_Reason and 16#ffff#);
 802
 803       --D @Text Section => impl_exit_handler
 804       --D The \texttt{Handle\_Vmx\_Exit} procedure first saves the state of the
 805       --D subject that has just trapped into the exit handler, along with the
 806       --D register values and the exit reason, see
 807       --D \ref{impl_subjects_state_save}.
 808       --D Analogously, the FPU state of the current subject is saved.
 809       Subjects.Save_State (ID          => Current_Subject,
 810                            Exit_Reason => Exit_Reason,
 811                            Regs        => Subject_Registers);
 812
 813       FPU.Save_State (ID => Current_Subject);
 814
 815       VMX.VMCS_Read (Field => Constants.VMX_EXIT_INTR_INFO,
 816                      Value => Exit_Interruption_Info);
 817
 818       --D @Text Section => impl_exit_handler
 819       --D Then, the exit reason is examined and depending on the cause the
 820       --D corresponding handler is called.
 821       --D \paragraph{}
 822       --D If an unrecoverable error occurs, i.e. NMI or MCE, a crash audit
 823       --D record with the appropriate error information is allocated and the
 824       --D kernel performs a controlled system restart.
 825       if Basic_Exit_Reason = Constants.EXIT_REASON_EXTERNAL_INT then
 826          Handle_Irq (Vector => Byte'Mod (Exit_Interruption_Info));
 827       elsif Basic_Exit_Reason = Constants.EXIT_REASON_VMCALL
 828         and then Subjects.Is_CPL_0 (ID => Current_Subject)
 829       then
 830          Handle_Hypercall (Current_Subject    => Current_Subject,
 831                            Unchecked_Event_Nr => Subject_Registers.RAX);
 832       elsif Basic_Exit_Reason = Constants.EXIT_REASON_TIMER_EXPIRY then
 833          Handle_Timer_Expiry (Current_Subject => Current_Subject);
 834       elsif Basic_Exit_Reason = Constants.EXIT_REASON_INTERRUPT_WINDOW then
 835
 836          --  Resume subject to inject pending interrupt.
 837
 838          VMX.VMCS_Set_Interrupt_Window (Value => False);
 839       elsif Basic_Exit_Reason = Constants.EXIT_REASON_EXCEPTION_NMI
 840         and then
 841           (Exit_Interruption_Info and Exception_Mask) = Exception_NMI
 842       then
 843          pragma Debug (Dump.Print_Message
 844                        (Msg => "*** CPU APIC ID " & Strings.Img
 845                         (Byte (CPU_Info.APIC_ID))
 846                         & " VM exit due to NMI; interruption information "
 847                         & Strings.Img (Exit_Interruption_Info)));
 848          Error (Reason => Crash_Audit_Types.Hardware_VMexit_NMI);
 849       elsif Basic_Exit_Reason = Constants.EXIT_REASON_EXCEPTION_NMI
 850         and then (Exit_Interruption_Info and Exception_Mask) = Exception_MCE
 851       then
 852          pragma Debug (Dump.Print_Message
 853                        (Msg => "*** CPU APIC ID " & Strings.Img
 854                         (Byte (CPU_Info.APIC_ID))
 855                         & " VM exit due to MCE; interruption information "
 856                         & Strings.Img (Exit_Interruption_Info)));
 857          declare
 858             Ctx : Crash_Audit_Types.MCE_Context_Type;
 859          begin
 860             MCE.Create_Context (Ctx => Ctx);
 861             Error (Reason  => Crash_Audit_Types.Hardware_VMexit_MCE,
 862                    MCE_Ctx => Ctx);
 863          end;
 864       elsif Basic_Exit_Reason = Constants.EXIT_REASON_ENTRY_FAIL_MCE then
 865          pragma Debug (Dump.Print_Message
 866                        (Msg => "*** CPU APIC ID " & Strings.Img
 867                         (Byte (CPU_Info.APIC_ID))
 868                         & " VM entry failed due to MCE"));
 869          declare
 870             Ctx : Crash_Audit_Types.MCE_Context_Type;
 871          begin
 872             MCE.Create_Context (Ctx => Ctx);
 873             Error (Reason  => Crash_Audit_Types.Hardware_VMentry_MCE,
 874                    MCE_Ctx => Ctx);
 875          end;
 876       elsif Basic_Exit_Reason = Constants.EXIT_REASON_XSETBV then
 877          Handle_Xsetbv (Current_Subject => Current_Subject,
 878                         RAX             => Subject_Registers.RAX,
 879                         RDX             => Subject_Registers.RDX,
 880                         RCX             => Subject_Registers.RCX);
 881       else
 882          Handle_Trap (Current_Subject => Current_Subject,
 883                       Trap_Nr         => Basic_Exit_Reason);
 884       end if;
 885
 886       --D @Text Section => impl_exit_handler
 887       --D \paragraph{}
 888       --D Once the exit has been dealt with, the execution of the next subject
 889       --D is prepared. Pending target events, if present, are handled see
 890       --D \ref{impl_handle_target_event}.
 891       Current_Subject := Scheduler.Get_Current_Subject_ID;
 892       Handle_Pending_Target_Event (Subject_ID => Current_Subject);
 893       --D @Text Section => impl_exit_handler
 894       --D Then, a pending interrupt, if present, is prepared for injection, see
 895       --D \ref{impl_inject_interrupt}.
 896       Inject_Interrupt (Subject_ID => Current_Subject);
 897
 898       --D @Text Section => impl_exit_handler
 899       --D \paragraph{}
 900       --D Finally, the VMX preemption timer is armed, the FPU and subject states
 901       --D are restored, see \ref{impl_subjects_state_restore}. Additionally, to
 902       --D ensure the precondition of \texttt{Subjects.Restore\_State}, the state
 903       --D is filtered beforehand, see \ref{impl_subjects_state_filter}.
 904       Scheduler.Set_VMX_Exit_Timer;
 905       FPU.Restore_State (ID => Current_Subject);
 906       Subjects.Filter_State (ID => Current_Subject);
 907       Subjects.Restore_State
 908         (ID   => Current_Subject,
 909          Regs => Subject_Registers);
 910       --D @Text Section => impl_exit_handler
 911       --D The register values of the subject to be executed are returned by the
 912       --D procedure. The calling assembler code then performs an entry to
 913       --D VMX non-root mode, thereby instructing the hardware to resume
 914       --D execution of the subject designated by the currently active VMCS.
 915    end Handle_Vmx_Exit;
 916
 917    -------------------------------------------------------------------------
 918
 919    --D @Section Id => impl_subject_init, Label => Subject Initialization, Parent => impl_kernel_init_sched, Priority => 20
 920    --D @Text Section => impl_subject_init
 921    --D Clear all state associated with the subject specified by ID and
 922    --D initialize to the values of the subject according to the policy. These
 923    --D steps are performed during startup and whenever a subject is reset.
 924    --D @OL Id => subject_init_steps, Section => impl_subject_init, Priority => 10
 925    procedure Init_Subject (ID : Skp.Global_Subject_ID_Type)
 926    is
 927       Controls  : constant Skp.Subjects.VMX_Controls_Type
 928         := Skp.Subjects.Get_VMX_Controls (Subject_ID => ID);
 929       VMCS_Addr : constant Word64
 930         := Skp.Subjects.Get_VMCS_Address (Subject_ID => ID);
 931       MSR_Count : constant Word32
 932         := Skp.Subjects.Get_MSR_Count (Subject_ID => ID);
 933    begin
 934       --D @Item List => subject_init_steps
 935       --D Reset FPU state for subject with given ID.
 936       FPU.Reset_State (ID => ID);
 937       --D @Item List => subject_init_steps
 938       --D Clear pending events of subject with given ID.
 939       Subjects_Events.Clear_Events (Subject => ID);
 940       --D @Item List => subject_init_steps
 941       --D Initialize pending interrupts of subject with given ID.
 942       Subjects_Interrupts.Init_Interrupts (Subject => ID);
 943       --D @Item List => subject_init_steps
 944       --D Initialize timed event of subject with given ID.
 945       Timed_Events.Init_Event (Subject => ID);
 946
 947       if MSR_Count > 0 then
 948          --D @Item List => subject_init_steps
 949          --D Clear all MSRs in MSR storage area if subject has access to MSRs.
 950          Subjects_MSR_Store.Clear_MSRs (Subject => ID);
 951       end if;
 952
 953       --D @Item List => subject_init_steps
 954       --D Reset VMCS of subject and make it active by loading it.
 955       VMX.Reset (VMCS_Address => VMCS_Addr,
 956                  Subject_ID   => ID);
 957       VMX.Load  (VMCS_Address => VMCS_Addr);
 958       --D @Item List => subject_init_steps
 959       --D Set VMCS control fields according to policy.
 960       VMX.VMCS_Setup_Control_Fields
 961         (IO_Bitmap_Address  => Skp.Subjects.Get_IO_Bitmap_Address
 962            (Subject_ID => ID),
 963          MSR_Bitmap_Address => Skp.Subjects.Get_MSR_Bitmap_Address
 964            (Subject_ID => ID),
 965          MSR_Store_Address  => Skp.Subjects.Get_MSR_Store_Address
 966            (Subject_ID => ID),
 967          MSR_Count          => MSR_Count,
 968          Ctls_Exec_Pin      => Controls.Exec_Pin,
 969          Ctls_Exec_Proc     => Controls.Exec_Proc,
 970          Ctls_Exec_Proc2    => Controls.Exec_Proc2,
 971          Ctls_Exit          => Controls.Exit_Ctrls,
 972          Ctls_Entry         => Controls.Entry_Ctrls,
 973          CR0_Mask           => Skp.Subjects.Get_CR0_Mask
 974            (Subject_ID => ID),
 975          CR4_Mask           => Skp.Subjects.Get_CR4_Mask
 976            (Subject_ID => ID),
 977          Exception_Bitmap   => Skp.Subjects.Get_Exception_Bitmap
 978            (Subject_ID => ID));
 979       --D @Item List => subject_init_steps
 980       --D Setup VMCS host fields.
 981       VMX.VMCS_Setup_Host_Fields;
 982       --D @Item List => subject_init_steps
 983       --D Setup VMCS guest fields according to policy.
 984       VMX.VMCS_Setup_Guest_Fields
 985         (PML4_Address => Skp.Subjects.Get_PML4_Address (Subject_ID => ID),
 986          EPT_Pointer  => Skp.Subjects.Get_EPT_Pointer (Subject_ID => ID));
 987       --D @Item List => subject_init_steps
 988       --D Reset CPU state of subject according to policy.
 989       Subjects.Reset_State
 990         (ID         => ID,
 991          GPRs       => Skp.Subjects.Get_GPRs (Subject_ID => ID),
 992          RIP        => Skp.Subjects.Get_Entry_Point (Subject_ID => ID),
 993          RSP        => Skp.Subjects.Get_Stack_Address (Subject_ID => ID),
 994          CR0        => Skp.Subjects.Get_CR0 (Subject_ID => ID),
 995          CR0_Shadow => Skp.Subjects.Get_CR0_Shadow (Subject_ID => ID),
 996          CR4        => Skp.Subjects.Get_CR4 (Subject_ID => ID),
 997          CR4_Shadow => Skp.Subjects.Get_CR4_Shadow (Subject_ID => ID),
 998          Segments   => Skp.Subjects.Get_Segment_Registers (Subject_ID => ID));
 999    end Init_Subject;
1000
1001    -------------------------------------------------------------------------
1002
1003    procedure Init_Subjects
1004    is
1005       use type Skp.CPU_Range;
1006    begin
1007       --D @Item List => impl_kernel_init_steps, Priority => 10
1008       --D Setup VMCS and state of each subject running on this logical CPU,
1009       --D see \ref{impl_subject_init}.
1010       for I in Skp.Global_Subject_ID_Type loop
1011          if Skp.Subjects.Get_CPU_ID (Subject_ID => I) = CPU_Info.CPU_ID then
1012             Init_Subject (ID => I);
1013          end if;
1014       end loop;
1015    end Init_Subjects;
1016
1017    -------------------------------------------------------------------------
1018
1019    --D @Section Id => impl_kernel_init, Label => Initialization, Parent => implementation, Priority => -10
1020    --D @Text Section => impl_kernel_init
1021    --D The \verb!SK.Kernel.Initialize! procedure is the Ada/SPARK entry point
1022    --D into the kernel during the boot phase. It is invoked from Assembler code
1023    --D after low-level system initialization has been performed.
1024    --D Kernel initialization consists of the following steps:
1025    --D @OL Id => impl_kernel_init_steps, Section => impl_kernel_init, Priority => 10
1026    procedure Initialize (Subject_Registers : out CPU_Registers_Type)
1027    is
1028    begin
1029       --D @Item List => impl_kernel_init_steps
1030       --D Initialize interrupt table (GDT, IDT) and setup interrupt stack.
1031       Interrupt_Tables.Initialize
1032         (Stack_Addr => Skp.Kernel.Intr_Stack_Address);
1033
1034       pragma Debug (CPU_Info.Is_BSP, KC.Init);
1035       pragma Debug (CPU_Info.Is_BSP, KC.Put_Line
1036                     (Item => "Booting Muen kernel "
1037                      & Version.Version_String & " ("
1038                      & Standard'Compiler_Version & ")"));
1039
1040       if CPU_Info.Is_BSP then
1041          --D @Item List => impl_kernel_init_steps
1042          --D Setup crash audit (BSP-only).
1043          Crash_Audit.Init;
1044       end if;
1045
1046       declare
1047          Init_Ctx : Crash_Audit_Types.Init_Context_Type;
1048
1049          Valid_Sys_State, Valid_FPU_State, Valid_MCE_State,
1050          Valid_VTd_State : Boolean;
1051       begin
1052          --D @Item List => impl_kernel_init_steps
1053          --D Validate required CPU (\ref{impl_kernel_init_check_state}),
1054          --D FPU, MCE and VT-d features.
1055          System_State.Check_State
1056            (Is_Valid => Valid_Sys_State,
1057             Ctx      => Init_Ctx.Sys_Ctx);
1058          FPU.Check_State
1059            (Is_Valid => Valid_FPU_State,
1060             Ctx      => Init_Ctx.FPU_Ctx);
1061          MCE.Check_State
1062            (Is_Valid => Valid_MCE_State,
1063             Ctx      => Init_Ctx.MCE_Ctx);
1064          VTd.Check_State
1065            (Is_Valid => Valid_VTd_State,
1066             Ctx      => Init_Ctx.VTd_Ctx);
1067
1068          if not (Valid_Sys_State
1069                  and Valid_FPU_State
1070                  and Valid_MCE_State
1071                  and Valid_VTd_State)
1072          then
1073             declare
1074                Audit_Entry : Crash_Audit.Entry_Type;
1075             begin
1076                pragma Debug (KC.Put_Line
1077                              (Item => "System initialisation error"));
1078
1079                --D @Item List => impl_kernel_init_steps
1080                --D If a required feature is not present, allocate a crash audit
1081                --D entry designating a system initialization failure and
1082                --D provide initialization context information.
1083                Subject_Registers := Null_CPU_Regs;
1084                Crash_Audit.Allocate (Audit => Audit_Entry);
1085                Crash_Audit.Set_Reason
1086                  (Audit  => Audit_Entry,
1087                   Reason => Crash_Audit_Types.System_Init_Failure);
1088                Crash_Audit.Set_Init_Context
1089                  (Audit   => Audit_Entry,
1090                   Context => Init_Ctx);
1091                Crash_Audit.Finalize (Audit => Audit_Entry);
1092             end;
1093          end if;
1094
1095          --D @Item List => impl_kernel_init_steps
1096          --D Enable hardware features (FPU, APIC, MCE).
1097          FPU.Enable;
1098          Apic.Enable;
1099          MCE.Enable;
1100
1101          if CPU_Info.Is_BSP then
1102             --D @Item List => impl_kernel_init_steps
1103             --D Setup of Multicore memory barries (BSP-only).
1104             MP.Initialize_All_Barrier;
1105
1106             --D @Item List => impl_kernel_init_steps
1107             --D Disable legacy PIC/PIT (BSP-only).
1108             Interrupts.Disable_Legacy_PIT;
1109             Interrupts.Disable_Legacy_PIC;
1110
1111             --D @Item List => impl_kernel_init_steps
1112             --D Setup of VT-d DMAR and IR (BSP-only).
1113             VTd.Initialize;
1114             VTd.Interrupts.Setup_IRQ_Routing;
1115
1116             --D @Item List => impl_kernel_init_steps
1117             --D Initialize subject pending events (BSP-only).
1118             Subjects_Events.Initialize;
1119
1120             --D @Item List => impl_kernel_init_steps
1121             --D Wake up application processors (BSP-only).
1122             Apic.Start_AP_Processors;
1123          end if;
1124
1125          --D @Item List => impl_kernel_init_steps
1126          --D Synchronize all CPUs to make sure APs have performed all steps up
1127          --D until this point.
1128          MP.Wait_For_All;
1129
1130          --D @Item List => impl_kernel_init_steps
1131          --D Perform Intel microcode update on all cores. This is only done
1132          --D if the policy specifies an MCU blob.
1133          MCU.Process;
1134
1135          --D @Item List => impl_kernel_init_steps
1136          --D Enable VMX and enter VMX root-mode.
1137          System_State.Enable_VMX_Feature;
1138          VMX.Enter_Root_Mode;
1139          Init_Subjects;
1140
1141          --D @Item List => impl_kernel_init_steps, Priority => 20
1142          --D Finish setup by initializing the scheduler.
1143          Scheduler.Init;
1144
1145          --D @Item List => impl_kernel_init_steps, Priority => 20
1146          --D Synchronize all logical CPUs prior to setting VMX preemption
1147          --D timer.
1148          MP.Wait_For_All;
1149
1150          --D @Item List => impl_kernel_init_steps, Priority => 20
1151          --D Arm VMX Exit timer of scheduler for preemption on end of initial
1152          --D minor frame.
1153          Scheduler.Set_VMX_Exit_Timer;
1154
1155          declare
1156             Current_Subject : constant Skp.Global_Subject_ID_Type
1157               := Scheduler.Get_Current_Subject_ID;
1158          begin
1159             --D @Item List => impl_kernel_init_steps, Priority => 20
1160             --D Prepare state of initial subject for execution.
1161             Subjects.Filter_State (ID => Current_Subject);
1162             Subjects.Restore_State
1163               (ID   => Current_Subject,
1164                Regs => Subject_Registers);
1165             FPU.Restore_State (ID => Current_Subject);
1166          end;
1167       end;
1168
1169       --D @Text Section => impl_kernel_init, Priority => 30
1170       --D Registers of the first subject to schedule are returned by the
1171       --D initialization procedure to the calling assembler code. The assembly
1172       --D then restores the subject register values prior to launching the first
1173       --D subject.
1174       --D This is done this way so the initialization code as well as the main
1175       --D VMX exit handler (\ref{impl_exit_handler}) operate the same way and
1176       --D the Assembler code in charge of resuming subject execution can be
1177       --D shared, which further simplifies the code flow.
1178    end Initialize;
1179
1180 end SK.Kernel;