[XEN PATCH v1 0/2] docs/fusa: coverage-gap justifications and generic timer arch spec

[XEN PATCH v1 0/2] docs/fusa: coverage-gap justifications and generic timer arch spec

[Ayan Kumar Halder]

This series adds two pieces of Functional Safety documentation under
docs/fusa/.

Patch 1 introduces docs/fusa/coverage_gap.rst, a table that records the
code regions excluded from the coverage report because they are
unreachable by design. Code that no test can reach (for example a
defensive default arm of a switch that no caller can reach) would
otherwise show up as a permanent coverage gap even though it is correct.
Each exclusion is given a stable id, the excluded source location, and a
justification stating why the code is unreachable and what would make it
reachable again, so that a genuine gap is never hidden behind an LCOV
marker. The two vGICv3 default arms are documented as the first entries.

Patch 2 adds the arm64 generic timer architecture specification under
docs/fusa/architecture_specs/. An architecture spec is a prose document
that explains how Xen uses a piece of hardware -- what the hardware
does, which parts Xen drives directly, which parts it emulates for a
guest, and how they interact over the lifetime of a VM. This one covers
the Arm Generic Timer and traces to the existing
XenSwdgn~arm64_generic_timer_* design requirements.

Both documents are wired into the docs/fusa Sphinx toctree.

Ayan Kumar Halder (2):
  docs/fusa: add coverage_gap.rst tabulating vGICv3 LCOV exclusions
  docs/fusa: add generic timer arch spec with ASCII diagrams

 .../fusa/architecture_specs/generic_timer.rst | 215 ++++++++++++++++++
 docs/fusa/architecture_specs/index.rst        |   9 +
 docs/fusa/coverage_gap.rst                    |  41 ++++
 docs/fusa/index.rst                           |   2 +
 4 files changed, 267 insertions(+)
 create mode 100644 docs/fusa/architecture_specs/generic_timer.rst
 create mode 100644 docs/fusa/architecture_specs/index.rst
 create mode 100644 docs/fusa/coverage_gap.rst

-- 
2.25.1

[XEN PATCH v1 1/2] docs/fusa: add coverage_gap.rst tabulating vGICv3 LCOV exclusions

[Ayan Kumar Halder]

Some code is unreachable by design (for example a defensive default arm
of a switch that no caller can reach) and can therefore never be
executed by any test. Such code shows up as a permanent gap in the
coverage report even though it is correct. To keep the report meaningful
we exclude these regions from coverage, but every exclusion must be
justified and reviewable so that a genuine gap is never hidden behind an
LCOV marker. This file is that record: it gives each exclusion a stable
id, points at the excluded source, and states why the code is
unreachable and what would make it reachable again.

Record the LCOV_EXCL regions in xen/arch/arm/vgic-v3.c as a table with
columns coverage_gap_id, file, line numbers and SHA, plus a
justification taken from each COV-GAP-VGICV3 "Reason for exclusion".

Use upstream xen (xenbits/master) line ranges and SHA, with line numbers
given in vgic-v3.c:Lstart-Lend notation, and state explicitly that each
excluded default arm becomes reachable only if a caller is modified to
forward an offset the handler has no case for, at which point the
exclusion must be removed. Wire the file into the docs/fusa toctree.

Signed-off-by: Ayan Kumar Halder <ayan.kumar.halder@amd.com>
---
The coverage gap justification may be used to state why a piece of code
cannot be tested within the scope of our safety and it cannot be removed
as well. Thus, we use the justification to analyse and document the
behavior of untested code in safety certifiable Xen.

 docs/fusa/coverage_gap.rst | 41 ++++++++++++++++++++++++++++++++++++++
 docs/fusa/index.rst        |  1 +
 2 files changed, 42 insertions(+)
 create mode 100644 docs/fusa/coverage_gap.rst

