Well typed OS

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
39 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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Vanessa McHale
There's a lot of other stuff going on too, not just binary sizes - GHC's
runtime, a dynamic memory allocator, etc. I would hesitate to use
Haskell in the embedded context or for hardware-level stuff. I presume
GHC's approach to laziness has a role in this.

I don't have much experience with OCaml but my experience with ATS is
that it's very much possible to have functional, ML-style programming
without a runtime or even dynamic memory allocation.

On 10/19/18 4:02 PM, Andreas Reuleaux wrote:

> 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.

_______________________________________________
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

Jeffrey Brown
I don't know whether this is helpful, but Purescript provides a way to specify the kinds of IO a monad can do. For instance, the Extensible Effects section[1] of Purescript by Example includes this code snippet:

    > :type main
    forall eff. Eff (console :: CONSOLE, random :: RANDOM | eff) Unit



On Fri, Oct 19, 2018 at 8:11 PM Vanessa McHale <[hidden email]> wrote:
There's a lot of other stuff going on too, not just binary sizes - GHC's
runtime, a dynamic memory allocator, etc. I would hesitate to use
Haskell in the embedded context or for hardware-level stuff. I presume
GHC's approach to laziness has a role in this.

I don't have much experience with OCaml but my experience with ATS is
that it's very much possible to have functional, ML-style programming
without a runtime or even dynamic memory allocation.

On 10/19/18 4:02 PM, Andreas Reuleaux wrote:
> 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.

_______________________________________________
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.


--
Jeff Brown | Jeffrey Benjamin Brown
Website   |   Facebook   |   LinkedIn(spammy, so I often miss messages here)   |   Github   

_______________________________________________
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

Will Yager
In reply to this post by Vanessa McHale


> On Oct 20, 2018, at 09:11, Vanessa McHale <[hidden email]> wrote:
>  I would hesitate to use
> Haskell in the embedded context or for hardware-level stuff. I presume
> GHC's approach to laziness has a role in this.

There’s a bit of a complication here. It’s true that standard GHC generated code is unsuitable for hard-real-time/embedded environments (although I would argue that it’s actually fine for general purpose OS programming). However, as far as hardware goes, the semantics of (a non-monomorphically-recursive subset of) Haskell is actually a surprisingly close match for the semantics of hardware (as in LUTs and flip-flops, not as in random microcontrollers).

This is the basis of projects like Clash (Haskell to HDLs).  I imagine one could extend the clash approach to generate allocation-free assembly from the same (large) subset of Haskell.

>
> I don't have much experience with OCaml but my experience with ATS is
> that it's very much possible to have functional, ML-style programming
> without a runtime or even dynamic memory allocation.
>>

It’s possible to write low-allocation (I wouldn’t call it “allocation free” - usually just the hot loops don’t allocate) OCaml with the standard tools. However, it requires a fairly non-idiomatic style.

—Will


_______________________________________________
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

Vanessa McHale
Interesting! It's been awhile since I've worked on FPGAs :)

ATS is the only language I've seen that advertises stack-allocated
closures, and I think GHC's approach to laziness requires heap
allocation, so there's still a few targets (AVR off the top of my head)
that GHC would need significant modification to work on.

On 10/20/18 9:52 PM, Will Yager wrote:

>
>> On Oct 20, 2018, at 09:11, Vanessa McHale <[hidden email]> wrote:
>>  I would hesitate to use
>> Haskell in the embedded context or for hardware-level stuff. I presume
>> GHC's approach to laziness has a role in this.
> There’s a bit of a complication here. It’s true that standard GHC generated code is unsuitable for hard-real-time/embedded environments (although I would argue that it’s actually fine for general purpose OS programming). However, as far as hardware goes, the semantics of (a non-monomorphically-recursive subset of) Haskell is actually a surprisingly close match for the semantics of hardware (as in LUTs and flip-flops, not as in random microcontrollers).
>
> This is the basis of projects like Clash (Haskell to HDLs).  I imagine one could extend the clash approach to generate allocation-free assembly from the same (large) subset of Haskell.
>
>> I don't have much experience with OCaml but my experience with ATS is
>> that it's very much possible to have functional, ML-style programming
>> without a runtime or even dynamic memory allocation.
> It’s possible to write low-allocation (I wouldn’t call it “allocation free” - usually just the hot loops don’t allocate) OCaml with the standard tools. However, it requires a fairly non-idiomatic style.
>
> —Will
>
>

