[PATCH] docs: fusa: Add requirements for mapping domain address to machine address

[PATCH] docs: fusa: Add requirements for mapping domain address to machine address

[Ayan Kumar Halder]

The following are the requirements written mapping :-
domain virtual address to machine address
intermediate physical address to machine address

Signed-off-by: Ayan Kumar Halder <ayan.kumar.halder@amd.com>
---
 .../design-reqs/arm64/domain_buffer_copy.rst  | 172 ++++++++++++++++++
 docs/fusa/reqs/market-reqs/reqs.rst           |  30 +++
 docs/fusa/reqs/product-reqs/arm64/reqs.rst    |  40 +++-
 3 files changed, 240 insertions(+), 2 deletions(-)
 create mode 100644 docs/fusa/reqs/design-reqs/arm64/domain_buffer_copy.rst

diff --git a/docs/fusa/reqs/design-reqs/arm64/domain_buffer_copy.rst b/docs/fusa/reqs/design-reqs/arm64/domain_buffer_copy.rst
new file mode 100644
index 0000000000..67a70a35c4
--- /dev/null
+++ b/docs/fusa/reqs/design-reqs/arm64/domain_buffer_copy.rst
@@ -0,0 +1,172 @@
+.. SPDX-License-Identifier: CC-BY-4.0
+
+Translate domain address to machine address
+-------------------------------------------
+
+`XenSwdgn~arm64_translate_domain_addr_to_machine_addr~1`
+
+Description:
+Xen shall translate a domain address to machine address using Address
+Translation Stage 1+2 Non-Secure Kernel Read/Write registers.
+
+Rationale:
+
+Comments:
+
+Covers:
+ - `XenProd~translate_domain_va_to_ma~1`
+
+Get machine address
+-------------------
+
+`XenSwdgn~arm64_get_machine_addr~1`
+
+Description:
+Xen shall be able to get the machine address for a domain by reading
+the physical address register.
+
+Rationale:
+
+Comments:
+It should return the fault information if the translation has failed.
+
+Covers:
+ - `XenProd~translate_domain_va_to_ma~1`
+ - `XenProd~access_check_fetch_page~1`
+
+Translate domain address to intermediate physical address
+---------------------------------------------------------
+
+`XenSwdgn~arm64_translate_domain_addr_to_ipa~1`
+
+Description:
+Xen shall translate a domain address to intermediate physical address using
+Address Translation Stage 1 Non-Secure Kernel Read/Write registers.
+
+Rationale:
+
+Comments:
+
+Covers:
+ - `XenProd~access_check_fetch_page~1`
+
+Set domain address as intermediate physical address
+---------------------------------------------------
+
+`XenSwdgn~arm64_set_ipa_eq_gva~1`
+
+Description:
+Xen shall set domain virtual address as intermediate physical address when EL1
+MMU is disabled.
+
+Rationale:
+
+Comments:
+
+Covers:
+ - `XenProd~access_check_fetch_page~1`
+
+Walk the domain's stage 1 page tables to translate 4KB domain address to IPA
+----------------------------------------------------------------------------
+
+`XenSwdgn~arm64_walk_stage1_page_table_4KB_gva_ipa_ttbr0~1`
+
+Description:
+Xen shall walk the stage 1 page tables to translate domain address to
+intermediate physical address for 4KB page granularity using TTBR0
+for intermediate physical address size = 48 bits.
+
+Rationale:
+
+Comments:
+
+Covers:
+ - `XenProd~access_check_fetch_page~1`
+
+Walk the domain's stage 1 page tables to translate 16KB domain address to IPA
+-----------------------------------------------------------------------------
+
+`XenSwdgn~arm64_walk_stage1_page_table_4KB_gva_ipa_ttbbr0~1`
+
+Description:
+Xen shall walk the stage 1 page tables to translate domain address to
+intermediate physical address for 16KB page granularity using TTBR0 for
+intermediate physical address size = 48 bits.
+
+
+Rationale:
+
+Comments:
+
+Covers:
+ - `XenProd~access_check_fetch_page~1`
+
+Walk the domain's stage 1 page tables to translate 64KB domain address to IPA
+-----------------------------------------------------------------------------
+
+`XenSwdgn~arm64_walk_stage1_page_table_4KB_gva_ipa_ttbr0~1`
+
+Description:
+Xen shall walk the stage 1 page tables to translate domain address to
+intermediate physical address for 64KB page granularity using TTBR0 for
+intermediate physical address size = 48 bits.
+
+Rationale:
+
+Comments:
+
+Covers:
+ - `XenProd~access_check_fetch_page~1`
+
+Walk the domain's stage 1 page tables to translate 4KB domain address to IPA
+----------------------------------------------------------------------------
+
+`XenSwdgn~arm64_walk_stage1_page_table_4KB_gva_ipa_ttbr1~1`
+
+Description:
+Xen shall walk the stage 1 page tables to translate domain address to
+intermediate physical address for 4KB page granularity using TTBR1 for
+intermediate physical address size = 48 bits.
+
+Rationale:
+
+Comments:
+
+Covers:
+ - `XenProd~access_check_fetch_page~1`
+
+Walk the domain's stage 1 page tables to translate 16KB domain address to IPA
+-----------------------------------------------------------------------------
+
+`XenSwdgn~arm64_walk_stage1_page_table_4KB_gva_ipa_ttbbr1~1`
+
+Description:
+Xen shall walk the stage 1 page tables to translate domain address to
+intermediate physical address for 16KB page granularity using TTBR1 for
+intermediate physical address size = 48 bits.
+
+
+Rationale:
+
+Comments:
+
+Covers:
+ - `XenProd~access_check_fetch_page~1`
+
+Walk the domain's stage 1 page tables to translate 64KB domain address to IPA
+-----------------------------------------------------------------------------
+
+`XenSwdgn~arm64_walk_stage1_page_table_4KB_gva_ipa_ttbr1~1`
+
+Description:
+Xen shall walk the stage 1 page tables to translate domain address to
+intermediate physical address for 64KB page granularity using TTBR1 for
+intermediate physical address size = 48 bits.
+
+Rationale:
+
+Comments:
+
+Covers:
+ - `XenProd~access_check_fetch_page~1`
+
diff --git a/docs/fusa/reqs/market-reqs/reqs.rst b/docs/fusa/reqs/market-reqs/reqs.rst
index ca020f9a33..9b6852d746 100644
--- a/docs/fusa/reqs/market-reqs/reqs.rst
+++ b/docs/fusa/reqs/market-reqs/reqs.rst
@@ -60,5 +60,35 @@ Rationale:
 
 Comments:
 