diff --git a/docs/fusa/coverage_gap.rst b/docs/fusa/coverage_gap.rst
new file mode 100644
index 0000000000..9d14f7b264
--- /dev/null
+++ b/docs/fusa/coverage_gap.rst
@@ -0,0 +1,41 @@
+.. SPDX-License-Identifier: CC-BY-4.0
+
+Coverage gaps
+=============
+
+This table documents the ``LCOV_EXCL`` regions in the Xen source. Each excluded
+region is tagged in the source with a ``COV-GAP-<COMPONENT>-NNN`` marker that
+matches an entry below. A region is excluded from the coverage report only when
+it is unreachable by design, so it can never be reported as covered.
+
+.. list-table::
+   :header-rows: 1
+   :widths: 15 25 10 12 38
+
+   * - coverage_gap_id
+     - file
+     - line numbers
+     - SHA
+     - justification
+   * - COV-GAP-VGICV3-001
+     - xen/arch/arm/vgic-v3.c
+     - L796-L800
+     - 351d41e8aecc3f7566a0baa7b4066d06dedd7113
+     - Both callers select the register offset with their own ``switch`` and
+       forward only offsets the handler has an explicit ``case`` for, so no
+       forwarded offset can fall through to ``default:``. (The SGI_base-frame
+       ``GICR_*`` offsets one caller forwards are numerically equal to the
+       ``GICD_*`` offsets the handler cases on.) The ``default:`` is kept as
+       defensive programming; it becomes reachable only if a caller is
+       modified to forward an offset the handler has no ``case`` for, at
+       which point this exclusion must be removed.
+   * - COV-GAP-VGICV3-002
+     - xen/arch/arm/vgic-v3.c
+     - L954-L958
+     - 351d41e8aecc3f7566a0baa7b4066d06dedd7113
+     - Same design as COV-GAP-VGICV3-001, for the write path: both callers
+       forward only offsets the handler has an explicit ``case`` for, so the
+       ``default:`` arm cannot be reached and is kept as defensive
+       programming; it becomes reachable only if a caller is modified to
+       forward an offset the handler has no ``case`` for, at which point this
+       exclusion must be removed.
diff --git a/docs/fusa/index.rst b/docs/fusa/index.rst
index 5f1e8acfc4..dd5ca4dd95 100644
--- a/docs/fusa/index.rst
+++ b/docs/fusa/index.rst
@@ -7,3 +7,4 @@ Functional Safety documentation
    :maxdepth: 2
 
    reqs/index
+   coverage_gap
-- 
2.25.1

[XEN PATCH v1 2/2] docs/fusa: add generic timer arch spec with ASCII diagrams

[Ayan Kumar Halder]

An architecture specification is a prose document that describes how Xen
uses a particular piece of hardware: what the hardware does, which parts
of it Xen drives directly, which parts it emulates on behalf of a guest,
and how the two interact over the lifetime of a VM. It sits between the
high-level requirements and the source code, giving a reviewer or
safety assessor a readable explanation of the design without having to
reconstruct it from the code, and it is the anchor that the design
requirements trace to.

This adds the arm64 generic timer architecture spec, which explains
Xen's usage of the Arm Generic Timer: the system counter and the
physical and virtual timers, how Xen sets up the timer for a VM at
creation, and how it traps, emulates and injects timer interrupts while
the VM runs. The spec's Covers list points at the existing
XenSwdgn~arm64_generic_timer_* design-requirement IDs, matching the OFT
tag convention already used throughout docs/fusa/reqs/design-reqs.

Wire the section into the docs/fusa toctree.

Signed-off-by: Michal Orzel <michal.orzel@amd.com>
Signed-off-by: Ayan Kumar Halder <ayan.kumar.halder@amd.com>
---
The architecture spec explains the detailed design of a component in Xen.
Together with design requirements, the architecture spec helps to define the
test cases to prove that the component can be used in a safety environment.

 .../fusa/architecture_specs/generic_timer.rst | 215 ++++++++++++++++++
 docs/fusa/architecture_specs/index.rst        |   9 +
 docs/fusa/index.rst                           |   1 +
 3 files changed, 225 insertions(+)
 create mode 100644 docs/fusa/architecture_specs/generic_timer.rst
 create mode 100644 docs/fusa/architecture_specs/index.rst

