## Archive for the ‘Haskell’ Category

### Viva La Resistance! A Resistance Game Solver

February 8, 2016

Update (Feb142016): see bottom for an improved strategy.

## The Game

At a December workshop, I played The Resistance, a game in which there are two teams, the resistance and the spies. The spies know everyone’s identity; each resistance player knows only one’s own. Overall, the goal of the spies is to remain undetected; the goal of the resistance is to discover who the spies are.

Play proceeds in rounds in which a player nominates a subgroup to go on a “mission”. The nomination is then voted on. If the vote succeeds, every member of a mission plays either a “success” or “failure” card for the mission. One or two failure cards (depending on the mission size) causes the mission to fail. The cards played in a mission are public, but it is secret who played which card. (If the vote fails, the next player nominates a subgroup.)

The spies’ goal is to fail missions without being detected, and the resistance goal is to have missions succeed. So the spies generally wish to play failure cards while in a mission. Furthermore, spies always want some spy in the mission to spoil it. The resistance wants no spies to go on missions. The problem for the resistance is that when a mission fails, they know one or more of the subgroup is a spy, they just don’t know which one.

The spies win the game if they can cause three missions to fail before the resistance can cause three missions to succeed.

The game is simple but engaging, and similar in spirit to the game Mafia (Werewolf).y

## The Problem

I played the game with computer scientists from the top universities and research labs. We debated strategy and were generally pretty bad at the game, despite having a lot of fun. In particular, the spies seemed to win a lot.

The problem is: what is the optimal approach to game play?

## The Approach

The problem is a great fit for Bayesian Analysis. In each round, we learn partial information about the players from the group outcome. Only spies play failure cards. We can use that information to update our believe in the probability that a player is a spy.

Suppose there are four players, $[ a, b, c, d]$ and two spies. Initially each player has the same probability of being a spy, $2/4 = 0.5$. Now suppose that $[ a, b, c ]$ go on a mission, and return the set of cards $\{Success, Fail, Fail\}$. How do we update the spy probabilities of the group?

Bayes Theorem states that

$P(A|B) = \dfrac{P(A)P(B|A)}{P(B)}$

In our case, “A” is the event that a particular player is a spy, and “B” is the event that we we observed a particular set of mission cards. We wish to compute $P(A|B)$, the updated probability that a player is a spy given the cards played in the mission.

So for each mission, we apply Bayes’ Theorem to each player, including the players not in the mission—if the spy probabilities increase (or decrease) for the mission players, then they decrease (or increase) for the non-mission players.

From the cards $\{Success, Fail, Fail\}$, we know that two of $[ a, b, c ]$ are spies (and so $d$ is definitely not a spy, since there are two spies, total). Let’s compute the updated spy probability for player $a$.

$P(A) = 0.5$, the original spy probability for player $a$ (or any other player). To calculate $P(B)$, we first determine every possible assignment of players in the mission to spies and non-spies (there are $\binom{2}{3}$ such assignments). In the mission, there are three possibilities:

1. spies $= [a, b]$
2. spies $= [a, c]$
3. spies $= [b, c]$

For each combination, we multiply the probabilities for the assignments. So in case (1), we have

$0.5(0.5)(1-0.5) = 1/8$

for assigning players $a$ and $b$ to being spies and c to being a non-spy. Then we sum the probabilities for all three combinations. In our example, we get

$\frac{1}{8} + \frac{1}{8} + \frac{1}{8} = \frac{3}{8}$

So $P(B) = 0.375$.

To compute P(B|A), we assume that player a is a spy, and now recompute the probability that $[b, c]$ contains the remaining one spy. Using the same approach as for computing $P(B)$, we get $P(B|A) = 0.5$. Now we can apply Bayes’ Theorem:

$\dfrac{0.5(0.5)}{0.375} = 2/3$

So player’s a probability of being a spy shot up to 0.66, and so did player b’s and c’s.

Player $d$‘s spy probability drops to 0. The updated spy probabilities for any player not in the mission can be computed just as we did for the mission players, except we take the total number of spies and subject the number of failure cards observed. In this case, however, since we know all the spies were in the group, $d$‘s spy probability must be 0. (Another way of thinking about it is that there is an invariant that the sum of the player’s spy probabilities must always be the total number of spies in the group.)

## The Strategies

How should the game be played by the resistance and spies, respectively, to increase the odds of winning?

For the resistance, picking the players the least likely to be spies is optimal. Let’s call this the pick-lowest strategy.

One possible optimization is to always pick yourself in a mission. The rational is that you know if you are part of the resistance, and you pick yourself for a mission, then you have at least one guaranteed non-spy. So even if your probability of being a spy as known to the group is higher than others, you have perfect knowledge of yourself. Let’s call this the pick-myself strategy,

For the spies, there are a few options. By default, the spies could always play a failure card (fail-always). But a spy might also play a success card to avoid detection; doing so is especially advantageous in the early rounds; one strategy is to never fail the first round (succeed-first). If the spies can collude to ensure only one plays a failure card during a mission, that provides the least amount of information to the resistance (fail-one).

There are other strategies and other combinations of strategies, but this is a good representative sample.

Which are the best strategies?

## Findings

To discover the best strategies, we use Monte-Carlo simulations on the strategies over each number of players (with different number of players, there are different number of spies and missions). I found a few interesting results:

• The best chance of wining for the resistance, and the closest odds between the resistance and spies, is with six players. At six players, the resistance has a 30-40% chance of winning under different strategies. The worst configuration is eight players, with not more than a 14% chance of winning for the resistance. During actual game play, it seemed that the odds favored the spies.
• The best strategy for the resistance is the pick-lowest strategy. The strategy may be counter-intuitive, but consider this: the pick-myself strategy provides the spies an opportunity to always include themselves in a mission when picking a mission. The pick-myself strategy is an instance of a local maxima (i.e., local knowledge of knowing yourself to be part of the resistance) that is non-optimal.
• Moreover, voting becomes a no-op. The game includes a voting round in which players vote on the proposed players for a mission. But If the resistance agrees on an optimal strategy, any deviation from the strategy by a player is because the player is a spy. If the person does deviation, the resistance votes against it (and resistance outnumber spies, so will win the vote), and we now have complete assurance the proposer is a spy. The spies have no choice but to follow the optimal strategy of the resistance.
• Of the spy strategies listed above, the best is the fail-one strategy, which is intuitive. The succeed-first strategy is another example of a local maxima that is non-optimal; while it protects that particular spy from detection, it is more valuable for the spies in general to fail the mission.

The related Mafia game has some analytical results, giving bounds on (their version of) the resistance to spies. I have not done that, nor have I done Monte-Carlo analysis to determine what proportion of resistance and spies and mission sizes gives a more even chance of winning. In Mafia, it is noted that in actual game play, the resistance wins more often than simulations/analytical analysis would suggest, with different attributions (e.g., people are bad at lying over iterative rounds).