+Needs:
+ - XenProd
+
+Copy buffer to domain
+---------------------
+
+`XenMkt~copy_buffer_to_domain~1`
+
+Description:
+Xen shall support copying a buffer to a domain.
+
+Rationale:
+
+Comments:
+
+Needs:
+ - XenProd
+
+Copy buffer from domain
+-----------------------
+
+`XenMkt~copy_buffer_from_domain~1`
+
+Description:
+Xen shall support copying a buffer from a domain.
+
+Rationale:
+
+Comments:
+
 Needs:
  - XenProd
\ No newline at end of file
diff --git a/docs/fusa/reqs/product-reqs/arm64/reqs.rst b/docs/fusa/reqs/product-reqs/arm64/reqs.rst
index 0453dbb862..e2ab5ea43e 100644
--- a/docs/fusa/reqs/product-reqs/arm64/reqs.rst
+++ b/docs/fusa/reqs/product-reqs/arm64/reqs.rst
@@ -53,10 +53,46 @@ Rationale:
 
 Comments:
 
+Covers:
+ - `XenMkt~static_vm_definition~1`
+
+Needs:
+ - XenSwdgn
+
+Translate domain virtual address to machine address
+---------------------------------------------------
+
+`XenProd~translate_domain_va_to_ma~1`
+
+Description:
+Xen shall support translating domain's virtual address to machine address.
+
 Rationale:
 
