6.031
6.031 — Software Construction
Spring 2022

Reading 23: Mutual Exclusion

Software in 6.031

Safe from bugsEasy to understandReady for change
Correct today and correct in the unknown future. Communicating clearly with future programmers, including future you. Designed to accommodate change without rewriting.

Objectives

This reading brings together the ideas of concurrency and promises, in the context of an asynchronous abstract data type – an ADT with asynchronous operations that might run concurrently with each other, accessing the same shared (mutable) rep.

We will see how this raises the risk of concurrency bugs, such as race conditions and deadlocks, which threaten the invariants and specifications that the ADT is striving to guarantee.

By reasoning about interleaving of concurrent code, and taking advantage of mutual exclusion (periods when code is running by itself without interleaving), we can defend against those bugs.

Library example

As a running example, let’s think about a library that allows users to borrow and return books. First, we’ll need some types to represent books and users:

// Book represents a physical copy of a book.
// Equality operation is ===, safe for use in sets and maps.
class Book { ... }

// User represents a human patron of the library.
// Equality operation is ===, safe for use in sets and maps.
class User { ... }

The operations have been omitted, because we won’t be calling any operations on users or books, just using them for their identity.

Here is the library, and its two key operations checkout and checkin:

// Library represents a mutable collection of books that can be borrowed by users.
// At any time, there is a set of books physically present at the library,
// and for each user, a set of books borrowed by that user.
// These sets are all disjoint because a book can't be in two places at once.
interface Library {

    /**
     * Check out every book in `books` so that `user` is now borrowing it.
     * Requires every book in `books` to be physically present at the library.
     */
    checkout(books: Array<Book>, user: User): void;

    /**
     * Check in every book in `books` so that it is physically in the library.
     * If any such book was previously borrowed by a user, it is now back in the library.
     */
    checkin(books: Array<Book>): void;

}

This initial spec for checkout is rather weak, and we are going to iterate on it. The design of this operation is problematic for other reasons as well, which will uncover some of the challenges we face in the world of concurrent programming.

reading exercises

Using the library

Given the spec for Library shown above, and the following declarations:

const library: Library = new MITLibrary();

const frodo = new User('Frodo Baggins');
const bilbo = new User('Bilbo Baggins');
const gandalf = new User('Gandalf the Grey');

const hobbit = new Book('The Hobbit');
const fellowship = new Book('The Fellowship of the Ring');
const twoTowers = new Book('The Two Towers');
const returnOfKing = new Book('The Return of the King');

Assume that:

  • hobbit is physically present in the library
  • no other books are physically present or checked out.

Which of the following are true statements about the Library spec?

(missing explanation)

Synchronous ADT

Let’s get started with implementing this weak spec, using a straightforward rep that directly represents the sets mentioned in the abstraction:

class MITLibrary implements Library {

    private inLibrary: Set<Book> = new Set();
    private borrowed: Map<User, Set<Book>> = new Map();

    // AF(inLibrary, borrowed) = the library such that 
    //    the books physically present is the set `inLibrary`,
    //    and the books borrowed by user u are borrowed.get(u)

    // RI(inLibrary, borrowed) = the sets of books of `inLibrary` and `borrowed` are all disjoint

    // Safety from rep exposure: all rep fields are private, and the mutable types in the rep (Set and Map)
    //     are not taken or returned by any of the methods (which only use Array, Book, and User)

    private checkRep(): void {
        // assert that every book in the rep appears exactly once
        const allBooks: Set<Book> = new Set(this.inLibrary);
        this.borrowed.forEach((borrowedBooks:Set<Book>) => {
            borrowedBooks.forEach((book: Book)=> {
                assert( ! allBooks.has(book) );
                allBooks.add(book);
            });
        });
    }

    public constructor() {
        this.checkRep();
    }

    /** @inheritdoc */
    public checkout(books: Array<Book>, user: User): void {
        // borrow the books
        for (const book of books) {
            this.inLibrary.delete(book);
            this.borrowedByUser(user).add(book);
        }

        this.checkRep();
    }

    /** @inheritdoc */
    public checkin(books: Array<Book>): void {
        for (const book of books) {
            // book is no longer borrowed, so remove it from all borrowed sets
            for (const borrowedBooks of this.borrowed.values()) {
                borrowedBooks.delete(book); // at most one of these sets has the book
            }

            // book is back in the library
            this.inLibrary.add(book);
        }

        this.checkRep();
    }

