Introduction

Setting up translation hardware is a security and correctness critical operation. Any mistake can lead to program crashes, data corruption and loss, or violation of isolation guarantees. System software (e.g., firmware, bootloaders, hypervisors, or operating systems) interface with translation hardware to set up the right translations adhering to the security and isolation policies in the system.

Up to now, system software developers needed to implement the drivers to interface with the translation hardware for every new platform and for every piece of system software. This means that work not only had to be duplicated over and over again, but also potential errors would be replicated as well.

In contrast, VelosiRaptor uses a single specification of translation hardware that is expressed in an intuitive domain specific language to describe the behavior of translation hardware. From this specification we can generate both, the system software code that interfaces with the translation hardware, and the translation hardware itself.

This removes the burden to write translation hardware driver code from system software developers: new architectures and translation hardware is supported by simply writing a spec and then having the relevant systems code generated. VelosiRaptor uses software synthesis to support generation of higher-level functions like map/unmap/protect.

Lastly, VelosiRaptor enables research in translation hardware itself by specifying a tailored translation scheme for a specific use case (e.g., FPGAs, accelerators, ...). VelosiRaptor can not only generate the system software components to interface with the translation hardware, but also produce the corresponding hardware descriptions (eventually / future work).

This Document

This document describes the architecture of the VelosiRaptor toolchain, its command line interface, the specification language, and its synthesis/code generation functionality.

• Introduction
• Command Line Interface
• Architecture
• Specification Language
• Synthesis
• Code Generation

Command Line Interface

This section explains the CLI interface of the VelosiRaptor compiler (vrc)

VelosiRaptor Compiler

USAGE:
    vrc [FLAGS] [OPTIONS] <input>

FLAGS:
    -h, --help       Prints help information
    -v               Sets the level of verbosity
    -V, --version    Prints version information

OPTIONS:
    -b, --backend <backend>    the code backend to use [rust, c]
    -e, --Werror <error>       Treat warnings to errors.
    -o, --output <output>      the output file
    -p, --pkg <pkg>            the package name to produce

ARGS:
    <input>    Sets the input file to use

Architecture

This section provides an overview of the VelsoRaptor compiler w

Parsing

TODO.

AST Transformations

TODO.

Synthesis

TODO.

Code Generation

TODO.

Hardware Descriptions

TODO.

The VelosiRaptor Specification Language

This section describes the VelosiRaptor Specification Language (vrs) including its syntax. The goal of the language is to provide an intuitive concise way of describing any translation hardware including its translation semantics, its state and software visible interface.

Ultimately, the language should serve as a basis for generating both, an OS driver and a hardware component implementing the translation hardware, either simulated or a real implementation in a hardware description language.

HowTo: Specifying Translation Hardware

The goal of the specification is to faithfully capture the translation semantics of a real (or imaginary) piece of translation hardware such as an MMU, segment registers, etc.

This section outlines a general strategy to specify the translation hardware as a collection of units.

As a running example, consider an x86_64 MMU.

1. Identify the State

The initial question to ask is what determines how the hardware actually translates memory addresses. In other words, what is the state that defines the translation function? For example, this may be some specific registers, or an in-memory data structure such as the page table. This step also identifies the layout of the state (the meaning of bits), and how the translation is defined with respect to those bits.

x86_64 MMU

• radix tree with four levels: PML4, PDPT, PDIR, PT
• CPU registers: CR3, CR4
• entry: base address and flags, only translates if the present bit is set.

2. Identify the Units

The next step involves identifying the units. Note, there may be more than one way to represent a specific translation hardware in terms of a collection of units.

The following a few rules of thumb.

Rule 1: one state, one unit. Translation hardware may make use of different in-memory data structures, or registers (e.g., a page directory table is different from a page table). Thus, to represent a four-level page table implies 5 different units (one for each level of the page table, plus one to express the processor registers).

Rule 2: One unit for each array of entries Translation hardware may allow controlling several regions in the same fashion (e.g., a page table has a set of equal entries that control a portion of the translation). This suggests expressing the entry as its own unit, and the table as a separate unit that has collection of these entry units.

x86_64 MMU

Applying those rules to the identified state yields nine different units:

• Units: PML4, PML4_Entry, PDPT, PDPT_Entry, PDIR, PDIR_Entry, PT, PT_Entry, x86MMU

3. Identify the Interface

System software interacts with the translation hardware in a certain way. This may be through a register interface, or by writing to a specific memory location. This step identifies the interface used with its fields and the meaning its contents.

x86_64 MMU

• page tables: load-store interface to memory, one field (the entry) with present bit, base ...
• CPU registers: CR3 holding base and context identifier, CR4 to enable/disable translation

4. Putting it Together

The previous steps identified:

1. the units with their state
2. the interface software uses to interact with the units.
3. how hardware translates with respect to the current state.

Using this information, one can now write down the specification of the translation hardware.

unit X86PageTableEntry(base: addr) {
    state = Memory(base: addr) {
        entry [base, 0, 8] {
             0  0 present,
            // more fields omitted
            12 63 frame_addr
        };
    };
    // the interface has the same
    interface = Memory;

    // the translation semantics
    fn translate(va: addr, flags: int) -> addr
      requires state.entry.present; // present bit must be set
    {
        return (state.frame_addr << 12) + va;
    }
};

