Home

Lightweight static resources

Lightweight static resources: Sexy types for embedded and systems programming. Oleg Kiselyov and Chung-chieh Shan.

It is an established trend to develop low-level code—embedded software, device drivers, and operating systems—using high-level languages, especially the advanced abstraction facilities in functional programming. To be reliable and secure, low-level
code must correctly manage space, time, and other resources, so special type systems and verification tools arose to regulate resource access statically. However, a general-purpose functional programming language practical today can provide the same static assurances, also with no run-time overhead. We substantiate this claim and promote the trend with two security kernels in the domain of device drivers:
1. one built around raw pointers, to track and arbitrate the size, alignment, write permission, and other properties of memory areas across indexing and casting;
2. the other built around a device register, to enforce protocol and timing requirements while reading from the register.
Our style is convenient in Haskell thanks to custom kinds and predicates (as type classes); type-level numbers, functions, and records (using functional dependencies); and mixed type- and term-level programming (enabling partial type signatures).


The related source code is also available.

Ken and Oleg's work is always worth checking out, so I urge LtU readers to go and see the solutions they propose aimed at allowing programmers of low level system software to work with raw pointers, device registers etc., while statically enforcing invariants such as pointer validity and in-bounds memory access.

The link is to a near final draft of a paper to be presented at TFP2007, and comments - I'm told - will be appreciated, especially as regards the "Related Work" section. Be quick with your comments, though, since the "camera ready" date is tomorrow...

By Ehud Lamm at 2007-03-08 12:50 | Functional | Software Engineering | Type Theory | other blogs | 12361 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Comments please!