## Play Along at Home

I have implemented the Bayesian solver in a webserver hosted on Amazon Web Services. You can use the solver when playing with others.

If you want to run Monte Carlo simulations, you will have to download the code and run it locally, however.

## Implementation

https://github.com/leepike/theresistance

## Update (Feb142016)

It has been pointed out by Eike Schulte in the comments and Iavor Diatchki that by including some additional information, the strategy might be improved. This is indeed the case. The intuition is that if a group has previously included a spy, that group should not be selected again, even if it is the lowest probability group. For example, with five players, consider the following rounds:

• Round 0: players [0,1] are selected and there is one fail card.
• Round 1: players [2,3,4] are selected and there is one fail card.
• Round 2: players [2,3] are selected and there are no fail cards.

At this point, players [0,1] have a 0.5 probability of being a spy and players [2,3,4] have a 1/3 probability. So in round 3, we do not want to select players [2,3,4] even if they have the lowest probabilities. So we select a group with the lowest spy probability that has not already included a spy. The server has been updated to include this strategy. The strategy does better; for example, at 6 players, we have just over a 50% chance of winning!

October 10, 2014

I wanted to try out a recent feature in GHC this week, so I was using HEAD. When I say using, I mean it: I wasn’t developing with it, but using it to build Ivory, our safe C EDSL, as well as some libraries written in Ivory. I want to point out a few dragons that lay ahead for others using HEAD (7.9.xxx) today.

• The Functor, Applicative, Monad hierarchy (as well as the Alternative and MonadPlus hierarchy) is no longer a warning but an error. You’ll be adding a lot of instances to library code.
• You’ll need to update Cabal, which comes as a submodule with the GHC sources. Unfortunately, building Cabal was a pain because of the bootstrapping problem. The bootstrap.sh script in cabal-install is broken (e.g., outdated dependency versions). Getting it to work involved using runhaskell directly, modifying a bunch of Cabal’s dependencies, and getting a little help from Iavor Diatchki.
• Some of the datatypes in Template Haskell have changed; notably, the datatypes for creating class constraints have been folded into the datatype for constructing types (constraint kinds!). Many libraries that depend on Template Haskell breaks as a result.
• I won’t mention the issues with package dependency upper bounds. Oops, I just did.

Fortunately, once Cabal is updated, Cabal sandboxes work just fine. I wrote a simple shell script to swap out my sandboxes to switch between GHC versions. (It would be a nice feature if Cabal recognized you are using a different version of GHC than the one the cabal sandbox was originally made and created a new sandbox automatically.)

Because I’m on OSX and use Homebrew, I tried using it to manage my GHC versions, including those installed with Brew and those built and installed manually. It works great. When building GHC, configure it to install into your Cellar, or wherever you have Brew install packages. So I ran

> ./configure --prefix=/usr/local/Cellar/ghc/7.9

which makes Brew aware of the new version of GHC, despite being manually installed. After it’s installed,

> brew switch ghc 7.9

takes care of updating all your symbolic links. No more making “my-ghc-7.9” symbolic links or writing custom shell scripts.

### SmartChecking Matt Might’s Red-Black Trees

August 20, 2014

Matt Might gave a nice intro to QuickCheck via testing red-black trees recently. Of course, QuickCheck has been around for over a decade now, but it’s still useful (if underused–why aren’t you QuickChecking your programs!?).

In a couple of weeks, I’m presenting a paper on an alternative to QuickCheck called SmartCheck at the Haskell Symposium.

SmartCheck focuses on efficiently shrinking and generalizing large counterexamples. I thought it’d be fun to try some of Matt’s examples with SmartCheck.

The kinds of properties Matt Checked really aren’t in the sweet spot of SmartCheck, since the counterexamples are so small (Matt didn’t even have to define instances for shrink!). SmartCheck focuses on shrinking and generalizing large counterexamples.

Still, let’s see what it looks like. (The code can be found here.)

SmartCheck is only interesting for failed properties, so let’s look at an early example in Matt’s blog post where something goes wrong. A lot of the blog post focuses on generating sufficiently constrained arbitrary red-black trees. In the section entitled, “A property for balanced black depth”, a property is given to check that the path from the root of a tree to every leaf passes through the same number of black nodes. An early generator for trees fails to satisfy the property.

To get the code to work with SmartCheck, we derive Typeable and Generic instances for the datatypes, and use GHC Generics to automatically derive instances for SmartCheck’s typeclass. The only other main issue is that SmartCheck doesn’t support a forall function like in QuickCheck. So instead of a call to QuickCheck such as

 > quickCheck (forAll nrrTree prop_BlackBalanced) 

We change the arbitrary instance to be the nrrTree generator.

Because it is so easy to find a small counterexample, SmartCheck’s reduction algorithm does a little bit of automatic shrinking, but not too much. For example, a typical minimal counterexample returned by SmartCheck looks like

 T R E 2 (T B E 5 E) 

which is about as small as possible. Now onto generalization!

There are three generalization phases in SmartCheck, but we’ll look at just one, in which a formula is returned that is universally quantified if every test case fails. For the test case above, SmartCheck returns the following formula:

 forall values x0 x1: T R E 2 (T B x1 5 x0) 

Intuitively, this means that for any well-typed trees chosen that could replace the variables x0 and x1, the resulting formula is still a counterexample.

The benefit to developers is seeing instantly that those subterms in the counterexample probably don’t matter. The real issue is that E on the left is unbalanced with (T B E 5 E) on the right.

One of the early design decisions in SmartCheck was focus on structurally shrinking data types and essentially ignore “base types” like Int, char, etc. The motivation was to improve efficiency on shrinking large counterexamples.

But for a case like this, generalizing base types would be interesting. We’d hypothetically get something like

 forall values (x0, x1 :: RBSet Int) (x2, x3 :: Int): T R E x2 (T B x1 x3 x0) 

further generalizing the counterexample. It may be worth adding this behavior to SmartCheck.

SmartCheck’s generalization begins to bridge the gap from specific counterexamples to formulas characterizing counterexamples. The idea is related to QuickSpec, another cool tool developed by Claessen and Hughes (and SmallBone). Moreover, it’s a bridge between testing and verification, or as Matt puts it, from the 80% to the 20%.

### SmartCheck: Redux

June 16, 2014

A few years ago, I started playing with the idea of making counterexamples from failed tests easier to understand. (If you’re like me, you spend a lot of time debugging.) Specifically, I started from QuickCheck, a test framework for Haskell, which has since been ported to many other languages. From this, a tool called SmartCheck was born.

In this post, I’m not going to describe the technical details of SmartCheck. There’s a paper I wrote for that, and it was just accepted for publication at the 2014 Haskell Symposium (warning: the paper linked to will change slightly as I prepare the final version).

Rather, I want to give a bit of perspective on the project.