unit X86PageTable(base: addr) {
    // the table itself doesn't have state or interface

    // it has 512 entries expressed as a map
    staticmap = [ X86PageTableEntry(base + i * 8) for i in 0..512 ];

    // translate basically forwards the translation to the entry
    // this is for illustration purposes only, and is not required,
    // as it is derived from the staticmap description
    fn translate(va: addr, flags: int) -> addr {
        return staticmap[va / 4096].translate(va % 4096, flags)
    }
};

Lexer

The lexer converts the input character stream of the specification file into a token stream. This section explains and provides examples of the various tokens recognized and produced by the lexer.

Conventions

Whitespace The VelosiRaptor language is not whitespace sensitive.

Rule We define rules using uppercase letters and an assignment operator. The following defines a rule with a single body.

RULEID := RULE_BODY

Alternatives Alternative rule components are separated using the pipe | operator. For example, the following rule matches either rule body A or A.

RULEID := RULE_BODY_A | RULE_BODY_B

The first alternative that matches will be taken.

Subrules Parts of the rule body can be grouped together using square brackets. Here the rule matches a A_1 or A_2 followed by B

RULEID := [ RULE_A_1 | RULE_A_2 ] RULE_B

Repetitions Subrules can be repeated using the + operator indicating one or more occurrences of the subrule, and * operator for zero or more. The following has at least one occurrence of rule body A, and zero or more of rule body B.

RULEID := [ RULE_BODY_A ]+ [RULE_BODY_B]*

Optional Subrules To denote a subrule that may be left out the question mark operator ? is used.
Here, the rule body A is optional.

RULEID := RULE_BODY_A? RULE_BODY_B

Special Rules To recognize the end of line explicitly where needed, the EOL rule is used.

EOL

To match any element until the next subrule is met, the ANY rule is used.

ANY

Digits and Characters

The following rules recognize a single digit or character.

Digit Recognizes a single digit from a base-ten number (e.g, 5)

DIGIT    := 0-9

Binary Digit Recognizes a digit from a binary number (e.g., 0)

BINDIGIT := 01

Octal Digit Recognizes a digit from an octal number (e.g., 7)

OCTDIGIT := 0-7

Hex Digit Recognizes a digit from a hexadecimal number (e.g., a) in either uppercase or lowercase form.

HEXDIGIT := 0-9a-fA-F

Alpha Character Recognizes a character from the ASCII alphabet in either lowercase or uppercase form.

ALPHA    := A-Za-z

Alphanumeric Character Recognizes either a character from the ASCII alphabet in lowercase or uppercase form, or a digit.

ALPHANUM := ALPHA | DIGIT

Numbers

Numbers represent a numeric literal. The lexer supports recognition of binary, octal, hexadecimal and decimal numbers. The following describes the lexer rules.

The lexer will check for overflows when parsing the number.

Decimal Numbers

A base-ten number is at least one digit followed by zero or more digits that may be separated by underscores ("_")

NUM10 := DIGIT+ [ "_" | DIGIT ]*

Examples: 1000, 2_300_500, 999_99_9

Binary Number

A binary number is then the string "0b" followed by one or more binary digits, and zero or more binary digit groups separated by an underscore ("_").

NUM2 := "0b" BINDIGIT+ [ "_" | BINDIGIT ]*

Examples: 0b0, 0b1000_1000

Octal Number

An octal number is then the string "0o" followed by one or more octal digits, and zero or more octal digit groups separated by an underscore ("_").

NUM8 := "0o" OCTDIGIT+ [ "_" | OCTDIGIT ]*

Examples: 0o755, 0o7000_1234

Hexadecimal Number

A hexadecimal number is the string "0x" followed by one or more hex digits, and zero or more hex digit groups separated by an underscore ("_"). Both, uppercase and lowercase numbers are supported.

NUM16 := "0x" HEXDIGIT+ [ "_" | HEXDIGIT+ ]*

Examples: 0x1000, 0x4000_0000

Number

A number is then either one of the four base numbers:

NUMBER := NUM10 | NUM16 | NUM8 | NUM2

Examples: 0o7000_1234, 0x4000_0000, 10, 0b01001

Identifiers

Identifiers represent symbols and names in the VelosiRaptor language and thus play a central role when specifying translation units.

Identifier

An identifier begins with either an alpha character or an underscore, and may be followed by a sequence of alphanumeric characters and underscores.

IDENT := [ ALPHA | "_" ] [ALPHANUM | "_" ]*

Example: foo, foo_bar, foobar_1234

Naming Conventions

The VelosiRaptor language roughly follows the naming convention of Rust The compiler will display a warning

Keywords

Keywords are identifiers with special meaning. They are used to structure the language. Keywords are considered reserved words and cannot be used as identifiers.

The complete list of keywords is as follows:

