Pranav Bansal

Pranav Bansal

An Introduction to Behaviour Oriented Concurrency (BoC)

Introduction

Writing correct concurrent programs is notoriously difficult. Race conditions, deadlocks, and hard-to-reproduce heisenbugs often plague even experienced developers. Behaviour Oriented Concurrency (BoC) offers a fresh perspective on this challenge by providing strong guarantees about program behavior.

Developed through a collaboration between Microsoft Research, Imperial College London, and Uppsala University as part of Project Verona, BoC represents a significant advancement in concurrent programming paradigms. As a part of my Master’s thesis, I worked on operational semantics for BoC that would allow for formal reasoning about BoC programs. This post is a summary of the key ideas behind BoC and why it is interesting.

What is BoC?

The way a concurrency paradigm handles parallelism and synchronisation almost completely defines the paradigm itself. Therefore, the way in which a paradigm exposes these choices to a programmer has a direct impact on the complexity and ease of reasoning about programs.

The building blocks of the BoC paradigm are:

  • cowns (pronounced “cones”) or concurrent owners that protect the specified resource from concurrent access
  • behaviours are atomic units of work that can be executed concurrently.

Concurrent Owners (cowns)

cowns are used to protect resources. So, if we put a string in a cown, we can’t read or write to it without owning the cown. In the following example, we can not access the contents (a string) of the cown c without owning it.

let c = new Cown("Hello, World!")

While this might remind you of Rust Mutexes, cowns offer unique properties that become apparent when combined with behaviours.

Behaviours

Behaviours in BoC serve as the fundamental unit of concurrent execution. The when keyword along with a set of cowns and a closure is used to spawn a behaviour. The following code snippet shows a contrived hello world program in BoC. On line 4, the contents of cown msg_cown are bound to msg i.e, the contents of the cown can be accessed and mutated via the msg variable.

In the following example, the behaviour $b$ is spawned on line 4 and will execute asynchronously once it has exclusive access to the msg_cown. Behaviours gain exclusive access to the cowns they require based on the happens-before ordering.

main() {
    let msg_cown = new Cown("hello world!")

    when(msg = msg_cown) { // Behaviour b
        print(msg)
    }
}

The Magic: Happens-Before Ordering

Let’s say we have two behaviours $b$, $b'$, we say $b \prec b'$ (read as $b$ happens before $b'$) if and only if:

  • $b$ and $b'$ have overlapping sets of required cowns
  • $b$ spawned before $b'$

In the following example, the behaviour $b$ happens before $b'$ because $b$ was spawned before $b'$ and both behaviours access the same cown msg_cown. Therefore, the output of the program will always be “For the first time” followed by “This is getting old now”.

main() {
    msg_cown = cown.create("hello world!")

    when(msg = msg_cown) { // b
        print("For the first time")
        print(msg)
    }

    when(msg = msg_cown) { // b'
        print("This is getting old now")
        print(msg)
    }
}

Nesting Behaviours

Note, that nesting a behaviour in another behaviour will only spawn the inner behaviour. After spawning, the behaviour will need to acquire the required cowns before it can execute. It is important to note that the nested behaviour does not have access to the cowns of the outer behaviour.

The following is invalid because the inner behaviour does not have access to acc.

let acc_cown = new Cown( new Account(...) )
let log_cown = new Cown( new Log(...) )


when(acc = acc_cown) {
    // ...
    when(log = log_cown) {
        log.append("acquired account belonging to", acc.owner()) //invalid!!!!
    }
}

To fix the issue, we need to specify the acc_cown as a required cown for the inner behaviour as well.

let acc_cown = new Cown( new Account(...) )
let log_cown = new Cown( new Log(...) )


when(acc = acc_cown) {
    // ...
    when(log = log_cown, acc = acc_cown) {
        log.append("acquired account belonging to", acc.owner()) //invalid!!!!
    }
}

Note, that this is equivalent to the following code snippet:

let acc_cown = new Cown( new Account(...) )
let log_cown = new Cown( new Log(...) )

when(acc = acc_cown) {
    // ...
}

when(log = log_cown, acc = acc_cown) {
    log.append("acquired account belonging to", acc.owner()) //invalid!!!!
}

Why BoC matters

Additionally, the cown system ensures that no two behaviours can simultaneously access the same resource providing data race freedom and the happens-before ordering prevents circular dependencies ensuring deadlock freedom.

At its core, BoC addresses two fundamental challenges in concurrent programming:

  • How to safely share resources between concurrent operations
  • How to determine the order of concurrent operations

The restricted determinism introduced by the happens-before ordering allows for easier reasoning about programs and makes it easier to write correct concurrent programs.

Notes

Page of
Download