Towards Porting Operating Systems with Program Synthesis

Memory Model.

Alewife memory regions, \(\mathit {x_{mem}}\), have finite lengths with types \(\mathit {N}_1\ \mathtt {bit}\ \mathit {N}_2 \mathtt {len}\ \mathit {N}_3\ \texttt {ref}\); such a region contains \(\mathit {N}_2\) elements, each of which is an \(\mathit {N}_1\)-bit value; pointers into the region are \(\mathit {N}_3\)-bit values. \(\mathit {N}_1\), \(\mathit {N}_2\), and \(\mathit {N}_3\) here can be either concrete lengths or abstract symbolic constants. For example in Figure 4, the type of the DispMem region has three symbolic constants: it has DISP_MAX locations (DISP_MAX len), each containing a bitvector with length wordsize (wordsize bit), whose pointers are wordsize-bit values (wordsize ref). We discuss the concretization of these abstract values in Section 5.

Memory is addressed by pointers, which are pairs of a memory region and offset; a pointer to the nth element of memory region \(\mathit {x_{mem}}\) is represented by the pair \(\mathit {(}\mathit {x_{mem}}, n\mathit {)}\). Memory regions do not overlap; that is, given two memory regions \(\mathit {x_{mem 1}}\) and \(\mathit {x_{mem 2}}\), a pointer \(\mathit {(}\mathit {x_{mem 1}}, \_\mathit {)}\) can never alias a pointer \(\mathit {(}\mathit {x_{mem 2}}, \_\mathit {)}\). This “swiss-cheese” memory model is inspired by DieHard’s miniheaps [Berger and Zorn 2006] and array separation logic [Brotherston et al. 2017] and reflects the C standard. Memory regions are second-class; pointers may be passed around, but memory regions may not and every pointer must explicitly name a specific memory region.

A memory region can optionally have a label, which is the symbol used to refer to its base address in assembly language text. Note that while this symbol refers to a constant, the value of the constant is not known until the code is assembled and linked into the final output program; or in the case of typical shared libraries or position-independent executables, not until program execution. In general, position-independent code and ordinary code must use different instructions to refer to labels. For this reason, and because Barrelfish links its kernel as position-independent code, we attach an access type to each label.

It is allowable to declare a memory region with 0 len, which means that we model only the existence of the region but not its internal workings. OS designers generally do not need to know the synthesis algorithm when writing these Alewife specifications. However, limiting memory regions to their minimum size improves performance, since adding extra state slows down synthesis.

Abstract Declarations and Abstract Functions. Values imported with require (lines 2–6 in Figure 4), such as the register pc_reg and integer wordsize, are examples of abstract declarations, allowing an Alewife specification to omit details of how an implementation represents and stores data. This is the key to making Alewife specifications machine-independent. Such identifiers must be defined elsewhere for each target machine; we bind the abstract declarations and their corresponding machine-dependent definitions in a later step, before conducting synthesis. Alewife types (the complete specification is in Section A.6) can contain symbolic bit lengths and abstract type identifiers, which will be specialized to different bit lengths and Cassiopea types by Cassiopea machine descriptions and machine-dependent lowerings before synthesis takes place. For example, in Figure 4, the value wordsize, imported with require in line 2, is used to define the dispatcher memory region DispMem on line 8. A machine description, written in Cassiopea, provides the definition for wordsize appropriate for a specific machine. Similarly, the size of the (machine-dependent) dispatcher structure is specified using an abstract integer DISP_MAX. We discuss details of the concretization of these abstract states and functions in Sections 4 and 5, with examples from two different architectures (MIPS and ARMv7) whose relevant Cassiopea descriptions appear in Figure 5 and the lowering files in Figure 6.

Fig. 5.

View Figure

Fig. 6.

View Figure

Alewife specifications also use abstract functions. For example, line 7 of Figure 4 declares a function get_crit_ptr. This example does not refer to machine state, but others might. The predicate interrupts_are_on mentioned earlier, for example, will.

The keyword lower-with (e.g., line 9 in Figure 4) is used to name modules from which to get the machine-dependent instantiations of the abstract definitions. In this case, there are three: definitions related to disp_check, permission to change the processor flags on machines that have them, and scratch register assignments for this block. These are called lowering modules and are discussed in more detail in Section 5.

Frame Conditions. An Alewife specification may optionally provide frame conditions that permit a block to modify additional machine state (registers or register fields and memory). By default, synthesized code can modify only the machine state explicitly mentioned in the postcondition. All other state elements’ final values must equal their initial values. The modify frame condition identifies additional (abstract) state elements that may be modified (e.g., scratch registers). As we discuss in Section 5, lowering modules can also add frame conditions. In practice, this is where most frame conditions come from. The frame conditions are more than synthesis heuristics that help to prune the search space; they are a useful shorthand to materially affect the specification.

The default behavior is desirable: most blocks should not modify states irrelevant to their postcondition. However, some computations require scratch registers. Additionally, it is sometimes necessary to read a register and write the same value back. For example, many control registers contain multiple fields but can only be read and written as a unit; changing one field requires reading the whole register, updating the desired field, and writing the whole register back. It is important both to permit these accesses and to ensure that the other fields are not arbitrarily modified. On MIPS, for example, bit 0 of the status register controls the interrupt state; but the register contains many other fields where arbitrary changes can have unwanted consequences, such as switching between 32-bit and 64-bit mode. A correct MIPS implementation of code to enable or disable interrupts must be able to write to the bit controlling 64-bit mode, but must not change it.

Since we do not prohibit writes entirely, in theory, the synthesizer can generate programs that change registers in arbitrary ways and then restore their initial value. In practice, this is not an issue, because our synthesis technique preferentially produces smaller programs, excluding programs with redundant operations. Another potential problem is that the synthesizer is obliged to waste time considering and ruling out programs that make unwanted changes. We address this in the implementation by gating registers (Section 6.3.2) that are irrelevant to the specification; this removes them entirely from consideration.

