Well typed OS

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
25 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Vanessa McHale

The problem with an IR is that some languages would inevitably suffer - LLVM in particular was designed as a backend for a C compiler, and so it is not necessarily well-suited for lazy languages, immutable languages, etc. (not to mention self-modifying assembly and other such pathological beasts...)


On 10/06/2018 08:31 PM, William Yager wrote:


On Sat, Oct 6, 2018 at 11:03 PM Barak A. Pearlmutter <[hidden email]> wrote:
At a high level, you seem to be proposing encoding and enforcing
safety properties of executables using a type system. One
instantiation of this idea is proof-carrying-code (Necula and Lee,
1996, see https://en.wikipedia.org/wiki/Proof-carrying_code), which
ensures safety properties of machine code. 

I would guess a factor that prevented something like PCC from taking off is the fact that proofs over binaries are relatively pretty challenging to express and verify, and ISA semantics tend to be really complicated.

I think an intermediate approach that might be a lot cheaper to implement is to ship some sort of IR (rather than machine code) that is A) relatively cheap to check and compile and B) carries some variety of safety guarantee.

As I recall, A) is already in use. Apple requires developers to submit applications as LLVM IR rather than machine code.

LLVM IR definitely isn't designed with B) in mind, however. I could imagine something like Core being useful here. A fully annotated type-checked language with semantics amenable to formal analysis.

You could add some sort of effects system to the type system of the IR, as a basis for enforcing security policies. E.g. network access could be an effect.

The advantage of doing this over PCC is that we don't have to retrofit the proof system to match the ISA, but instead can design the IR specifically to make the proof system easy. A downside is that you have to compile the application once upon downloading it, but this doesn't seem to cause too much of an issue in practice.


  


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