    /**
     * @returns mutable set of books borrowed by `user`,
     * creating the set if `user` hasn't borrowed before
     */
    private borrowedByUser(user: User): Set<Book> {
        let books = this.borrowed.get(user);
        if (books === undefined) {
            books = new Set();
            this.borrowed.set(user, books);
        }
        return books;
    }
}

You can look at and download the code for Library.

Asynchronous methods

One problem with checkout that a library patron will quickly discover: what if a book is not currently in the library? For example:

library.checkout([fellowship], bilbo);
library.checkout([fellowship], frodo);

First Bilbo checks out Fellowship of the Ring, and now Frodo is asking for it too. With the current spec, this second call is actually illegal, because it violates the precondition that all the requested books be physically present in the library. But how is Frodo to know that? This is a very hard operation for a client to use.

Let’s tackle this problem by making checkout asynchronous. Instead of requiring all the books to be in the library when the method is called, checkout will wait for them to be returned, and then check them out. The wait will be accomplished by returning a promise:

/**
 * Check out every book in `books` so that `user` is now borrowing it.
 * If any of them is not in the library, waits until it is checked in,
 * resolving the promise only when all the books have been successfully borrowed by `user`.
 */
checkout(books: Array<Book>, user: User): Promise<void>;

Now we can think about Frodo and Bilbo running in separate asynchronous functions of their own, interacting with the library and awaiting the promise:

await library.checkout([fellowship], bilbo);
... // Bilbo spends some time reading the book
library.checkin([fellowship]);
await library.checkout([fellowship], frodo);
... // Frodo spends some time reading the book
library.checkin([fellowship]);

How do we implement the asynchronous checkout? Here’s a sketch of what we might try:

public async checkout(books: Array<Book>, user: User): Promise<void> {
    // wait for all the books to be returned
    for (const book of books) {
        if ( ! this.inLibrary.has(book) ) {
            // book is checked out right now
            // TODO -- wait somehow
        }
    }

    // borrow the books
    for (const book of books) {
        this.inLibrary.delete(book);
        this.borrowedByUser(user).add(book);
    }
}

The first part of the operation checks whether every book is in the library. If so, it immediately proceeds to the second part, which borrows them all and returns.

But if one of the books is currently checked out, then we reach the TODO. We have to figure out how to wait until the book gets checked in.

reading exercises

How not to wait

Let’s look at one bad way to fill in the TODO:

public async checkout(books: Array<Book>, user: User): Promise<void> {
    // wait for all the books to be returned
    for (const book of books) {
        while ( ! this.inLibrary.has(book) ) {
            // book is checked out right now, so loop until the book comes back
        }
    }

    // borrow the books
    for (const book of books) {
        this.inLibrary.delete(book);
        this.borrowedByUser(user).add(book);
    }
}

What happens when we reach the highlighted code? Check all that apply.

(missing explanation)

Another way not to wait

Let’s look at another bad way to fill in the TODO:

public async checkout(books: Array<Book>, user: User): Promise<void> {
    // wait for all the books to be returned
    for (const book of books) {
        while ( ! this.inLibrary.has(book) ) {
            // book is checked out right now,
            // so wait 100 milliseconds to see if it comes back
            await timeout(100);
        }
    }

    // borrow the books
    for (const book of books) {
        this.inLibrary.delete(book);
        this.borrowedByUser(user).add(book);
    }
}

At least this code doesn’t get stuck – await returns to the event loop and allows other asynchronous functions to proceed, so that hopefully the book is eventually returned. But this kind of code is rarely written in practice because it has bad concurrent performance.

Suppose the book is returned quickly: only 1 millisecond after the while loop starts. How long does this code delay after that (in milliseconds) before this code can proceed?

(missing explanation)

Suppose the book is returned slowly: slightly more than 10 seconds after the while loop starts. How many total times did we call this.inLibrary.has(book) for the whole loop?

(missing explanation)

Making and keeping a promise

When a book is missing, we need to wait for it to be checked into the library. Let’s create a promise representing that event. Then checkout can await that promise, which is how it will accomplish its wait. Who will resolve the promise, signaling to checkout that it can proceed? That will happen in the body of the checkin operation, at the moment the book is checked in.