Limitations of Alewife. Alewife specifications are based on the premise that the machine-dependent code in an OS is made up of machine-dependent instantiations of machine-independent constructs; this allows the bulk of the specification to be machine-independent with relatively minor parts substituted on a per-machine basis. In practice, this is largely, but not entirely, true. Some machine-dependent code in OSs is not just machine-dependent but machine-specific: it handles concepts that do not exist on other machines, e.g., segment tables on x86. These concepts primarily arise in code that is called directly by the machine (such as trap handlers and the kernel startup code) rather than by the machine-independent part of the OS. It is possible to specify such code in Alewife, but only in a degenerate form, where the entire specification is abstracted into a single pre- and postcondition pair in the lowering file.

Register Model.

Registers in Cassiopea have types of the form \(\mathit {C}\ \texttt {reg}\), which indicates that a register can hold \(\mathit {C}\)-bit values (line 4). Registers are first-class values and can be passed as arguments to functions and operations. Each register has the text form used in the machine’s assembly language associated with it. The synthesis engine uses this to produce the synthesized assembly code; it allows working with non-identifier register names, such as \%eax on x86.

Memory Model.

Cassiopea uses the same “swiss-cheese” memory model as Alewife does (described in Section 3). However, unlike Alewife, Cassiopea memory regions, \(\mathit {x_{mem}}\), have finite, statically known lengths. Unbounded or variable-length memory regions do not typically appear in assembly-language machine-dependent OS components. Cassiopea memory regions have types of the form \(\mathit {C}_1\ \mathtt {bit}\ \mathit {C}_2\ \mathtt {len}\ \mathit {C}_3\ \texttt {ref}\), where \(\mathit {C}_1\), \(\mathit {C}_2\), and \(\mathit {C}_3\) must be concrete constants. As in Alewife, labels have an access type that indicates whether references should be position-independent; instruction definitions that use labels can query or assert about the access type so that the synthesis engine produces the appropriate code. Note that most memory regions appear in Alewife specifications and not in machine descriptions: we provide a programmer’s view of the machine, so the memory regions available are the ones associated with the code at hand and not the machine’s entire memory space.

Bitvectors and Pointers.

In a typical ISA, all values are bitvectors and can be used by any operation. In contrast, as in typed assembly language [Morrisett et al. 1999] and the Compcert backend [Leroy 2009], Cassiopea distinguishes between finite bitvector constants and pointers into memory regions. The distinction is not statically checked, however; the type \(\mathit {C}\ \mathtt {bit}\) includes both \(\mathit {C}\)-length bitvectors and pointers into memory regions of type \(\mathit {C}_1\ \mathtt {bit}\ \mathit {C}_2\ \mathtt {len}\ \mathit {C}\ \texttt {ref}\). It is a runtime error to apply bitvector operations to pointer values and vice versa, though we overload some operations to allow limited pointer arithmetic. We deliberately omit the ability to convert between pointer values and bitvectors, since we do not model absolute memory addresses. This model simplifies reasoning about the semantics of programs, since they cannot create pointers to arbitrary regions. It is also a runtime error to make unaligned or out-of-bounds accesses to memory.

Machine State.

All machine state is either registers or memory. Such a state is global in scope and declared using letstate. Registers and memory can contain only bitvectors and pointers. Cassiopea code can manipulate integers, booleans, and registers to define instruction semantics, but these values cannot be stored directly in the machine state.

We refer to the state of a machine \(\mathbf {M}\) with the notation \(\Sigma _\mathbf {M}\), which is a pair \((\rho , \sigma)\). \(\rho\) is a map from registers to values of bitvector type, and \(\sigma\) is a map from pointers to values of bitvector type.

Our example in Figure 5 declares several pieces of machine state. The general-purpose register r0 for both MIPS and ARM appears on line 6. Its assembly output text is specified by binding r0.txt, which appears on line 11 in Figure 5(A) and line 12 in Figure 5(B). We also show one control register for each machine: cp0_12_ie in MIPS (line 9 in Figure 5(A)) and the Z flag in ARM (line 9 in Figure 5(B)). (Control registers vary widely across machines.) There are no memory regions in the example because, as discussed previously, memory regions normally arise in program specifications and not in the machine model itself (see Figure 4, line 8).

Operations and Programs.

Machine state in Cassiopea is manipulated by operations. These are typically a single assembly instruction but may represent a group of instruction variants and/or a short sequence. In the examples, lines 15–29 and 30–38 of Figure 5(A) and lines 15–26 and 27–38 of Figure 5(B) define operations with defop.

Each operation definition has two parts: txt is an expression that constructs the assembly text representation of the operation, and sem is a Cassiopea statement defining the operation’s full concrete semantics in terms of the machine state. In the definition, most operations check the validity of each operand first. The MIPS instructions shown are SLTU (unsigned set less than) and LW (load word). The ARM instructions shown are MOV_imm (move immediate to register) and LDR_imm (load with immediate value offset).

Borrowing from JitSynth [Van Geffen et al. 2020], an operation is a pair \((op, \mathbf {T})\), where op is an opcode, and \(\mathbf {T}\) is a map from argument name to type, which can include registers, booleans, concrete bitvectors, and labels. (When used as an argument to an instruction that accepts labels, a label provides a pointer to the first entry in its memory region.) Each operation defines a set of instructions \((op, \mathbf {v})\) where \(\mathbf {v}\) is a map from argument name to value, where for each argument x, \(\mathbf {v}(x)\) is of type \(\mathbf {T}(x)\). For a machine \(\mathbf {M}\), we denote its set of instructions as \(\mathcal {I}_\mathbf {M}\).

Cassiopea machine descriptions define the semantics of instruction as a partial function (partial due to the possibility of runtime errors) from a machine state to a new machine state accompanied by a branching state: \(\begin{align*} [\![ (op, \mathbf {v}) ]\!] _\mathbf {M} : \sum _\mathbf {M} \rightharpoonup \sum _\mathbf {M} \times \left(\mathbb {N} \cup \lbrace \cdot , \mathtt {ext}\rbrace \right) \end{align*}\) The branching state indicates the destination of a branch instruction. Operations in Cassiopea may only branch forward, so the branching state indicates that execution should proceed with either the next instruction (\(\cdot\)), an external assembler label (\(\mathtt {ext}\)), or the instruction after skipping n instructions forward (\(\mathbb {N}\)) (where n should be at least 1).