signature.asc (499 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Joachim Durchholz
Am 08.10.2018 um 01:34 schrieb Vanessa McHale:
> The problem with an IR is that some languages would inevitably suffer -
> LLVM in particular was designed as a backend for a C compiler, and so it
> is not necessarily well-suited for lazy languages, immutable languages,
> etc. (not to mention self-modifying assembly and other such pathological
> beasts...)
Actually LLVM is built for being adaptable to different kinds of
languages. It does have a bias towards C-style languages, but you can
adapt what doesn't fit your needs *and still keep the rest*.

The following was true a few years ago:

When I asked, the LLVM IR was intentionally not specified to be reusable
across languages, so that different compiler toolchain could adapt the
IR to whatever needs their language or backend infrastructure needed.

Garbage collection is one area where you have to do a lot of work. There
are some primitive instructions that support it, but the semantics is
vague and doesn't cover all kinds of write barriers. You'll have to roll
your own IR extensions - or maybe I didn't understand the primitives
well enough to see how much they cover.
Anyway, LLVM does not come with a GC implementation.
OTOH, it does not prevent you from doing a GC. In particular, you're
free to avoid C-style pointers, so you have the full range of GC
algorithms available.

Laziness? No problem. If you do tagless/spineless, you'll code the
evaluation machine anyway. Just add an IR instructions that calls the
interpreter.

Immutability? No problem - actually nowhere a problem. Immutability
happens at the language level, at the IR level it is pretty irrelevant
because compilers try to replace object copying by in-place modification
wherever possible, anyway.

Self-modifying assembly? No IR really supports that. Mostly it's
backends that generate self-modifying code from IR instructions for
specific backends.

TL;DR: For its generality, LLVM IR is better suited to languages with
specific needs in the backend than anything else that I have seen (which
means C runtimes, various VM proofs of concept which don't really count,
and JVM - in particular I don't know how .net compares).

Regards,
Jo
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Gleb Popov


On Mon, Oct 8, 2018 at 8:53 AM Joachim Durchholz <[hidden email]> wrote:
Am 08.10.2018 um 01:34 schrieb Vanessa McHale:
> The problem with an IR is that some languages would inevitably suffer -
> LLVM in particular was designed as a backend for a C compiler, and so it
> is not necessarily well-suited for lazy languages, immutable languages,
> etc. (not to mention self-modifying assembly and other such pathological
> beasts...)
Actually LLVM is built for being adaptable to different kinds of
languages. It does have a bias towards C-style languages, but you can
adapt what doesn't fit your needs *and still keep the rest*.

The following was true a few years ago:

When I asked, the LLVM IR was intentionally not specified to be reusable
across languages, so that different compiler toolchain could adapt the
IR to whatever needs their language or backend infrastructure needed.

Garbage collection is one area where you have to do a lot of work. There
are some primitive instructions that support it, but the semantics is
vague and doesn't cover all kinds of write barriers. You'll have to roll
your own IR extensions - or maybe I didn't understand the primitives
well enough to see how much they cover.
Anyway, LLVM does not come with a GC implementation.
OTOH, it does not prevent you from doing a GC. In particular, you're
free to avoid C-style pointers, so you have the full range of GC
algorithms available.

Laziness? No problem. If you do tagless/spineless, you'll code the
evaluation machine anyway. Just add an IR instructions that calls the
interpreter.

I'm far from expert in this area, but isn't that "interpreter" a simple yet slow approach to codegen? My understanding is that when you use, say, a global variable as a register for your evaluation machine, it is slower than if you somehow pin real hardware register for that purpose. I think this is what "registerized" GHC build means.
In LLVM you can't use, say, RSP in a way you want, but it is doomed to be "stack pointer register", even if you don't use stack at all.

As I read in some blog, you can slightly affect LLVM codegen by adding calling conventions, but the real solution would be another algorithm for instruction selection. No one implemented that yet, AFAIK.


Immutability? No problem - actually nowhere a problem. Immutability
happens at the language level, at the IR level it is pretty irrelevant
because compilers try to replace object copying by in-place modification
wherever possible, anyway.

Self-modifying assembly? No IR really supports that. Mostly it's
backends that generate self-modifying code from IR instructions for
specific backends.

TL;DR: For its generality, LLVM IR is better suited to languages with
specific needs in the backend than anything else that I have seen (which
means C runtimes, various VM proofs of concept which don't really count,
and JVM - in particular I don't know how .net compares).

Regards,
Jo
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Joachim Durchholz
Am 08.10.2018 um 09:08 schrieb Gleb Popov:

>
>     Laziness? No problem. If you do tagless/spineless, you'll code the
>     evaluation machine anyway. Just add an IR instructions that calls the
>     interpreter.
>
> I'm far from expert in this area, but isn't that "interpreter" a simple
> yet slow approach to codegen? My understanding is that when you use,
> say, a global variable as a register for your evaluation machine, it is
> slower than if you somehow pin real hardware register for that purpose.
> I think this is what "registerized" GHC build means.

My impression has been that GHC is compiling everything down to machine
code. FWIW most mentions I saw were of the kind "we replace
tagless/spineless with X", not of the "we build on tagless/spineless
doing Y". Not that I have read many papers - I'm awfully behind on these
topics.

> In LLVM you can't use, say, RSP in a way you want, but it is doomed to
> be "stack pointer register", even if you don't use stack at all.

Actually it seems possible since some version between 3.4 and 3.6.
https://stackoverflow.com/questions/29365198/how-to-use-llvm-intrinsics-llvm-read-register 
discusses a way of doing exactly that.

Not sure about ramifications though.

Still, seeing how many wildly varying languages use LLVM for code
generation, it seems to be widely considered to be the most flexible
available one.
If somebody knows of something more flexible, paint me interested :-)

Regards,
Jo
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Andreas Reuleaux-2
In reply to this post by Yotam Ohad
While this may not be an answer to your specific question,
you may want to have a look at MirageOS, the Operating System
written in Ocaml by Anil Madhavapeddy el.,
https://mirage.io/


We had discussed this some while ago in our seminar,
and I learned that Ocaml may be a better fit for
writing an operating system than Haskell, due to Ocaml's
ability to produce small binaries, smaller than Haskell
binaries in any case usually. - Being involved with
Haskell personally, I would like to be proven wrong,
of course (ie. I would like to see small Haskell binaries),
and I have heard of some former efforts of writing an OS in Haskell
as well (but I would have to search for links).


just my 2 cents,
  Andreas




Yotam Ohad <[hidden email]> writes:

>  Hi,
> In the last couple of days, I've been toying with the thought of an
> operating system in which programs (or more accurately, any process) has a
> distinct type which limits
> its use of the machine. For example, `echo` (String -> String) won't be
> able to print an output without a second program which would handle
> changing stdout.
>
> I think it could "break down" the IO monad into other structures that are
> better at specifying what is changing: A file is read / memory written /
> etc.
> I do, however, not sure how to incorporate drivers (which handles IO and
> external devices) into this. Giving them an `IO a` type feels like
> cheating. I would be much cooler if there was a way
> to treat them like the `echo` function from earlier.
>
> What are your thoughts/suggestions? I'll be happy to hear them.
>
> Yotam
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
12