+Comments:
+
 Covers:
- - `XenMkt~static_vm_definition~1`
+ - `XenMkt~copy_buffer_from_domain~1`
+ - `XenMkt~copy_buffer_to_domain~1`
 
 Needs:
- - XenSwdgn
\ No newline at end of file
+ - XenSwdgn
+
+Access check and fetch page from domain
+---------------------------------------
+
+`XenProd~access_check_fetch_page~1`
+
+Description:
+Xen shall support access check and fetching page from a domain.
+
+Rationale:
+
+Comments:
+
+Covers:
+ - `XenMkt~copy_buffer_from_domain~1`
+ - `XenMkt~copy_buffer_to_domain~1`
+
+Needs:
+ - XenSwdgn
-- 
2.25.1

Re: [PATCH] docs: fusa: Add requirements for mapping domain address to machine address

[Bertrand Marquis]

Hi Ayan,

First a general comment: you use some terms such as machine address or domain
address which are a bit undefined to me. This needs some definition first for those to
be clear. Maybe use Virtual, IPA and PA instead all the time.

> On 4 Nov 2024, at 20:06, Ayan Kumar Halder <ayan.kumar.halder@amd.com> wrote:
> 
> The following are the requirements written mapping :-
> domain virtual address to machine address
> intermediate physical address to machine address
> 
> Signed-off-by: Ayan Kumar Halder <ayan.kumar.halder@amd.com>
> ---
> .../design-reqs/arm64/domain_buffer_copy.rst  | 172 ++++++++++++++++++
> docs/fusa/reqs/market-reqs/reqs.rst           |  30 +++
> docs/fusa/reqs/product-reqs/arm64/reqs.rst    |  40 +++-
> 3 files changed, 240 insertions(+), 2 deletions(-)
> create mode 100644 docs/fusa/reqs/design-reqs/arm64/domain_buffer_copy.rst
> 
> diff --git a/docs/fusa/reqs/design-reqs/arm64/domain_buffer_copy.rst b/docs/fusa/reqs/design-reqs/arm64/domain_buffer_copy.rst
> new file mode 100644
> index 0000000000..67a70a35c4
> --- /dev/null
> +++ b/docs/fusa/reqs/design-reqs/arm64/domain_buffer_copy.rst
> @@ -0,0 +1,172 @@
> +.. SPDX-License-Identifier: CC-BY-4.0
> +
> +Translate domain address to machine address
> +-------------------------------------------
> +
> +`XenSwdgn~arm64_translate_domain_addr_to_machine_addr~1`
> +
> +Description:
> +Xen shall translate a domain address to machine address using Address
> +Translation Stage 1+2 Non-Secure Kernel Read/Write registers.

domain address here is a bit unprecise. Do you mean VA or IPA ?

Also is this only in the MPU case ?

> +
> +Rationale:
> +
> +Comments:
> +
> +Covers:
> + - `XenProd~translate_domain_va_to_ma~1`
> +
> +Get machine address
> +-------------------
> +
> +`XenSwdgn~arm64_get_machine_addr~1`
> +
> +Description:
> +Xen shall be able to get the machine address for a domain by reading
> +the physical address register.

This needs rephrasing to remove the "be able to":
Xen shall use the physical address register to retrieve the machine address.

Also what you mean by "machine address" needs to be defined here.

> +
> +Rationale:
> +
> +Comments:
> +It should return the fault information if the translation has failed.

I do not understand this one. Maybe this requirement needs more context to be understood.