A program is a series of instructions. We define the result of running a program P (a list of instructions) on a machine state \((\rho , \sigma) \in \Sigma _\mathbf {M}\) using a partial function \(run_\mathbf {M} : \mathcal {P}_\mathbf {M} \times \Sigma _\mathbf {M} \rightharpoonup \Sigma _\mathbf {M} \times bool\) where \(\mathcal {P}_\mathbf {M}\) is the set of programs for machine \(\mathbf {M}\) and the result includes a boolean representing the branchto value, indicating whether the program jumped to the special external assembler label. \(\begin{align*} run_\mathbf {M}(P, (\rho , \sigma)) = {\left\lbrace \begin{array}{ll} (\rho , \sigma , false) & P = nil \\ (\rho ^{\prime }, \sigma ^{\prime }, true) & [\![ head(P) ]\!] _\mathbf {M}(\rho , \sigma) = (\rho ^{\prime }, \sigma ^{\prime }, \mathtt {ext}) \\ run(drop(P, 1), (\rho ^{\prime }, \sigma ^{\prime })) & [\![ head(P) ]\!] _\mathbf {M}(\rho , \sigma) = (\rho ^{\prime }, \sigma ^{\prime }, \cdot) \\ run(drop(P, n), (\rho ^{\prime }, \sigma ^{\prime })) & [\![ head(P) ]\!] _\mathbf {M}(\rho , \sigma) = (\rho ^{\prime }, \sigma ^{\prime }, n) \wedge n \le len(P) \\ \bot & [\![ head(P) ]\!] _\mathbf {M}(\rho , \sigma) = \bot \\ \bot & [\![ head(P) ]\!] _\mathbf {M}(\rho , \sigma) = (\rho ^{\prime }, \sigma ^{\prime }, n) \wedge n \gt len(P) \\ \end{array}\right.} \end{align*}\) The function \(head(\ell)\) is the first element of a list \(\ell\), \(drop(\ell , n)\) is the tail of the list \(\ell\) after removing n elements, and \(len(\ell)\) is the length of the list \(\ell\).

Other Elements.

Cassiopea files may define type aliases, values, functions, and procedures and use them in the definitions of operations. (Functions are pure; procedures may alter machine state.) Both the MIPS and ARM descriptions define word as a type of 32 bits (line 3) and register as the type of 32-bit registers (line 4). The value wordsize, discussed in Section 3, is also specified as 32 on both 32-bit MIPS and 32-bit ARMv7 (line 2) and 64 for x86_64 (not shown). Function valid_gpreg checks whether the given operand is a general purpose register (line 21–23 in Figure 5(A) and line 22 in Figure 5(B)). This prevents generating code that tries to use special registers or control registers that happen to be the same size as general-purpose registers and thus have the correct type to pass as operands. LW in MIPS uses a function sign_extend (line 37 in Figure 5(A), definition not shown), which implements sign extension on bitvectors. LDR_imm in ARM uses a function zero_extend (line 36 in Figure 5(B)), which implements (unsigned) zero-extension. Common functions and procedures, such as those used for bitvector manipulation, can be defined in separate files and reused by inclusion in different machine descriptions.

It is also possible to define machine invariants. These are predicates that must hold true before and after block execution. The invariant statement in line 13 in Figure 5(A) declares that the value in register r0 is always 0.

Execution Model.

Cassiopea is not Turing-complete; machine models are finite-state and evaluation of Cassiopea functions, procedures, and operations always terminates. We deliberately restrict Cassiopea’s ability to model control flow: Cassiopea operations may only branch forward, so assembly snippets modeled in Cassiopea are loop-free. The semantics of Cassiopea do not include clocks and timers, concurrency, hazards, or weak memory models. The minimalistic design of Cassiopea allows symbolic execution to generate complete logical descriptions of our models and helps to simplify synthesis. We show in Section 7 that Cassiopea remains sufficiently expressive to support assembly synthesis for many OS components.

Because Cassiopea models ISAs at the assembler level, Cassiopea models need not be wire- or bit-level accurate. Our goal is to generate code to be assembled and linked into an (existing) OS, using that OS’s compiler and toolchain. Thus, Cassiopea descriptions need not capture phenomena hidden by the assembler (e.g., branch delay slots on MIPS). Moreover, machine descriptions need to contain only those parts necessary to synthesize targeted machine-dependent OS components; a surprising finding of this work is how little of an ISA needs to be specified to synthesize significant parts of an OS. Although we anticipate a world where vendors provide descriptions of ISA semantics, we currently write Cassiopea machine descriptions manually.

6.3.1 Read/Write Constraints.

We add constraints to restrict the registers that an operation is allowed to read, based on the specification and preceding operations. Specifically, an operation may read only those registers either mentioned by the specification (including frame conditions) or written by preceding operations. We call these available registers. For each operation, we add constraints to ensure that any registers it reads are contained in the available register set.

We note that in some machines, operations may read some registers (e.g., control registers) implicitly. We annotate these registers with the control keyword (as shown in Figure 5) and include them in the set of available registers for each operation.

Intuitively, registers not in the available register set contain arbitrary values, since they are neither constrained by the specification nor defined by preceding operations. As such, we expect that they should not be read in candidate programs.

6.3.2 State Gating.

State gating removes registers and operations that are not needed to produce a correct implementation for a machine-dependent specification. If a register is not mentioned in a precondition, postcondition, or frame condition of a specification, it contains an arbitrary value that is not restricted by the specification, and we consider it irrelevant. A register not mentioned in the postcondition or in a frame condition may not be modified by a correct implementation; registers that are additionally not mentioned in the precondition also do not contain information that needs to be read.

We cannot delete all unnecessary registers immediately, because assembly instructions often access registers implicitly; for example, many instructions in 32-bit ARM have conditional versions that access flag bits in the control register. We analyze the machine description to find the registers that operations can access together with relevant registers and add these to the set of registers that should be retained. We forbid read/write access to all other registers by removing them from the machine description. We additionally remove operations that require access to an irrelevant register, either explicitly or when all possible values for an operand are irrelevant.

6.3.3 Dependency Constraints.

We analyze the specification and machine description to discover dependency constraints to further prune the search space. Where a specification ensures that the final value of a location is uniquely determined by the initial state, we determine which values in the initial state affect it. We then require that guessed programs exhibit these dependencies, i.e., the computation of the final value does indeed depend on the relevant parts of the initial state.