diff --git a/docs/fusa/architecture_specs/generic_timer.rst b/docs/fusa/architecture_specs/generic_timer.rst
new file mode 100644
index 0000000000..6caeffca13
--- /dev/null
+++ b/docs/fusa/architecture_specs/generic_timer.rst
@@ -0,0 +1,215 @@
+.. SPDX-License-Identifier: CC-BY-4.0
+
+Generic Timer
+=============
+
+`XenArch~arm64_generic_timer~1`
+
+Covers:
+ - `XenSwdgn~arm64_generic_timer_probe_dt~1`
+ - `XenSwdgn~arm64_generic_timer_read_freq~1`
+ - `XenSwdgn~arm64_generic_timer_access_cntkctlel1~1`
+ - `XenSwdgn~arm64_generic_timer_access_virtual_timer~1`
+ - `XenSwdgn~arm64_generic_timer_access_physical_timer~1`
+ - `XenSwdgn~arm64_generic_timer_trigger_virtual_interrupt~1`
+ - `XenSwdgn~arm64_generic_timer_trigger_physical_interrupt~1`
+
+Needs:
+ - XenVerTestCase
+
+This document aims to explain the usage of Arm generic timer during the
+lifetime of a VM.
+
+Introduction
+------------
+
+The Generic Timer:
+
+- provides a system counter that measures the passing of time in real-time,
+- supports virtual counters that measure the passing of virtual-time. That is,
+  a virtual counter can measure the passing of time on a particular
+  virtual machine,
+- can trigger events after a period of time has passed.
+
+Types of timers
+---------------
+
+Xen exposes two types of timer on behalf of VM's lifetime:
+
+- physical timer
+- virtual timer
+
+::
+
+    +------------------+
+    |  System Counter  |
+    +--------+---------+
+             | System Time Bus
+             +----------------------------+
+             |                            |
+             |                            v
+             |                        +-------+       +----------+
+             |                        |   -   |<------|  CNTVOFF |
+             |                        +---+---+       +----------+
+             |                            |
+             v                            v
+        +---------+                  +---------+
+        |  CNTPCT |                  |  CNTVCT |
+        +---------+                  +---------+
+        +---------+                  +---------+
+        | Physical|                  | Virtual |
+        |  Timer  |                  |  Timer  |
+        +---------+                  +---------+
+    ( PE )
+
+The physical timer measures the passage of time in relation to the physical
+counter. It is used to broadcast the wall-clock time (i.e. the number of clock
+cycles since Xen boot). It is accessed by the following registers:
+
+- CNTPCT_EL0 - physical count value
+- CNTP_CTL_EL0 - control register
+- CNTP_CVAL_EL0 - compare value register
+- CNTP_TVAL_EL0 - timer value register
+
+The virtual timer measures the passage of time in relation to the virtual
+counter. It is used to broadcast the virtual time (physical - offset). Offset is
+set by Xen (CNTVOFF_EL2 register) during VM creation. As a result, the virtual
+time will report time from the creation of the VM. It is accessed by the
+following registers:
+
+- CNTVCT_EL0 - virtual count value
+- CNTV_CTL_EL0 - control register
+- CNTV_CVAL_EL0 - compare value register
+- CNTV_TVAL_EL0 - compare value register
+
+CNTFRQ_EL0 reports the frequency of the system counter. However, this register
+is not populated by hardware. The register is write-able at the highest
+implemented Exception level and readable at all Exception levels. Firmware,
+typically running at EL3, populates this register as part of early system
+initialization. Higher-level software, like an operating system, can then use
+the register to get the frequency.
+
+Generic timer usage during VM creeation
+---------------------------------------
+
+While preparing the device tree for a VM, Xen creates a timer node (based on the
+spec[1]) for the VM. For this, host device tree is expected to have a node for
+the generic timer.
+
+During the VM creation, Xen sets the offset (CNTVOFF_EL2) used to broadcast the
+virtual time for a VM and assigns the following per processor interrupts for
+timers.
+
+.. list-table::
+   :header-rows: 1
+
+   * - Name
+     - Interrupt id
+
+   * - Virtual timer
+     - 27
+
+   * - physical secure timer
+     - 29
+
+   * - physical non secure timer
+     - 30
+
+Xen reserves the 27, 29 and 30 interrupt ids in the virtual GIC. The exception
+to this is for hardware VM, where the VM will be assigned interrupt numbers the
+same as in the host device tree.
+
+The parent interrupt is linked to the Generic interrupt controller node.
+
+If the host device tree node for the generic timer contains the property
+"clock-frequency", the same is passed on to the guest device tree.
+
+During the VM vCPU creation, Xen initializes the internal/background timers (one
+for physical timer and one for virtual timer).
+
+Generic timer interface between Xen and VM
+------------------------------------------
+
+VM can make use of both the physical and virtual timer.
+
+Physical timer
+^^^^^^^^^^^^^^
+
+Xen traps accesses to system registers related to physical timer (except
+CNTPCT_EL0). This is done to allow Xen to emulate the physical timer for a VM
+(e.g. checking the right access, taking into account the time when Xen was not
+running). Xen does not route the physical timer interrupt to guest or itself.
+Instead, it makes use of the internal timer used for the physical timer
+emulation to schedule the interrupt injection into the VM.
+
+The flow can be depicted as follows:
+
+::
+
+    +---------------------------------------------------+
+    | VMs read or write                                 |
+    | any of CNTP_CTL, CNTP_CVAL, CNTP_TVAL             |
+    +-------------------------+-------------------------+
+                              |
+                              v
+    +---------------------------------------------------+
+    | MSR/MRS instruction is trapped by Xen             |
+    +-------------------------+-------------------------+
+                              |
+                              v
+    +---------------------------------------------------+
+    | Xen reads or writes to the register               |
+    | on behalf of VM                                   |
+    |                                                   |
+    |  1. For read access : Xen returns the value from  |
+    |     the VM's vcpu physical timer context.         |
+    |  2. For write access : Xen saves the value in the |
+    |     VM's vcpu physical timer context. Depending   |
+    |     on the value, it schedules the internal timer |
+    |     for interrupt injection.                      |
+    |                                                   |
+    |  Increments the VM program counter                |
+    |  and returns control to VM.                       |
+    +---------------------------------------------------+
+
+Virtual timer
+^^^^^^^^^^^^^
+
+Xen does not trap accesses to system registers related to virtual timer.
+The timer context (i.e. content of timer registers) is saved/restored during the
+vCPU context switch. At save time, Xen initializes an internal timer to make
+sure the VM's vCPU is scheduled at the time of the next virtual timer interrupt.
+The virtual timer interrupt is first routed to Xen, masked and injected into the
+VM. The interrupt behave in a level-sensitive manner, meaning the timer will
+continue to signal the interrupt until one of the following situations occurs:
+
+- interrupt is masked
+- timer is disabled
+- firing condition is no longer met
+
+Xen masks the interrupt (using the CNTV_CTL_EL0 register) before injecting it
+into the VM to avoid an interrupt storm that could otherwise occur if the VM
+did not handle the interrupt properly.
+
+Error propagation
+-----------------
+
+The following Generic Timer device-tree faults observed during early boot
+trigger an unrecoverable panic:
+
+- No device-tree node advertising a compatible ARM Generic Timer
+  identifier (for example "arm,armv8-timer"): Xen matches the timer by the
+  node's "compatible" property rather than its name, so if no node carries
+  a supported timer compatible string the lookup returns nothing and Xen
+  panics with "Unable to find a compatible timer in the device tree".
+- Timer node with a "clock-frequency" value less than 1000: Xen cannot
+  derive a usable timer rate and panics with "Timer frequency is less
+  than 1 KHz".
+- Timer node missing the "interrupts" property (or whose interrupts entry
+  for the timer in use cannot be parsed): Xen cannot retrieve the timer
+  IRQ from the device tree and panics with "Timer: Unable to retrieve IRQ
+  N from the device tree" (where N identifies which of the timer
+  interrupts could not be parsed).
+
+| [1] Arm Architecture Reference Manual for A-profile architecture, Chapter 11
+| [2] https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/tree/Documentation/devicetree/bindings/timer/arm,arch_timer.yaml
diff --git a/docs/fusa/architecture_specs/index.rst b/docs/fusa/architecture_specs/index.rst
new file mode 100644
index 0000000000..395e3c1225
--- /dev/null
+++ b/docs/fusa/architecture_specs/index.rst
@@ -0,0 +1,9 @@
+.. SPDX-License-Identifier: CC-BY-4.0
+
+Architecture specifications
+===========================
+
+.. toctree::
+   :maxdepth: 2
+
+   generic_timer
diff --git a/docs/fusa/index.rst b/docs/fusa/index.rst
index dd5ca4dd95..88aaafe7a6 100644
--- a/docs/fusa/index.rst
+++ b/docs/fusa/index.rst
@@ -7,4 +7,5 @@ Functional Safety documentation
    :maxdepth: 2
 
    reqs/index