Before we get into that, we need to look again at the promise ADT. An ADT is defined by its operations, so what are the operations for promises? So far we have only seen then(), which acts as both a producer and an observer. Recall that await uses then() internally.

But what about a creator? All the promises we’ve used so far (for timers, file I/O, and web page loading) have been created for us by lower-level libraries. Now we’re in a situation where our own code needs to create a promise, which will be resolved by an event within our own code. No external device like a clock or I/O system is involved. So we need to be able to create a promise too.

And a promise is a mutable thing – where are its mutator operations? How does its state change from pending to fulfilled or rejected?

The answer to this question lies in the fact that Promise has two different clients: the consumer of the promise, who uses then() or await to schedule additional computation using its value; and the promiser, the code that is computing the value for the promise. Promises are designed so that only the promiser should have access to the resolve() and reject() mutators that change the promise’s state.

What a promiser needs is a new Promise<T> object, plus its associated mutator operations, resolve and reject. The Promise constructor is designed to take a synchronous callback that gives access to those mutators:

  • new Promise((resolve, reject) => { ... }) creates a new promise and immediately provides its mutators as parameters to the callback:
    • resolve(t:T)is a mutator that resolves the promise with the value t
    • reject(err:Error) is a mutator that rejects the promise with the given error

An important consequence of this design is that only the promiser – the code that called the Promise constructor and provided the callback – ends up having access to these mutators. The mutators are not public instance methods on the Promise object.

Because this constructor-with-callback idea is subtle, another common design pattern involves creating a type Deferred<T>, which bundles up a Promise<T> together with its mutators:

  • new Deferred<T>() makes a new Deferred<T> object
  • deferred.promise is the Promise<T> associated with the Deferred object
  • deferred.resolve(t:T) resolves the associated promise with the value t
  • deferred.reject(err:Error) rejects the associated promise with the given error

So Deferred has the necessary mutators needed by the promiser. The promiser holds onto this object so that it can mutate the promise later. The promiser hands the associated Promise value back to the consumer of the promise, for use in await or then().

Deferred does not exist in the standard Node or JavaScript library, but it can be implemented using the Promise constructor.

You can look at example code for Deferred.

reading exercises

Timeout using Promise

The timeout function that we’ve been using doesn’t exist in the standard JavaScript or Node library either. Let’s implement it using setTimeout and the Promise constructor.

/**
 * @param milliseconds duration to wait
 * @returns a promise that fulfills `milliseconds` after timeout() was called
 */
function timeout(milliseconds:number):Promise<void> {
    return new Promise((resolve, reject) => __________);
}

Which of the following expressions can fill the blank?

(missing explanation)

Timeout using Deferred

Let’s implement timeout using Deferred.

/**
 * @param milliseconds duration to wait
 * @returns a promise that fulfills `milliseconds` after timeout() was called
 */
function timeout(milliseconds:number):Promise<void> {
    const deferred = new Deferred<void>();
    setTimeout(___A___, milliseconds);
    return ___B___;
}

Which of the following expressions can fill the ___A___ blank?

(missing explanation)

Which of the following expressions can fill the ___B___ blank?

(missing explanation)

Asynchronous method making a promise

Let’s use the Deferred approach for making promises, because it has the nice feature of keeping the resolve/reject mutators wrapped up with the promise in a single object. That Deferred object will represent a familiar notion from real libraries: putting a book on hold. When checkin eventually sees the book come back to the library, it will look up the hold for the book and call resolve() to resolve the promise, which will enable the waiting checkout to resume.

Multiple users may be waiting on hold for the same book, so each book needs a list of holds in the rep:

private holds: Map<Book, Array<Deferred<void>>>;

When checkout wants to wait for a book, it creates a Deferred object, puts it on the hold list, and waits for its promise. The new code is highlighted in yellow:

public async checkout(books: Array<Book>, user: User): Promise<void> {
    // wait for all the books to be returned
    for (const book of books) {
        if ( ! this.inLibrary.has(book) ) {
            // book is checked out right now, so
            // put ourselves on the hold list and wait
            const hold = new Deferred<void>();
            this.holdsForBook(book).push(hold);
            await hold.promise;
        }
    }

    // borrow the books
    for (const book of books) {
        this.inLibrary.delete(book);
        this.borrowedByUser(user).add(book);
    }
}