We find locations \(\ell\) that are uniquely determined by the initial state by querying whether there exists an initial state for which the postcondition holds for two distinct values in \(\ell\): \(\begin{align*} \exists \sigma , \sigma ^{\prime }, \sigma ^{\prime \prime }\ .\ \text{pre}(\sigma) \wedge \text{post}(\sigma , \sigma ^{\prime }) \wedge \text{post}(\sigma , \sigma ^{\prime \prime }) \wedge \sigma ^{\prime }[\ell ] \ne \sigma ^{\prime \prime }[\ell ] \end{align*}\) If this query is UNSAT, then for any initial state, the final value in the location is uniquely determined.

For such a location \(\ell\), we then perform a series of SMT queries to identify on which universally quantified variables in the precondition the final value of \(\ell\) depends. Specifically, for each variable x in the precondition, we ask whether there exists an initial state \(\sigma\) and distinct values \(v_1\) and \(v_2\) such that \(\sigma [x \mapsto v_1]\) and \(\sigma [x \mapsto v_2]\) produce two different correct values for location \(\ell\): \(\begin{align*} \exists \sigma , \sigma ^{\prime }, \sigma ^{\prime \prime }, v_1, v_2\ .\ &\text{pre}(\sigma [x \mapsto v_1]) \wedge \text{pre}(\sigma [x \mapsto v_2]) \\ \wedge \ &\text{post}(\sigma [x \mapsto v_1], \sigma ^{\prime }) \wedge \text{post}(\sigma [x \mapsto v_2], \sigma ^{\prime \prime }) \\ \wedge \ &\sigma ^{\prime }[\ell ] \ne \sigma ^{\prime \prime }[\ell ] \end{align*}\) If this query is SAT, then \(\ell\) depends on x.

We add constraints to ensure that guessed programs exhibit these dependencies; we analyze the symbolic program to compute an assertion on control variables that ensures that variable x is used in the computation of location \(\ell\).⁸ Intuitively, these assertions are effective in accelerating guessing, because they enable the solver to quickly reject programs that do not exhibit the appropriate dependencies and, therefore, cannot possibly be correct.

6.3.4 Rule-based Decomposition.

Our synthesis engine augments syntax-guided synthesis with a heuristic rule-based decomposition algorithm to achieve performance and scalability. Rule-based decomposition uses a set of machine-independent decomposition rules that decompose a specification into specifications for smaller subprograms (“subgoals”). Our algorithm combines decomposition and syntax-guided synthesis in an iterative scheme, alternately using rules to decompose subgoals and using pure syntax-guided synthesis to discharge subgoals. The procedure is described in Algorithm 1.

Rule-based decomposition allows us to improve performance over syntax-guided synthesis. Syntax-guided synthesis scales poorly with increasing program length; decomposing the specification into subgoals for smaller programs reduces the size of each syntax-guided synthesis invocation, significantly accelerating synthesis overall. Meanwhile, using syntax-guided synthesis as a final code generation stage allows our rules to remain machine-independent.

Search Algorithm. During synthesis, our synthesis engine performs a search over possible trees of rule applications to the input specification instance, maintaining a set of trees encountered (S in Algorithm 1). Each tree T corresponds to one possible subdivision of the specification into subgoals; each subgoal has an instruction count n, which is an upper bound on the number of instructions that will be used to satisfy the subgoal. In each iteration, the synthesis engine selects a tree from this set and a subgoal from the tree and invokes syntax-guided synthesis up to n instructions to try to discharge the subgoal (line 10). The synthesis engine selects the next tree to attempt according to a cost heuristic (TakeBest); our heuristic scores a tree by the lengths of its remaining subgoals, weighting each subgoal exponentially in its length.

If syntax-guided synthesis fails on a subgoal, our synthesis engine attempts to decompose the subgoal by applying each rule (Decompose, line 15). Each new tree obtained is added to the set (line 17). The synthesis engine also retains the original tree, increasing the subgoal instruction count to \(n+1\) for later exploration (line 19). If syntax-guided synthesis succeeds, the synthesis engine stores the partially discharged tree and continues (lines 11–13). If the synthesis engine discharges a tree’s last remaining subgoal, it combines the results to produce a program that is correct with respect to the original goal (line 7).

Rule Selection. Our implementation of rule-based decomposition includes five rules. All of our rules are specific instances of sequential composition; they generate subgoals such that \(\text{post}(g_i) = \text{pre}(g_{i + 1})\). As such, subprograms that satisfy the generated subgoals may be composed by sequence to produce a correct program for the input goal.

We base our rule selection on observations of common properties of OS assembly code and assembly languages. First, OS assembly code typically performs simple calculations and otherwise serves only to move or set state. Often, these moves and sets are performed by independent program fragments. Second, many assembly languages support arithmetic over only a subset of their registers; a significant fraction of assembly programs is dedicated to moving values for calculations then storing the results. We use rules that generate (1) independent subgoals for programs to satisfy independent pieces of state and (2) subgoals that move data to and from general-purpose registers. Due to our choice of rules, our algorithm does not speed up synthesis for programs that mainly perform arithmetic.

Our rules are nondeterministic: more than one rule may be applicable to a specification, and one rule may apply in several ways. For instance, SetReg may apply to several registers in a specification. Our rules are not, in general, invertible [Liang and Miller 2009]. Applying an invertible rule to a derivable goal will produce only derivable subgoals. Applying non-invertible rules may require backtracking. Our rules are also incomplete: it is possible that no rule applies to a given specification instance, in which case our synthesis engine regresses to normal syntax-guided synthesis. However, our rules are sound: if synthesis succeeds on the generated subgoals, then the resulting program is correct against the input specification instance.

Separation Logic. Internally, we use a separation-logic-like representation of the specification, inspired by SuSLik’s [Polikarpova and Sergey 2019] use of separation logic to represent synthesis goals for imperative heap-manipulating programs. This allows our rules to structurally decompose specifications by simple pattern-matching.

swi-handler (SWI).

This is the machine-level system call trap from the ARMv7 implementation. “SWI” stands for “software interrupt”, which is ARM terminology for a system call trap. From our machine-independent specifications, we generate comparable system call handlers for MIPS, RISC-V, and x86_64. There are 13 synthesis blocks, of which two are empty on ARM but were necessary for one or more of the other machines.

cpu-start (CS).

This is the entry point for application-core kernels⁹ from the ARMv7 port. It consists of two parts. The first part is considered as a synthesis block:

