Dhall expressions for compiling Genode configuration XML
Add constrainPhys to Init/Start/Type
Simplify child routing function
Update Prelude

refs

master
browse log

clone

read-only
https://git.sr.ht/~ehmry/dhall-genode
read/write
git@git.sr.ht:~ehmry/dhall-genode

You can also use your local clone with git send-email.

Dhall expressions for Genode configurations

Motivation

Humans cannot be trusted to write XML correctly, yet a large corpus of hand-written Genode XML configuration can be found checked into Git. The proliferation of raw XML configuration in version control happens because once an example is given in raw XML, the intuitive way to write configuration is to copy XML in bulk and iteratively hand edit until parsing or runtime errors vanish.

The situation is made worse by adding configuration fallthroughs directly into Genode component runtime code. The init component is with the root of the trusted-computing-base but accepts <default-route/> and <any-service/> fallthroughs for critical system services because writing each route by hand would be impractical. As a safety measure the configuration of init requires redundant declarations of parent routes in the form of a <parent-provides/> header. Despite this, its not difficult to find unintended service routing in deployment.

The immediate solution to any bad abstraction is of course further abstraction. Luckily, the matter of configuration is abstract enough that raw XML can be uplifted to an intermediate representation that can be readily formalized and composed.

Dhall

Dhall is a configuration language with strict typing and purely functional semantics. The language is simple enough to guarantee that the evaluation of a configuration will halt, but is expressive enough to transform high-level configuration directly to raw XML text.

To begin with, compare the concept of Genode service route as expressed by XML and Dhall.

The XML snipplet:

<service name="…" label="…">
    [ <parent label="…"/> | <child name="…" label="…"/> ]
</service>

A Dhall record type of Service:

let Service = { name : Text, label : Optional Text }

{- All services have a name, some services are further qualified by label -}

A route may be expressed by a union of records:

let Route =
      < Parent :
          { label : Optional Text }
      | Child :
          { name : Text, label : Optional Text }
      >
{- Parent: some routes to the parent are re-labeled.
   Child: all childen are named, some are routes are re-labeled.
-}

And a route to a service may be expressed by a composition of these types:

let ServiceRoute = { service : Service, route : Route }

A Dhall interpreter type-checks expressions, which protects against simple spelling errors or malformed documents. In practice this check is part of application of functions.

A function to declare a route to a file-system service at the parent, matched by label:

let parentFs = \(fsLabel : Text) ->
      { service =
          { name = "File_system", label = Some fsLabel }
      , route =
          Route.Parent { label = Some fsLabel }
      }

This fuction applied as parentFs "foo" and the result transformed to XML (not described here, but a relatively simple transformation) would appear as such:

<service name="File_system" label="foo">
    <parent label="foo"/>
</service>

Is this not just fuctional programing performance art? Why program a configuration when the XML is easy enough to write? Consider the following:

<route>
    <service name="File_system" label="bin">
        <parent label="bin"/>
    </service>
    <service name="File_system" label="tmp">
        <parent label="tmp"/>
    </service>
    <service name="File_system" lable="secrets">
        <parent label="secrets"/>
    </service>
</route>

This hand-written configuration was accepted by an XML linter, but there is a minor spelling error. Requests not matching bin or tmp are routed to the parent with the label secrets. That is fine if the only additional service request for File_system is intended for secrets, but if the configuration is later used as a copy-paste template, there may be problems. Schema validation could fix this, but involves an even more miserable XML dialect, XSD.

Composing the parentFs and the standard List/map functions yields the correct configuration:

let fsRoutes = List/map Text ServiceRoute parentFs [ "bin" "tmp" "secrets" ]

{- List/map is applied to the list input type, list output type,
   transformation, and a list of values.
 -}

The important consideration is that the configuration is composable using functional programing. The aformentioned problem of ambiguous routing via wildcard routes can be solved programatically when compiling XML.

let mkParentRoute = λ(name : Text) ->  : ServiceRoute

let withDefaultRoutes =
        λ(serviceRoutes : List ServiceRoute)
       let defaultRoutes =
              [ mkParentRoute "PD"
              , mkParentRoute "CPU"
              , mkParentRoute "RM"
              , mkParentRoute "ROM"
              ]
        
        in  serviceRoutes # defaultRoutes
              {- catenate route lists -}

Components may also be accompanied by functions that generate routing configuration using typed argumens:

let composeRoutes =
        λ(Args : Type)
       λ(parse : Args  List Route)
       λ(args : Args)
       parse args

let TimerRoutesType = { irq : Route, ioMem : Route, ioPort : Route }
      {- A type specific to configuring the timer -}

let serviceRoute = λ(name : Text) -> λ(route : Route) ->  : ServiceRoute

let parseTimerRoutes =
        λ(routes : TimerRoutesType)
       [ serviceRoute "IRC" routes.irq
        , serviceRoute "IO_MEM" routes.ioMem
        , serviceRoute "IO_PORT" routes.ioPort
        ]
      {- A function for transforming the typed record to a list -}

let composeTimerRoutes = composeRoutes TimerRoutesType parseTimerRoutes
      {- Compose a routing configuration function specific to timer -}

let parentRoute =  : Route

let childRoute = λ(name : Text) ->  : Route

{---}

let commonRoutes =
      { irq = parentRoute
      , ioMem = parentRoute
      , ioPort = parentRoute
      }

let routesA = composeTimerRoutes
      commonRoutes

let routesB = composeTimerRoutes
      commonRoutes  { irq = childRoute "irq_trace" }
        {- override the standard irq route -}

Roadmap

The long-term goal is to compose Genode systems using as little raw XML as possible, while still parsing XML configurations at runtime for the sake of simplicity. Evaulating Dhall at runtime, and only a subset, is only possible by porting the Haskell engine or reimplementing Dhall in another language.

Expressing configuration in Dhall will be an iterative process starting from the highest configuration model down to the configuation of each component. To this aim the runtime files of depot_deploy and the configuration of init can be effectively expressed, the next step being utilities such as sequence, followed by the actual components.

Howto

How to render Dhall to XML and integrate into a deployment workflow is best described by example. Some familiarity with Dhall is required, the JSON tutorial is a good place to start: https://github.com/dhall-lang/dhall-lang/wiki/Getting-started%3A-Generate-JSON-or-YAML

Example expressions: - noux-system: https://git.sr.ht/~ehmry/genode-ehmry/tree/master/runtimes/noux-system/pkg.dhall