A haskell implementation of the µOz abstract machine and the CaReDeb causal-consistent reversible debugger

• The CaReDeb debugger by Elena Giachino (developer), Ivan Lanese (developer) and Claudio A. Mezzina (main developer).
• pi-calculus by Will de Renzy-Martin.

The semantics of the µOz abstract machine implemented here are detailed in this paper:

A Reversible Abstract Machine and Its Space Overhead

This project uses stack as the build tool and for dependency management. Stack will install the correct version of the haskell compiler; stack is really the only thing you'll need.

Once installed, the program can be run with

# download the ghc compiler (if needed)
stack setup

# builds the project (downloads dependencies if needed)
stack build 

# run the debugger with an example MicroOz file
stack exec reversible-debugger -- examples/send_receive.txt

The Examples folder contains a couple of µOz programs that you can step through.

The µOz language instruction set is roughly equivalent to the haskell union type below:

data Program 
    = Sequence Program Program
    | Let Identifier Value Program
    | If BoolExp Program Program
    | SpawnThread Program
    | Skip
    | Apply Identifier (List Identifier)
    | Send Identifier Identifier
    | Assert BoolExp

Where Identifier is a wrapper around string, and Value is defined by

data Value
    = VTrue
    | VFalse
    | Receive Identifier
    | Procedure (List Identifier) Program 
    | Port 
    | VInt IntExp

The exact details and implementations for renaming variables can be found in Types.hs

One of the main insights I had is that a good interpreter does not necesarilly give a good debugging experience. The µOz language can be used to express concurrent operations (really, that's its raison d'etre), but debugging concurrently is not a fun expereience.

So this interpreter simulates concurrency, but isn't actually in itself concurrent.

We want to be able to step through our program, so given some program state, we need a function that executes exactly one instruction. This function is called forwardThread. Here is a short snippet:

    Apply functionName arguments -> do
        ( parameters, body ) <- lookupProcedure functionName 

        let withRenamedVariables = 
                foldr (uncurry renameVariable) body (zip parameters arguments)

        continue (CalledProcedure functionName arguments) (withRenamedVariables : rest)
                    
    Send channelName variable -> do
        writeChannel name channelName variable 
        continue (Sent channelName variable) rest

The function pattern matches on the next instruction, and for each instruction defines some modification to

• the context - defining a variable, sending over a channel
• the history - enough information is kept to be able to revert the instruction
• the rest of the program

A thread in this interpreter is defined by its name, a stack of history instructions and a stack of remaining program instructions.

data Thread a = Thread ThreadName (List History) (List a) 

Now that we can move one thread forward, let's look at how we can keep track of multiple threads. We can define a tree-like structure to store the child-parent relationships:

data Task a 
    = Singleton (Thread a)
    | Parallel (Thread a) (Map ThreadName (Task a))

To move our program forward, we can go through the tree, and find the first thread that can make progress. A thread can make progress when

• its list of instructions is not empty and
• it is not blocked on a receive.

We introduce a type that keeps track of which instruction is evaluated and with what elements. Because we know exactly what instructions produce each history instruction, we can reverse the execution

Caveat: In actual systems it might not be possible to construct the exact reverse of an action.

The history type is defined as:

data History 
    = Skipped
    | Composed 
    | Sent Identifier Identifier
    | Received Identifier Identifier
    | CreatedVariable Identifier
    | CreatedChannel Identifier
    | CalledProcedure Identifier (List Identifier)
    | SpawnedThread ThreadName
    | BranchedOn BoolExp Bool Program 
    | AssertedOn BoolExp

With the stack of history instructions that forward evaluation produces, we can undo every instruction in the instruction set. First of all on a per-thread level:

    ( Skipped, restOfProgram ) ->
        continue (Skip : program)

    ( Composed, first : second : restOfProgram ) ->
        continue (Sequence first second : restOfProgram)

    ( CreatedVariable identifier, continuation : restOfProgram ) -> do
        value <- lookupVariable identifier 
        removeVariable identifier 
        continue (Let identifier value continuation : restOfProgram )

We have to pattern match both on the history instruction, and the remainder of the program.

There is some extra logic that will first roll back a child thread before its spawning instruction is rolled back.

many functions have the return type Interpreter a, defined as

type Interpreter a = StateT Context (Either Error) a

Which can be read as "a computation that can read from and write to some state value Context and produces Either and Error or a value of type a".

Where error describes all the errors that can occur in evaluating the program

data Error
    = UndefinedVariable Identifier
    | UndefinedThread ThreadName
    | UndefinedChannel Identifier
    | TypeError Identifier String Value
    | AssertionError BoolExp
    | BlockedOnReceive ThreadName 
    | RuntimeException String

And context stores variable assignment, the variable count (used to generate fresh variable names), how many children every thread has (used to generate fresh thread names) and the available channels.

Leading underscores in field names are used to prevent name clashes

data Context = 
    Context 
        { _threads :: Map ThreadName Int
        , variableCount :: Int
        , _bindings :: Map Identifier Value
        , _channels :: Map Identifier (Queue Identifier)
        }