The second part is the same as the initstack block from the swi-handler example (SWI-12), so we reuse the same Alewife specification for this part and do not count it as an extra synthesis block for the evaluation.

setjmp (SJ).

This is the C standard library function setjmp. It stores callee-saved registers and the stack pointer and returns 0. It is composed of two blocks:

longjmp (LJ).

This is the C standard library function longjmp. It reloads the registers saved by setjmp and and arranges to return a caller-supplied value from the setjmp call. It is composed of two blocks:

crt0 (CRT).

This is the startup code (crt0) for user-level programs. It contains seven synthesis blocks:

syscallstub (SYS).

This is a user-level system call stub. It has three synthesis blocks:

cpu-irqoff (IRQ).

This procedure turns interrupts off for the current processor. It is just one block:

(Turning interrupts on is effectively the same and omitted for brevity. A related function for idling the processor consists mostly of interrupt state manipulation, along with a special instruction for idling that we do not attempt to synthesize, and is also omitted.)

thread-switch (TS).

This is a complete kernel-level thread switch; it saves the state of the current thread and restores the state of the next thread to run. It consists of six blocks:

ARM.

The 32-bit ARM model has three-operand instructions, 16 registers, and a status register. We do not include Thumb instructions, the 16-bit variant of the ARM ISA. Most ARM instructions are all conditionally executed based on the flags in the status register. We model the status register as multiple smaller register fields, as direct access to the entire status register is rare in ARM code. In ARM, many immediate values are represented as an 8-bit field rotated right by an even 4-bit shift amount between 0 and 30. We model this directly and thus emit only valid immediates. This is necessary because the ARM assembler will not emit extra instructions to encode impossible immediates. We do not include multiple data transfer instructions such as LDM/STM, since they can always be replaced by multiple single load/store and arithmetic instructions.

MIPS.

Our MIPS model has three-operand instructions and 32 general-purpose registers. Most kernel-mode phenomena are handled by control registers, which are composed of fixed-size fields; we model each field separately in Cassiopea and concatenate the fields together when accessed as a register. In MIPS, general-purpose register 0 is always zero, and writes to it are discarded. We handle this by treating register 0 as special in every instruction and adding a machine invariant to the Cassiopea machine description (see Figure 5(A)). We handle the branch delay slots associated with jumps by using the assembler mode that hides branch delay slots.

RISC-V.

Our 32-bit RISC-V model has three-operand instructions, 32 general-purpose registers, and a supervisor-mode status register similar to that of MIPS. We again model the status register by separating it into fixed-size fields and concatenating them together when accessing it as a whole. As in MIPS, general-purpose register 0 is always zero, and we encode this as a machine invariant.

x86_64.

We modeled x86_64 with AT&T syntax [Narayan 2007]. Our x86_64 model has two-operand instructions, 16 registers, and a flags register interrogated by certain branch instructions. We model the flags register as separate 1-bit registers.

Completeness.

We implemented 34 operations in ARM, 37 in MIPS, 37 in RISC-V, and 56 in x86_64. All models include assembly operations for arithmetic, bitwise logic and shifts, comparison, moves, memory accesses, conditional branching, and supervisor operations. This is a small fraction of the total instructions available on each machine (especially x86_64) but covers all the basic operations. Each machine model also includes all the general-purpose registers, the basic processor flags on machines that have them, and a selection of control registers as needed for our use cases. Table 1 shows line, operation, and register counts for each machine model.

Shortened Machine Descriptions.

Because including the full complement of general-purpose registers makes even the simplest synthesis problems extremely slow in the absence of state gating, for each machine we prepared a single alternate description with most of the general-purpose registers commented out, retaining only 6–8 of the most commonly used ones. We use this shorter description for all the use cases it can support, that is, those that do not require the registers it comments out. The blocks that use the full descriptions are

This trimming reflects what one might readily do by hand in the absence of state gating. (It is, indeed, what we did by hand before we had state gating.) Note that this change is strictly adverse to our evaluation, in that it makes our baseline considerably more performant.

Verification.

Table 2 reports the verification performance of our synthesis engine on all use cases. We verified all machine-independent Alewife specifications against the hand-written assembly programs, which are taken from existing implementations, to support the validity of our specifications. In most cases, the synthesis engine verifies both our hand-written programs and the synthesized implementations in milliseconds. We are able to verify the whole of thread-switch (TS), our longest hand-written program at 26 instructions, in less than one second. During synthesis, our synthesis engine uses verification as part of the CEGIS loop; because guessing is much slower than verification, this occupies only a small fraction of the total synthesis time, often \(\lt\)1%.

Synthesis.

Synthesis in general is difficult, and synthesis of assembly is particularly hard. The size of the space of possible programs is combinatorial in the number of registers, memory locations, and immediate values, and exponential in the number of instructions [Hu et al. 2019]. This especially affects the performance of syntax-guided synthesis. As a first-order approximation, in our machine descriptions, the overall sizes of the search spaces for programs of length n are \(2^{40.3n}\) in ARM, \(2^{36.6n}\) in MIPS, \(2^{36.3n}\) in RISC-V, and \(2^{74.7n}\) in x86_64.

Table 2 summarizes the synthesis performance of our synthesis engine on all machine-independent specifications with all optimizations enabled. We ran the experiments with a half-hour timeout; no cases timed out. Our synthesis times vary widely with architecture and machine-independent specification. Examining these use cases more closely, we see that SWI-1 is a register spill, requiring a series of stores followed by a subtraction that sets the stack pointer appropriately: each instruction is relatively independent and no value in the final state requires multiple arithmetic operations to calculate. In contrast, SWI-5 loads a value from memory then uses it to perform a conditional branch; this requires that the solver reason about conditional execution and arithmetic to produce a correct program. This leads to entirely different synthesis times under each of the four architectures, especially for ARM and RISC-V. Note that our synthesis engine discharges all two-instruction machine-independent specifications in less than ten seconds.

ISA Instruction Selection.

One critical issue is the level of completeness of the ISA description. A more complete description could enable the synthesis of more OS components; on the other hand, including more instructions negatively impacts the synthesis performance and the ease of writing machine descriptions. Fortunately for the latter, expressiveness does not require the ISA description to include most of the available instructions. For example, the x86 architecture contains many instructions that are not necessary for full expressiveness, such as the specialized vector operations in the 64-bit version. Excluding these reduced the work required for us to produce ISA descriptions, although we expect that manufacturer-supplied ISA descriptions would be relatively more complete.

