Formal specification of DIF

[dstolfa]

Given that DIF is an intermediate representation that DTrace currently uses and compilers will have to map their language into DIF, it would be useful to have a formal specification of DIF in Isabelle/HOL [1] or Coq [2] as a long term goal. This would allow for a clear specification of DIF without a reference implementation and would resolve potential ambiguity in the text.

Furthermore, writing it this way would allow for proofs about DIF to be constructed under certain agreed on assumptions (such as builtin variables returning an arbitrary value of a certain type, following pointers results in a valid memory location etc) various properties such as termination and certain types of safety. This also allows one to expose information from a concrete implementation of a DIF interpreter/JIT compiler and assert that it adheres to the specification (given that the assumptions hold). This would also make it easier to understand the implications of changes to DIF (such as addition of instructions or change of semantics).

[1] http://isabelle.in.tum.de
[2] https://coq.inria.fr

[hannesm]

IMHO the first steps would be to formalise DIF in ott and/or lem. there is already the C semantics cerberos developed in lem, from which DIF may borrow some bits and pieces (such as integer arithmetics etc.).

[dstolfa]

@hannesm I quite like the idea of using ott or lem, as they provide translation to other proof assistants. Do you know if they have any special requirements to get working on platforms that have an OCaml compiler/runtime or should they just work out of the box on any system where OCaml works?

[hannesm]

@dstolfa ott is released to opam, after installing ocaml-opam, you should be able to opam install ott to install it into ~/.opam/YYY/bin/ott! lem I've so far built only manually from a checkout, it works (worked?) on FreeBSD flawlessly.