+   architecture_specs/index
    coverage_gap
-- 
2.25.1

Re: [XEN PATCH v1 1/2] docs/fusa: add coverage_gap.rst tabulating vGICv3 LCOV exclusions

[Jan Beulich]

On 21.07.2026 14:47, Ayan Kumar Halder wrote:
> --- /dev/null
> +++ b/docs/fusa/coverage_gap.rst
> @@ -0,0 +1,41 @@
> +.. SPDX-License-Identifier: CC-BY-4.0
> +
> +Coverage gaps
> +=============
> +
> +This table documents the ``LCOV_EXCL`` regions in the Xen source. Each excluded
> +region is tagged in the source with a ``COV-GAP-<COMPONENT>-NNN`` marker that
> +matches an entry below. A region is excluded from the coverage report only when
> +it is unreachable by design, so it can never be reported as covered.
> +
> +.. list-table::
> +   :header-rows: 1
> +   :widths: 15 25 10 12 38
> +
> +   * - coverage_gap_id
> +     - file
> +     - line numbers
> +     - SHA

What specific algorithm? Or wait, this isn't a hash of the file, but a commit
hash. This imo wants clarifying.

> +     - justification
> +   * - COV-GAP-VGICV3-001
> +     - xen/arch/arm/vgic-v3.c
> +     - L796-L800
> +     - 351d41e8aecc3f7566a0baa7b4066d06dedd7113
> +     - Both callers select the register offset with their own ``switch`` and
> +       forward only offsets the handler has an explicit ``case`` for, so no
> +       forwarded offset can fall through to ``default:``. (The SGI_base-frame
> +       ``GICR_*`` offsets one caller forwards are numerically equal to the
> +       ``GICD_*`` offsets the handler cases on.) The ``default:`` is kept as
> +       defensive programming; it becomes reachable only if a caller is
> +       modified to forward an offset the handler has no ``case`` for, at
> +       which point this exclusion must be removed.