Using only a sufficiently expressive ISA description additionally helps with synthesis performance. This gives a reasonably sized search space to allow the synthesis engine to create an initial runnable program. Once we have a runnable program, we can apply superoptimization [Schkufza et al. 2013] or standard compiler techniques [Debray et al. 2000] to obtain a more efficient program that uses a larger machine model.

Our expressiveness decisions were driven by our use case requirements. Consequently, as discussed in Section 7.2, we constructed our machine models to include at least the following general-purpose components:

We also include the full set of general-purpose registers for each machine and any special-purpose registers used by ordinary code, such as the flags word.

Beyond these, we include a selection of pertinent control registers and the instructions that manipulate them, as this is a common OS operation. In general, each block we synthesize needs access to conceptually similar pieces of machine state in each architecture.

What We do not Synthesize.

To strike the balance between the expressiveness and complexity of the languages, there are important pieces of OS code that we do not synthesize. We do not synthesize call and return instructions (nor do we synthesize system call instructions). Procedure calls are different from ordinary assembly instructions. There are two ways one could imagine synthesis interacting with procedure calls. The first way is to let the specification explicitly indicate what procedure to call. This is the approach we take; we generate the call and return instructions with other Aquarium tools [Holland 2020]. The second way is to make the specification more expressive about procedure calls and use synthesis to select a particular call from a set of choices. This is a higher-level synthesis task, which is orthogonal to our goal of synthesizing assembly language.

Furthermore, there are small portions of OS code that are not merely machine-dependent, but are machine-specific, which cannot be expressed in a machine-independent way. Well-known examples include the code to set up x86 segment tables and SPARC register window trap handling. A less well-known example that affects our use cases is that ARM exception handlers must manipulate exception-related processor modes that do not exist on other architectures.

Scalability of Assembly Synthesis.

Furthermore, scalability poses a serious challenge. Synthesis of assembly is particularly hard since the characteristics of assembly languages cause a combinatorial explosion in the number of possible instructions that must be considered [Hu et al. 2019]. This detrimentally affects the performance of syntax-guided synthesis.

This difficulty is a general feature of assembly languages. Even though our synthesis is parameterized on a Cassiopea machine description, an approach specialized for a single machine or a low-level intermediate language must still address the fundamental problem of search space size. Although our optimizations significantly reduce the search space, it is still quite easy to write specifications for which synthesis always times out.

Currently, using pure inductive synthesis, we can generate up to five (occasionally only four) instructions in a reasonable time; with our rule-based decomposition synthesis technique, we can synthesize programs with up to twelve instructions for certain well-structured specifications. Therefore, we expect to be able to handle most small pieces of assembly code; besides the assembly blocks demonstrated in our use cases, Alewife and Cassiopea can probably also handle frame push and pop operations, stack handling, and simple bit manipulations without further extension. Although this is sufficient for many machine-dependent OS components, some require significantly longer implementations. For example, the MIPS general exception handler in NetBSD 9 is about 100 instructions. For these our methodology of decomposition into steps becomes critical.

Ultimately, while blocks of four or five instructions are small, they are still useful, since other tools in our ecosystem allow composing them into larger chunks. For example, as discussed in Sections 7.1 and 8.3, the TS example is composed of six steps. Two of these we compile; the other four we synthesize. Those four are all one instruction each on most or all architectures. Yet combined, these six blocks are a complete kernel-level thread switch, similar to that found in any OS kernel. The setjmp (SJ) and longjmp (LJ) examples are similarly decomposed; combining the pieces gives the complete implementations. Other examples are a subject of ongoing research; this includes the crt0 (CRT) use cases.

Concurrency and Time.

Cassiopea and Alewife do not model concurrency or time. Reasoning about time typically involves temporal logics that are not SMT solvable. This is likely a fatal obstacle for working with real-time OSs (especially hard real-time), but for conventional systems, machine-dependent code handles time only when interacting with timer hardware. We have not addressed this issue in our current work; in future work, we plan to investigate whether the temporal aspects of timer control can be adequately abstracted away such that the low-level specifications (and thus code synthesis) can be expressed in Alewife.

We chose not to burden Cassiopea with support for reasoning about concurrent executions. Our use cases do not require concurrency support. This is representative of the majority of the machine-dependent part of an OS: most of it executes below the level where concurrent things happen. (For example, the thread switch code in our use cases executes on a single CPU, on CPU-private data, and with interrupts already disabled by higher-level machine-independent code; it itself need not reason about other CPUs, other threads running time-sliced on the same CPU, or about being interrupted.)

However, this means we cannot model instructions related to concurrent executions. The machine-independent code in a typical OS is written in terms of a small set of concurrency primitives. Producing these is part of generating a new port, but one we decided not to tackle in this work. Currently, they are provided by the porter as prewritten assembly blocks that can be composed with other blocks via other Aquarium tools. For a typical OS, this means implementations of spinlocks, a small set of atomic operations, and a small set of memory barriers. Note that all of these are also small blocks of assembly code and likely amenable to synthesis using other tools, though the specifications are nontrivial [Bornholt and Torlak 2017] and (particularly for memory barriers, which are always either zero or one instruction) likely to significantly outweigh the output code.

Performance.

Finally, we do not reason about the performance of synthesized code. Although the synthesis engine chooses the shortest sequence of instructions that meets a specification, this may not correlate to performance. We assume that optimization can be performed after synthesis and block composition. Furthermore, low-level OS code typically does not involve expensive computation. We discuss the related problem of synthesizing the fastest possible assembly program, or superoptimization [Massalin 1987], in Section 9.

SMT Encodings.

Before building our synthesis engine, we experimented with an assembly synthesizer written in Rosette [Torlak and Bodik 2014] and explored language designs and theory combinations. We found that combinations of integer and bitvector theories led to poor performance. We also experimented with using the theory of arrays for updates to registers and memory, but found it markedly slower and abandoned it in favor of a direct encoding.

Accumulation Algorithm.