Thanks for the publicity (: and let me emphasize that we would appreciate any comments or suggestions people might have, for both the draft proceedings and a final paper.

By Chung-chieh Shan at Thu, 2007-03-08 14:10 | login or register to post comments

Runtime

Having a good type system is certainly an enabler for haskell, but how is it supposed to be used for space constrained devices or anything close to real time? The garbage collector behavior is hard to track(regions would help) and the runtime is bigger than other similar languages like OCaml.

Would be nice if the paper at least briefly mentioned limitations/abilities of the haskell runtime footprint.

By taras at Thu, 2007-03-08 18:08 | login or register to post comments

different thing

I believe the paper talks about how to statically reason about resources manipulated by the program and ensure the correctness in certain properties, rather than the resources that one need to run the program with.

So this is different from reasoning about the behavior of runtime, i.e., how much heap space it consumes or how many CPU cycles it takes to execute a loop body.

I'd hope the paper can make this distiction more apparent though.

By ninegua at Thu, 2007-03-08 20:06 | login or register to post comments

Timber

Yet another example of resource-constraining of some computations is Tim-
ber [21], where timing constraints are attached only to monadic actions. Timber,
based on reactive objects and specifically aimed at real-time systems, is not strictly
speaking a general-purpose functional language.

(Pulled from Section 4).

What makes something qualify as a general purpose functional language? Does O'Haskell qualify?

By Peter A Jonsson at Thu, 2007-03-08 14:23 | login or register to post comments

Timing...

I've had a quick skim through your paper and wow! This is very impressive, I'd love to give you some decent feedback before your camera deadline but sadly I have a submission deadline in 4 days so I'll be too busy. I'll come back and post some proper feedback after the CHES deadline.

[Background: My PhD contained a timing verification system for embedded devices written in Haskell, as well as a logic-based synthesis tool. The project that I was working on at the time looked into static verification of resource usage, modelled in Prolog, and the research that I'm writing up at the moment is program transformation targetting a GPU]

By Andrew Moss at Thu, 2007-03-08 14:36 | login or register to post comments

Replies

Andrew Moss wrote: ``I'll come back and post some proper feedback
after the CHES deadline.''
We'll appreciate that indeed! The feedback will be very useful as we
prepare the presentation.

``I was working on at the time looked into static verification of
resource usage, modelled in Prolog..''
One can write Prolog-like programs in typeclasses, complete with
backtracking...

Peter A Jonsson wrote: ``What makes something qualify as a general
purpose functional language?'' I'd put that ``who makes the
language qualify as a general-purpose functional language''. The answer
is: the developers of the language. The web pages haskell.org or
ocaml.org state ``Haskell [Ocaml] is a general purpose ...'' in the
very first sentence. In contrast, the Timber Technical report is
entitled ``Timber: A programming language for real-time embedded
systems.'' Throughout the papers and technical reports the developers
of Timber emphasize the focus of the language on real-time
programming.

alanine wrote: ``I believe the paper talks about how to statically
reason about resources manipulated by the program and ensure the
correctness in certain properties, rather than the resources that one
need to run the program with.'' That is indeed the main focus of the
paper. When we write, for example, a user-land device driver -- or
even a system-land device driver (e.g., USB keyboard driver)
under Minix, we are not constrained that much by the memory footprint
of the driver; we still need to correctly manipulate memory areas,
device register ranges, respect alignment and endianness, etc. I
should also point to House (bare-metal OS written in Haskell), which
might benefit from our techniques.

Still, we believe our approach may be useful, albeit indirectly, if
the goal is truly to produce code for a memory constrained real-time
device. That device of course won't be running Haskell code. Rather,
Haskell code will generate the code for that device. We refer in the
paper, several times, to Conal Elliott's work on writing Haskell
programs that generate GPU codes. The type of a function emitting a
GPU instruction can be tagged with the number of cycles or other
resources the instruction may take. We can then statically track and
accumulate such resource bounds. In short, we can statically
reason about the generated code; by imposing type constraints on the
generator we can ensure that (just-in-time) generated code will
be within certain resource bounds.

I guess the paper didn't quite get these points across; we have to
work on it more. Thank you!

By Oleg at Fri, 2007-03-09 05:59 | login or register to post comments

Some comments

Ahh, the woosh of a deadline passing by...

This is a great paper. I've seen similar work in an entirely different context and there are some places where you hint at this direction. In particular when you describe the static type-system code as a "logic" language ontop of the run-time functional layer; in the logic community they are approaching this problem from the other side. CiaoPP layers several types of programming ontop of a logical core, and the constraint propagation used to provide static complexity proofs or type guarantees might be interesting for your future work.

I'm amazed that you've managed to make the Haskell type system do quite so much; do you have source code available for people to play with? During your presentation I would really emphasize that you've made this work entirely within Haskell without any sugar, or language extensions.

There's a small typo in the biliography - reference 16 is still blanked from the anonymous copy. Another small thing that is confusing is the use of gcd in checking address alignment - don't you mean the residue module 4/8/16 etc?

The comment at the end of section 2 reads as a little strange. The penultamate sentence about a programmer rendering the system unsafe, even though their program passes the type checks. Could you expand on this a little please? Do you mean that the contract that the program is held to is not tight enough, ie a particular sequence of register writes could crash the machine?

But other than those small niggles congratulations on a really solid paper. I hope that your presentation goes well.

By Andrew Moss at Wed, 2007-03-14 18:09 | login or register to post comments

Thank you for the comments

Thank you very much for your comments! The complete code is available,

http://pobox.com/~oleg/ftp/Computation/resource-aware-prog/

``There's a small typo in the bibliography - reference 16 is still
blanked from the anonymous copy.'' You mean refs 17 and 18, with the
key HW? These are the references to the proceedings of the Haskell
workshops as a whole; HW is my unfortunate cryptic choice for the
bibtex entry key.

``Another small thing that is confusing is the use of gcd in checking
address alignment - don't you mean the residue module 4/8/16 etc?''
Actually we took that (along with the whole driver example) from
Diatchki and Jones. I think the justification for that is that
k=gcd(n,m) is the largest integer such that
forall a. a=0 (mod n) implies a+m=0 (mod k) holds.

``The penultimate sentence about a programmer rendering the system
unsafe, even though their program passes the type checks.'' That
phrase was indeed confusing. We changed it a bit in the final version
(the version on my web site is updated too). We had in mind the
following example: the hardware manual may state that the video RAM
starts at the absolute address 0xb8000. I misread the manual and put
0xd8000 in the code. Running the code isn't going to produce a happy
result. Alas, no type system could have prevented it...

Thank you for the suggestions about the presentation and the pointer
to CiaoPP. Incidentally, Martin Sulzmann compellingly argues that
type-level programming should be exactly constraint logic
programming.

By Oleg at Thu, 2007-03-15 07:27 | login or register to post comments

haskell to C++ compiler ?

Are there any haskell to c/c++ compiler ? Many embedded OS, like Symbian, while quite powerful, don't have haskell, or even Lisp. With haskell to c++ compiler such work as that could be very useful, and not only for embedded...

By serg271 at Fri, 2007-03-09 06:08 | login or register to post comments

GHC

The GHC haskell compiler can emit C code for portability.

By Gavin Harrison at Fri, 2007-03-09 15:12 | login or register to post comments