Reasoning with Arrays

Abstract program logics such as Hoare logic typically do not worry about data types beyond simple primitives such as integers and booleans, however this is not enough to model all aspects of programming. Gries introduces a model of arrays, where an array of type \([T]\) is treated as a function from some finite contiguous subset of the natural numbers (including zero) to \(T\), and array assignment is modelled as functional override.

This post is lifted entirely out of my dissertation (chapter 4, “The Heap as an Array”).

Continue reading

Garbage Collection

My final year project is on the correctness of garbage collectors, this post is largely derived from parts of my literature review. The dissertation (thus far), can be seen on GitHub.

To start with, we’re going to need to know what we’re talking about, so let’s introduce a couple of terms:

  • A garbage collector is an algorithm which scans the heap for unused memory cells, and frees them. It may also do some reorganisation of live cells (such as compaction) as it does so, in order to improve memory access characteristics of the program.

  • A mutator is a program which has its heap garbage collected. It is so called because it mutates the heap, which the garbage collector has just (so kindly) organised for it.

Good! Now I’m going to introduce the most common types of garbage collector, and then conclude by talking a little about what it means for a garbage collector to be correct (which is what I’m currently struggling with in my project).

Continue reading

Deriving Programs from Types

It is sometimes said about Haskell that the type system is so restrictive, that even randomly-generated code is likely to do something useful, as long as it type checks. There is a program, Djinn, which does just this. However, Djinn has some issues (such as not supporting some common types, like lists and Maybe) which I wanted to address. Before starting this, I only had a very basic notion of how to implement such a program, so I’ve probably gone for the most brute-force and naive approach, but it works for some simple things, and should be fairly extensible.

This post is based on my thoughts when writing Spirit

Continue reading

Hiding Communications with Noise

With cryptography, we can create a network such that an outside observer cannot easily determine what is being communicated, but by watching the rate of data transfer, they can still infer when messages are being sent and received. If these times can then be correlated with something else, it may be possible to extract information from the system which the participants don’t want known. Surely, however, this is just an inherent property of communication networks: if there’s nothing to say, there’s nothing meaningful to transmit.

Continue reading

Witch Hunts (Not) Considered Harmful, or, A General Algorithm for Trust in a Network

In a distributed system, we quite often want to have some sort of “trust” or “opinion” metric, by which we can tell if a node is good or bad. These come in many forms, and so in here I shall describe a fairly general algorithm with which we can extend (for the cost of a small communication and memory overhead) any distributed system to have trust.

Continue reading

A Gentle Introduction to Parsec

It seems to me that there aren’t many step-by-step introductions to parsec, where you build up a parser as you go. This is especially the case for applicative parsec, which is a shame as applicative functors are nice. So, I wrote one. Today, we are going to learn how to use applicatives and parsec to parse a CSV file. We’ll start off with a very basic one where there can be no commas or escape characters in the fields, then add support for quoted fields which can contain any character, and then we’ll add support for special escape characters (numeric literals and the like). Finally, I’ll leave two small exercises that you might want to work on, just to check that you managed to get everything.

Continue reading

Indexing collections in Haskell, or, Abstraction with Typeclasses

A typeclass in Haskell is a family of types, all of which implement some common operations. For example, the Num typeclass implements operations like (+) and (-), the Monad typeclass implements (>>=) and return. We can define typeclasses for pretty much any behaviour we want, and I’m going to use indexable data structures to show how we can go from an initially fairly concrete specification to a more abstract one.

Indexable structures are a good example, I think, as three immediately come to mind, [], Array, and Map, all of which have indexing operations, all of which have different names ((!!), (!), and lookup, respectively). If we could just have one operator to extract a value from a container by index, that would surely be much better, and we could write more generic code.

Just to clarify, we want to go from this mess:

> (!)    :: Ix i => Array a -> i -> a
> (!!)   :: [a] -> Int -> a
> lookup :: Ord k => Map k a -> Maybe a

To this beauty:

> (!!!) :: indexable container -> index -> value

Let’s also add an operator to handle cases where we don’t know if the index is valid:

> (!+!) :: indexable container -> index -> Maybe value

Continue reading

Dealing Cards Fairly, or, Verifying Agent Behaviour After the Fact

Card games are fun, everyone likes card games. However, can they be more fun? Well, I find it fun to try and solve nonexistent problems, so (if you’re me), yes! Now, what prevents me from going through the entire deck of cards and picking out only the cards that I want, when it’s my turn to draw? Everyone else watching me, of course. How can we replicate this in a decentralised system? Well, let’s more precisely state what it is we want to do:

  1. Shuffle the deck in a way that every player agrees is random, and in such a way that no player knows the order of the cards.
  2. Allow players to draw from the deck, in such a way that they do not get to choose the card they draw, and such that no other player knows what they drew.
  3. Allow players to discard cards, in such a way that no other player knows what they discarded (optional).

Continue reading

Allocating Roles in a Game, or, Communally Generating Random Sequences

This post is an indirect follow-on of How to Play Rock-Paper-Scissors Online, or, Committing to Choices in Decentralised Systems, and assumes familiarity with commitment schemes.

Let’s say that a group of people want to play a game, and there are a number of roles that must be played. Some are generally considered better than others, and so everyone simply picking their favourite role won’t work out. If there is some sort of trusted game master, then they can allocate the roles randomly, but such an invigilator is never completely above the influence of the other players. If someone really wants to play the wizard, they could threaten the game master’s family. So, we want a way for the players to randomly allocate the roles, in such a way that everyone agrees the allocation is random.

Continue reading