Since our implementation of syntax-guided synthesis proceeds in stages, we experimented with an accumulation algorithm. In general, in stage n, we attempt to synthesize an n-operation program. Starting at stage 0 (which succeeds only if the specification is vacuous), our synthesis engine proceeds to stage \(n+1\) when synthesis at stage n fails, iterating until synthesis succeeds or times out. The accumulation method attempts to reuse work done at stage n in later stages. Specifically, in a later stage \(n+k\) we use the last guessed program from stage n as the initial n operations, and attempt to synthesize only the last k operations. Intuitively, the n-operation program might be “almost correct,” since it avoids many generated counterexamples. Accumulation accelerates synthesis when the final candidate guessed during synthesis for length n is a prefix of a correct program. Trying to synthesize k operations is typically much faster than synthesizing \(n+k\) operations, so accumulation could be worthwhile and relatively cheap. If none of the accumulated program prefixes can be extended to a correct program, stage \(n+k\) proceeds to attempt to synthesize all \(n+k\) operations. When we evaluated the effectiveness of accumulation we found that it can help, but infrequently. When it does help, it can result in significant improvements, making syntax-guided synthesis up to \(7\times\) faster on a couple of our use cases. However, in the worst case, accumulation caused synthesis to take twice as long.

Instruction Dependency Graph.

We experimented with adding constraints to require specific dependencies between instructions, for example, requiring the locations read by the third instruction to intersect with the locations written by the first instruction. In essence, this enforces a given dependence graph over instructions in a block. Although this can significantly reduce synthesis times, we could not find suitable heuristics for identifying appropriate dependencies, since implementations of the same block on different machines often require different dependency graphs.

Multiple Counterexamples per Loop.

We experimented with collecting multiple counterexamples per CEGIS loop iteration, instead of the standard single counterexample per loop. We analyzed the effect on the total number of CEGIS iterations and the synthesis time. Although additional counterexamples consistently reduced the number of iterations, we found it difficult to determine an effect on overall synthesis time. We also tried retaining counterexamples across stages as part of our accumulation approach. This also led to fewer iterations but sometimes longer synthesis times. Ultimately, we found that additional counterexamples increased both the variance and average of the total synthesis time.

Candidate Buckets.

Due to the high time cost of generating program candidates with multiple counterexamples, we also experimented with grouping candidates across CEGIS iterations into several candidate buckets and generating counterexamples that worked for all candidates in a bucket. This method led to less synthesis time for one CEGIS iteration but more iterations in total for some use cases. The total synthesis time tended to increase overall.

Interactive Assembly Synthesis.

Assuage [Hu et al. 2021], based on our synthesis engine, presents a parallel interactive assembly synthesizer that engages the user as an active collaborator. Users, who are familiar with the high-level concepts of assembly languages, provide multiple types of guidance during synthesis, while the synthesizer provides users with different representations of progress feedback. Assuage enables synthesis to scale beyond current limits.

Guaranteed Correctness can Improve Security.

The machine-dependent parts of an OS rarely implement policy; they translate policy decisions into hardware implementations. In this sense, a correct implementation does enforce certain security properties, and a verified implementation does provide some extra security assurance. However, in general, one must also verify that the machine-independent code invokes the machine-dependent operations at the correct points, which is a much larger issue we do not attempt to address. Also, note that many of the possible errors in low-level code do not have subtle consequences: the system hangs or crashes, or violently corrupts memory. Identifying the source of such problems can be extremely expensive, and verification can save much debugging time; however, identifying their existence is typically less challenging, so they are relatively unlikely to survive long enough to become vulnerabilities in the field.

For example, machine-dependent code must properly update page tables. Failure to perform such operations correctly, such as setting the wrong page permissions or using the wrong address-space ID, can create security vulnerabilities. However, verifying the page table updates will not protect against the machine-independent virtual memory system failing to revoke access permissions at the proper times. Correspondingly, setting the wrong page permissions will in general result in denying accesses that should succeed, which will cause programs (or the system) to crash, which in turn is relatively unlikely to be missed during development.

Furthermore, incorporating security-related restrictions into synthesis is an interesting direction for future investigation. Integrating them with the specification or even adding as extra constraints can, in general, allow rejecting vulnerable assembly programs during synthesis, which would provide further security guarantees.

Synthesis is not a Security Panacea.

There is a large class of security bugs that arise when microarchitectural implementation details leak through to the instruction level. Spectre and Meltdown [Hill et al. 2019], and Rowhammer [Mutlu and Kim 2020] are, perhaps, the most well-known of such attacks. Synthesis and verification do nothing to address such issues. Cassiopea specifications describe the instruction set architecture; nothing in the Aquarium ecosystem is aware of microarchitectural implementation details, so there is no way to reason about any unwanted effects that might arise. However, given rules for mitigating such vulnerabilities, we expect to be able to synthesize code that adheres to those rules. Furthermore, as always, verification against a specification is only as good as the correctness of the specification.

Program Synthesis.

Modern program synthesis began in 2006 with the introduction of Sketch [Solar-Lezama et al. 2006], in which a programmer provides a partial program and specifications for “holes” in the program, and Sketch fills in the holes. Following this work, CEGIS [Solar-Lezama 2008] generalizes sketching for infinite state programs. However, for infinite state programs, the verifier is typically an unsound, bounded model checker. Although we use CEGIS, we restrict ourselves to finite-state programs.

Another category of program synthesis, programming by example (PBE), takes input-output examples to demonstrate desired program behaviors [Singh and Gulwani 2015; Gulwani et al. 2017]. In the assembly programming context, examples that include concrete machine states are much more challenging to provide than formal specifications.

While the DSLs used in early CEGIS systems, e.g., [Solar-Lezama et al. 2005; Solar-Lezama et al. 2006], handle many of the same concepts as does Cassiopea (e.g., precise bit manipulation), the problem of synthesizing assembly code is significantly harder than that of synthesizing high-level languages. OS machine code manipulates only untyped memory and worse, all state is global. While programs in high-level languages contain these features, they are typically used parsimoniously. In contrast, untyped memory and global state are inherent to, and unavoidable in, assembly code. Consequently, assembly code synthesis has enormous search spaces that are exponential in program length and combinatorial in the number of instructions (at least the dozens), registers (also dozens), memory locations (possibly the hundreds or thousands if one considers kernel structures, such as page tables), and immediate values.

Superoptimization and Assembly Synthesis.