As one reviewer for the paper noted, the paper is not fundamentally about functional programming but about testing. This is exactly right. From the perspective of software testing in general, I believe there are two novel contributions (correct me ASAP if I’m wrong!):

1. It combines counterexample generation with counterexample reduction, as opposed to delta-debugging-based approaches, which performs deterministic reduction, given a specific counterexample. One possible benefit is SmartCheck can help avoid stopping at local minima during reduction, since while shrinking, new random values are generated.  Update: as John Regehr points out in the comments below, his group has already done this in the domain of C programs.  See the paper.
2. Perhaps the coolest contribution is generalizing sets of counterexamples into formula that characterize them.

I’d be interested to see how the work would be received in the software testing world, but I suppose first it’d need to be ported to a more mainstream language, like C/C++/Java.

Compared to QuickCheck specifically, QuickCheck didn’t used to have generics for implementing shrinking functions; recent versions include it, and it’s quite good. In many cases, SmartCheck outperforms QuickCheck, generating smaller counterexamples faster.  Features like counterexample generalization are unique to SmartCheck, but being able to test functions is unique to QuickCheck. Moreover, I should say that SmartCheck uses QuickCheck in the implementation to do some of the work of finding a counterexample, so thanks, QuickCheck developers!

When you have a tool that purports to improve on QuickCheck in some respects, it’s natural to look for programs/libraries that use QuickCheck to test it. I found that surprisingly few Hackage packages have QuickCheck test suites, particularly given how well known QuickCheck is. The one quintessential program that does contain QuickCheck tests is Xmonad, but I challenge you to think of a few more off the top of your head! This really is a shame.

The lack of (public) real-world examples is a challenge when developing new testing tools, especially when you want to compare your tool against previous approaches. More generally, in testing, it seems there is a lack of standardized benchmarks. What we really need is analogue of the SPEC CPU2000 performance benchmarks for property-based testing, in Haskell or any other language for that matter.  I think this would be a great contribution to the community.

In 1980, Boyer and Moore developed a linear-time majority vote algorithm and verified an implementation of it. It took until 1991 to publish it after many failed tries. Indeed, in the decade between invention and publication, others had generalized their work, and it being superseded was one of the reasons reviewers gave for rejecting it! (The full story can be found here.)

To a small extent, I can empathize. I submitted a (slightly rushed) version of the paper a couple years ago to ICFP in what was a year of record submissions. One reviewer was positive, one luke-warm, and one negative. I didn’t think about the paper much over the following year or two, but I got a couple of requests to put the project on Hackage, a couple of reports on usage, and a couple of inquiries about how to cite the draft paper. So after making a few improvements to the paper and implementation, I decided to try again to publish it, and it finally will be.

As I noted above, this is not particularly a Haskell paper. However, an exciting aspect of the Haskell community, and more generally, the functional programming community, is that it is often exploring the fringes of what is considered to be core programming language research at the time. I’m happy to be part of the fringe.

### SMACCMPilot

October 7, 2013

Over on the Galois blog is a post about my current project, building a secure high-assurance autopilot called SMACCMPilot.  SMACCMPilot is open-source; http://smaccmpilot.org/ is the project’s landing page that describes the technologies going into the project with links to the software repositories.  Check it out!

Galois’ main approach to building SMACCMPilot is to use embedded domain-specific languages (EDSLs), embedded in Haskell that compile down to restricted versions of C.  (If you’re not familiar with the “EDSL approach”, and particularly how it might improve the assurance of your systems, check out this paper we wrote about our experiences on a separate NASA-sponsored project.)  The project is quickly approaching one of the larger EDSL projects I know about, and it’s still relatively early in its development.  The EDSLs we’re developing for SMACCMPilot, Ivory (for embedded C code generation) and Tower (for OS task setup and communication), are suitable for other embedded systems projects as well.

Like many young and active open-source projects, the code is hot off the presses and under flux, and the documentation always lags the implementation, so let me know if you try using any of the artifacts and have problems.  We’re happy to have new users and contributors!

### Lowering the Bar

October 2, 2012

I gave a talk (video, slides, and paper) at ICFP last month, arguing that it can be easy to build a high-assurance compiler. I gave a similar talk as a keynote a couple weeks later at the very enjoyable Midwest Verification Day, hosted by Kansas University this year (thanks Andy Gill and Perry Alexander for inviting me!). This paper wraps up the Copilot project. I had a great time (I mean, how often do formal methods engineers get to be around NASA subscale jet aircraft?!?).

### SmartCheck

July 26, 2012

I’ve been working on a Haskell library for testing Haskell programs I call SmartCheck. SmartCheck is focused on testing algebraic data and generalizing counterexamples found. Below is the README for SmartCheck, which I have located on GitHub (I haven’t put it on Hackage yet). The following is a high-level explanation that doesn’t go into details about the algorithms or implementation (that’s another post!).

I’d be interested in feedback on

• Real-world examples to try SmartCheck on.
• Whether there are other interesting ways to generalize counterexamples.
• If there’s similar work out there I should know about (in addition to QuickCheck and SmallCheck.
• Your experiences, if you try the library out.

Thanks!

## Synopsis

SmartCheck is a smarter QuickCheck, a powerful testing library for Haskell. The purpose of SmartCheck is to help you more quickly get to the heart of a bug and to quickly discover each possible way that a property may fail.

SmartCheck is useful for debugging programs operating on algebraic datatypes. When a property is true, SmartCheck is just like QuickCheck (SmartCheck uses QuickCheck as a backend). When a property fails, SmartCheck kicks into gear. First, it attempts to find a minimal counterexample to the property is a robust, systematic way. (You do not need to define any custom shrink instances, like with QuickCheck, but if you do, those are used. SmartCheck usually can do much better than even custom shrink instances.) Second, once a minimal counterexample is found, SmartCheck then attempts to generalize the failed value d by replacing d‘s substructures with new values to make d', and QuickChecking each new d'. If for each new d' generated, the property also fails, we claim the property fails for any substructure replaced here (of course, this is true modulo the coverage of the tests).

SmartCheck executes in a real-eval-print loop. In each iteration, all values that have the “same shape” as the generalized value are removed from possible created tests. The loop can be iterated until a fixed-point is reached, and SmartCheck is not able to create any new values that fail the property.

## A typical example

In the package there is an examples directory containing a number of examples. Let’s look at the simplest, Div0.hs.

> cd SmartCheck/examples
> ghci -Wall Div0.hs


Div0 defines a toy language containing constants (C), addition (A), and division (D):

data M = C Int
| A M M
| D M M


Because SmartCheck performs data-generic operations using GHC.Generics we have to derive Typeable and Generic. To use GHC.Generics, you also need the following pragmas: and the single automatically-derived instance:

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}

instance SubTypes M


Let’s say we have a little interpreter for the language that takes care to return Nothing if there is a division by 0:

