What would a monitor for rust look like?

[ivanperez-keera]

Copilot-generated C code connects to C systems in a very specific way:

• Inputs are passed as global variables.
• "Outputs", that is, monitors going off or property violations, are communicated back by executing trigger or handler functions, which may receive arguments.
• Monitors are executed by calling a Copilot-generated function (called step by default).

These ideas may not translate well into Rust. A first topic to discuss, then, would be what a Rust monitor would look like in general (even without Copilot anywhere in the mix). That is, if there is a program written in rust, and you wanted to create a module that checks if some property holds over the execution of the program, what would such a monitor look like?

[antanas-kalkauskas-sensmetry]

A couple of existing runtime verification tools for Rust

I did a quick look into the literature to see what other runtime verification frameworks have Rust monitor generation implemented. One of the tools is TeSSLa which can compile runtime monitors to Rust (and Scala). Another one is RTLola which had a publication a few years ago on generating Rust monitors and there is a repo for the artefacts of the paper though I could not find the Rust monitor generation code. But there is an interpreter that could take a monitoring specification and run a monitor as part of a Rust application.

What does TeSSLa monitor look like?

A description of the generated Rust monitor interface can be found here. In brief:

There is a generated State that holds the internal monitor state, has methods setting input signals, performing a step and holds references to output callback functions.

The user initializes the state struct by providing references to output callbacks (or specifying callback functions in terms of lambdas). Afterwards, the main loop (implemented by the user) looks as follows:

1. Values of input streams at the current timestamp are set by the user using generated setters.
2. Step function is executed. This mutates the state for the current timestamp and triggers needed output callbacks.
3. Timestamp is incremented.

What does RTLola interpreter monitor look like?

Documentation on RTLola monitor interface can be found here. In brief:

It seems that a monitor struct is created at runtime by providing a specification string (which is then parsed and translated to some internal representation). The monitor struct has functions to accept events or accept time.

• Accepting an event at a given timestep changes the input stream values at given timesteps and calculates the new values of periodic streams up to the given timestep.
• Accepting a timestamp calculates the new values of periodic streams up to the given timestep.

Both functions for accepting an event and time return a vector of verdicts (because they both advance monitor time). There are different choices on how verdicts can be reported, e.g. totally by giving the full statuses of verdicts or incrementally by only providing the changes in verdicts during the most recent timestamp advance. As opposed to Copilot and TeSSLa, there is no mechanism for triggering the user provided functions based on monitor verdicts.

Note: Generated RTLola Rust monitors as described in the paper might have a different interface than RTLola interpreter. But looking at the code in the repo for the artefacts of the paper, it seems that the interface there is not really fleshed out: e.g. inputs are taken from inside of unsafe blocks from static global arrays. The code structure there might have been tailored to primarily deliver a prototype of verifying the functionality of the core monitoring logic using Viper toolkit (this seems to be one of the main research targets of the paper).

What could a (Rust) monitor look like

I thought about the questions, here are some ideas that I had on implementing a monitor after observing the ways it was implemented in other Rust runtime monitoring tools. Feel free to correct me or comment, I have little experience with Rust.

Providing inputs

There could be different ways of providing inputs to monitors:

1. Monitor takes input values from global variables. This is how it is done in Copilot C backend. But this might be discouraged in Rust as one would need to use unsafe to access these variables.
2. Step function takes inputs as an argument. Most likely a struct definition could be generated and a user would be responsible for filling the struct and providing a value or a reference to it.
3. Monitor API exposes a way to set single input values. In TeSSLa this is done using setters. In RTLola interpreter this can be done using events for inputs (or also groups of signals can be set with special events).
4. User provides callbacks to monitor to get input signals. Monitor state could hold references to functions for pulling the signals. This seems a bit more complicated than the above choices.
5. User implements getter functions to pull input signals. The difference from the above is that instead of callbacks that are passed to monitor at runtime, a user would need to implement static functions with a certain name and signature without which an application would not compile. As an example, in C backend, a header is generated with trigger function declarations and it is the user's responsibility to implement those trigger functions. I do not know if there is a neat way to do this in Rust (i.e. something analogous to generating a header in C with function declarations that the user needs to implement).

My subjective preference would be the number 2. as in this way the step function is more explicit and about values it depends on.

Communicating outputs