/**
 * @returns mutable hold list for `book`,
 * creating the hold list if it doesn't already exist
 */
private holdsForBook(book: Book): Array<Deferred<void>> {
    ... // similar to borrowedByUser() helper method
}

Later, when checkin sees the book come back, it locates the hold and resolves it:

public checkin(books: Array<Book>): void {
    for (const book of books) {
        // book is no longer borrowed, so remove it from all borrowed sets
        for (const borrowedBooks of this.borrowed.values()) {
            borrowedBooks.delete(book); // at most one of these sets has the book
        }

        // book is back in the library
        this.inLibrary.add(book);

        // wake up the first person on the hold list for this book (if any)
        const holds = this.holds.get(book);
        if (holds !== undefined) {
            const deferred = holds.shift();
            if (deferred !== undefined) {
                deferred.resolve();
            }
        }
    }
}

Let’s see how this works with one possible interleaving of our two concurrent book-readers, Bilbo and Frodo:

await library.checkout([fellowship], bilbo);
... // Bilbo spends some time reading the book
library.checkin([fellowship]);
await library.checkout([fellowship], frodo);
... // Frodo spends some time reading the book
library.checkin([fellowship]);
  1. Suppose Bilbo calls checkout first. He gets the book, and checkout returns immediately, its promise fulfilled, and Bilbo starts happily reading.

  2. Now Frodo calls checkout, finds the book is not in the library, and puts a hold on it. Frodo’s call to checkout returns a Promise, which Frodo is now awaiting (and which is tied to the hold’s promise, because this call to checkout is waiting to resume after await hold.promise).

  3. Eventually Bilbo calls checkin, which first puts the book back in the library, then finds the hold on it and resolves the promise associated with the hold.

  4. This allows Frodo’s checkout to move past the await and finish checking out the book to Frodo.

  5. Frodo reads the book, and then calls checkin to put it back in the library.

If Frodo instead won the race to be the first to check out the book, the computation would evolve the same way, just with Frodo and Bilbo’s roles exchanged:

  1. Frodo checks out the book.

  2. Bilbo puts a hold on the book and waits.

  3. Frodo returns the book.

  4. Bilbo finishes checking out the book.

  5. Bilbo returns the book.

Race conditions

But all is not well in our library. Let’s see what happens with these three borrowers:

await library.checkout([
    twoTowers
], bilbo);
... // reading
library.checkin([
    twoTowers
]);
await library.checkout([
    fellowship, twoTowers
], frodo);
... // reading
library.checkin([
    fellowship, twoTowers
]);
await library.checkout([
    fellowship
], gandalf);
... // reading
library.checkin([
    fellowship
]);

Here is one possible interleaving, which is fine:

  1. Bilbo checks out Two Towers.

  2. Frodo sees that Fellowship is still in the library, puts a hold on Two Towers, and waits.

  3. Bilbo returns Two Towers and releases the hold on it for Frodo.

  4. Frodo resumes, and finishes checking out both books.

  5. Gandalf tries to check out Fellowship, and puts a hold on it.

  6. Frodo returns both books, and releases the hold on Fellowship for Gandalf.

  7. Gandalf finishes checking out Fellowship, reads it, and returns it.

But here is another interleaving, which doesn’t work out so well (steps that are different are highlighted in yellow):

  1. Bilbo checks out Two Towers.

  2. Frodo sees that Fellowship is still in the library, puts a hold on Two Towers, and waits.

  3. Gandalf checks out Fellowship.

  4. Bilbo returns Two Towers and releases the hold on it for Frodo.

  5. Frodo resumes, and having waited for both books, finishes checking out both Fellowship and the Two Towers.

Unfortunately Frodo is wrong in that last step! While Frodo was waiting for Two Towers, Gandalf snuck in and grabbed Fellowship. Fellowship is no longer in the library.

This implementation of checkout has a race condition, because it behaves correctly for some interleavings but not for others. If Gandalf happens to check out Fellowship during the time while Frodo is waiting for Two Towers, then the program fails. The correctness of a concurrent program should not depend on accidents of timing.

reading exercises

Racing to a crash

What is the result of the bad interleaving just above?

(missing explanation)

Fixing the race

Here’s a natural way to fix the race condition we just discovered: checkout could check out each book as soon as possible, rather than waiting for the end of the method.

