This document describes the folder structure generated by HAMR code generation for the seL4 Microkit platform with Rust component implementations. The generated code is placed in hamr/microkit/ under the project root (as specified by the --output-dir configuration).

Overall Project Layout

A HAMR project has two main areas: models and HAMR-generated output. When using SysMLv2, the conventional project structure is outlined below.

<project-root>/
  sysmlv2/                          # SysMLv2 model source
    aadl-lib/                       # HAMR/AADL library definitions (shared across projects)
      aadl.library/                 # Standard AADL property sets as SysMLv2
      hamr.aadl.library/            # HAMR-specific SysMLv2 definitions (e.g., HAMR.sysml, HAMR_AADL.sysml)
    <model-package>/                # Project-specific model files
      <Model>.sysml                 # Main model file (includes //@ HAMR: config comment)
  hamr/                             # HAMR code generation output (--output-dir target)
    microkit/                       # Platform-specific subfolder for Microkit target
      ...                           # (structure detailed below)

Generated Microkit Folder Structure

Legend:

  • [auto-gen] – Fully auto-generated by HAMR. Overwritten on every code generation run. Marked with // Do not edit this file as it will be overwritten if codegen is rerun.
  • [auto-gen]* – Auto-generated but contains BEGIN CONTENT MARKER / END CONTENT MARKER regions where developer content is preserved across re-generation.
  • [EDITABLE] – Generated once with skeletons/templates. Not overwritten on subsequent code generation runs. Marked with // This file will not be overwritten if codegen is rerun. Contains BEGIN MARKER / END MARKER regions that HAMR auto-updates (e.g., contracts, state variable declarations) while preserving developer code outside those regions.
hamr/microkit/
  Makefile                          # [auto-gen] Top-level Makefile (build, test, verus targets)
  system.mk                         # [auto-gen] Detailed build rules for all components
  microkit.system                   # [auto-gen*] Microkit system description XML (protection domains, memory regions, channels)
  microkit.schedule.xml             # [editable] Static cyclic schedule (domain time slots)
  microkit.dot                      # [auto-gen] Graphviz visualization of system architecture
  build/                            # Build output directory
    Makefile                        # [auto-gen] Copy of system.mk used during build
  components/                       # C bridge/infrastructure code for each thread component
    <component>/                    # One directory per thread component
      include/
        <component>.h               # [auto-gen] C header with type includes and declarations
      src/
        <component>.c               # [auto-gen] Main C seL4 entry points (init, notified) and port get/put implementations
        <component>_MON.c           # [auto-gen] Monitor (scheduling dispatcher) that relays pacer notifications
        <component>_user.c          # [auto-gen] C-to-Rust FFI bridge (calls into Rust extern "C" functions)
    pacer/                          # Special HAMR-generated scheduling component
      src/
        pacer.c                     # [auto-gen] Implements static cyclic scheduling via Microkit notifications
  crates/                           # Rust crates
    data/                           # [auto-gen] Shared data type definitions
      Cargo.toml
      rust-toolchain.toml
      src/
        lib.rs                      # [auto-gen] Crate root (re-exports modules)
        sb_event_counter.rs         # [auto-gen] Event counter types for port communication
        sb_microkit_types.rs        # [auto-gen] Microkit type aliases (e.g., microkit_channel)
        <PackageName>/              # Module per SysMLv2 package containing data definitions
          mod.rs                    # [auto-gen] Module declarations
          <DataType>.rs             # [auto-gen] Rust struct/enum for each model-level data type
    <component>/                    # One Rust crate per thread component
      Cargo.toml                    # [auto-gen] Crate manifest (dependencies: data, vstd, proptest, etc.)
      Cargo.lock                    # [auto-gen] Dependency lock file
      Makefile                      # [auto-gen] Crate-level build targets (build-release, test, verus)
      rust-toolchain.toml           # [auto-gen] Rust toolchain specification
      src/
        lib.rs                      # [auto-gen] Crate root: wires together modules, defines static app state and extern "C" entry points
        logging.rs                  # [auto-gen] Logging initialization
        bridge/                     # [auto-gen] HAMR-generated infrastructure code
          mod.rs                    # [auto-gen] Module declarations
          <component>_api.rs        # [auto-gen] Port API traits and Application_Api struct (get_/put_ methods with Verus contracts)
          extern_c_api.rs           # [auto-gen] Extern "C" declarations for port access (production uses Microkit shared memory; test uses Mutex-guarded statics)
          <component>_GUMBOX.rs     # [auto-gen] Executable (boolean function) versions of GUMBO contracts for testing/monitoring
        component/                  # Developer-editable application code
          mod.rs                    # [auto-gen] Module declarations
          <component>_app.rs        # [EDITABLE] Application logic: state struct, initialize and compute entry points
        test/                       # Test infrastructure
          mod.rs                    # [auto-gen] Module declarations
          tests.rs                  # [EDITABLE] Unit tests and property-based test configurations
          util/
            mod.rs                  # [auto-gen] Module declarations
            test_apis.rs            # [auto-gen] Test helper APIs: put_/get_ for ports and GUMBO state variables, PreStateContainer structs
            cb_apis.rs              # [auto-gen] Contract-based test harness: testInitializeCB, testComputeCB, testComputeCBwGSV, PropTest macros
            generators.rs           # [auto-gen] PropTest value generators for each data type (default and customizable strategies)
  types/                            # [auto-gen] Shared C type definitions for inter-component communication
    include/
      sb_types.h                    # [auto-gen] Master type include
      sb_aadl_types.h               # [auto-gen] C struct definitions for model data types
      sb_event_counter.h            # [auto-gen] Event counter type for port communication
      sb_queue_<Type>_<size>.h      # [auto-gen] Lock-free queue header for each data port connection type
    src/
      sb_queue_<Type>_<size>.c      # [auto-gen] Lock-free queue implementation for each data port connection type
  util/                             # [auto-gen] C utility code
    include/
      printf.h                      # [auto-gen] Printf header
      util.h                        # [auto-gen] Utility header
    src/
      printf.c                      # [auto-gen] Printf implementation for Microkit (serial output)
      util.c                        # [auto-gen] Utility functions

Key Files for Developers

The developer’s primary task is implementing application logic and writing tests. The key files to edit are:

Application Logic: crates/<component>/src/component/<component>_app.rs

This file contains the component’s application state and entry point methods. On initial generation it contains:

  • A struct for the component state, with GUMBO-declared state variables in BEGIN MARKER STATE VARS / END MARKER STATE VARS regions
  • A new() constructor with initial values in marker regions
  • An initialize() entry point skeleton with GUMBO-generated ensures contracts in marker regions
  • A timeTriggered() (periodic) or event handler (sporadic) entry point skeleton with GUMBO-generated requires/ensures contracts in marker regions
  • A notify() method for unhandled Microkit channel notifications
  • GUMBO-derived helper functions in BEGIN MARKER GUMBO METHODS / END MARKER GUMBO METHODS regions

The developer implements the bodies of initialize() and the compute entry point(s), using port API methods:

  • api.get_<port_name>() to read input port values
  • api.put_<port_name>(value) to write output port values

The developer may also need to struct and the associated constructor if any non-GUMBO declared local state is added.

Also, new logging functions in other helper methods may be added to support the coding of the entry point methods.

Tests: crates/<component>/src/test/tests.rs

This file contains unit tests. On initial generation it contains minimal skeleton tests. The developer writes one or more of the following:

  1. Manual unit tests – Directly construct inputs via test_apis::put_<port>(), invoke entry points, and check outputs via test_apis::get_<port>() with assertions.

  2. Manual GUMBOX (contract-based) tests – Directly construct inputs and call cb_apis::testComputeCB() or cb_apis::testComputeCBwGSV(), which automatically check pre/post conditions from GUMBO contracts. Returns a HarnessResult (Passed, RejectedPrecondition, or FailedPostcondition).

  3. Automated property-based GUMBOX tests – Use HAMR-generated macros (testInitializeCB_macro!, testComputeCB_macro!, testComputeCBwGSV_macro!) with PropTest to automatically generate random test vectors. The developer configures:

    • Number of test cases, rejection ratio, verbosity
    • Value generation strategies from generators.rs (default or custom ranges)

Schedule: microkit.schedule.xml

This file defines the static cyclic schedule. HAMR generates an initial candidate schedule, and the developer may adjust time slot allocations. Each <domain> entry specifies a scheduling domain and its execution time within the major frame.

Auto-Generated Infrastructure (Do Not Edit)

C Bridge Layer (components/)

For each thread component, HAMR generates C code that:

  • <component>.c – Implements the Microkit init() and notified() entry points. Manages port queues (enqueue/dequeue) via shared memory. Calls into Rust application code via extern “C” FFI.
  • <component>_MON.c – A monitor protection domain that receives pacer notifications and forwards them to the child component’s protection domain.
  • <component>_user.c – Thin C wrapper that calls the Rust extern “C” functions.

Rust Bridge Layer (crates/<component>/src/bridge/)

  • <component>_api.rs – Defines traits and the Application_Api struct that provide typed get_/put_ methods for ports. Initialize entry points only have Put_Api (no reading inputs). Compute entry points have Full_Api (both get and put). Port access methods include Verus contracts derived from GUMBO integration constraints.
  • extern_c_api.rs – Provides the actual port read/write implementations. In production (no_std), these call C functions via FFI. In test mode, these use Mutex<Option<T>> statics for isolated testing.
  • <component>_GUMBOX.rs – Executable (boolean function) versions of all GUMBO contracts: integration assumptions, initialize post-conditions, compute pre-conditions and post-conditions (including individual guarantee and case clauses). Used by the test harness for runtime checking.

Rust Test Infrastructure (crates/<component>/src/test/util/)

  • test_apis.rs – Provides put_/get_ functions for all ports and GUMBO state variables. Also defines PreStateContainer and PreStateContainer_wGSV structs for bundling test inputs.
  • cb_apis.rs – Contract-based test harness functions (testInitializeCB, testComputeCB, testComputeCBwGSV) and PropTest macros. These orchestrate: precondition check, port setup, entry point invocation, output retrieval, and postcondition check.
  • generators.rs – PropTest strategies for generating random values of each data type. Provides _default() strategies (full range) and _cust() strategies (parameterized ranges/biases).

Crate Root: lib.rs

Wires all modules together. Defines static mutable state for the component application instance and API objects. Exposes extern "C" functions (<component>_initialize, <component>_timeTriggered, <component>_notify) that are called from the C bridge layer. In test mode (#[cfg(test)]), includes the test module.

Shared Types (types/)

C header and source files implementing lock-free queues for inter-component communication via shared memory. One queue type is generated per unique data type/queue-size combination used in port connections.

Build System

  • Makefile – Top-level entry point with targets: all (build system image), test (run component tests), verus (run Verus verification), qemu (run on QEMU simulator), clean/clobber.
  • system.mk – Detailed build rules: compiles C components, invokes Rust crate builds, links ELF images, and runs the Microkit tool to produce the final system image.
  • microkit.system – Microkit XML system description defining protection domains (with nesting for MON/child pairs), shared memory regions for port connections, and notification channels for scheduling.
  • microkit.dot – Graphviz DOT file visualizing the protection domain hierarchy, shared memory mappings, and notification channels.