Arduino programming with Idris

[Jurriën Stutterheim]

Hi all,

Inspired by the "Safety first: targeting embedded systems with full-spectrum dependent types" paper presented at TFP 2015, I was wondering whether it is possible to program Arduino(-like) hardware with Idris. I imagine there are plenty of obstacles: (very) limited hardware resources, getting the program onto the Arduino itself, etc. Googling about the possibilities, I ran into the idris-blink repository [2] where the README states there are plenty of problems with GC consuming all hardware resources for even very small programs. Are these problems still present and that severe? Or does the work described in the aforementioned paper (partially) solve these problems and can we now write dependently typed Arduino programs? If so, are there any special flags or other things that I should be aware of?

Cheers,

Jurriën

[1] ftp://ftp-sop.inria.fr/indes/TFP15/TFP2015_submission_3.pdf

[2] https://github.com/stepcut/idris-blink

[Jeremy Shaw]

Hello,

Author of idris-blink here. As far as I know the GC problems still exist -- and they are quite significant.  The good news is that the way the Idris RTS is designed makes it pretty easy to supply an alternative garbage collector. The difficulty is in writing an alternative garbage collector.

In that paper they appear to be targeting an MSP-430 -- which I believe has between 256MB and 512MB of RAM. The Arduino has 2k.

Along similar lines to idris-blink, I have hacked up IdrOS:

https://github.com/stepcut/idrOS

Which could be suitable for targeting something like a Raspberry Pi. Though it has it's own separate garbage collection related issues at the moment.

Getting the compiled code onto the Arduino is actually not hard at all. You load it on like any other Arduino code.

I definitely would love to see more work done is this direction though. Being able to accurately model your hardware and check that the code you are writing actually matches the system would be awesome, IMO.

- jeremy

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Norm 2782]

Are there any particular (Idris-specific) difficulties in writing a more memory efficient GC? Or are you simply referring to the fact that writing a decent GC for these kind of systems isn't trivial? What kind of GC is Idris currently using?

Granted, 2k of memory is not a lot at all. Though there are some Arduinos now (particularly the 101) with 32k memory. Still not a lot, but a big improvement over 2k.

You received this message because you are subscribed to a topic in the Google Groups "Idris Programming Language" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/idris-lang/NsxReBzk7LQ/unsubscribe.
To unsubscribe from this group and all its topics, send an email to idris-lang+...@googlegroups.com.

[Jeremy Shaw]

The primary difficulties in writing a garbage collector for the Arduino is that it only has 2K of physical RAM and no virtual memory. Also, unlike most architectures, it actually has byte addressable memory. So you have to be careful if you want to use pointer tagging. Though that is pretty trivial to deal with.

The current garbage collector is a standard cheney style collector:

https://en.wikipedia.org/wiki/Cheney%27s_algorithm

You can see it in all its glory here:

https://github.com/idris-lang/Idris-dev/blob/master/rts/idris_gc.c

The heap allocator might also need some changes:

https://github.com/idris-lang/Idris-dev/blob/master/rts/idris_heap.c

The FORCE_ALIGNMENT ifdef was added specifically to deal with the Arduino byte-addressable issue I mentioned above.

I personally use the Teensy 3.1/3.2 for everything these days, so I get a whopping 64K.

The big issue with the cheney collector is that it divides the RAM in half and then copies objects back and forth. So you can't use more than half your RAM. On a system with virtual memory, that might not be such a big deal, since you could still use all your physical ram. But on a system with out virtual memory, that is pretty brutal.

I think a good starting point might be to read and understand this paper:

http://www.cs.virginia.edu/~cs415/reading/bacon-garbage.pdf

Something closer to reference counting might be more appropriate for an embedded system due to potentially better use of the physical ram and shorter pause times making timing critical code more practical.

Depending on your preferences, this could be something that takes a few days to implement or it could be a PhD thesis. Unfortunately, I do not have time for either of those options at the moment.

- jeremy

[Jurriën Stutterheim]

OK, so it's really just a hardware resource problem. Perhaps it would be worth exploring some form of mark-compact garbage collection? At least that doesn't cut the available memory in half. Hopefully I will have some time read up on GC in Idris and to play around with alternative GC strategies during the Christmas holidays.

A colleague of mine pointed me at the Intel Edison [1], by the way. It has impressive specs for such a small device. A bit more expensive, but at least it has an x86 CPU and 1GB of RAM. The Raspberry Pi compute module [2] looks impressive as well.

[1] https://en.wikipedia.org/wiki/Intel_Edison
[2] https://www.raspberrypi.org/products/compute-module/

[Jeremy Shaw]

There are definitely several levels within the embedded market. The sub $20 market microprocessor systems like teensy, arduino, etc, are great for a lot of things. But definitely starved for CPU and RAM. In the $20-$99 range you can pretty quickly get up to systems with serious amounts of RAM and CPU. Though, of course, there are tradeoffs. The RPi, for example, consumes a lot more power, has far fewer IO pins, and takes up a lot more space. I can put a teensy inside an LED hula-hoop. RPi -- no way.

I'd be surprised if Idris was ever truly viable on the Arduino (2K), could imagine that some apps could run on the teensy (64K) and expect it could do quite well on RPi, Edison, Beagleboard, etc, (256MB+).

I'm thinking that lots of people get along just fine on the Arduino. The teensy has 32 times more RAM, so even if Idris requires 4 times as much RAM as C, you'd still have 8x more RAM than what most Arduino people are using.