_______________________________________________
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

Raoul Duke
tower? atom?

_______________________________________________
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
In reply to this post by Will Yager
Am 21.10.18 um 04:52 schrieb Will Yager:
>
> This is the basis of projects like Clash (Haskell to HDLs).  I imagine one could extend the clash approach to generate allocation-free assembly from the same (large) subset of Haskell.

Is that subset described somewhere?

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

Siddharth Bhat
Kind of tangential, but bluespev verilog is a "Haskell inspired" version of verilog that has a strong Haskell flavour (typeclasses, purity, a rudimentary effect system that tracks combinational versus state based logic, clock domains embedded into the type, width polymorphic functions, etc).

It's a really great way to see what a haskell-like-hardware description language could look like :)

Cheers
siddharth

On Sun 21 Oct, 2018, 12:34 Joachim Durchholz, <[hidden email]> wrote:
Am 21.10.18 um 04:52 schrieb Will Yager:
>
> This is the basis of projects like Clash (Haskell to HDLs).  I imagine one could extend the clash approach to generate allocation-free assembly from the same (large) subset of Haskell.

Is that subset described somewhere?

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.
--
Sending this from my phone, please excuse any typos!

_______________________________________________
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

Will Yager
In reply to this post by Joachim Durchholz


On Sun, Oct 21, 2018 at 3:04 PM Joachim Durchholz <[hidden email]> wrote:

Is that subset described somewhere?


So there are two possible answers to this:

1. The subset that Clash supports is a bit complicated and increases from time to time, depending mostly on the internal details of the clash compiler

2. The subset that Clash *could* support with (roughly) its current approach, which I think I can answer a bit better: 

I gave a brief hand-wavy description earlier - "non-monomorphically-recursive"

That is, any recursion has to be unrolled at the hardware level, and monomorphically (i.e. normally) recursive functions cannot (generally) stop being unrolled after a finite number of iterations. Sure, you can sometimes use fancy tricks (an SMT solver or something) to prove termination, but these come with a number of other challenges. For hardware you want a small, concrete number of recursions, which leads to lots of complications (e.g. need for dependent types to relate input values and recursion depth).

Much simpler is to simply disallow monomorphic recursion, and then you shift the work of proving finite recursion depth to the type level. 

There's then a simple (constructive) rule for proving termination and calculating the number of recursive calls.

Given

F :: * -> *
f :: a = ... (f :: F a) ...

used at some site

... f ...

0. let seen_types = ∅
1. let t = the type of "f"
2. If t ∈ seen_types, fail - unbounded recursion
3. Add t to seen_types
4. Inline the definition of "f"
5. Goto 1, with any newly introduced call to "f"

This construction inlines every recursive call, which gives you a hardware-friendly representation without recursion at the end. This also supports multiple recursion, like over a binary tree (important for efficient hardware). 

To give a concrete example of how this works, consider

sum :: ∀ n . Vec n Int -> Int
sum :: Vec 0       Int -> Int = \Empty -> 0 -- Non-recursive
sum :: Vec (n+1) Int -> Int = \(hd:tl) -> hd + (sum :: Vec n Int -> Int) tl

This function is polymorphically recursive and perfectly reasonable to instantiate in hardware. The rule above succeeds in synthesizing the "sum" function, but will reject monomorphically recursive functions like "sum :: [Int] -> Int" or functions that end up being monomorphically recursive through a few polymorphically recursive "layers".