public async checkout(books: Array<Book>, user: User): Promise<void> {
    for (const book of books) {
        if ( ! this.inLibrary.has(book) ) {
            // book is checked out right now, so
            // put ourselves on the hold list and wait
            const hold = new Deferred<void>();
            this.holdsForBook(book).push(hold);
            await hold.promise;
        }
        // borrow the book right away
        assert(this.inLibrary.has(book));
        this.inLibrary.delete(book);
        this.borrowedByUser(user).add(book);
    }
}

Let’s see how this fixes the bad interleaving:

await library.checkout([
    twoTowers
], bilbo);
... // reading
library.checkin([
    twoTowers
]);
await library.checkout([
    fellowship, twoTowers
], frodo);
... // reading
library.checkin([
    fellowship, twoTowers
]);
await library.checkout([
    fellowship
], gandalf);
... // reading
library.checkin([
    fellowship
]);
  1. Bilbo checks out Two Towers

  2. Frodo sees that Fellowship is still in the library and immediately marks it as checked out to himself.

  3. Frodo puts a hold on Two Towers, and waits.

  4. Gandalf tries to check out Fellowship, now sees that it’s checked out to Frodo, and waits.

  5. Bilbo returns Two Towers and releases the hold on it for Frodo.

  6. Frodo resumes, and finishes checking out both Fellowship and Two Towers.

  7. Frodo returns both books.

  8. Gandalf resumes and finishes checking out Fellowship.

Success!

Deadlock

Unfortunately the revised implementation of checkout can now fail in a new way. Bilbo is reading Two Towers, as before. But now Frodo and Gandalf are requesting all three books in the series, and they happen to list them in opposite order when calling checkout:

await library.checkout([
    twoTowers
], bilbo);
... // reading
library.checkin([
    twoTowers
]);
await library.checkout([
    fellowship, twoTowers, returnOfKing
], frodo);
... // reading
library.checkin([
    fellowship, twoTowers, returnOfKing
]);
await library.checkout([
    returnOfKing, twoTowers, fellowship
], gandalf);
... // reading
library.checkin([
    returnOfKing, twoTowers, fellowship
]);

Here is one possible interleaving:

  1. Bilbo checks out Two Towers

  2. Frodo sees that Fellowship is still in the library and immediately marks it as checked out to himself.

  3. Frodo puts a hold on Two Towers, and waits.

  4. Gandalf immediately checks out Return of the King to himself.

  5. Gandalf puts a hold on Two Towers, and waits.

  6. Bilbo returns Two Towers and releases the hold on it for Frodo (the first person on the hold list).

  7. Frodo resumes, and immediately checks out Two Towers.

  8. Frodo puts a hold on Return of the King, and waits.

Now we are stuck. Frodo is waiting for Return of the King, which Gandalf currently has. But Gandalf is waiting for Two Towers, which Frodo has. Neither of them can make progress until the other one releases their hold. Frodo and Gandalf are frozen in a “deadly embrace,” and they will never finish waiting.

Deadlock occurs when concurrent modules are stuck waiting for each other to do something. A deadlock may involve more than two modules, e.g., A may be waiting for B, which is waiting for C, which is waiting for A. None of them can make progress. The essential feature of deadlock is a cycle of dependencies like this.

reading exercises

Sets of books

What if we change the type of books from Array to Set:

checkout(books: Set<Book>, user: User): Promise<void>;

so that Frodo and Gandalf are now passing sets:

await library.checkout( new Set( [
    fellowship, twoTowers, returnOfKing
]), frodo);
...
await library.checkout( new Set( [
    returnOfKing, twoTowers, fellowship
]), gandalf);
...

The implementation of checkout is still the same, because the for-of loop works just as well with a set as with an array.

Can this code still reach a deadlock?

(missing explanation)

Singleton books

What if we change checkout to only take a single book:

checkout(book: Book, user: User): Promise<void>;

so that Frodo and Gandalf must now call it multiple times:

await library.checkout(fellowship, frodo);
await library.checkout(twoTowers, frodo);
await library.checkout(returnOfKing, frodo);
...
await library.checkout(returnOfKing, gandalf);
await library.checkout(twoTowers, gandalf);
await library.checkout(fellowship, gandalf);
...

The implementation of checkout is fundamentally the same – just reduced to the body of the for-of loop, without the surrounding loop.

Does it still reach a deadlock?

(missing explanation)

