formalize barrelfish's existing hamlet DSL

mwookawa commented 7 years ago

Hamlet describes capability types, giving each type of capability a set of fields and a set of explicit relationships to other capability types. Our notional abstraction is that a capability type A can only be retyped to a capability type B if there is such a relationship from A to B explicitly in the hamlet file describing A and B.

mwookawa commented 7 years ago

synthesize syscalls

mwookawa commented 7 years ago

we are sticking to FoF right now for DSL metalanguage

alexpatel commented 7 years ago

Some other @mwookawa notes:

come up with a language for what retyping means and what a type is
most kernel operations are just re-typing, so you're describing a lot of the operations of the kernel as semantically defined retypings of record
hamlet more interesting than mackerel, but mackerel is important for defining these operations because we take these mackerel defined symbolic values about registers, but in current implementation they are arbitrary/programmatic
- if we understnad mackerel in a better structured way is to give it a formally verified semantics
- mackerel has semantics that should be easy to define, amenable to synthesis
- they claim that hamlet is the most amenable for simple synthesis because of syscalls just being retypings
  - if you look at the retypings semantically blindly, it's just top - generate syscalls for caps and then synthesis callers
  - one step further: build an actual semantics for it
  - can also say something about the language of the whole and the limits on it so that we can say how it is domain-specific
  - can say that the translation definitely terminates

mwookawa commented 7 years ago

child of #45

mwookawa commented 7 years ago

https://github.com/Harvard-PRINCESS/Guppy/blob/dev/capabilities/caps.hl#L22-L24

language semantics rely on literals drawn from code:

https://github.com/Harvard-PRINCESS/Guppy/blob/dev/include/barrelfish_kpi/capabilities.h#L19-L50

as per ETH, this needs to be fixed in any modification of hamlet and cannot be present in formalism..

mwookawa commented 7 years ago

this is subsumed by alewife formulation

Harvard-PRINCESS / Guppy

formalize barrelfish's existing hamlet DSL #23