Saturday, April 19, 2014

QuickCheck is Amazing

  QuickCheck, the Haskell testing library, is a pretty amazing thing. The idea is that you don't specify test cases when testing your code, you specify what properties your code has. The QuickCheck library (which I'm using through the Tasty testing framework) will generate random data to check that your specified properties hold. If a test fails, it will try to reduce the generated input to a simple form and present it to you as a counterexample of the property.

There is a lot to say about this, so I'll just go over some things I liked:

1) Your test cases become a specification. Each test case declares a property of your code, and all together they give a description of what your intentions where.

2) Splitting pure and impure code is good practice, and QuickCheck certainly encourages this. You can test impure code with it too, but pure code is easier to test, its easier to generate repeatable cases for, and the examples should be easier to shrink. I've seen a lot of Genetic Algorithm libraries mix the generation of random data and the application of that data to modify a population. There is no need to mix these two concerns, and splitting them out has definitely helped me with writing these tests.

3) You have to put some thought into what you meant when you wrote your code. I had a complex function at the heart of a Genetic Algorithm library I've been writing, and when I started writing test cases, I realized that it was not easy for me to say what properties it had. This indicates to me that I need to break it into smaller pieces that can be understood and tested separately. This means that QuickCheck didn't just give me counter examples, it is helping me improve the overall structure of my code!

4) Once you get used to creating Arbitrary instances and using them to come up with test cases, it is pretty easy to specify a lot of properties. This requires a different way of thinking about testing, but it seems very effective and quite manageable.

 5) Testing a complex, efficient algorithm against a simple specification can give you confidence in your code. Being able to generate hundreds of random cases and comparing the results seems like the perfect test.
  I'm using an implementation of Point Mutation that is much more efficient then the usual implementation seen in nearly all Genetic Algorithm libraries, and I'm going to be very interested to test its correctness against the naive definition. I would bet there is some way to even take performance data and cause a test to fail if the "efficient" implementation is slower (within a certain margin) then the simple one. This would be one nice way to regression test your efficiency concerns.

 6) For random algorithms, there are stories of incorrect implementations giving bad research data. There are a lot of properties of a Genetic Algorithm that could be specified in this way to ensure that the implementation does contain certain types of mistakes.
  For example- mutation increases diversity (usually), selection reduces diversity, elitism maintains the best k individuals, a Genetic Algorithm out-performs another algorithm (say, a hill-climber) on a particular problem, a mutation rate of 0.5 (50%) on a bitdata individual mutates approximately 50% of its bits, etc. These tests can fail a certain number of times, but must hold if enough random tests are performed.


  I can see why the Haskell community loves this technique so much. I've not looked into its cousins (SmallCheck and SmartCheck) but I fully expect that they are just are effective.
  I recommend this technique very much. There are ports of this concept to quite a few languages, so there are no excuses.

Using Forth/Copilot/FreeRTOS With the Arduino

After over a year of absence, I'm back to blogging. This time its about the Arduino and my continued quest to program it with something other then C. I've written multiple Forth-like languages for it, but I am yet to actually reprogram it with something like amforth. Instead, I've been investigating other languages one can use.

  The program I've been playing with is to get the Arduino to control RGB LEDs where each color's brightness is controlled with PWM. The setup only requires a handful of pins since the outputs are through shift registers. The point of this is to create cool light shows. My first attempt worked pretty well, but that was many months ago. I decided to try start over with the Forth approach, alongside a Haskell DSL to compile an array of opcodes that are stored in flash and run by a C program.

Forth:
   The C program can allocate "fibers" (cooperative threads) so each LED is handled by a separate task. This makes programming in this language pretty easy, and you can control different outputs this way (I also had a 7 segment display working with this scheme at one point).
  This whole scheme was fine, but it has a definite limit- on the Arduino you can't program flash (without changing the bootloader). This makes writing a Forth interpreter difficult. You can use RAM if you use a case-threaded interpreter, but you can't save words across resets unless you want to use the tiny 512 bytes of EEPROM. Using flash is okay if you are willing to accept a static program, but anything slightly dynamic (like allocating variables) would be awkward and clunky. Despite these limitation, I've been pretty happy with the simple light shows that I've been able to create. I'm definitely a much better embedded systems programmer, and I can see the difference in ability and understanding that my professional life has brought to these hobby projects.

 Copilot:
  My next attempt was with to use Copilot, a Haskell DSL for stream programming that can generate C code. You can do several other things with your programs, like verify their properties or interpret them, but I didn't look into those aspects of the Copilot project. The point is really about formal methods and software correctness, which is interesting stuff.
  Copilot programs specify a stream of values and tie them to your hardware with a little C, and the Copilot compiler takes care of generating most of the code and generating a schedule that updating everything at the required rates.
  This is pretty cool, and I managed to put together a program that does in fact blink LEDs. I eventually got PWM working, although there is something visibly jittery about it. I found that the schedule was meeting the 1ms timing, however, so it is probably a problem with my own code, not the efficiency of the generated code.
  Some cool things are- writing a latch (stream that holds the value of another stream whenever a boolean stream goes "true" and holds that value while it is false, figuring out how to divide down streams to slow the LEDs down so you can see them, and tying the languages together to add capabilities to both.
  Programming a little DSL like this is a fun puzzle (like puzzle-script) and I can appreciate the added safely of using a constrained language. The concept of a stream is a pretty accurate model of a lot of embedded systems, and I love being able to describe things directly rather then building up the same concept indirectly in C.

FreeRTOS:
  My next attempt was to use a port of FreeRTOS (http://code.google.com/p/rtoslibs/). This was fun, as the application structure can be made much nicer and we can express things like blocking directly. Its also fun to have a little operating system on my Arduino. I have an ISR giving a semaphore, a high priority task taking that semaphore, shifting out an output and periodically giving a semaphore, and a low priority take blocking on a semaphore and calculating a new output. This structure works well, and I would like to play around with it more.
  The problem with the Arduino Uno is its tiny tiny memory. Tasks and semaphores and scheduling and other mechanisms take up space, and there is not much to be had here. So far I still have 1343 bytes left, which is (relatively) good. A couple more tasks, a message queue, and a data structure and I'll use it all up, though.


 There is more to come with my Arduino. I have lots of plans.