eval :: M -> Maybe Int
eval (C i) = Just i
eval (A a b) = do
i <- eval a
j <- eval b
return $i + j eval (D a b) = if eval b == Just 0 then Nothing else do i <- eval a j <- eval b return$ i div j


Now suppose we define a set of values of M such that they won’t result in division by 0. We might try the following:

divSubTerms :: M -> Bool
divSubTerms (C _)       = True
divSubTerms (D _ (C 0)) = False
divSubTerms (A m0 m1)   = divSubTerms m0 && divSubTerms m1
divSubTerms (D m0 m1)   = divSubTerms m0 && divSubTerms m1


So our property (tries) to state that so long as a value satisfies divSubTerms, then we won’t have division by 0 (can you spot the problem in divSubTerms?):

div_prop :: M -> Property
div_prop m = divSubTerms m ==> eval m /= Nothing


Assuming we’ve defined an Arbitrary instance for M (just like in QuickCheck—however, we just have to implement the arbitrary method; the shrink method is superfluous), we are ready to run SmartCheck.

divTest :: IO ()
divTest = smartCheck args div_prop
where
args = scStdArgs { qcArgs   = stdArgs
, treeShow = PrintString }


In this example, we won’t redefine any of QuickCheck’s standard arguments, but it’s certainly possible. the treeShow field tells SmartCheck whether you want generalized counterexamples shown in a tree format or printed as a long string (the default is the tree format).

Ok, let’s try it. First, SmartCheck just runs QuickCheck:

*Div0> divTest
*** Failed! Falsifiable (after 7 tests):
D (D (D (A (C (-20)) (D (D (C 2) (C (-19))) (C (-8)))) (D (D (C (-23)) (C 32)) (C (-7)))) (A (A (C 2) (C 10)) (A (C (-2)) (C 13)))) (D (A (C 12) (C (-7))) (D (A (C (-29)) (C 19)) (C 30)))


Oh, that’s confusing, and for such a simple property and small datatype! SmartCheck takes the output from QuickCheck and tries systematic shrinking for the one failed test-case, kind of like SmallCheck might. We get the following reduced counterexample:

*** Smart Shrinking ...
*** Smart-shrunk value:
D (C 0) (D (C 0) (C (-1)))


Ok, that’s some progress! Now SmartCheck attempts to generalize this (local) minimal counterexample. SmartCheck has two generalization steps that we’ll explain separately although SmartCheck combines their results in practice (you can turn off each kind of generalization in the flags). First, SmartCheck tries to generalize values in the shrunk counterexample. SmartCheck returns

*** Extrapolating values ...
*** Extrapolated value:
forall x0:

D x0 (D (C 0) (C (-1)))


Ahah! We see that for any possible subvalues x0, the above value fails. Our precondition divSubTerms did not account for the possibility of a non-terminal divisor evaluating to 0; we only pattern-matched on constants.

In addition, SmartCheck tries to do something I call constructor generalization. For a datatype with a finite number of constructors, the idea is to see if for each subvalue in the counterexample, there is are subvalues that also fail the property, using every possible constructor in the datatype. So for example, for our counterexample above

*** Extrapolating constructors ...
*** Extrapolated value:
forall C0:
there exist arguments s.t.

D (C 0) (D C0 (C (-1)))