KW_ADDR        := "addr"
KW_ASSERT      := "assert"
KW_BOOLEAN     := "bool"
KW_CONST       := "const"
KW_ELSE        := "else"
KW_ENSURES     := "ensures"
KW_EXISTS      := "exists"
KW_FN          := "fn"
KW_FOR         := "for"
KW_FORALL      := "forall"
KW_IF          := "if"
KW_IMPORT      := "import"
KW_IN          := "in"
KW_INTEGER     := "int"
KW_INTERFACE   := "interface"
KW_LAYOUT      := "Layout"
KW_LET         := "let"
KW_Memory      := "Memory"
KW_MMIO        := "MMIO"
KW_NONE        := "None"
KW_READACTION  := "ReadAction"
KW_REGISTER    := "Register"
KW_REQUIRES    := "requires"
KW_RETURN      := "return"
KW_SIZE        := "size"
KW_STATE       := "state"
KW_STATICMAP   := "staticmap"
KW_UNIT        := "unit"
KW_WRITEACTION := "WriteAction"

Tokens

Tokens provide other language constructs such as punctuations, parentheses, and other operators.

Punctuations

DOT            :=  "."
COMMA          :=  ","
COLON          :=  ":"
SEMICOLON      :=  ";"

Parenthesis

LPAREN         :=  "("
RPAREN         :=  ")"
LBRACE         :=  "{"
RBRACE         :=  "}"
LBRACKET       :=  "["
RBRACKET       :=  "]"

Arithmetic Operators

PLUS          :=  "+"
MINUS         :=  "-"
STAR          :=  "*"
SLASH         :=  "/"
PERCENT       :=  "%"
LSHIFT        :=  "<<:
RSHIFT        :=  ">>:

Bitwise Operators

XOR           :=  "^"
NOT           :=  "~"
AND           :=  "&"
OR            :=  "|"

Logical Operators

LNOT          :=  "!"
LAND          :=  "&&"
LOR           :=  "||"

Comparison Operators

EQ            :=  "=="
NE            :=  "!="
LT            :=  "<"
GT            :=  ">"
LE            :=  "<="
GE            :=  ">="

Arrows

LARROW        :=  "<-"
RARROW        :=  "->"
BIDIRARROW    :=  "<-->"
FATARROW      :=  "=>"
BIDIRFATARROW :=  "<=>"
RLONGFATARROW :=  "==>"

Others

ASSIGN        :=  "="
AT            :=  "@"
DOTDOT        :=  ".."
PATHSEP       :=  "::"
WILDCARD      :=  "?"

Comments

The VeloSiraptor language uses similar comment style like C / Rust / Java.

Line Comments

Line comments mark everything from the start of comment marker // up to and including the end of line marker as a comment.

LINECOMMENT := "//" ABY EOL

Example

// this is a comment

Block Comments

A block comment takes everything from the start of comment marker /* up to and including to the end of comment marker */ as a comment.

BLOCKCOMMENT := /* ANY */

Example

/* this is a
multiline comment */

/* this is a comment */ 1234

Nesting Block comments may contain line comments, but block comments must not be nested.

Specification Language

This section describes the VelosiRaptor Specification Language (VSL) using the tokens outlined in the previous section.

Specification Files

A translation hardware component is specified in a VelosiRaptor Specification Language file (*.vrs). At the top level, there are three possible constructs:

1. Imports to include other specification files.
2. Constants that defines globally visible constants.
3. Units that specify translation hardware components.

The unit is the core element of the specification language.

Encoding The encoding of the file should be plain ASCII, and process

Naming Currently all specification files should be placed in the same directory, and must have a filename in the form of an identifier followed by the *.vrs extension.

There is no restriction regarding the name of the unit specified in the file, and the filename itself.

Example

// A sample specification file

// import of the global constants, defined in another file
import globals;

// define some constants used in the spec
const NUM_ENTRIES : int = 512;
const PAGE_TABLE_SIZE : int = NUM_ENTRIES * POINTER_SIZE;

// define the page table unit
unit PageTable(base : addr) {
    state = ...
    interface = ...

    fn translate(va: addr, flags: int) -> addr {
        ...
    }
}

Imports

Often, specifications may become large: for example, current page-table-based translation schemes may result in multiple unit specifications (e.g., one for each level), and one would like to separate different units into different files. Moreover, modularization allows specifications to be reusable and to define constants in a single location.

Grammar

IMPORT := KW_IMPORT IDENT SEMICOLON

Example

import x86_page_table_entry;
import x86_constants;

Description

The evaluation of import directives is recursive: starting at the supplied root file name, the compiler will resolve all imports recursively, while skipping already imported files.

Circular imports (e.g., A imports B and B imports A) will trigger an error.

Each specification file on its own must have all imports.

Constants

Specifications of translation hardware may include specific, constant values such as the number of segment registers, the size of a page table, or the width of the addressing mode. These values may be used at multiple locations. To avoid in-coherency, constants provide a mechanism to give a constant value a name and re us that within the unit definitions.

Grammer

CONST := KW_CONST IDENT COLON TYPEDEF EQ EXPR SEMICOLON

Examples

const PAGESIZE : int = 4096;
const ADDRESSWIDTH : int = 64;
const PAGE_TABLE_SIZE : int = PAGE_TABLE_ENTRIES * PAGE_TABLE_ENTRY_SIZE;

Description

A constant definition assigns an identifier to an expression that must evaluate to a constant value at compile time.

Each constant definition has a given type, and the expression must produce a value of that type.