> +
> +Covers:
> + - `XenProd~translate_domain_va_to_ma~1`
> + - `XenProd~access_check_fetch_page~1`
> +
> +Translate domain address to intermediate physical address
> +---------------------------------------------------------
> +
> +`XenSwdgn~arm64_translate_domain_addr_to_ipa~1`
> +
> +Description:
> +Xen shall translate a domain address to intermediate physical address using
> +Address Translation Stage 1 Non-Secure Kernel Read/Write registers.
> +
> +Rationale:
> +
> +Comments:
> +
> +Covers:
> + - `XenProd~access_check_fetch_page~1`
> +
> +Set domain address as intermediate physical address
> +---------------------------------------------------
> +
> +`XenSwdgn~arm64_set_ipa_eq_gva~1`
> +
> +Description:
> +Xen shall set domain virtual address as intermediate physical address when EL1
> +MMU is disabled.

Here you start using virtual address. I also do not get what is to be set here.
Do you mean that Xen shall consider VA=IPA when EL1 MMU is disabled ?

> +
> +Rationale:
> +
> +Comments:
> +
> +Covers:
> + - `XenProd~access_check_fetch_page~1`
> +
> +Walk the domain's stage 1 page tables to translate 4KB domain address to IPA
> +----------------------------------------------------------------------------
> +
> +`XenSwdgn~arm64_walk_stage1_page_table_4KB_gva_ipa_ttbr0~1`
> +
> +Description:
> +Xen shall walk the stage 1 page tables to translate domain address to
> +intermediate physical address for 4KB page granularity using TTBR0
> +for intermediate physical address size = 48 bits.

Is this always the case ? aren't there cases where we should not do that ?

Do we really want in the certified case to accept to have to walk stage 1 page
tables instead of using the hardware way ?

> +
> +Rationale:
> +
> +Comments:
> +
> +Covers:
> + - `XenProd~access_check_fetch_page~1`
> +
> +Walk the domain's stage 1 page tables to translate 16KB domain address to IPA
> +-----------------------------------------------------------------------------
> +
> +`XenSwdgn~arm64_walk_stage1_page_table_4KB_gva_ipa_ttbbr0~1`

Req is name 4KB for 16KB

> +
> +Description:
> +Xen shall walk the stage 1 page tables to translate domain address to
> +intermediate physical address for 16KB page granularity using TTBR0 for
> +intermediate physical address size = 48 bits.

I am not quite sure that it is a good solution to duplicate for each page table size here.
Do you want to support all possibilities ?

> +
> +
> +Rationale:
> +
> +Comments:
> +
> +Covers:
> + - `XenProd~access_check_fetch_page~1`
> +
> +Walk the domain's stage 1 page tables to translate 64KB domain address to IPA
> +-----------------------------------------------------------------------------
> +
> +`XenSwdgn~arm64_walk_stage1_page_table_4KB_gva_ipa_ttbr0~1`

Same here

> +
> +Description:
> +Xen shall walk the stage 1 page tables to translate domain address to
> +intermediate physical address for 64KB page granularity using TTBR0 for
> +intermediate physical address size = 48 bits.

Ditto

> +
> +Rationale:
> +
> +Comments:
> +
> +Covers:
> + - `XenProd~access_check_fetch_page~1`
> +
> +Walk the domain's stage 1 page tables to translate 4KB domain address to IPA
> +----------------------------------------------------------------------------
> +
> +`XenSwdgn~arm64_walk_stage1_page_table_4KB_gva_ipa_ttbr1~1`
> +
> +Description:
> +Xen shall walk the stage 1 page tables to translate domain address to
> +intermediate physical address for 4KB page granularity using TTBR1 for
> +intermediate physical address size = 48 bits.
> +

You duplicate the requirement for TTBR1 but do not say when TTBR0 or TTBR1
shall be used.