So in the hole C0, SmartCheck was able to build a value using each of the constructors C, A, and D (well, it already knew there was a value using CC 0.

SmartCheck asks us if we want to continue:

Attempt to find a new counterexample? ('Enter' to continue; any character
then 'Enter' to quit.)


SmartCheck will omit any term that has the “same shape” as D (C 0) (D (C 0) (C (-1))) and try to find a new counterexample.

*** Failed! Falsifiable (after 9 tests):
A (A (D (C (-20)) (A (C (-5)) (C (-32)))) (D (A (C 6) (C 19)) (A (C (-3)) (A (C (-16)) (C (-13)))))) (D (C 29) (D (C (-11)) (D (C 11) (C 23))))

*** Smart Shrinking ...
*** Smart-shrunk value:
A (C (-1)) (D (A (C 1) (C 1)) (D (C 1) (C 2)))

*** Extrapolating values ...

*** Extrapolating Constructors ...

*** Extrapolated value:
forall values x0 x1:

A x1 (D x0 (D (C 1) (C 2)))


We find another counterexample; this time, the main constructor is addition.

We might ask SmartCheck to find another counterexample:

...

*** Extrapolating ...
*** Could not extrapolate a new value; done.


At this point, SmartCheck can’t find a newly-shaped counterexample. (This doesn’t mean there aren’t more—you can try to increase the standard arguments to QuickCheck to allow more failed test before giving up (maxDiscard) or increasing the size of tests (maxSize). Or you could simply just keep running the real-eval-print loop.)

November 26, 2011

Stable names in GHC “are a way of performing fast (O(1)), not-quite-exact comparison between objects.”  Andy Gill showed how to use them to extract the explicit graph from writing recursive functions in his Data.Reify package (and associated paper).  It’s a great idea and very practical for embedded domain-specific languages—we’ve used the idea in Copilot to recover sharing.

However, consider this example, with three tests executed in GHCI.

For a function with type constraints, stable names fails to “realize” that we are pointing to the same object. As a couple of my colleagues pointed out, the cause is the dictionary being passed around causing new closures to be created. Simon Marlow noted that if you compile with -O, the explicit dictionaries get optimized away.

Here are the solutions I have to “fixing” the problem, in the context of a DSL:

• Tell your users that recursive expressions must be monomorphic—only “pure functions” over the expressions of your DSL can be polymorphic.
• Implement a check in your reifier to see how many stable names have been created—if some upper-bound is violated, then the user has created an infinite expression, the expression is extremely large (in which case the user should try to use some sharing mechanism, such as let-expressions inside the language), or we’ve hit a stable-names issue.
• Ensure your DSL programs are always compiled.
• Of course, you can always take another approach, like Template Haskell or not using recursion at the Haskell level; also check out Andy Gill’s paper for other solutions to the observable sharing problem.

I don’t see how to use (deep)seq to fix the problem, at least as it’s presented in the example above, but I’d be keen to know if there are other solutions.

### Meta-Programming and eDSLs

January 30, 2011

I’ve been working on a domain-specific language that is embedded in Haskell (an “eDSL”) that essentially takes a set of Haskell stream (infinite list) equations and turns them into a real-time C program implementing the state-machine defined by the streams. It’s called Copilot, and in fact, it’s built on top of another Haskell eDSL called Atom,1 which actually does the heavy lifting in generating the C code.

For example, here’s the Fibonacci sequence in Copilot:

fib = do let f = varW64 "f" f .= [0,1] ++ f + (drop 1 f) 

I’ve been writing Copilot libraries recently, and I’ve had the following realization about eDSLs and meta-programming (let me know if someone has had this idea already!). Many languages treat meta-programming as a second-class feature—I’m thinking of macros used by the C preprocessor, for example (it’s probably generous even to call the C preprocessor ‘meta-programming’). One reason why Lisp-like languages were exciting is that the language is a first-class datatype, so meta-programming is on par with programming. In my experience, you don’t think twice about meta-programming in Lisp. (Haskell is more like C in this regard—you do think twice before using Template Haskell.)

So languages generally treat meta-programming as either second-class or first-class. What’s interesting about eDSLs, I think, is that they treat meta-programming as first-class, but programming as second-class! This isn’t surprising, since an eDSL is a first-class datatype, but the language is not first-class—its host language is.

Practically, what this means is that you spend very little time actually writing eDSL programs but rather generating eDSL programs. It is natural to layer eDSLs on top of other eDSLs.

This is just how Copilot came about: I was writing various Atom programs and realized that for my purposes, I just needed a restricted set of behaviors provided by Atom that are naturally represented by stream equations (and make some other tasks, like writing an interpreter, easier).

But as soon as Copilot was written, we2 started writing libraries implementing past-time linear temporal logic (LTL) operators, bounded LTL operators, fault-tolerant voting algorithms, regular expressions, and so on.

You wouldn’t think about combining the intermediate languages of a compiler into the same program. The idea of a language is more fluid, more organic in the context of eDSLs, where now libraries can be quickly written and different levels can be easily combined.

1Tom Hawkins wrote Atom.
2Credit for Copilot also goes to Sebastian Niller, Robin Morisset, Alwyn Goodloe.

### Haskell and Hardware for the Holidays

December 18, 2010

Looking to make a statement this holiday season?  You could try to win the office “ugly holiday sweater” contest.  Or, you could play “Jingle Bells” on your Arduino microcontroller, using Haskell.  This post is about the latter.

We’re going to write this small program using the Copilot embedded domain-specific language (on Hackage and the source on Github).  Copilot is a stream language that allows you to generate embedded C code from programs written essentially as Haskell lists (using Atom as a backend for the C code generation).  This post is about how to use Copilot/Haskell (v. 1.0) to make your embedded C programming easier and more likely to be correct.  Here’s what we’re going to do—please don’t look too closely at my soldering, and turn the volume up, since a piezo speaker isn’t loud:

(For the impatient, the Haskell file is here, and the generated .c and .h files are here and here, respectively.)

We’re going to essentially recreate this C/Wiring program, plus flash some LEDs, but hopefully in a easier, safer way.  We need to manage three tasks:

1. Determine the note and number of beats to play.
2. Play the piezo speaker.
3. Flash the LEDs.

We’ll start by defining which pins control what function:

-- pin numbers
speaker, red, green :: Spec Int32
speaker = 13
red     = 12
green   = 11

The type Spec Int32 takes an Int32 and lifts it into a Copilot expression.

We’ll call the program cycleSong. The type of a Copilot program is Streams, which is a collection of Spec as, and it resides within the Writer Monad. First, we’ll declare some variables.

cycleSong :: Streams
cycleSong = do
-- Copilot vars
let idx       = varI32 "idx"
notes     = varI32 "notes"
duration  = varI32 "duration"
odd       = varI32 "odd"
even      = varI32 "even"
playNote  = varB   "playNote"
-- external vars
note = extArrI32 "notes" idx
beat = extArrI32 "beats" idx

There are two classes of variables: Copilot variables that will refer to streams (infinite lists), and external variables, which can refer to data from C (including the return values of functions, global variables, and arrays). The constructors are mnemonics for the type of the variables; for example, varI32 is a variable that will refer to a stream of Int32s. Similarly, extArrI32 is an external variable referring to a C array of Int32s (i.e., int32_t). Notice the idx argument—it is the stream of values from which the index into the array is drawn (constants can also be used for indexes).

Now for the actual program:

 idx      .= [0] ++ (idx + 1) mod (fromIntegral $length notesLst) notes .= note duration .= beat * 300 odd .= mux (idx mod 2 == 1) green red even .= mux (idx mod 2 == 1) red green playNote .= true -- triggers trigger playNote "digitalWrite" (odd <> true) trigger playNote "digitalWrite" (even <> false) trigger playNote "playtone" (speaker <> notes <> duration) And that’s basically it. There are two parts to the program, the definition of Copilot streams, which manage data-flow and control, and triggers, which call an external C function when some property is true. Copilot streams look pretty much like Haskell lists, except that functions are automatically lifted to the stream level for convenience. Thus, instead of writing,  x = [0] ++ map (+1) x in Copilot, you simply write  x .= [0] ++ x + 1 Similarly for constants, so the Copilot stream definition playNote .= true lifts the constant true to an infinite stream of true values. The function mux is if then elsemux refers to a 2-to-1 multiplexer. So that means that the stream odd takes the value of green when idx is odd, and red otherwise, where green and red refer to the pins controlling the respective LEDs. Just to round out the description of the other defined streams, idx is the index into the C arrays containing the notes and beats, respectively—that’s why we perform modular arithmetic. The stream duration tells us how long to hold a note; 300 is a magic “tempo” constant. Now for the triggers. Each of our triggers “fires” whenever the stream playNote is true; in our case, because it is a constant stream of trues, this happens on each iteration. So on each iteration, the C functions digitalWrite and playTone are called with the respective function arguments (‘<>‘ separates arguments). The function digitalWrite is a function that is part of the Wiring language, which is basically C with some standard libraries, from which digitalWrite comes. We’ll write playTone ourselves in a second. ## The C Code We need a little C code now. We could write this directly, but we’ll just do this in Haskell, since there’s so little we need to write—the Copilot program handles most of the work. But a caveat: it’s a little ugly, since we’re just constructing Haskell strings. Here are a few functions (included with Copilot) to make this easier, and here are some more. (If someone properly writes a package to write ad-hoc C code from Haskell, please leave a comment!) First, we need more magic constants to give the frequency associated with notes (a space is a rest). freq :: Char -> Int32 freq note = case note of 'c' -> 1915 'd' -> 1700 'e' -> 1519 ...  and here are the notes of the song and the beats per note: jingleBellsNotes = "eeeeeeegcdefffffeeeddedgeeeeeeegcdefffffeeggfdc" jingleBellsBeats = [ 1,1,2 , 1,1,2, 1,1,1,1, 4 , 1,1,1,1, 1,1,2, 1,1,1,1, 2,2 , 1,1,2 , 1,1,2, 1,1,1,1, 4 , 1,1,1,1, 1,1,2, 1,1,1,1, 4 ] The other main piece of C code we need to write is the function playtone. The piezo speaker is controlled by pulse width modulation, basically meaning we’ll turn it on and off really fast to simulate an analogue signal. Here is it’s definition (using a little helper Haskell function to construct C functions):  [ function "void" "playtone" ["int32_t speaker", "int32_t tone", "int32_t duration"] P.++ "{" , "#ifdef CBMC" , " for (int32_t i = 0; i < 1; i ++) {" , "#else" , " for (int32_t i = 0; i < duration * 1000; i += tone * 2) {" , "#endif" , " digitalWrite(speaker, HIGH);" , " delayMicroseconds(tone);" , " digitalWrite(speaker, LOW);" , " delayMicroseconds(tone);" , " }" , "}" ] HIGH, LOW, digitalWrite, and delayMicroseconds are all part of the Wiring standard library. That ifdef is for verification purposes, which we’ll describe in just a bit. Besides a little more cruft, that’s it! ## Test, Build, Verify “Jersey Shore” may have introduced you to the concept of gym, tan, laundry, but here we’ll stick to test, build, verify. That is, first we’ll test our program using the Copilot interpreter, then we’ll build it, then we’ll prove the memory safety of the generated C program. • Interpret. We define a function that calls the Copilot interpreter: interpreter = interpret cycleSong 20$ setE (emptySM {i32Map = fromList [ ("notes", notesLst)
, ("beats", beatsLst)]})
baseOpts