Constants can be defined on a global level, or within the scope of a unit.

Constants shall have a SCREAMING_SNAKE_CASE format.

Units

The unit is the core part of the specification. It combines the state, the interface and translation semantics to build a model of the translation hardware unit and how it translates input addresses.

Note, a complete translation scheme (e.g., an x86 memory management unit) is expressed as a collection of units each of which modeling a specific aspect of it (e.g, a page table entry at a specific level). The full specification is a composition of these units (e.g., a page table is a composition of 512 page table entries).

                        interface
                            |
                            v
                +-----------------------+
  input addr    |                       |  output addr
 -------------> | translate(input addr) | ------------->
                |                       |
                +-----------------------+
                          unit

Conceptually, a unit translates an input address to an output address -- analogous (but not limited) to a virtual to physical address translation. There are two distinct translation behaviors:

1. The static map defines a fixed translation function known at compile time.
2. The configurable segment defines a configurable translation function that depends on the runtime state.

Thus, to model a translation unit one needs to find a representation in terms of a combination of static maps and configurable segments.

In the page table example, the page table as a whole is a fixed mapping of an input address onto one of the 512 entries, and in turn each entry is a configurable unit defining the translation of the page depending on the state of the entry.

Grammar

UNIT         := KW_UNIT LPAREN ARGLIST RPAREN UNIT_DERIVE LBRACE UNIT_BODY RBRACE

UNIT_DERIVE  := COLON IDENT
UNIT_BODY    := CONST*  STATE?  INTERFACE?  MAP?  METHOD*

ARGLIST      := [ ARG [COMMA ARG]* ]?
ARG          := IDENT COLON TYPE

Example

unit Simple(base : addr) : Segment {
    // the state
    state = ...

    // the interface
    interface = ...

    // translation semantics
    fn translate(va: addr, flags: int) -> addr
        ...

    // unmapping an entry
    fn unmap(va: addr, sz: size) -> bool
        ...

    // mapping an entry
    fn map(va: addr, sz: size, flags: int, pa : addr) -> bool
        ...

    // protecting the entry, i.e., change its permission
    fn protect(flags: int) -> bool
        ...
};

Static Map Units

Conceptually, the static map unit type defines a list of input address ranges. Each range has a well-defined mapping onto either an output address range or another unit.

This modifies the address in the following way:

OUT = IN - REGION_BASE + OFFSET

This normalizes the address to be translated, i.e., it falls within [OFFSET, OFFSET + REGION_SIZE). For example, an x86_64 page table is a static map of 512 ranges each of which has size 4096. A page-table entry in turn translates a range [0, 4096).

Configurable Segment Units

Configurable units are abstracted as a segment, i.e., a range of addresses [0, size) that map to an output range [pa, pa + size).

This modifies the address in the following way:

OUT = IN + BASE

Unit Components

The following table outlines the main components and which unit type they are required for.

State Description A configurable unit has a state description. The state of the unit defines its translation behavior. Methods can reference the state through the state symbol.

Interface Description A configurable unit has an interface description. The interface defines how software can interact with the unit to change its translation behavior. Interface fields are referenced through the interface symbol.

Map Description A static unit has a map description defining a static address translation function that is fixed at compile time.

Translate Description A configurable unit has a translate description. This defines the translation behavior of the unit.

Map/Unmap/Protect A unit may define map/unmap/protect functions. These methods provide constraints used by the synthesis step.

Additional Unit Components

Constants Units can have constant definitions. In contrast to the constants defined at the top level, those constants are available within the scope of the unit.

Methods Units can have method definitions that provide a mechanism to provide a commonly used computation over the state.

Unit Parameters

A unit may be parameterized. This is required to define the state of the unit that may be located at a specific address that is unknown at compile time. For example, a page table may be allocated anywhere in memory subject to alignment constraints.

Derivation (Inheritance)

A unit can be derived from another unit. This is similar to inheritance. The deriving units can overwrite certain aspects, or fill in blanks in a template provided by the derived unit.

State

The state defines how a translation hardware unit translates memory addresses, i.e., its translation behavior is a function over the state. Conceptually, the state consist of a set of fields, where each field has bitslices assigning meaning to a range of bits. The state can be located inside the translation hardware, or external to it (i.e., in some memory).

Grammar

STATE := MEMORY_STATE | REGISTER_STATE | NONE_STATE

MEMORY_STATE       := KW_MEMORY LPAREN ARGLIST RPAREN FIELD_BLOCK
REGISTER_STATE     := KW_REGISTER FIELD_BLOCK
NONE_STATE         := KW_NONE

FIELD_BLOCK        := LBRACE [ FIELD ]+ RBRACE
FIELD              := IDENT FIELD_PARAMS BITSLICE_BLOCK? SEMICOLON
FIELD_PARAMS       := LBRACK [IDENT COMMA NUM COMMA ]? NUM RBRACK

BITSLICE_BLOCK     := LBRACE BITSLICE RBRACE
BITSLICE           := NUM NUM IDENT

ARGLIST            := [ ARG [COMMA ARG]* ]?
ARG                := IDENT COLON TYPE

Example