> +Rationale:
> +
> +Comments:
> +
> +Covers:
> + - `XenProd~access_check_fetch_page~1`
> +
> +Walk the domain's stage 1 page tables to translate 16KB domain address to IPA
> +-----------------------------------------------------------------------------
> +
> +`XenSwdgn~arm64_walk_stage1_page_table_4KB_gva_ipa_ttbbr1~1`
> +
> +Description:
> +Xen shall walk the stage 1 page tables to translate domain address to
> +intermediate physical address for 16KB page granularity using TTBR1 for
> +intermediate physical address size = 48 bits.
> +
> +
> +Rationale:
> +
> +Comments:
> +
> +Covers:
> + - `XenProd~access_check_fetch_page~1`
> +
> +Walk the domain's stage 1 page tables to translate 64KB domain address to IPA
> +-----------------------------------------------------------------------------
> +
> +`XenSwdgn~arm64_walk_stage1_page_table_4KB_gva_ipa_ttbr1~1`
> +
> +Description:
> +Xen shall walk the stage 1 page tables to translate domain address to
> +intermediate physical address for 64KB page granularity using TTBR1 for
> +intermediate physical address size = 48 bits.
> +
> +Rationale:
> +
> +Comments:
> +
> +Covers:
> + - `XenProd~access_check_fetch_page~1`
> +
> diff --git a/docs/fusa/reqs/market-reqs/reqs.rst b/docs/fusa/reqs/market-reqs/reqs.rst
> index ca020f9a33..9b6852d746 100644
> --- a/docs/fusa/reqs/market-reqs/reqs.rst
> +++ b/docs/fusa/reqs/market-reqs/reqs.rst
> @@ -60,5 +60,35 @@ Rationale:
> 
> Comments:
> 
> +Needs:
> + - XenProd
> +
> +Copy buffer to domain
> +---------------------
> +
> +`XenMkt~copy_buffer_to_domain~1`
> +
> +Description:
> +Xen shall support copying a buffer to a domain.

What kind of buffer ?
This requirement is very generic and not that precise.
At the end this is just saying that Xen shall be able to copy memory.

> +
> +Rationale:
> +
> +Comments:
> +
> +Needs:
> + - XenProd
> +
> +Copy buffer from domain
> +-----------------------
> +
> +`XenMkt~copy_buffer_from_domain~1`
> +
> +Description:
> +Xen shall support copying a buffer from a domain.
> +
> +Rationale:
> +
> +Comments:
> +
> Needs:
>  - XenProd
> \ No newline at end of file
> diff --git a/docs/fusa/reqs/product-reqs/arm64/reqs.rst b/docs/fusa/reqs/product-reqs/arm64/reqs.rst
> index 0453dbb862..e2ab5ea43e 100644
> --- a/docs/fusa/reqs/product-reqs/arm64/reqs.rst
> +++ b/docs/fusa/reqs/product-reqs/arm64/reqs.rst
> @@ -53,10 +53,46 @@ Rationale:
> 
> Comments:
> 
> +Covers:
> + - `XenMkt~static_vm_definition~1`
> +
> +Needs:
> + - XenSwdgn
> +
> +Translate domain virtual address to machine address
> +---------------------------------------------------
> +
> +`XenProd~translate_domain_va_to_ma~1`
> +
> +Description:
> +Xen shall support translating domain's virtual address to machine address.

I find the "support" here a bit strange.

Maybe it would be simpler to define that Xen shall have a function named xxx to
do this ?

I am not quite convince this is not only a design req.

> +
> Rationale:
> 
> +Comments:
> +
> Covers:
> - - `XenMkt~static_vm_definition~1`
> + - `XenMkt~copy_buffer_from_domain~1`
> + - `XenMkt~copy_buffer_to_domain~1`
> 
> Needs:
> - - XenSwdgn
> \ No newline at end of file
> + - XenSwdgn
> +
> +Access check and fetch page from domain
> +---------------------------------------
> +
> +`XenProd~access_check_fetch_page~1`
> +
> +Description:
> +Xen shall support access check and fetching page from a domain.

This should be split in 2 reqs.

> +
> +Rationale:
> +
> +Comments:
> +
> +Covers:
> + - `XenMkt~copy_buffer_from_domain~1`
> + - `XenMkt~copy_buffer_to_domain~1`
> +
> +Needs:
> + - XenSwdgn
> -- 
> 2.25.1
>