This calls the Copilot interpreter, saying to unroll cycleSong 20 times. Because the Copilot program samples some external C values, we need to provide that data to the interpreter. Fortunately, we have those arrays already defined as Haskell lists. Executing this, we get the following:

period: 0   duration: 300   even: 11   idx: 0   notes: 1519   odd: 12   playNote: 1
period: 1   duration: 300   even: 12   idx: 1   notes: 1519   odd: 11   playNote: 1
period: 2   duration: 600   even: 11   idx: 2   notes: 1519   odd: 12   playNote: 1
period: 3   duration: 300   even: 12   idx: 3   notes: 1519   odd: 11   playNote: 1
period: 4   duration: 300   even: 11   idx: 4   notes: 1519   odd: 12   playNote: 1
period: 5   duration: 600   even: 12   idx: 5   notes: 1519   odd: 11   playNote: 1
period: 6   duration: 300   even: 11   idx: 6   notes: 1519   odd: 12   playNote: 1
. . .

Good, it looks right. (period isn’t a Copilot variable but just keeps track of what round we’re on.)

• Build. To build, we generate the C code from the Copilot program, then we’ll use a cross-compiler targeting the ATmega328. The easiest way (I’ve found) is via Homin Lee’s Arscons. Arscons is based on Scons, a Python-based build system. Arscons makes three assumptions: (1) the program is written as a Wiring program (e.g., there’s a loop() function instead of a main() function is the main difference), (2) the extension of the Wiring program is .pde, and (3) the directory containing the XXX.pde is XXX. For us, all that really means is that we have to change the extension of the generated program from .c to .pde. So we define
main :: IO ()
main = do
compile cycleSong name
$setPP cCode -- C code for above/below the Copilot program$ setV Verbose -- Verbose compilation
baseOpts
copyFile (name P.++ ".c") (name P.++ ".pde") -- SConstruct expects .pde

and then execute

> runhaskell CopilotSong.hs

to do this.

To build the executable, we issue

> scons

then

scons upload

when we’re ready to flash the microcontroller.

• Verify. Is the generated C program memory safe?  Wait… What do I mean by ‘memory safe’?  I’ll consider the program to be memory safe if the following hold:
• No arithmetic underflows or overflows.
• No floating-point not-a-numbers (NaNs).
• No division by zero.
• No array bounds underflows or overflows.
• No Null pointer dereferences.

Of course this is an approximates memory-safety, but it’s a pretty good start. If the compiler is built correctly, we should be pretty close to a memory-safe program. But we want to check the compiler, even though Haskell’s type system gives us some evidence of guarantees already. Furthermore, the compiler knows nothing about arbitrary C functions, and it doesn’t know how large external C arrays are.

We can prove that the program is memory safe. We call out to CBMC, a C model-checker developed primarily by Daniel Kröning. This is whole-program analysis, so we have to provide the location of the libraries. We define

verifying :: IO ()
verifying =
verify (name P.++ ".c") (length notesLst * 4 + 3)
(     "-DCBMC -I/Applications/Arduino.app/Contents/Resources/Java/hardware/arduino/cores/arduino/ "
P.++ "-I/Applications/Arduino.app/Contents/Resources/Java/hardware/tools/avr/avr-4/include "
P.++ "--function cbmc")

which calls cbmc on our generated C program. Let me briefly explain the arguments. First we give the name of the C program.

Then we say how many times to unroll the loops. This requires a little thinking. We want to unroll the loops enough times to potentially get into a state where we might have an out of bounds array access (recall that the Copilot stream idx generates indexes into the arrays). The length of the C arrays are given by length notesLst. When compiling the Copilot program (calling the module’s main function, a periodic schedule is generated for the program). From the schedule, we can see that idx is updated every fourth pass through the loop. So we unwind it enough loop passes for the counter to have the opportunity to walk off the end of the array, plus a few extra passes for setup. This is a minimum bound; you could of course over-approximate and unroll the loop, say, 1000 times.

Regarding loop unrolling, remember that #ifdef from the definition of playtone()? We include that to reduce the difficulty of loop unrolling. playtone() gets called on every fourth pass through the main loop, and unrolling both loops is just too much for symbolic model-checking (at least on my laptop). So we give ourselves an informal argument that the loop in playtone() won’t introduce any memory safety violations, and the #ifdef gives us one iteration through the loop if we’re verifying the system. A lot of times with embedded code, this is a non-issue, since loops can just be completely unrolled.

The -D flag defines a preprocessor macro, and the -I defines a include path. Finally, the --function flag gives the entry point into the program. Because we generated a Wiring program which generates a while(1) loop for us through macro magic, we have to create an explicit loop ourselves for verification purposes.

If you’re interested in seeing what things look like when they fail, change the idx stream to be

  idx .= [0] ++ (idx + 1)


and cbmc will complain

Violated property:
file CopilotSing.c line 180 function __r11
array beats' upper bound
(long int)__1 < 47

VERIFICATION FAILED


So that’s it. Happy holidays!

November 20, 2010

A lot has been going on since the announcement of Copilot, a Haskell DSL for generating hard real-time C monitors. We’ve presented Copilot a few times, including at Runtime Verification 2010, at a Galois Technical Seminar (video of the talk is here), and at a recent NASA Technical Interchange.

Copilot has had five releases since we originally open-sourced the project.  Recent work has focused on making the language more straightforward and improving Copilot libraries.  But first, let me remind you how to use Copilot: you can compile specs to hard real-time C code, you can interpret them, you can model-check them, and you can generate specs to test the compiler and interpreter—you can see a bit about usage here.

For example, here’s a Copilot specification that generates the Fibonacci sequence (over Word64s) and tests for even numbers:

fib :: Streams
fib = do
let f = varW64 "f"
let t = varB "t"
f .= [0,1] ++ f + (drop 1 f)
t .= even f
where even :: Spec Word64 -> Spec Bool
even w' = w' mod 2 == 0