Memory(base : addr) {
    address [base, 0, 8] {
        0  63 base
    };
    sz [base, 8, 8] {
        0  63 bytes
    };
    flags [base, 16, 8] {
        0 0 present
    };
};

External State

External state (or memory state) utilizes some region of main memory to hold translation information. One prime example for external state would be the page table: the location of the page table is external to the translation hardware that itself issues load/stores to memory to read (and write) the data structure.

This state is fully visible to system software.

To perform a translation, the translation hardware will interpret a memory location identified by some base pointer and performs address transformation depending on the contents of this memory location.

For example, the bit pattern of a page table entry defines whether there exists a valid translation, and whether the translation points to another page table or to a physical frame.

Internal State

Internal state (or register state) utilizes some form of memory inside the translation hardware to hold the current translation state. In contrast to the in-memory state, the actual layout of the internal state representation may not be strictly defined.

This state is not directly visible to system software. Hardware may expose the state (or parts of it) through a register interface.

To perform a translation, the translation hardware uses the internal state to determine the translation function.

For example, the contents of the system control register defines whether the translation hardware is activated or not.

Fields

Within a state definition, each field must have a unique identifier.

The identifiers in the FIELD_PARAM block must be defined in the field ARGLIST

The identifiers in the field ARGLIST must be defined in the unit ARGLIST

The two numbers indicate offset from base, and the size of the field in bytes.

The size of the field must be 1, 2, 4, or 8.

Bitslices

Within a field, each bitslice must have a unique identifier.

The two numbers indicate the start and end (including) bits of the slice.

To denote a single bit, set the start == end bit.

The bit slices must not overlap

The bit slices must not exceed the size of the field.

Interface

The interface of a unit provides the set of operations that system software can perform to configure the translation hardware. Similarly to the state, the interface consists of a set of fields that represent the API of the translation unit. System software can only interact with the translation hardware configuration through its interface.

             +-------------+                      +-------------+
 operation   |             |  state transitions   |             |
-----------> |  Interface  | <=================>  |    state    |
             |             |                      |             |
             +-------------+                      +-------------+

Grammar

INTERFACE           := NONE_INTERFACE
                     | MMIO_INTERFACE
                     | MEMORY_INTERFACE
                     | REGISTER_INTERFACE

NONE_INTERFACE      := KW_NONE SEMICOLON

MMIO_INTERFACE      := KW_MMIO LPAREN ARGLIST RPAREN INTERFACE_BODY

MEMORY_INTERFACE    := KW_MEMORY LPAREN ARGLIST RPAREN INTERFACE_BODY

REGISTER_INTERFACE  := KW_REGISTER LPAREN ARGLIST RPAREN INTERFACE_BODY

INTERFACE_BODY      := LBRACE [ INTERFACE_FIELD ]+ RBRACE

INTERFACE_FIELD     := IDENT FIELD_PARAMS LBRACE
                       LAYOUT READACTION? WRITEACTION? RBRACE SEMICOLON

LAYOUT              := KW_LAYOUT BITSLICE_BLOCK

READACTION          := KW_READACTION ACTIONS_BLOCK SEMICOLON
WRITEACTION         := KW_READACTION ACTIONS_BLOCK SEMICOLON

ACTIONS_BLOCK       := LBRACE [ ACTION [COMMA ACTION]* ] RBRACE
ACTION              := EXPR [LARROW | RARROW ] EXPR

ARGLIST             := [ ARG [COMMA ARG]* ]?
ARG                 := IDENT COLON TYPE

Example

interface = Memory(base : addr) {
    address [base, 0, 8] {
        Layout {
            0  63 base
        };
        ReadAction {
            interface.address <- state.address;
        };
        WriteAction {
            interface.address -> state.address;
        };
    };
    sz [base, 8, 8] {
        Layout {
            0  63 bytes
        };
        ReadAction {
            interface.sz <- state.sz;
        };
        WriteAction {
            interface.sz -> state.sz;
        };
    };
}

Interface Kinds

Currently, the language supports four different interface kinds that define how system software needs to invoke the interface.

None. There is nothing to be configured by this unit, i.e., the unit is merely a static map.

Memory Interface. This is the interface to an in-memory data structure (e.g., a page table). Software uses loads/stores to interact with it. This means, the interface is in fact an identity of the state, and software can effectively access the entire state.

MMIO Interface. These are memory mapped registers. Software uses non-cached load/stores to interact with this interface. In contrast to the memory interface, parts of the state may not be directly accessible from the interface.

Register Interface These are registers that do not have a memory address, but rather the CPU uses loads/stores to an special CPU registers, or even issues a specific instruction to do so

Actions

Recall the set of interface fields correspond to the API system software uses to interact with the translation hardware where each field corresponds to a function. This API function in turn can be invoked through a read or write operation on the field.

To specify the behavior, the interface specification includes a set of actions that may modify the state of the translation hardware. This set of actions connect the state with the interface: The following example expresses a single address field with the corresponding actions. Writing to the address field copies the content into the address field of the state. Likewise, reading the address field copies the current value in the state.

interface = Memory(base : addr) {
    address [base, 0, 8] {
        Layout {
            0  63 base
        };
        ReadAction {
            interface.address <- state.address;
        };
        WriteAction {
            interface.address -> state.address;
        };
    };
};

