Module Rig_pci.Page_table

The type for the memory an entry points into.

The type for a vendor's page-table format and the access to the GPU's memory that holds the tables. This module keeps what each entry holds and never reads one back, so a format may write through a window Function.map made with ~combine:true. An entry in memory that zero zeroed maps nothing.

This module calls set_page only at the leaf level or where large holds, with an address below 2{^pa_bits}, and set_table only with tables in the GPU's memory. The setters, clear and zero must raise nothing.

The type for the page tables and physical memory of one GPU.

The type for where page tables come from.

create ~base fmt s ~memory ~boot ~tables ~pages manages memory bytes of a GPU's physical memory: a boot pool of its first boot bytes, the page tables' pool if tables is Pool, and the main pool. pages lists the physical block sizes, with their alignments, that alloc tries, largest first. The tables translate the addresses from base on, some of which s hands out: where the GPU's MMU starts translating, such as address 0 for an MMU that indexes each level with the address's own bits. create allocates the root table in the boot pool and starts booting.

Raises Invalid_argument if fmt's levels do not rise from 12 to below bits, its pa_bits is below 12 or past 61, base is not a multiple of the largest page a level maps, the pools do not fit in memory or the boot pool cannot hold the root table.

booted t ends booting. Tables and memory then come from the other pools.

space t is the virtual address space t maps.

base t is the first virtual address the tables translate.

span t is the number of virtual addresses the tables reach from base: 2{^bits}.

root t is the physical address of the root table.

memory t is the number of bytes of the GPU's physical memory t manages: memory of create.

pa_bits t is the number of bits of a physical address t's entries hold: pa_bits of its format.

main_pool t is the number of bytes of the main pool, memory less the boot pool and the tables' pool.

palloc t n is the physical address of n' new bytes, n rounded up to 4 KiB, aligned to align (defaults to 4096) and zeroed if zero (defaults to true). They come from the boot pool if boot and from the main pool otherwise; boot defaults to whether t is booting. It is Some _ while the pool has a free block of 2 * (n' + align) bytes, and may be None with a smaller one that would fit.

Raises Invalid_argument if n <= 0 or align is not a positive power of two.

pfree t pa frees the block of physical memory at pa that palloc returned or that a mapping of alloc holds.

Raises Invalid_argument if no such block starts at pa, or if a table is there.

The type for mapped virtual ranges.

map t ~va tg ranges maps the physical ranges of tg, in order, from va on, creating the tables it needs, and flushes, whatever the flush returns. uncached and snooped default to false. It is None if the GPU's memory has no room for a table it needs, after unmapping what it mapped and freeing the tables it made. Another exception, such as an asynchronous one at an allocation, does the same before it passes, as far as nothing raises it again; discard clears what is left.

Raises Invalid_argument, changing nothing, if va or an address or length of ranges is not a multiple of 4 KiB, a range ends past the addresses pa_bits bits hold, the range is not within span bytes from base, or an address of it is mapped already.

tables t ~va n is the physical addresses of the tables from the root down to the one whose entries would map the n bytes from va, root first. It creates those that are missing and flushes, as map does. These tables are never freed, so a driver may write the entries that map those bytes itself. t does not see the entries the driver writes, so map maps over them without refusing. It is None if the GPU's memory has no room for a table, keeping those it made.

Raises Invalid_argument if the range is not as map requires, or a page larger than n bytes maps va.

unmap t ~va n unmaps the n bytes mapped from va, frees the tables that become empty, and flushes. The tables go back to their pool before the flush, whatever it returns. It is true iff the flush was confirmed, so that the GPU no longer reaches the memory. On false it may still reach it.

Raises Invalid_argument, changing nothing, if the range is not as map requires, an address of it is not mapped, or a page maps addresses on both sides of its bounds.

discard t ~va n is unmap of whatever the n bytes from va map, none or part of them included, as a map that an exception ended part-way leaves them. A page that maps addresses on both sides of the range's bounds is unmapped whole.

Raises Invalid_argument, changing nothing, if the range is not as map requires.

alloc t h n is n bytes, rounded up to 4 KiB, of new physical memory from the pool palloc takes from by default, mapped at new virtual addresses of space t, with h's hold on them (Space.alloc).

• With ~contiguous:true (defaults to false) the memory is one zeroed block, aligned as the largest block of pages it could hold when the pool has one, so that it maps with large pages.
• Otherwise it is the largest blocks of pages the pool has, not zeroed.

With below, the memory lies at physical addresses that end at or below below, such as the part of the GPU's memory its BAR reaches. The memory is chosen before anything is written.

It is None if the space or the pool cannot supply the memory, as Space.alloc and palloc bound each request, or if a table has no room, after giving back what it took. An exception that ends it, such as an asynchronous one, leaves the addresses to h's release (Space.release).

Raises Invalid_argument if n <= 0.

free t x m unmaps m, which alloc gave with the hold x, and flushes. It is true iff the flush was confirmed, and then it has freed x (Space.free) and, if m is in the GPU's own memory (Gpu), its physical memory. On false it keeps both, which the GPU may still reach.