Notice that lists look almost exactly like Haskell lists.

What about something a little more complicated?  Consider the property:

If the temperature rises more than 2.3 degrees within 2 seconds, then the engine has been shut off.

We might use a Copilot specification like the following to express it, assuming that temp and shutoff are C variables being sampled at phases 1 and 2 respectively, and the period of execution is 1 second:

engine :: Streams
engine = do
-- external vars
let temp     = extF "temp" 1
let shutoff  = extB "shutoff" 2
-- Copilot vars
let temps    = varF "temps"
let overTemp = varB "overTemp"
let trigger  = varB "trigger"
-- Copilot specification
temps    .= [0, 0, 0] ++ temp
overTemp .= drop 2 temps > 2.3 + temps
trigger  .= overTemp ==> shutoff

Here’s something that I think shows why you want to write your DSLs in Haskell: Haskell gives you a macro language for your DSL… for free.  For example, consider the following (more complicated) property:

“If the engine temperature exeeds 250 degrees, then the engine is shut off within one second, and in the 0.1 second following the shutoff, the cooler is engaged and remains engaged.”

We can more succinctly specify this property using past-time linear temporal logic (ptLTL).  There’s a Copilot library for writing those kind of specs, which can be interspersed with normal Copilot streams—the ptLTL specs are highlighted in blue below.  Again, assume a period of execution of 1 second:

engine :: Streams
engine = do
-- external vars
let engineTemp = extW8 "engineTemp" 1
let engineOff  = extB "engineOff" 1
let coolerOn   = extB "coolerOn" 1
-- Copilot vars
let cnt        = varW8 "cnt"
let temp       = varB "temp"
let cooler     = varB "cooler"
let off        = varB "off"
let monitor    = varB "monitor"
-- Copilot specification
temp    ptltl (alwaysBeen (engineTemp > 250))
cnt     .=      [0] ++ mux (temp && cnt < 10) (cnt + 1) cnt
off     .=      cnt >= 10 ==> engineOff
cooler  ptltl (coolerOn since engineOff)
monitor .=      off && cooler

Today, I finished updating another feature of Copilot: the ability to send stream values over ports to other components in a distributed system. We had an implementation of this, but it was a bit hacky. Hopefully, it’s a bit less hacky now. For example, consider the following specification:

distrib :: Streams
distrib = do
-- Copilot vars
let a = varW8 "a"
let b = varB "b"
-- Copilot spec
a .= [0,1] ++ a + 1
b .= mod a 2 == 0
-- send commands
send "portA" (port 2) a 1
send "portB" (port 1) b 2

The blue commands are send commands.  For example, the first command says, “call the C function portA(str, num), where argument str is the value of stream a and num is port number 1.” The port number says who to send it to.

These are just a few of the recent updates. We’re still working on Copilot, so let me know if you have questions or comments.

Interested? Get Copilot on Hackage or GitHub.

### Copilot: a DSL for Monitoring Embedded Systems

September 25, 2010

In case you missed all the excitement on the Galois blog, what follows is a re-post.

# Introducing Copilot

Can you write a list in Haskell? Then you can write embedded C code using Copilot. Here’s a Copilot program that computes the Fibonacci sequence (over Word 64s) and tests for even a numbers:


