#020

I passed.

There’s one optional correction, writing about some closely related work I haven’t mentioned, but I’m undecided whether I want to do that yet.

I implemented concurrency invariants in the dejafu 2.0.0.0 branch. These let you check properties of shared state, and abort the computation by throwing an exception if you don’t like it. Here’s a very contrived example:

let setup = do
      var <- newEmptyMVar
      registerInvariant $ do
        value <- inspectMVar var
        when (value == Just False) $
          throwM (AssertionFailed "MVar contains False")
      pure var
in withSetup setup $ \var -> do
     fork $ putMVar var True
     fork $ putMVar var False
     readMVar var

Here we create an MVar called var, and create an invariant (registerInvariant) which reads it (inspectMVar) and checks that it doesn’t contain the value False. The main computation forks two threads, one writes True to the MVar, the other writes False, and then reads it. In executions where the False thread wins, the computation will be terminated immediately after the putMVar with an InvariantFailure condition, which contains the exception which was raised.

There’s a few things to note here:

• The invariant checker isn’t totally naive, it only tests an invariant if one of the shared variables (which can be IORefs, MVars, or TVars) have been written to since the last time the invariant passed.

• Invariants are atomic, and have no visible side-effects. They don’t change the values of any shared variables, and they don’t enforce a memory barrier. This is achieved by using a new Invariant monad to limit what you can do, rather than allowing arbitrary concurrency effects.

• Invariants (and so the shared variables they check) have to be created in the setup phase, and get checked in the main phase. Creating an invariant in the main phase won’t achieve anything.

The only things remaining in my dejafu 2.0.0.0 checklist are documentation things, and having a go at optimising it. Though, unsurprisingly, I optimised all the low-hanging fruit in dejafu a while ago.

I found that Adjoint are using dejafu in the testsuite of their Raft library for Haskell, which is pretty neat. I think all the actual uses of dejafu I’ve come across in the wild are for distributed systems—which I didn’t design it to support—and not regular concurrent programs—which I did.

I finally had a use for what I’m calling the “‘~’ instance pattern”, and wrote a memo.

I was pleasantly surprised by how easy switching bank accounts is. I used the Current Account Switch Service to change from Santander (who finally bumped me off a graduate account, onto one with no interest) to Nationwide (and an account which does give interest), and everything just worked. The only things I changed manually were a couple of services which were using my debit card details (rather than a direct debit) to do billing.

I fermented some carrot sticks, with some cloves of garlic and radishes, and they turned out pretty well after five days. I probably should have thought about what to use them for beforehand. Apparently they can be used in borscht, though I used regular carrots, rather than the black carrots the recipe calls for.

I got the urge to play some Runescape on Saturday evening, and made a new account. In some ways it’s very different to when I last played, but in others very similar. The graphics are still pretty bad (which is funny as it told me to upgrade my graphics drivers), but it’s fun.