All of this is liable to go stale. Once it has gone stale, this information
is pretty much useless aiui. And it may well be worse than that, if the
"must be removed" isn't actually followed (perhaps simply because there's
no link from the source to here). How's all of this going to be helpful
longer term?

Jan

Re: [XEN PATCH v1 1/2] docs/fusa: add coverage_gap.rst tabulating vGICv3 LCOV exclusions

[Halder, Ayan Kumar]

Hi Jan,

On 21/07/2026 14:00, Jan Beulich wrote:
> On 21.07.2026 14:47, Ayan Kumar Halder wrote:
>> --- /dev/null
>> +++ b/docs/fusa/coverage_gap.rst
>> @@ -0,0 +1,41 @@
>> +.. SPDX-License-Identifier: CC-BY-4.0
>> +
>> +Coverage gaps
>> +=============
>> +
>> +This table documents the ``LCOV_EXCL`` regions in the Xen source. Each excluded
>> +region is tagged in the source with a ``COV-GAP-<COMPONENT>-NNN`` marker that
>> +matches an entry below. A region is excluded from the coverage report only when
>> +it is unreachable by design, so it can never be reported as covered.
>> +
>> +.. list-table::
>> +   :header-rows: 1
>> +   :widths: 15 25 10 12 38
>> +
>> +   * - coverage_gap_id
>> +     - file
>> +     - line numbers
>> +     - SHA
> What specific algorithm? Or wait, this isn't a hash of the file, but a commit
> hash. This imo wants clarifying.
It is a commit hash.
>
>> +     - justification
>> +   * - COV-GAP-VGICV3-001
>> +     - xen/arch/arm/vgic-v3.c
>> +     - L796-L800
>> +     - 351d41e8aecc3f7566a0baa7b4066d06dedd7113
>> +     - Both callers select the register offset with their own ``switch`` and
>> +       forward only offsets the handler has an explicit ``case`` for, so no
>> +       forwarded offset can fall through to ``default:``. (The SGI_base-frame
>> +       ``GICR_*`` offsets one caller forwards are numerically equal to the
>> +       ``GICD_*`` offsets the handler cases on.) The ``default:`` is kept as
>> +       defensive programming; it becomes reachable only if a caller is
>> +       modified to forward an offset the handler has no ``case`` for, at
>> +       which point this exclusion must be removed.
> All of this is liable to go stale. Once it has gone stale, this information
> is pretty much useless aiui. And it may well be worse than that, if the
> "must be removed" isn't actually followed (perhaps simply because there's
> no link from the source to here). How's all of this going to be helpful
> longer term?