No actions The set of actions can be empty. This means that the corresponding interface field does not have a "direct" connection to the state, i.e., when the interface field is written or read, nothing happens with regard to the state.

Multiple Actions The blocks can contain multiple actions. For example, setting the base address and the enabled bit at the same time, or some kind of "commit" semantics where a transition is prepared in some interface fields, then committed when writing to another field.

Static Maps

A static map defines a fixed translation function from input address ranges to output address ranges (destination units). The map is fixed at compile time, and thus cannot be configured at runtime.

Static maps are used to divide the input address range of a unit, and steer translations to configurable units. A page table, for instance, is a static map that selects the page table entry for the translation.

Grammar

MAP := KW_STATICMAP ASSIGN LBRACK [ MAP_EXPLICIT_LIST | MAP_LIST_CMPR ]  RBRACK SEMICOLON

MAP_EXPLICIT_LIST := MAP_ELEMENT [ COMMA MAP_ELEMENT ]*
MAP_LIST_COMPR := MAP_ELEMENT KW_FOR IDENT KW_IN RANGE_EXPR

MAP_ELEMENT := MAP_SRC? MAP_DST

MAP_SRC  := RANGE_EXPR RARROW

MAP_DEST := IDENT LPAREN EXPR_LIST RPAREN AT EXPR

EXPR_LIST := [ EXPR [ COMMA EXPR ]* ]?

Examples

// simple, explicit list
staticmap = [
    PageTableEntry(base + 0),
    PageTableEntry(base + 1),
];

// comprehension
staticmap = [
    PageTableEntry(base + i) for i in 0..512
];

// with input and output ranges
staticmap = [
    0x0000..0x0fff => DestUnit(base) @ 0x1000
]

Address Range Rules

An element of a static map has a well-defined input address range [base..limit].

The input address ranges of any two entries must not overlap.

The input address range must not exceed the available addressing width of the next unit.

Output Address Calculation

The output address, i.e., the address that will become the input address of the destination unit, is calculated as follows:

OUT_ADDR = IN_ADDR - ENTRY_BASE + OFFSET

Where, ENTRY_BASE is the base address of the matching entry of the map, and OFFSET is the value of the @ expression.

The output address range must not exceed the available addressing width of the next unit.

Methods

Methods are mathematical functions: they perform a computation using the supplied parameters and the current state of the translation unit. Generally, they are internal to the translation hardware and cannot be invoked by system software. Methods define certain procedures such as extracting the base address from the state, or match supplied flags.

Methods contain statements and/or pre- and post-conditions that contain expressions.

Grammar

METHOD       := KW_FN IDENT LPAREN ARGLIST RPAREN RARROW TYPE
                  REQUIRES* ENSURES* METHOD_BODY

REQUIRES     := KW_REQUIRES BOOL_EXPR SEMICOLON

ENSURES      := KW_ENSURES BOOL_EXPR SEMICOLON

ARGLIST      := [ ARG [COMMA ARG]* ]?

ARG          := IDENT COLON TYPE

METHOD_BODY  := RBRACE [ STMT ]* LBRACE

STMT := STMT_RETURN | STMT_LET | STMT_ASSERT | STMT_COND
STMT_RETURN  := KW_RETURN EXPR SEMICOLON
STMT_LET     := KW_LE IDENT COLON TYPE EQ EXPR SEMICOLON
STMT_ASSERT  := KW_ASSERT LPAREN BOOL_EXPR RPAREN SEMICOLON
STMT_COND    := KW_IF BOOL_EXPR LBRACE STMT+ RBRACE [KW_ELSE LBRACE STMT+ RBRACE]?

Example

fn get_base() -> addr {
    return state.entry.base << 12;
}

fn calc_size(val : int) -> int
  requires val < 1024;
  ensures calc_size(val) < 4096;
{
    return val * 4;
}

Method Types

There are two distinct method types:

1. External methods that are abstract and provide constraints to the code generation system.
2. Internal methods with an implementation used by the translation hardware

External Methods

External methods are generally abstract and correspond to operations that are executed by system software. They are abstract because their implementation will be provided by the code generation framework through the synthesis process.

These methods are useful to provide additional constraints to the code generation module. For more information see Map/Unmap/Protect

Map (required)

This method ensures that the translation of a certain range (addr-size-tuple) produces an address within the destination range. This is a state modifying operation.

Unmap (optional)

This method ensures that the range of addresses won't be mapped anymore. This is a state modifying operation.

Protect (optional)

This method changes the protection of an already mapped region. This is a state modifying operation.

Internal methods

As mentioned above, internal methods provide a way to structure the implementation of the translation hardware itself. This would correspond to procedures and functions that are implemented by the simulator or the corresponding hardware description language.

Translate (required)

The translate method must be defined for each unit. It defines the translation semantics. This is a function state, address and flags, to a new address (technically a partial function).

The translation function may make use of any other defined methods of the unit.

Other Methods

Additional methods can be declared in a unit context. All of them are internal methods and are available as predicates and/or within the translation method.

Pre- and Post-Conditions