To the best of our knowledge, the first encoding of assembly language into SMT was the Stoke algorithm for stochastic superoptimization [Schkufza et al. 2013]. The superoptimization problem for machine code [Massalin 1987; Phothilimthana et al. 2016; Bansal and Aiken 2006] is: given a piece of machine code and an execution context, find the lowest cost semantically equivalent piece of code. Stoke formulates correctness and performance improvement into a cost function, then uses a Markov Chain Monte Carlo sampler to find an implementation that, with high probability, outperforms the original (already optimized by LLVM [Lattner and Adve 2004]). Superoptimizers work on straight-line, intraloop, and intraprocedural code.

Superoptimization avoids some challenges presented by the general synthesis problem: first, a superoptimizer can fail to optimize a snippet, since the original snippet can be used instead. In contrast, if Aquarium fails to synthesize a snippet, it is a showstopper. Second, superoptimization is bootstrapped by a correct snippet of code to be optimized; in contrast, we have only a declarative, machine-independent specification and must produce a working implementation. This rules out, for example, subdividing the problem by computing intermediate machine states to use as subgoals.

Srinivasan and Reps also consider the problem of synthesizing assembly programs from semantic specifications [Srinivasan and Reps 2015; Srinivasan et al. 2016; , 2017], developing several synthesis optimizations similar to ours. Like us, they use a divide-and-conquer scheme that attempts to find independent sub-specifications that can be solved separately. Whereas their algorithm divides specifications greedily, our rule-based decomposition (Section 6.3.4) divides lazily, when we find that a specification cannot be solved by a one-instruction program. We use an ordering heuristic to select the split that should be considered next. Their conquer phase exhaustively enumerates instruction opcode and register arguments, using CEGIS to solve immediate arguments. Using enumeration means that their conquer phase does not scale beyond two- or three-instruction programs, whereas our fully solver-based CEGIS can synthesize certain sequences up to nine instructions long. Their footprint-based pruning approach can be compared to our read/write constraints. Their bits-lost pruner is similar to our dependency constraints (Section 6.3.3) in that it prunes program prefixes that discard necessary dependencies, but it employs finer-grained input tracking—at the level of bits rather than locations—and coarser availability tracking—at the level of whole program state rather than locations. Since their source code is not available, we cannot run a direct performance comparison.

Van Geffen et al. [2020] synthesize components of JIT compilers that produce sequences of assembly instructions, which correspond to instructions in kernel-level DSLs such as eBPF. They use a metasketch-based approach that optimizes synthesis using syntactic constraints on the output assembly programs. Their pre-load sketches load immediate values used by the rest of the program; our rule-based decomposition can do this in some cases, in particular when the program requires a value found at a label or in memory. Their read-write sketches constrain which instructions can be used depending on whether they access registers, memory, or both. This optimization can be compared to our read/write constraints and dependency constraints, which use assertions to restrict the search space according to a sound summary of instruction semantics. Our approach is more precise in that it can constrain instructions based on accesses to specific registers and memory locations as opposed to accesses to any register or any memory location.

Optimization in Synthesis.

Our dependency analysis represents one way to use abstraction to constrain search. Other works have found this general approach effective. In some sense CEGIS is such an approach; the abstraction it considers is the program behavior on a specific set of inputs. The Storyboard Programming [Singh and Solar-Lezama 2011] framework starts from sketches and synthesizes imperative programs that manipulate data structures using specifications that constrain the desired abstract behavior.

Cosette [Chu et al. 2017; Wang et al. 2018] searches for input tables that distinguish between two SQL queries by causing them to produce different outputs. To accelerate search, Cosette constrains input tables to contain only those tuples that can possibly affect the query output. Cosette finds these constraints by using the abstract semantics of SQL to obtain provenance predicates representing facts about input tuples that could pass through a query. Provenance predicates resemble our dependency analysis inasmuch as they are constructed by following dependencies of output on input; Cosette uses the abstract semantics of SQL to make provenance predicate discovery tractable. Our approach differs in that we reduce a program search space by introducing constraints on program abstract behavior.

Much like our Cassiopea DSL is an executable encoding of instruction semantics, Vale [Bond et al. 2017] encodes the semantics of each assembly instruction as a snippet of Dafny [Leino 2010]. While Vale enables verification of assembly snippets using Dafny’s pre- and postconditions, we use Alewife, a purpose-built DSL for specifications. Vale does not enable synthesis. An interesting avenue for future work would be to extend our synthesis work to the domain of cryptographic functions with Vale’s use cases.

Synthesis for OSs.

In the late 1980s and early 1990s, several groups experimented with OS customization [Bershad et al. 1995; Endo et al. 1996; Engler et al. 1995], performance optimization [Liedtke 1995], and specializing code to improve performance [Mosberger and Peterson 1996; Pu et al. 1988]. The specialization approach produced two interesting OS synthesis projects: The Synthesis Kernel [Pu et al. 1988] and Scout [Mosberger and Peterson 1996], both of which were based on the observation that OSes must handle all cases, although the vast majority of the time they are executing specific cases, where many of the decisions throughout a code path are determined a priori by system call parameter values. Creating versions of these code paths specialized to a given parameter improves performance. The Synthesis Kernel was custom-built to support this kind of synthesis. Scout took a similar approach, synthesizing fast-path implementations for network functionality.

The Synthesis Kernel and Scout both differ from Aquarium in two ways. First, they create customized code paths from existing general components, which differs from Aquarium’s synthesis using high-level, machine-independent specifications. Second, they perform runtime synthesis, relying on knowing specific parameter values. These approaches are orthogonal to ours; it is possible to combine such runtime approaches with modern program synthesis techniques.

More recently, Termite [Ryzhyk et al. 2009] and Termite-2 [Ryzhyk et al. 2014] synthesize device drivers. These use a different approach to synthesis (reactive synthesis rather than CEGIS) and synthesize to a C subset rather than assembly. More importantly, though, they concentrate on figuring out what to do, that is, what sequence of state changes to make, whereas our work concentrates primarily on figuring out how to make state changes, that is, the exact assembly instructions. One could imagine a system where something akin to Cassiopea figured out how to issue the device state changes directed by Termite-2, or where something akin to Termite-2 was used to figure out the specifications for the assembly code blocks Cassiopea generates. Thus this work is complementary to ours.