-
Notifications
You must be signed in to change notification settings - Fork 3
Interaction with the OS
We give here the history of the ways we explored to communicate with the OS from Coq.
At first there was a system to output individual messages, from a given sum type. At each input message, an event handler would be launched.
This system is primitive and could be used to solve any problem in theory. But, in practice, we needed a nice and generic way to handle:
- the association of an answer with its request, without having to explicitly use a global store remembering what requests were done
- the ordering of answers (packets from a socket, ...)
Each emitted message is given a fresh id. The OS responds to each message by one or many answers. A callback handles the results. Since a callback is a closure, it can contain data: this removes the need of a global store in most cases.
An open question is: how to handle a possibly infinite number of answers per request (like when listening to a socket)?
The first solution is to have a handler of type:
State -> Input -> M (option State)
The handler reacts to each input. It has a state to remember the previous inputs, if needed. It can return the new state, which will be given with the next input, or None in case it stops listening. So the handler way finish after a finite number of inputs or not.
We show that a program with a finite number of answers per request terminates. This is not obvious a priori: for example, if each handler creates one request, even if there just one answer per request, the program will not terminate.
We may want to enforce the termination of each fold. We can do so with an inductive type, hiding the state in a closure, using this kind of type:
Inductive t (sig : Signature.t) (I : Type) (A : Type) : Type :=
| Stop : t sig I A
| Continue : (I -> Memory.t sig -> t sig I A * Memory.t sig * A) -> t sig I A.
It is then possible to define an eval function by induction on t which will terminate by construction, given a list of inputs and memories. An analogous definition can be made with co-inductive types to represent non-terminating listeners.
But we are not sure yet that the termination is that important to enforce at this level. There are also many other ways to block. For example, a handler expecting two answers for a system call responding only once will not terminate by waiting indefinitely, and this a kind of non-termination the user may want to be protected against.
However, our hope is that more termination will bring simpler specifications, because everything will get a value and trace will be inductive instead of co-inductive. It also removes a whole class of bugs, with looping inputs/outputs.
We need to investigate now this option. The hope is to get a simpler architecture, with explicit termination, at the cost of performances.