Methods can be augmented with pre- and post-conditions using the requires and ensures clauses. This provides additional constraints to the synthesizing step. The following example indicates the use of pre- and post-conditions for the map function: it requires that the range must be within some limit, the addresses aligned to some page. Moreover, the function ensures that all addresses within the range are translated properly.

fn map(va: addr, sz: size, flags: int, pa: addr)
    requires va + sz < LIMIT;
    requires va % 4096 == 0;
    requires size == 4096;
    requires pa % 4096;
    ensures forall i : int :: 0 <= i && i < sz
                ==> translate(va + i, flags) == pa + i
{} // empty

Statements

The body of the units are restricted to four statement kinds each of which evaluate expressions.

Return Returns the value produced by the expression. Each branch must have a return statement.

Let Defines a local variable.

Assert Provides some additional constraint to the synthesizer

Conditional Provides an if-then-else statement. Both branches must have a return statement.

The Translate Method

The translate method is a special method that defines how a unit translates incoming addresses.

Definition

The translate function defines the translation semantics of a unit depending on its state.

Mathematically, this is a partial function taking a state, address, and some flags, to produce a new address.

translate :: State -> Addr -> Flags -> Addr option

The state is implicit in the specification language (i.e., it can be accessed with the state symbol). The signature of the translate method is as follows:

fn translate(va: addr, flags: int) -> addr

The preconditions should define the conditions under which the translation function is well-defined and produces a result. Thus, for all inputs satisfying the inputs, the function is guaranteed to produce an address, otherwise translation fails.

Example

In this example, translate requires that the supplied input address is within the defined range from [0, size) and that the present bit must be set. It then returns a new address by adding the base to the input address.

fn translate(va: addr, flags: int) -> addr
    requires va < state.sz.bytes;
    requires state.flags.present == 1;
{
    return va + state.address.base;
}

Synthesis

The translate method is the "verifier" in the synthesis process. For each program (i.e., implementation of the map/unmap/protect functions) the synthesis algorithm checks whether translate produces the expected result. For example, that forall addresses with the range [va, va + i) translate produces the right output address.

 forall i | 0 <= i < size :: translate(va + i, flags) == pa + i;

Flags

The flags define the permissions, modes, etc. for this translation. This may include, read/write/execute permissions, user/supervisor separation, memory protection keys, ...

TODO: finalize the notion of flags

Pre-Conditions

The pre-conditions state the conditions under which the translation is well-defined. There are three areas to consider when formulating the pre-conditions.

Input Address (va)

• what range of input addresses is valid
• does this depend on some state field?

Flags

• which kind of access flags do match the permissions set in the translation?
• Exact match, or what set of flags is still sufficient?

State

• Are there any predicates over the state that must be satisfied?

Static Map Units

The translation function of a static map unit is defined by the map definition, and does not need to be specified.

Map/Unmap/Protect Functions

The map/unmap/protect functions are higher-level operations that system software uses to configure the translation units. The implementations of these methods are synthesized by the toolchain.

The purpose of the map/unmap/protect functions is to provide the necessary constraints to the synthesis algorithm.

All three methods are causing state transitions, and they may or may not be supported by the underlying hardware.

Example

The following example provides an illustration: it adds constraints on the provided addresses and the size parameters.

fn map(va: addr, sz: size, flags: int, pa : addr) -> bool
    requires va == 0x0;
    requires pa <= 0xffffffffffff;
    requires pa + sz <= 0xffffffffffff;
    requires sz <= 0xffffffff;
    requires sz >= 16;

    ensures forall i : addr :: 0 <= i && i < sz && translate(va + i, flags) == pa + i;
{} // empty

Map

The map installs a new mapping with the given permissions. It ensures that the supplied address range [va, va + size) maps onto the range [pa, pa + size).

This corresponds to the following function:

map :: Addr -> Size -> Addr -> Flags -> State -> State

The signature in the specification language:

fn map(va: addr, sz: size, flags: int, pa : addr) -> bool;

In most cases, this will overwrite the already existing mapping.

Unmap

The unmap method removes the existing mapping in the translation unit. It ensures that the supplied address range [va, va+size) is no longer accessible. This is similar to removing all access rights with protect, but it also removes any information on the previous mapping.

This corresponds to the following function:

unmap :: Addr -> Size -> State -> State

The signature in the specification language:

fn unmap(va: addr, sz: size) -> bool;

In most cases, the input address and the size must match the already existing values, or it shrinks the second part of the mapping.

Protect

The protect method changes the access permissions on an existing mapping. It ensures that the supplied address range [va, va+size) adheres to the new access rights.

This corresponds to the following function:

protect :: Addr -> Size -> Flags -> State -> State

The signature in the specification language:

fn protect(va: addr, sz: size, flags: int) -> bool;

In most cases, the input address and the size must match the already existing values (i.e., there is no further split possible)

Pre-Conditions

The following some suggestions on the kind of pre-conditions one may write.

Input Address (VA)