Interleaving and mutual exclusion

In order to address the races and deadlocks in checkout, we need to think more pessimistically. Every time we await a promise, we might be giving up control. Other asynchronous code can interleave during that time. What can go wrong? What are we depending on? When we get control back, we may need to check some things again.

Second, we need to delay making mutations until everything is ready, and then do the changes all at once, without losing control with the mutation only partway done.

This leads to two important habits of thought for concurrent programming:

  • Where might risky interleaving happen? At what points in my code might other concurrently-running code cause problems?

  • Where must interleaving definitely not happen? Which part of my code will need to run without any interruption from concurrent code?

The first question helps us identify potential race conditions, places where we need to defend against concurrency bugs.

The second question asks where we should build a wall against those bugs, by exploiting or creating periods of time when we can access shared mutable data safely, alone, without other concurrent code getting in the way.

In the single-threaded TS/JS programming model, interleaving questions are actually easier to answer than in other concurrency models. Any await is a place where your code might give up control and allow concurrent code to run. During that time, the event loop might call an asynchronous callback, or another async function might resume from its await. For an ADT like Library, this could mean that asynchronous operations already in progress may resume executing (e.g. checkout resuming from an await), or that an asynchronous client might call a fresh ADT operation (checkout or checkin).

However, the code between those await points executes continuously, without giving up control. If you have a section of code that has no await statement in it whatsoever, then you can be confident that no asynchronous callbacks or async functions will interleave with it. The code might end prematurely (returning or throwing an exception), but if not, if control comes cleanly out the other end, then you know that it ran without interruption.

This property is called mutual exclusion, referring to a region of code that has only one computation running at a time, while other concurrent computations that might access the same shared data are excluded from running. Mutual exclusion is the fundamental idea for preventing race conditions.

reading exercises

Losing control

For each short block of code below, at which points might control be lost, allowing other asynchronous functions or callbacks to interleave?

1       const answer = 3**23 + 29;
2       console.log(answer);

(missing explanation)

1     await timeout(1000);
2     await timeout(2000);

(missing explanation)

1     timeout(4000);
2     console.log("done");

(missing explanation)

It’s awaits all the way down

For these two asynchronous functions:

    async function totalBalance():Promise<number> {
1       const checkingPromise = getBalance('checking');
2       const savingsPromise = getBalance('savings');
3       return (await checkingPromise) + (await savingsPromise);
    }

    async function getBalance(account: string):Promise<number> {
4       const data: string = await fs.promises.readFile(account, { encoding: 'utf-8' });
5       return parseInt(data);
    }

Suppose that some function main() (not shown) calls totalBalance(), which in turn calls getBalance() twice.

When control is lost at the await on line 4, where will it go? Whose code will execute next?

(missing explanation)

When control is lost at the first await on line 3, where will it go? What will execute next?

(missing explanation)

When control is lost at the second await on line 3, where will it go? What will execute next?

(missing explanation)

Find the awaits

Again for these two asynchronous functions:

    async function totalBalance():Promise<number> {
1       const checkingPromise = getBalance('checking');
2       const savingsPromise = getBalance('savings');
3       return (await checkingPromise) + (await savingsPromise);
    }

    async function getBalance(account: string):Promise<number> {
4       const data: string = await fs.promises.readFile(account, { encoding: 'utf-8' });
5       return parseInt(data);
    }

Which lines run with mutual exclusion – so that you can be guaranteed that no other asynchronous functions or callbacks will interleave while the line is executing?

(missing explanation)

Redesigning checkout

Let’s use this idea to redesign the implementation of checkout. The function will have two parts:

  • First it will use holds and await to make sure all the books are in the library. Since we need to wait for a complex condition to be satisfied (multiple books being back at the same time), we need to be conservative, and may need to run this part repeatedly.

  • Having established that all the books are checked in, we will then check them all out at once, in a section carefully written to guarantee mutual exclusion, so that none of them disappear before we’re done.

Let’s also change the for loops over the books into map/filter operations, which will allow us to use operations like Promise.all to wait for multiple promises at a time. As a starting point, let’s name some useful predicate functions, to make the code more readable and DRY:

const isInLibrary = (book: Book) => this.inLibrary.has(book);
const notInLibrary = (book: Book) => ! isInLibrary(book);