One thing that makes systems like the Arduino, teensy, etc different from desktops is that we know exactly how much RAM is available at compile time. I'm not quite sure what to do with that information, but it sure seems like something that would be good to exploit. Obviously, we'd like to prove that our application will never run out of RAM. At a more basic level -- we don't really need to use malloc/free on these systems. Since our app is the only thing using the RAM and the amount available is known at compile time, the garbage collector/heap allocator should just directly control everything.

Also, I wonder if perhaps Idris would have the power to somehow do region inference. This, of course, is where we start getting into the PhD level tinkering I think :)

- jeremy

[William ML Leslie]

On 20 November 2015 at 14:21, Jeremy Shaw <jer...@n-heptane.com> wrote:
> Also, I wonder if perhaps Idris would have the power to somehow do region
> inference. This, of course, is where we start getting into the PhD level
> tinkering I think :)
>
> - jeremy

+1

I managed to do Tofte/Birkedal style region inference on TT once; but
never got around to feeding it into the backend passes or back out
through the IDE system.

Edwin's uniqueness types could also be used for this - although
substructural typing is nowhere near as friendly or flexible as
regions.

--
William Leslie

Notice:
Likely much of this email is, by the nature of copyright, covered
under copyright law. You absolutely MAY reproduce any part of it in
accordance with the copyright law of the nation you are reading this
in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without
prior contractual agreement.

[William ML Leslie]

On 20 November 2015 at 14:50, William ML Leslie

<william.l...@gmail.com> wrote:
> On 20 November 2015 at 14:21, Jeremy Shaw <jer...@n-heptane.com> wrote:
>> Also, I wonder if perhaps Idris would have the power to somehow do region
>> inference. This, of course, is where we start getting into the PhD level
>> tinkering I think :)
>>
>> - jeremy
>
> +1
>
> I managed to do Tofte/Birkedal style region inference on TT once; but
> never got around to feeding it into the backend passes or back out
> through the IDE system.

To be clear: if you were just looking at region inference for memory
consumption purposes and had no desire to expose regions
syntactically, you want to infer regions after concrete arities are
inferred. A change in concrete arity can introduce an effect type in
region systems like the one I mentioned, which is why we struggled
with currying for so long in BitC.

*Maintaining* region and effect types through the
simplify/defunctionalise passes then is not simply a matter of
continuing to tag your terms with extra information, it's a careful
consideration of each of the transformations that get applied. Hence,
there's some work involved if you don't want to simply operate right
before the program is passed off to the backend.

[Jurriën Stutterheim]

Intuitively I would think it's possible to encode memory usage in a program's types somehow. That could give some static guarantees about memory usage. Though, I don't know if that would work. It definitely wouldn't be very pretty.

Uniqueness typing is indeed a great way to write more memory-efficient programs. We use it a lot in Clean. I suspect that any attempt at writing software for embedded devices will (have to) use uniqueness types extensively.

I'm afraid I can't really make any useful comments about region-inference, other than that various literature [1, 2] that I just found seems to suggest that it can result in some significant performance gains in both time and space. Still, from what I've read, one still requires a garbage collector to go alongside with regions, suggesting that a more memory-efficient GC is the (relatively) low-hanging fruit in this case.

[1] http://link.springer.com/article/10.1023%2FB%3ALISP.0000029446.78563.a4
[2] http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=9071620&fileId=S1471068412000075

[William ML Leslie]

On 20 November 2015 at 18:19, Jurriën Stutterheim <norm...@gmail.com> wrote:
> I'm afraid I can't really make any useful comments about region-inference, other than that various literature [1, 2] that I just found seems to suggest that it can result in some significant performance gains in both time and space. Still, from what I've read, one still requires a garbage collector to go alongside with regions, suggesting that a more memory-efficient GC is the (relatively) low-hanging fruit in this case.
>
> [1] http://link.springer.com/article/10.1023%2FB%3ALISP.0000029446.78563.a4
> [2] http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=9071620&fileId=S1471068412000075
>

Region analysis doesn't say anything about what you do with the result
of the analysis. There are region systems that work in tandem with
GC, such as that of MLKit (no relation), and there are region systems
in languages without GC, such as Cyclone, a variation of C. And
everything in between, I guess. Region analysis simply lets the
compiler determine if there is a well-determined site of
allocation/deallocation, allowing it to determine that references are
live before they are accessed. Sometimes people confuse region
analysis or region types with an implementation technique called
memory regions, which limits the scope that GC has to deal with in
some cases, but these are orthogonal concepts.

[Cliff L. Biffle]

On Wed, Nov 18, 2015 at 9:59 AM, Jurriën Stutterheim <norm...@gmail.com> wrote:

Inspired by the "Safety first: targeting embedded systems with full-spectrum dependent types" paper presented at TFP 2015, I was wondering whether it is possible to program Arduino(-like) hardware with Idris.

That paper mentions ATmega328P as a target, which is a common Arduino microcontroller.  So: yes, they are suggesting that it's possible, though their "paper" is awfully light on details.

(MSP430s are in the same class as the '328P, incidentally, with similar memory limitations.)

What I've done in the past for targeting machines that small is to implement a code-generating DSL, rather than a direct compiler.  Idris is particularly well-suited for this, IMHO, but there's previous work in the area in Haskell (e.g. Atom).  From their limited code samples, I can't tell whether this is the approach they've taken.

-Cliff