Using SPDX SBOM, you can link a document to a piece of code to a commit 
SHA. This was something that linux kernel has recently developed and 
upstreamed.

https://docs.kernel.org/tools/sbom/sbom.html . Zephyr project has 
developed this as well.

harunobu.kurokawa.dn@renesas.com is investigating this for Xen.

- Ayan

>
> Jan

RE: [EXTERNAL] [XEN PATCH v1 2/2] docs/fusa: add generic timer arch spec with ASCII diagrams

[Weber (US), Matthew L]

All,

> On 21.07.2026 14:47, Ayan Kumar Halder wrote:
> +Generic timer usage during VM creeation
> +---------------------------------------

Typo: "creeation" -> "creation"

> +- CNTVCT_EL0 - virtual count value
> +- CNTV_CTL_EL0 - control register
> +- CNTV_CVAL_EL0 - compare value register
> +- CNTV_TVAL_EL0 - compare value register

CNTV_TVAL_EL0 should be "timer value register", not "compare value
register". CVAL is the comparator, TVAL is the countdown/timer-value
alias. (Same naming as CNTP_TVAL_EL0 earlier in the same section.)

> +The interrupt behave in a level-sensitive manner, meaning the timer will

Grammar: "The interrupt behaves" (singular).

> +   * - physical non secure timer
> +     - 30

Nit: ARM uses "Non-secure" (hyphenated, capitalized). Suggest
"physical Non-secure timer" for consistency with the spec terminology.

> +| [1] Arm Architecture Reference Manual for A-profile architecture, Chapter 11
> +| [2] https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/tree/Documentation/devicetree/bindings/timer/arm,arch_timer.yaml

These would render better as proper RST footnotes:

  .. [1] Arm Architecture Reference Manual for A-profile architecture, Chapter 11
  .. [2] https://git.kernel.org/...

That way Sphinx cross-references and numbered citations work correctly
in the built HTML.

Overall the spec is well structured, thanks Ayan!

Reviewed-by: Weber (US), Matthew L <matthew.l.weber3@boeing.com>