fib :: Streams
fib = do
"fib" .= [0,1] ++ var "fib" + (drop 1 $varW64 "fib") "t" .= even (var "fib") where even :: Spec Word64 -> Spec Bool even w = w mod const 2 == const 0  Copilot contains an interpreter, a compiler, and uses a model-checker to check the correctness of your program. The compiler generates constant time and constant space C code via Tom Hawkin’s Atom Language (thanks Tom!). Copilot is specifically developed to write embedded software monitors for more complex embedded systems, but it can be used to develop a variety of functional-style embedded code. Executing > compile fib "fib" baseOpts generates fib.c and fib.h (with a main() for simulation—other options change that). We can then run > interpret fib 100 baseOpts to check that the Copilot program does what we expect. Finally, if we have CBMC installed, we can run > verify "fib.c" to prove a bunch of memory safety properties of the generated program. Galois has open-sourced Copilot (BSD3 licence). More information is available on the Copilot homepage. Of course, it’s available from Hackage, too. # Flight of the Navigator Copilot took its maiden flight in August 2010 in Smithfield, Virginia. NASA rents a private airfield for test flights like this, but you have to get past the intimidating sign posted upon entering the airfield. However, once you arrive, there’s a beautiful view of the James River. We were flying on a RC aircraft that NASA Langley uses to conduct a variety of Integrated Vehicle Health Management (IVHM) experiments. (It coincidentally had Galois colors!) Our experiments for Copilot were to determine its effectiveness at detecting faults in embedded guidance, navigation, and control software. The test-bed we flew was a partially fault-tolerant pitot tube (air pressure) sensor. Our pitot tube sat at the edge of the wing. Pitot tubes are used on commercial aircraft and they’re a big deal: a number of aircraft accidents and mishaps have been due, in part, to pitot tube failures. Our experiment consisted of a beautiful hardware stack, crafted by Sebastian Niller of the Technische Universität Ilmenau. Sebastian also led the programming for the stack. The stack consisted of four STM32 ARM Cortex M3 microprocessors. In addition, there was an SD card for writing flight data, and power management. The stack just fit into the hull of the aircraft. Sebastian installed our stack in front of another stack used by NASA on the same flights. The microprocessors were arranged to provide Byzantine fault-tolerance on the sensor values. One microprocessor acted as the general, receiving inputs from the pitot tube and distributing those values to the other microprocessors. The other microprocessors would exchange their values and perform a fault-tolerant vote on them. Granted, the fault-tolerance was for demonstration purposes only: all the microprocessors ran off the same clock, and the sensor wasn’t replicated (we’re currently working on a fully fault-tolerant system). During the flight tests, we injected (in software) faults by having intermittently incorrect sensor values distributed to various nodes. The pitot sensor system (including the fault-tolerance code) is a hard real-time system, meaning events have to happen at predefined deadlines. We wrote it in a combination of Tom Hawkin’s Atom, a Haskell DSL that generates C, and C directly. Integrated with the pitot sensor system are Copilot-generated monitors. The monitors detected • unexpected sensor values (e.g., the delta change is too extreme), • the correctness of the voting algorithm (we used Boyer-Moore majority voting, which returns the majority only if one exists; our monitor checked whether a majority indeed exists), and • whether the majority votes agreed. The monitors integrated with the sensor system without disrupting its real-time behavior. We gathered data on six flights. In between flights, we’d get the data from the SD card. We took some time to pose with the aircraft. The Copilot team from left to right is Alwyn Goodloe, National Institute of Aerospace; Lee Pike, Galois, Inc.; Robin Morisset, École Normale Supérieure; and Sebastian Niller, Technische Universität Ilmenau. Robin and Sebastian are Visiting Scholars at the NIA for the project. Thanks for all the hard work! There were a bunch of folks involved in the flight test that day, and we got a group photo with everyone. We are very thankful that the researchers at NASA were gracious enough to give us their time and resources to fly our experiments. Thank you! Finally, here are two short videos. The first is of our aircraft’s takeoff during one of the flights. Interestingly, it has an electric engine to reduce the engine vibration’s effects on experiments. http://player.vimeo.com/video/15198286 The second is of AirStar, which we weren’t involved in, but that also flew the same day. AirStar is a scaled-down jet (yes, jet) aircraft that was really loud and really fast. I’m posting its takeoff, since it’s just so cool. That thing was a rocket! http://player.vimeo.com/video/15204969 # More Details Copilot and the flight test is part of a NASA-sponsored project (NASA press-release) led by Lee Pike at Galois. It’s a 3 year project, and we’re currently in the second year. # Even More Details Besides the language and flight test, we’ve written a few papers: • Lee Pike, Alwyn Goodloe, Robin Morisset, and Sebastian Niller. Copilot: A Hard Real-Time Runtime Monitor. To appear in the proceedings of the 1st Intl. Conference on Runtime Verification (RV’2010), 2010. Springer. This paper describes the Copilot language. Byzantine faults are fascinating. Here’s a 2-page paper that shows one reason why. At the beginning of our work, we tried to survey prior results in the field and discuss the constraints of the problem. This report is a bit lengthy (almost 50 pages), but it’s a gentle introduction to our problem space. Yes, QuickCheck can be used to test low-level protocols. A short paper motivating the need for runtime monitoring of critical embedded systems. # You’re Still Interested? We’re always looking for collaborators, users, and we may need 1-2 visiting scholars interested in embedded systems & Haskell next summer. If any of these interest you, drop Lee Pike a note (hint: if you read any of the papers or download Copilot, you can find my email). ### Copilot: A Hard Real-Time Runtime Monitor August 22, 2010 I’m the principal investigator on a NASA-sponsored research project investigating new approaches for monitoring the correctness of safety-critical guidance, navigation, and control software at run-time. We just got a paper accepted at the Runtime Verification Conference on some of our recent work developing a language for writing monitors. The language, Copilot, is a domain-specific language (DSL) embedded in Haskell that uses the powerful Atom DSL as a back-end. Perhaps the best tag-line for Copilot is, “Know how to write Haskell lists? Good; then you’re ready to write embedded software.” Stay tuned for a software release and updates on a flight-test of our software on a NASA test UAV… In the meantime, check out the paper! ### Twinkle Twinkle Little Haskell May 31, 2010 Update Sept 28,2010: the Makefile mentioned below worked fine, except for something having to do with timing. I was too lazy to track the problem down, but fortunately, I found an scons script (using the scons build system) that I modified to run on Mac OSX, and it works perfectly. The original script is here—thanks Homin Lee! The post has been modified appropriately. Update Oct 1, 2010: Homin Lee has updated the script to work on Mac OSX, so you can just grab the original script now. It’s been a few months almost a year(!) since John Van Enk showed us how to twinkle (blink) an LED on his Arduino microcontroller using Atom/Haskell. Since that time, Atom (a Haskell embedded domain-specific language for generating constant time/space C programs) has undergone multiple revisions, and the standard Arduino tool-chain has been updated, so I thought it’d be worthwhile to “re-solve” the problem with something more streamlined that should work today for all your Haskell -> Arduino programming needs. With the changes to Atom, we can blink a LED with just a couple lines of core logic (as you’d expect given the simplicity of the problem). For this post, I’m using If you’ve played with the Arduino, you’ve noticed how nice the integrated IDE/tool-chain is. Ok, the editor leaves everything to be desired, but otherwise, things just work. The language is basically C with a few macros and Atmel AVR-specific libraries (the family to which Arduino hardware belongs). However, if you venture off the beaten path at all—say, trying to compile your own C program outside the IDE—things get messy quickly. Fortunately, with the scons script, things are a piece of cake. What we’ll do is write a Haskell program AtomLED.hs and use that to generate AtomLED.c. From that, the scons script will take care of the rest. ## The Core Logic Here’s the core logic we use for blinking the LED from Atom: ph :: Int ph = 40000 -- Sufficiently large number of ticks (the Duemilanove is 16MHz) blink :: Atom () blink = do on <- bool "on" True -- Declare a Boolean variable on, initialized to True. -- At period ph and phase 0, do ... period ph$ phase 0 $atom "blinkOn"$ do
on <== not_ (value on)  -- Flip the Boolean.

period ph $phase (quot ph 8)$ atom "blinkOff" \$ do
on <== not_ (value on)

And that’s it!  The blink function has two rules, “blinkOn” and “blinkOff”.  Both rules execute every 40,000 ticks.  (A “tick” in our case is just a local variable that’s incremented, but it could be run off the hardware clock.  Nevertheless, we still know we’re getting nearly constant-time due to the code Atom generates.)  The first rule starts at tick 0, and executes at ticks 40,000, 80,000, etc., while the second starts at tick 40,000/8 = 5000 and executes at ticks 5000, 45,000, 85,000, etc.  In each rule, after calling the avr_blink() C function (we’ll define), it modulates a Boolean upon which blink() depends. Thus, the LED is on 1/8 of the time and off 7/8 of the time. (If we wanted the LED to be on the same amount of time as it is off, we could have done the whole thing with one rule.)

## The Details

Really the only other thing we need to do is add a bit of C code around the core logic.  Here’s the listing for the C code stuck at the beginning, written as strings:
 [ (varInit Int16 "ledPin" "13") -- We're using pin 13 on the Arduino. , "void avr_blink(void);" ] 
and here’s some code for afterward:
 [ "void setup() {" , " // initialize the digital pin as an output:" , " pinMode(ledPin, OUTPUT);" , "}" , "" , "// set the LED on or off" , "void avr_blink() { digitalWrite(ledPin, state.AtomLED.on); }" , "" , "void loop() {" , " " ++ atomName ++ "();" , "}" ] 

The IDE tool-chain expects there to be a setup() and loop() function defined, and it then pretty-prints a main() function from which both are called. The code never returns from loop().

To blink the LED, we call digitalWrite() from avr_blink(). digitalWrite() is provided by the Arduino language.  (In John’s post, he manipulated the port registers directly, which is faster and doesn’t rely on the Arduino libraries, but it’s also lower-level and less portable between Atmel controllers.)  Atom-defined variables are stored in a struct, so state.AtomLED.on references the Atom Boolean variable defined earlier.

## Make it Work!

Now just drop the scons script into the directory (the directory must have the same name as the Haskell file, dropping the extension), and run
 > runhaskell AtomLED.hs > scons > scons upload