• Supported address values (min, max, alignment)?
• Is it always 0? (a segment is always [0, size)
• Limits w.r.t. va + size
• Same as existing value in the state?

Size

• Supported size values (min, max, alignment)?
• Same as existing value in the state?

Flags

• what flags are supported?

Output Address (PA)

• Supported size values (min, max, alignment)?
• Limits w.r.t. pa + size
• Same as existing value in the state?

Expressions

Expressions produce either an integer or boolean value, and can be used as part of the statement or method pre- and post-conditions.

Expressions are heavily influenced by how rust handles expressions, albeit a bit simiplified.

Grammar

// currently no distinction in the grammar
BOOL_EXPR           :=  EXPR
ARITH_EXPR          :=  EXPR

EXPR                :=  TERM_EXPR [OP EXPR]?

TERM_EXPR           := NUM_LITERAL_EXPR
                     | BOOL_LITERAL_EXPR
                     | FN_CALL_EXPR
                     | SLICE_EXPR
                     | ELEMENT_EXPR
                     | IDENT_EXPR

NUM_LITERAL_EXPR    := NUMBER
BOOL_LITERAL_EXPR   := BOOLEAN
FN_CALL_EXPR        := IDENT LPAREN [EXPR [COMMA EXPR]* ]? RPAREN
SLICE_EXPR          := IDENT RBRAK RANGE_EXPR LBRAK
RANGE_EXPR          := ARITH_EXPR DOTDOT ARITH_EXPR
ELEMENT_EXPR        := IDENT RBRAK ARITH_EXPR LBRAK
IDENT_EXPR          := IDENT

Operator Precedence

The operator precedence roughly follows the Rust model.

Quantifier Expressions

A quantifier expression produces a boolean value based on whether the mathematical quantifier expression (forall or exists) holds.

Grammar

QUANTIFIER_EXPR := FORALL_EXPR | EXISTS_EXPR

FORALL_EXPR := KW_FORALL ARGLIST PATHSEP BOOL_EXPR
EXISTS_EXPR := KW_EXISTS ARGLIST PATHSEP BOOL_EXPR

Example

forall x : int :: a + x > 0

Synthesis Notes

Examples

This section contains a few examples of translation hardware expressed in the specification language, and the corresponding generated systems code.

• x86 Page Table
• x86 Segmentation
• Xeon Phi SMPT
• Direct Segment

Example: Segmentation

This example models an x86 segment descriptor, an in-memory data structure.

Description

The following figure depicts the segment descriptor from the Intel 64 and IA-32 Architectures Software Developer’s Manual.

Segment Limit Is a 20-bit value, concatenation of the two fields in the descriptor.

• If G == 0 then size is incremented in one byte granularity (1--1MByte)
• If G == 1 then size is incremented in 4k granularity (4k--4GBytes)

Base Address Is a 32-bit value, concatenated of the two fields in the descriptor. Alignment is ideally on a 16-byte boundary.

DPL Privilege Levels, value of 0-3.

Type If S == 1 then bit 11 defines whether its

• data (0), writable (bit 9 == 1), or read-only (bit 9 == 0)
• code (1), readable (bit 9 == 1), or execute-only (bit 9 == 0) Bit 8 indicates the accessed flag.

If S == 0 this is a system-segment and gate-descriptor. Let's ignore that for now.

S Flag indicating whether this is a system segment (S == 0) or code/data (S == 1).

P Indicates whether the segment is present or not. If P == 0 translation results in exception.

D/B Should always be set to 1 for 32-bit code.

Unit Specification

Editable field to fill in the spec. Does not save

unit X86SegmentDescriptor(..) {
    ..
}

Example: x86 Page Table (32-bits)

This example models an x86 page table, an in-memory data structure.

Description

The following figure depicts the page table format from the Intel 64 and IA-32 Architectures Software Developer’s Manual.

CR3

Page Directory (Normal)

Page Directory (Super Page Mapping)

Page Table

The page table maps an aligned 4k page in memory.

Unit Specification (Page Table)

Editable field to fill in the spec. Does not save

unit X86PageTable(..) {
    ..
}

Example: Xeon Phi SMPT

Description

The Xeon Phi SMPT sits between the local physical address space of the co-processor and the system memory, i.e., memory accesses from the Xeon Phi to the host are translated by the SMPT.

The Xeon Phi has a 40-bit address space, where the upper half of it (512G - 1TB) is covered by the SMPT.

The SMPT translates addresses at 16GB granularity onto the 64-bit PCI Express address space (or host address space). Thus, the SMPT has a total of 32 entries each of which is controlled by a register.

The control registers are memory mapped and located at offset 0x3100 from the MMIO registers.

The register is 32-bits in size, where

• bit 0 controls snooping
• bits 31..2 contain the high bits of the host memory address

Unit Specification

Editable field to fill in the spec. Does not save

unit Smpt(..) {
    ..
}

Direct Segment

This translation hardware models a direct-segment-like translation scheme.

Description

The direct segment is a single, continuous address range controlled by three 64-bit registers. The region must be between 4G and 128TB, and must be aligned to 16 bytes.

VABase The base address of the virtual region covered by the direct segment.

Size The size of the region should be aligned to 16 bytes. A size of 0 disables translation.

DstBase The destination region must be within the available 46-bits of physical addresses, and should be 16 bytes aligned.

Register Accesss The registers are special CPU registers that can be accessed using load/stores (e.g., mov rax vabase).

Unit Specification

Editable field to fill in the spec. Does not save

unit DirectSegment(..) {
    ..
}