Now we can define some helpers, to make writing our interpreter easier:

freshIdentifier :: Interpreter Identifier
freshIdentifier = do
    -- get the context 
    context <- State.get

    -- increment the variable count by one
    let new = 1 + variableCount context
    State.put (context { variableCount = new } )

    -- create the fresh identifier 
    return $ Identifier $ "var" ++ show new

insertVariable :: Identifier -> Value -> Interpreter () 
insertVariable identifier value = 
    State.modify $ \context -> 
        let 
            newBindings = Map.insert identifier value (_bindings context)
        in
            context { _bindings = newBindings } 

Sending and receiving is essentially pushing and popping off a queue. A bit of extra plumbing is needed in case

• the channel doesn't exist
• an empty channel is read

The undefined channel error (produced in withChannel) will bubble up, BlockedOnReceive might get caught higher up and trigger evaluation of other threads.

readChannel :: ThreadName -> Identifier -> Interpreter Identifier
readChannel threadName identifier = 
    withChannel identifier $ \queue ->
        case Queue.pop queue of
            Just ( first, rest ) -> do 
                -- put the rest of the queue back into the context
                mapChannel identifier (\_ -> rest)
                return first

            Nothing ->
                throw $ BlockedOnReceive threadName  


writeChannel :: ThreadName -> Identifier -> Identifier -> Interpreter ()  
writeChannel threadName identifier payload = 
    mapChannel identifier (Queue.push payload)

On an abstract level, the implemenations don't differ that much. The main benefit of this implementation is that everything is data.

• we don't have to spawn threads, nor continually check that the current thread has enough memory available
• the complete state of the debugger can be dumped at any time
• the debugger state can be reliably serialized
• we can easily analyze the debugger state

Additionally, haskell has union types (also called sum types or tagged unions).
In this case, union types allow us to express the µOz AST structure in 10 lines instead of 10 files. When we do a pattern match on our program, the compiler will check that our patterns are exhaustive.

The use of a union type mitigates the need for dynamic casting. The java version uses an enum to store the exact type of an instruction, The instruction then has to be dynamically cast to the type that the enum value says it should have. This is inherently unsafe and annoying.

Finally, union types can be used to guarantee that failure cases are handled. Lookup in a key-value map can fail, and instead of throwing an exception, haskell gives back a Maybe a. To access the a, the failure case (the key is missing) must be handled.

Generality

This debugger works on any language that implements the ReversibleLanguage type class:

class (Eq a, Show a, Show (Value a), Show (History a), Eq (Value a), Eq (History a)) => ReversibleLanguage a where 
    data Value a :: * 
    data History a :: * 
    forwardThread  :: Thread a -> Interpreter (Value a) (Progress (Thread a))
    backwardThread :: Thread a -> Interpreter (Value a) (Progress (Thread a))

    spawn :: a -> a

    spawned :: History a -> Maybe ThreadName
    createdVariable :: History a -> Maybe Identifier

Achieving generality in a type-safe way requires the usage of some of haskell's more advanced features. Here we define a class with two associated data types: Value and History. These types need to implement the Show and Eq type classes.

Furthermore an instance needs to give two functions to move a thread forward and backward, a function to spawn a value, and two unpacking functions.

The instance of the MicroOz language looks like

instance ReversibleLanguage.ReversibleLanguage Program where 
    {-| Values in the language. These may appear on the right-hand side of a variable declaration -} 
    data Value Program 
        = VTrue
        | VFalse
        | Receive Identifier
        | Procedure (List Identifier) Program
        | Port 
        | VInt IntExp
        deriving (Show, Eq)


         
    {-| Data type representing actions that have lead to the current program state -} 
    data History Program
        = Skipped
        | Composed 
        | Sent Identifier Identifier
        | Received Identifier Identifier
        | CreatedVariable Identifier
        | CreatedChannel Identifier
        | CalledProcedure Identifier (List Identifier)
        | SpawnedThread ThreadName
        | BranchedOn BoolExp Bool Program 
        | AssertedOn BoolExp
        deriving (Eq, Show)

    forwardThread = advance
    backwardThread = rollback

    spawn = SpawnThread

    createdVariable history =
        case history of
            CreatedVariable name -> Just name
            _ -> Nothing  

    spawned history = 
        case history of
            SpawnedThread name -> Just name
            _ -> Nothing

• I had to write my own parser

You may considering questions such as the following:

• do both implementations accept and allow to debug the same input programs? (I would expect so, but you can exploit this to indicate interesting extensions for your debugger)
• how would users interact with the debugger in each case? (interfaces, outputs from the tool, etc)
• are there things easier to do in one tool than in the other? (here again you can use this to highlight the advantages of your approach)

In other words, your comments on 'differences' should reveal that

• you understand well CaReDeb
• you have a good motivation in following a different approach
• you obtained a new solution that is at least as good than CaReDeb (and that has potential for extensions not present in CaReDeb)