One downside of this approach is that if F is divergent (i.e. the type of "f" never cycles back on itself but it always changes), this will either hang the compiler or you have to have an upper bound on the allowed number of inlines. This is probably fine - if you're trying to represent a function with a huge recursion depth in hardware, your design sucks and will be slow anyway.

Again, reiterating that Clash doesn't *actually* support the entire subset mentioned above. That is just what one *could* support with the same conceptual approach. Instead, Clash has a few hard-coded things that it knows how to recurse over, like fixed-length vectors.

There are probably some errors in the above - I'm not an expert on the internals of the clash compiler and this is just a brain-dump of my vague thoughts on synthesis.

--Will 




_______________________________________________
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 21.10.18 um 11:16 schrieb William Yager:
> 2. The subset that Clash *could* support with (roughly) its current
> approach, which I think I can answer a bit better:

Thanks - that's exactly what I was after.
_______________________________________________
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

Vanessa McHale
In reply to this post by Joachim Durchholz
Others know more than I but the gist of it is that you can compile
functions to circuits. Haskell's functions are fundamentally different
from C's functions (which are basically procedures that sometimes have a
return value), but there's no reason you can't compile a non-strict
function to a circuit.

On 10/21/18 2:04 AM, Joachim Durchholz wrote:

> Am 21.10.18 um 04:52 schrieb Will Yager:
>>
>> This is the basis of projects like Clash (Haskell to HDLs).  I
>> imagine one could extend the clash approach to generate
>> allocation-free assembly from the same (large) subset of Haskell.
>
> Is that subset described somewhere?
>
> 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.

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

Re: Well typed OS

Vanessa McHale
In reply to this post by Siddharth Bhat

I've never understood why functional (and in particular Haskell-influenced) approaches to hardware never took off. I suspect it was political (Haskell is too academic, etc.), or perhaps the companies using it are just quiet about it :)

I think you could use monads for clock domains. Once something has a clocked input, its output will be clocked too - it fits well with the "lift anything unclocked to clocked, but once clocked it is *always* clocked".

On 10/21/18 2:59 AM, Siddharth Bhat wrote:
Kind of tangential, but bluespev verilog is a "Haskell inspired" version of verilog that has a strong Haskell flavour (typeclasses, purity, a rudimentary effect system that tracks combinational versus state based logic, clock domains embedded into the type, width polymorphic functions, etc).

It's a really great way to see what a haskell-like-hardware description language could look like :)

Cheers
siddharth

On Sun 21 Oct, 2018, 12:34 Joachim Durchholz, <[hidden email]> wrote:
Am 21.10.18 um 04:52 schrieb Will Yager:
>
> This is the basis of projects like Clash (Haskell to HDLs).  I imagine one could extend the clash approach to generate allocation-free assembly from the same (large) subset of Haskell.

Is that subset described somewhere?

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.
--
Sending this from my phone, please excuse any typos!

_______________________________________________
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

Vanessa McHale
In reply to this post by Will Yager

Anything that's tail recursive could be converted to a while loop and then clocked, no? You could for instance compile

fact :: Int -> Int

fact 0 = 1

fact n = n * fact (n - 1)

to hardware even if it would not be a good idea.

On 10/21/18 4:16 AM, William Yager wrote:


On Sun, Oct 21, 2018 at 3:04 PM Joachim Durchholz <[hidden email]> wrote:

Is that subset described somewhere?


So there are two possible answers to this:

1. The subset that Clash supports is a bit complicated and increases from time to time, depending mostly on the internal details of the clash compiler

2. The subset that Clash *could* support with (roughly) its current approach, which I think I can answer a bit better: 

I gave a brief hand-wavy description earlier - "non-monomorphically-recursive"

That is, any recursion has to be unrolled at the hardware level, and monomorphically (i.e. normally) recursive functions cannot (generally) stop being unrolled after a finite number of iterations. Sure, you can sometimes use fancy tricks (an SMT solver or something) to prove termination, but these come with a number of other challenges. For hardware you want a small, concrete number of recursions, which leads to lots of complications (e.g. need for dependent types to relate input values and recursion depth).

Much simpler is to simply disallow monomorphic recursion, and then you shift the work of proving finite recursion depth to the type level. 

There's then a simple (constructive) rule for proving termination and calculating the number of recursive calls.

Given

F :: * -> *
f :: a = ... (f :: F a) ...

used at some site

... f ...

0. let seen_types = ∅
1. let t = the type of "f"
2. If t ∈ seen_types, fail - unbounded recursion
3. Add t to seen_types
4. Inline the definition of "f"
5. Goto 1, with any newly introduced call to "f"

This construction inlines every recursive call, which gives you a hardware-friendly representation without recursion at the end. This also supports multiple recursion, like over a binary tree (important for efficient hardware). 

To give a concrete example of how this works, consider

sum :: ∀ n . Vec n Int -> Int
sum :: Vec 0       Int -> Int = \Empty -> 0 -- Non-recursive
sum :: Vec (n+1) Int -> Int = \(hd:tl) -> hd + (sum :: Vec n Int -> Int) tl

This function is polymorphically recursive and perfectly reasonable to instantiate in hardware. The rule above succeeds in synthesizing the "sum" function, but will reject monomorphically recursive functions like "sum :: [Int] -> Int" or functions that end up being monomorphically recursive through a few polymorphically recursive "layers".

One downside of this approach is that if F is divergent (i.e. the type of "f" never cycles back on itself but it always changes), this will either hang the compiler or you have to have an upper bound on the allowed number of inlines. This is probably fine - if you're trying to represent a function with a huge recursion depth in hardware, your design sucks and will be slow anyway.

Again, reiterating that Clash doesn't *actually* support the entire subset mentioned above. That is just what one *could* support with the same conceptual approach. Instead, Clash has a few hard-coded things that it knows how to recurse over, like fixed-length vectors.

There are probably some errors in the above - I'm not an expert on the internals of the clash compiler and this is just a brain-dump of my vague thoughts on synthesis.

--Will 




_______________________________________________
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
In reply to this post by Vanessa McHale
Am 21.10.18 um 19:43 schrieb Vanessa McHale:
> I've never understood why functional (and in particular
> Haskell-influenced) approaches to hardware never took off. I suspect it
> was political (Haskell is too academic, etc.), or perhaps the companies
> using it are just quiet about it :)

The usual reason is that they simply haven't seen it work, and are not
sure whether it will work. Also, retraining your engineers is VERY
expensive: expect a few weeks of training, plus a few months of reduced
effectivity; multiply with an engineer's cost per month, and you arrive
at really impressive figures.
If a company is successful, it sees no reason to go into that risk.
If a company is at the brink of defaulting, it cannot afford to try.
It's usually the second-in-line companies that try this kind of stuff,
and only if they have some risk appetite and need/want to catch up. In
these companies, there's room for experiment - but the experiment needs
to show success to be adopted, which is by no means guaranteed (you can
easily fail with a better methodology if you don't do it right).

And maybe functional really isn't a good match for hardware.
I don't expect that to be reality, but I have too little experience with
functional and almost zero with hardware, so I may be overlooking stuff
- the design space for hardware is pretty different than the design
space for software, pretty restrictive in some ways and unexpectedly
flexible in others.
Which brings me to another possible reason: Maybe functional isn't
solving any of the real problems in hardware design. That would then be
the "meh, nice but useless" reaction.
Just speculating about possibilities here; as I said: too little
hardware design experience here.

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

Will Yager
In reply to this post by Vanessa McHale


On Oct 22, 2018, at 01:43, Vanessa McHale <[hidden email]> wrote:

 or perhaps the companies using it are just quiet about it :)


It’s this. There are some companies you’ve heard of who are using it quietly :)

Anything that's tail recursive could be converted to a while loop and then clocked, no?

Yes, but the semantics of this are very different and the translation is much less straightforward (eg how many iterations will it take?). Better to do this “manually”, imo. Construct a mealy machine or something.   



_______________________________________________
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