Now we can say that the condition we are trying to establish is books.every(isInLibrary), and the list of books that aren’t yet available can be computed by books.filter(notInLibrary).

Let’s also define a function to wait for a missing book, by putting a hold on it as we did earlier:

const waitForBook = (book: Book) => { // requires notInLibrary(book)
    const hold = new Deferred<void>();
    this.holdsForBook(book).push(hold);
    return hold.promise;
};

Now we can collect all the promises we need with a single expression, and wait for them all at once:

await Promise.all(books.filter(notInLibrary).map(waitForBook));

For example, this line of code might put holds on Fellowship and Two Towers (currently checked out of the library), and it will not resume until both books at some point got checked back into the library. But it does not guarantee that both books are still in the library when the await finally resumes. As we saw in the race condition above, maybe Fellowship was returned first, and then checked out again while we were still waiting for Two Towers.

So we need to be conservative, and check the desired condition again, and possibly even wait some more, maybe for a new set of missing books. Let’s combine all this code into a loop:

// wait for all the books to be returned
while ( ! books.every(isInLibrary)) {
    await Promise.all(books.filter(notInLibrary).map(waitForBook));
}

Once we get past this loop, we know that all the books we want are now back in the library, so we can finish by checking them out all at once. Here’s the full code:

public async checkout(books: Array<Book>, user: User): Promise<void> {
    const isInLibrary = (book: Book) => this.inLibrary.has(book);
    const notInLibrary = (book: Book) => ! isInLibrary(book);
    const waitForBook = (book: Book) => { // requires notInLibrary(book)
        const hold = new Deferred<void>();
        this.holdsForBook(book).push(hold);
        return hold.promise;
    };

    // wait for all the books to be returned
    while ( ! books.every(isInLibrary) ) {
        await Promise.all(books.filter(notInLibrary).map(waitForBook));
    }

    // borrow the books
    assert(books.every(isInLibrary));
    for (const book of books) {
        assert(isInLibrary(book));
        this.inLibrary.delete(book);
        this.borrowedByUser(user).add(book);
    }

    this.checkRep();
}

Look back at the race condition and deadlock that we saw earlier in this reading – are they fixed now?

What about the kind of deadlock in the Singleton Books exercise — can Frodo and Gandalf still cause a deadlock by checking out one book at a time? What might we need to change about checkout in order to avoid this one?

Other techniques for mutual exclusion

TypeScript/JavaScript programs run in a single process with a single thread, using cooperative (non-preemptive) concurrency to pass control among concurrent modules. In that context, we can reason about interleaving and guarantee mutual exclusion by looking at the await points.

By contrast, in lower-level systems that have multiple threads sharing the same mutable data, the situation is much more complicated. Threads use preemptive concurrency, meaning that a thread can interrupt another thread at an arbitrary point in its computation, not just at a well-defined place like await. Reasoning about interleaving becomes much more complicated when you can be interrupted anywhere, and it is essential to create mutual exclusion using techniques like locks, mutexes, or semaphores. Preemptive concurrency is outside the scope of 6.031, but you can learn about it in 6.033 Computer System Engineering and 6.039 Operating System Engineering.

Another common approach to concurrent access to mutable shared data is worth mentioning: a database. Database systems are widely used for distributed client/server systems like web applications. Databases avoid race conditions by using transactions, which provide mutual exclusion for a sequence of reads and writes to the database. You can learn more about transactions in 6.814 Database Systems.

TypeScript/JavaScript is not the only language that supports coooperative concurrency with async and await, by the way. This approach also exists in Python, Swift, Rust, and C#.

Summary

Producing a concurrent program that is safe from bugs, easy to understand, and ready for change requires careful thinking. Building concurrent software is clearly a challenge for all three of these goals. We can break the issues into two general classes. When we ask whether a concurrent program is safe from bugs, we care about two properties:

  • Safety. Does the concurrent program satisfy its invariants and its specifications? Safety asks the question: can you prove that some bad thing never happens? Race conditions threaten safety.

  • Liveness. Does the program keep running and eventually do what you want, or does it get stuck somewhere waiting forever for events that will never happen? Can you prove that some good thing eventually happens? Deadlocks threaten liveness.

In single-threaded TypeScript/JavaScript with async and await, careful reasoning about interleaving (the places where other concurrent code can take control) and mutual exclusion (where no other concurrent code can interfere) is necessary to guarantee both properties.