1. Monitor triggers functions that the user implements according to the declaration/description generated by the backend. This is how it is done in Copilot C backend. I do not know if there is a neat way to do this in Rust (i.e. something analogous to generating a header in C with function declarations that the user needs to implement).
2. User provides callbacks for Monitor to trigger based on verdicts. This is how it is done in TeSSLa.
3. Monitor gives the verdict results as return values of functions. RTLola does this by returning monitor verdicts for every event update function call or time update function call. Copilot could return this as part of the step function call, or it could fill the reference for the struct. One issue is that a verdict in Copilot consists of a string (for trigger function name) and perhaps multiple arguments (arguments for trigger function). So some structure would be needed to hold this information (e.g. a large struct with many small heterogeneous structs, where each small struct holds a verdict status for single monitor + arguments) and it would be the user's responsibility to implement functions that act on those verdicts.

For a Rust backend prototype, I would say 3. might be the easiest to implement. Perhaps it might initially suffice to provide all verdicts as a struct/array of bools.

For a longer term solution, some variant of 1. or 2. or something else might be chosen.

Executing an iteration and handling the internal state

In Copilot C backend, the internal state of monitors is stored as many static variables, which again might be not a good idea in Rust, as one needs to use unsafe to mutate them. In both TeSSLa and RTLola the state is held by some struct called Memory, State or Monitor, those structs have some step functions to execute the monitor. I do not see a clear alternative to having some Rust struct containing monitor state with functions to perform a step or other routines.

If we decide to use callbacks either for getting inputs or triggers, it might be a good idea to separate those references from the internal monitor state (the one that stores e.g. buffers of past signal values, or some intermediate stream values). For testability (and perhaps replayability) it might be good to have some pure function for performing core stream logic and state updates, in Haskell terms, having a signature like this internalStep :: (MonitorState, MonitorInput) -> (MonitorState, MonitorOutput), though I do not have too many strong arguments for this. User facing step function could wrap this internalStep without exposing the internal state.

[ivanperez-keera]

Thanks a lot for the very detailed examination and the amount of thought you've already put into this.

I'd certainly be ok with I2-O3.

What you say about having some struct in rust containing the internal state(s) makes sense. As a functional programmer, that would also be the way I'd prefer to go (and I see other benefits of doing it that way).

I'd say let's not use callbacks at least for getting inputs. Those callbacks may have arbitrary effects, loop forever, etc. There's no guarantee of how long they'll take to execute. Expecting the inputs from the user makes it easier to statically analyze our code and determine how long it takes to run.

To make things perhaps a bit more precise, if we opt for I2-O3, what would that look like? For example, say we have a system where the vehicle speed is coming in from a sensor. For now, we can just fake it.

We want to monitor the vehicle speed and, if it's too high, execute some function in rust that would (presumably) lower the speed.

What would the main look like, and what would the monitor look like?

[ivanperez-keera]

And by the main, I mean the equivalent to C's main, which in the case of Copilot, it's the one that drives the monitors.

[antanas-kalkauskas-sensmetry]

I spent some time today and implemented several variations of a possible rust monitor here: https://github.com/antanas-kalkauskas-sensmetry/rust-monitor-examples

• In src/example1 the outputs are returned as a struct with bools for every trigger function (there are no trigger function arguments). main can decide to call trigger functions based on the outputs.
• In src/example2 the outputs are returned as a nested struct with boolean verdicts and arguments. main can then decide to execute based on outputs and is responsible for routing trigger function arguments.
• In src/example3 and src/example4, a trait with trigger function declarations is provided (e.g. here) and the user is responsible for providing an implementation of that trait (e.g. here). This is similar to what I wrote initially as O1 variant for communicating outputs (user implements trigger functions according to the declaration/description generated by the backend). An advantage of src/example3 and src/example4 variations is that there are static checks for exhaustiveness to consider all monitor outputs (one would get a compilation error if some trigger function is not implemented).

Something similar to example 1 might be slightly simpler to implement. Example 3 or 4 might have a nicer interface.

[ivanperez-keera]

I like the idea of the extra checks provided by example3 and example4. What's the difference between them?

[antanas-kalkauskas-sensmetry]

The difference is in the definition of the trait or the required signature of trigger functions.

In example4 the signature of trigger functions is simply the trigger arguments -> void, similar as in C99 backend.

In example 3 the trigger function signatures in the trait take also &mut self as an argument which allows the struct that implements the trait to hold some state. This might be more convenient in Rust while implementing trigger actions: e.g. the struct might hold information on how to send actuation commands without referring to some global state. It might also allow collecting some statistics/logging, e.g. I implemented here a counter that tracks how many times the trigger functions have been executed

[ivanperez-keera]

Galois has a C2Rust converter. If I paste one of our Copilot modules with https://c2rust.com/, here's what comes out:

#![allow(dead_code, mutable_transmutes, non_camel_case_types, non_snake_case, non_upper_case_globals, unused_assignments, unused_mut)]
#![register_tool(c2rust)]
#![feature(register_tool)]
extern "C" {
    static mut temperature: uint8_t;
    fn heaton(heaton_arg0_0: float_t);
    fn heatoff(heatoff_arg0_0: float_t);
}
pub type uint8_t = libc::c_uchar;
pub type float_t = libc::c_float;
static mut temperature_cpy: uint8_t = 0;
unsafe extern "C" fn heaton_guard() -> bool {
    return temperature_cpy as float_t * (150.0f32 / 255.0f32) - 50.0f32 < 18.0f32;
}
unsafe extern "C" fn heaton_arg0() -> float_t {
    return temperature_cpy as float_t * (150.0f32 / 255.0f32) - 50.0f32;
}
unsafe extern "C" fn heatoff_guard() -> bool {
    return temperature_cpy as float_t * (150.0f32 / 255.0f32) - 50.0f32 > 21.0f32;
}
unsafe extern "C" fn heatoff_arg0() -> float_t {
    return temperature_cpy as float_t * (150.0f32 / 255.0f32) - 50.0f32;
}
#[no_mangle]
pub unsafe extern "C" fn step() {
    let mut heaton_arg_temp0: float_t = 0.;
    let mut heatoff_arg_temp0: float_t = 0.;
    temperature_cpy = temperature;
    if heaton_guard() {
        heaton_arg_temp0 = heaton_arg0();
        heaton(heaton_arg_temp0);
    }
    if heatoff_guard() {
        heatoff_arg_temp0 = heatoff_arg0();
        heatoff(heatoff_arg_temp0);
    }
}

I would not suggest we approach it this way, but I thought, for completeness, it could be useful info.

[antanas-kalkauskas-sensmetry]

I could be very wrong about this, but I think a lot of Haskellers like rust. Maybe some community members would be willing to revamp that library a bit and make sure it can be used if there's actual applications willing to use it. Maybe a way to start is to try to use that library, see what's missing, and how much effort it would take to add that. If not much, then it would be possible to complete this backend and make a case for why maintaining that library would be useful for the community (rather than asking people to take a leap of faith).

I agree, it could be a good task now to check if language-rust works. I might try to use the library and define something like an AST for one of my example monitors and see if the pretty-printed code works.

[ivanperez-keera]

Update: language-rust as such may be in worse state than I thought, but either of the following may work better:

• Update to Rust 1.39 harpocrates/language-rust#34
• https://github.com/GaloisInc/language-rust

We are having a side conversation about whether either of those could be maintained long term. My inclination for now would be to pick whichever option gets a minimal prototype going (naive string construction being absolutely acceptable if none of those support everything needed out-of-the-box and with minimal setup), and revisit this later.

[antanas-kalkauskas-sensmetry]

I tried briefly the Galois fork a couple of weeks ago. It seemed to be runnable with newer GHC versions, I think all or almost all of the pretty printing test cases were passing. I managed to use the library to construct some bits of my monitor code AST (not close to a complete monitor yet) and I managed to pretty-print it. Pretty-printing test cases provide good examples for constructing AST.

AST manipulation in language-rust is quite low-level. It might be the case that eventually it would be useful to have a higher-level library wrapping language-rust, an analogue to language-c99-simple, but it is not clear whether this would be necessary.

[antanas-kalkauskas-sensmetry]

Actually, I and one of my colleagues had some time over the last couple of days and we implemented a prototype Rust backend for a subset of functionality (e.g. we did not consider struct streams or array streams, only a subset of stream operators). We will clean up the code and push it out in a few days.

[ivanperez-keera]

This is awesome. Looking forward to seeing it.