Programming model: asynchronous tasks

Task programming model is currently in-preview

The asynchronous tasks programming model of Coyote is based on the task-based asynchronous pattern. Coyote provides a drop in replacement for the native .NET Task type that works with the async and await C# keywords . To avoid confusion we will use the following terminology:

Short Name Fully Qualified Name
native Task System.Threading.Tasks.Task
controlled Task Microsoft.Coyote.Tasks.Task

A controlled Task is similar to a native Task type and can be used alongside the native Task type to easily invoke external asynchronous APIs from your code. We will discuss this in more detail below.

The benefit of using the controlled Task is that the Coyote runtime takes control of its execution and scheduling during systematic testing, enabling coyote test to explore various interleavings between controlled Task objects. In production, a controlled Task executes efficiently, as it a simple wrapper over a native Task, with operations being pass-through (Coyote takes control only during testing).


The core of the Coyote asynchronous tasks programming model is the controlled Task and Task<T> objects, which model asynchronous operations. They are supported by the async and await keywords.

This programming model is fairly simple in most cases:

  • For I/O-bound code, you await an operation which returns a controlled Task or Task<T> inside of an async method.
  • For CPU-bound code, you await an operation which is started on a background thread with the Task.Run method.

In more detail, a controlled Task is a construct used to implement what is known as the promise model of concurrency. A controlled Task basically offers you a promise that work will be completed at a later point, letting you coordinate with this promise using async and await. A controlled Task represents a single operation which does not return a value. A controlled Task<T> represents a single operation which returns a value of type T. It is important to reason about tasks as abstractions of work happening asynchronously, and not an abstraction over threading. By default, a controlled Task executes (using a Task) on the current thread and delegates work to the operating system, as appropriate. Optionally, a controlled Task can be explicitly requested to run on a separate thread via the Task.Run API.

The await keyword is where the magic happens. Using await yields control to the caller of the method that performed await, allowing your program to be responsive or a service to be elastic, since it can now perform useful work while a controlled Task is running on the background. Your code does not need to rely on callbacks or events to continue execution after the task has been completed. The C# language does that for you. If you’re using controlled Task<T>, the await keyword will additionally unwrap the value returned when the controlled Task is complete. The details of how await works are further explained in the C# docs.

During testing, using await allows the Coyote runtime to automatically inject scheduling points and thoroughly explore asynchronous interleavings to find concurrency bugs.

What happens under the covers

The C# compiler transforms an async method into a state machine (literally called IAsyncStateMachine) which keeps track of things like yielding execution when an await is reached and resuming execution when a background job has finished.

The controlled Task type uses a C# 7 feature known as async task types (see here) that allows framework developers to create custom task types that can be used with async and await. This is where the magic happens. In production, controlled Task enables C# to build a custom asynchronous state machine that uses regular Task objects. However, during testing, Coyote uses dependency injection to supply a custom asynchronous state machine that allows controlling the scheduling of controlled Task objects, and thus systematically exploring their interleavings.

How to use asynchronous tasks

We will now show how to write a program using the Coyote asynchronous task programming model. As mentioned before, the controlled Task type is a drop-in replacement for the Task type, and thus any prior experience writing asynchronous code using async and await is useful and relevant. If you are not already familiar with async and await, you can learn more in the C# docs.

Say that you have the following simple C# program:

// Use the Coyote controlled task type.
using Microsoft.Coyote.Tasks;
using Microsoft.Coyote.Specifications;

public class SharedEntry
    public int Value = 0;

public async Task WriteWithDelayAsync(SharedEntry entry, int value)
    await Task.Delay(100);
    entry.Value = value;

public async Task RunAsync()
    SharedEntry entry = new SharedEntry();

    Task task1 = WriteWithDelayAsync(entry, 3);
    Task task2 = WriteWithDelayAsync(entry, 5);

    await Task.WhenAll(task1, task2);

    Specification.Assert(entry.Value == 5, "Value is '{0}' instead of 5.", entry.Value);

The above program contains a SharedEntry type that implements a shared container for an int value. The WriteWithDelayAsync is a C# async method that asynchronously waits for a controlled Task to complete after 100ms (created via the Task.Delay(100) call), and then modifies the value of the SharedEntry object.

The RunAsync asynchronous method is creating a new SharedEntry object, and then twice invokes the WriteWithDelayAsync method by passing the values 3 and 5 respectively. Each method call returns a controlled Task object, which can be awaited using await. The RunAsync method first invokes the two asynchronous method calls and then calls Task.WhenAll(...) to await on the completion of both tasks.

Because WriteWithDelayAsync method awaits a Task.Delay to complete, it will yield control to the caller of the method, which is the RunAsync method. However, the RunAsync method is not awaiting immediately upon invoking the WriteWithDelayAsync method calls. This means that the two calls can happen asynchronously, and thus the value in the SharedEntry object can be either 3 or 5 after Task.WhenAll(...) completes.

Using Specification.Assert, Coyote allows you to write assertions that check these kinds of safety properties. In this case, the assertion will check if the value is 5 or not, and if not it will throw an exception, or report an error together with a reproducible trace during testing.

To try out more samples built using the asynchronous tasks programming model see the following: